Merge branch 'master' into new_lifetime_logic

.gitignore

@@ -9,4 +9,5 @@
 *~
 *.bak
 .coq-native/
+iris-enabled
 Makefile.coq

.gitlab-ci.yml

+image: coq:8.5
+
+stages:
+  - iris
+  - lrust
+
+iris:
+  stage: iris
+  tags:
+  - coq
+  script:
+  - coqc -v
+  # see if the Iris submodule needs cleaning, then build it
+  - 'git submodule status iris | egrep "^ " || (git submodule update --init iris && cd iris && git clean -xfd)'
+  - 'cd iris && make -j8'
+  only:
+  - master
+  - ci
+
+lrust:
+  stage: lrust
+  tags:
+  - coq
+  script:
+  - coqc -v
+  # prepare the environment, safeguard against outdated submodule
+  - 'git submodule status iris | egrep "^ "'
+  - 'ln -s iris iris-enabled'
+  # build local repo
+  - 'time make -j8'
+  only:
+  - master
+  - ci

.gitmodules

+[submodule "iris"]
+	path = iris
+	url = https://gitlab.mpi-sws.org/FP/iris-coq.git

Makefile

+
 # Makefile originally taken from coq-club
 
-%: Makefile.coq
-	+make -f Makefile.coq $@
+%: Makefile.coq phony
+	+@make -f Makefile.coq $@
 
 all: Makefile.coq
-	+make -f Makefile.coq all
+	+@make -f Makefile.coq all
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
+	+@make -f Makefile.coq clean
 	rm -f 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: all clean
+phony: ;
+
+.PHONY: all clean phony iris-local iris-system

README.md

+# 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.

_CoqProject

--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

iris @ bb5e21f2

+Subproject commit bb5e21f21fd1b5be820005eb53750f84270ab4ec