From 9a515ecb859712ce2c036e610de98216b057b5bb Mon Sep 17 00:00:00 2001 From: Ralf Jung <post@ralfj.de> Date: Tue, 1 Nov 2016 10:01:54 +0100 Subject: [PATCH] add iris as submodule --- .gitignore | 1 + .gitmodules | 3 +++ Makefile | 11 +++++++- README.md | 26 +++++++++++++++++++ _CoqProject | 37 ++++++++++++++------------- iris | 1 + adequacy.v => theories/adequacy.v | 0 derived.v => theories/derived.v | 0 heap.v => theories/heap.v | 0 lang.v => theories/lang.v | 0 lifetime.v => theories/lifetime.v | 0 lifting.v => theories/lifting.v | 0 memcpy.v => theories/memcpy.v | 0 notation.v => theories/notation.v | 0 perm.v => theories/perm.v | 0 perm_incl.v => theories/perm_incl.v | 0 proofmode.v => theories/proofmode.v | 0 races.v => theories/races.v | 0 tactics.v => theories/tactics.v | 0 type.v => theories/type.v | 0 type_incl.v => theories/type_incl.v | 0 typing.v => theories/typing.v | 0 wp_tactics.v => theories/wp_tactics.v | 0 23 files changed, 60 insertions(+), 19 deletions(-) create mode 100644 .gitmodules create mode 100644 README.md create mode 160000 iris rename adequacy.v => theories/adequacy.v (100%) rename derived.v => theories/derived.v (100%) rename heap.v => theories/heap.v (100%) rename lang.v => theories/lang.v (100%) rename lifetime.v => theories/lifetime.v (100%) rename lifting.v => theories/lifting.v (100%) rename memcpy.v => theories/memcpy.v (100%) rename notation.v => theories/notation.v (100%) rename perm.v => theories/perm.v (100%) rename perm_incl.v => theories/perm_incl.v (100%) rename proofmode.v => theories/proofmode.v (100%) rename races.v => theories/races.v (100%) rename tactics.v => theories/tactics.v (100%) rename type.v => theories/type.v (100%) rename type_incl.v => theories/type_incl.v (100%) rename typing.v => theories/typing.v (100%) rename wp_tactics.v => theories/wp_tactics.v (100%) diff --git a/.gitignore b/.gitignore index e38a0bd5..334369ae 100644 --- a/.gitignore +++ b/.gitignore @@ -9,4 +9,5 @@ *~ *.bak .coq-native/ +iris-project Makefile.coq diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..941d913e --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "iris"] + path = iris + url = https://gitlab.mpi-sws.org/FP/iris-coq.git diff --git a/Makefile b/Makefile index 6c3ca5b5..4ab350fe 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,4 @@ + # Makefile originally taken from coq-club %: Makefile.coq phony @@ -13,10 +14,18 @@ clean: Makefile.coq Makefile.coq: _CoqProject Makefile coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq +iris-local: clean + git submodule update --init iris + ln -s iris iris-enabled + +make -C iris -f Makefile + +iris-system: clean + rm -f iris-enabled + _CoqProject: ; Makefile: ; phony: ; -.PHONY: all clean phony +.PHONY: all clean phony iris-local iris-system diff --git a/README.md b/README.md new file mode 100644 index 00000000..b55b3347 --- /dev/null +++ b/README.md @@ -0,0 +1,26 @@ +# LAMBDA-RUST COQ DEVELOPMENT + +This is the Coq formalization of lambda-Rust. + +## Prerequisites + +This version is known to compile with: + + - Coq 8.5pl2 + - Ssreflect 1.6 + +You will furthermore need an up-to-date version of +[Iris](https://gitlab.mpi-sws.org/FP/iris-coq/). Run `git submodule status` to +see which git commit of Iris is known to work. You can pick between using a +system-installed Iris (from Coq's `user-contrib`) or a version of Iris locally +compiled for lambda-Rust. + +## Building Instructions + +To use the system-installed Iris (which is the default), run `make iris-system`. +This only works if you previously built and installed a compatible version of the +Iris Coq formalization. To use a local Iris (which will always be the right +version), run `make iris-local`. Run this command again later to update the +local Iris, in case the preferred Iris version changed. + +Now run `make` to build the full development. diff --git a/_CoqProject b/_CoqProject index 9769f2a7..c4ae5b38 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,18 +1,19 @@ --Q . lrust -adequacy.v -derived.v -heap.v -lang.v -lifting.v -memcpy.v -notation.v -proofmode.v -races.v -tactics.v -wp_tactics.v -lifetime.v -type.v -type_incl.v -perm.v -perm_incl.v -typing.v +-Q theories lrust +-Q iris-enabled iris +theories/adequacy.v +theories/derived.v +theories/heap.v +theories/lang.v +theories/lifting.v +theories/memcpy.v +theories/notation.v +theories/proofmode.v +theories/races.v +theories/tactics.v +theories/wp_tactics.v +theories/lifetime.v +theories/type.v +theories/type_incl.v +theories/perm.v +theories/perm_incl.v +theories/typing.v diff --git a/iris b/iris new file mode 160000 index 00000000..bb5e21f2 --- /dev/null +++ b/iris @@ -0,0 +1 @@ +Subproject commit bb5e21f21fd1b5be820005eb53750f84270ab4ec diff --git a/adequacy.v b/theories/adequacy.v similarity index 100% rename from adequacy.v rename to theories/adequacy.v diff --git a/derived.v b/theories/derived.v similarity index 100% rename from derived.v rename to theories/derived.v diff --git a/heap.v b/theories/heap.v similarity index 100% rename from heap.v rename to theories/heap.v diff --git a/lang.v b/theories/lang.v similarity index 100% rename from lang.v rename to theories/lang.v diff --git a/lifetime.v b/theories/lifetime.v similarity index 100% rename from lifetime.v rename to theories/lifetime.v diff --git a/lifting.v b/theories/lifting.v similarity index 100% rename from lifting.v rename to theories/lifting.v diff --git a/memcpy.v b/theories/memcpy.v similarity index 100% rename from memcpy.v rename to theories/memcpy.v diff --git a/notation.v b/theories/notation.v similarity index 100% rename from notation.v rename to theories/notation.v diff --git a/perm.v b/theories/perm.v similarity index 100% rename from perm.v rename to theories/perm.v diff --git a/perm_incl.v b/theories/perm_incl.v similarity index 100% rename from perm_incl.v rename to theories/perm_incl.v diff --git a/proofmode.v b/theories/proofmode.v similarity index 100% rename from proofmode.v rename to theories/proofmode.v diff --git a/races.v b/theories/races.v similarity index 100% rename from races.v rename to theories/races.v diff --git a/tactics.v b/theories/tactics.v similarity index 100% rename from tactics.v rename to theories/tactics.v diff --git a/type.v b/theories/type.v similarity index 100% rename from type.v rename to theories/type.v diff --git a/type_incl.v b/theories/type_incl.v similarity index 100% rename from type_incl.v rename to theories/type_incl.v diff --git a/typing.v b/theories/typing.v similarity index 100% rename from typing.v rename to theories/typing.v diff --git a/wp_tactics.v b/theories/wp_tactics.v similarity index 100% rename from wp_tactics.v rename to theories/wp_tactics.v -- GitLab