Merge branch 'submodule' into 'master'

add iris as submodule

These are my first experiments with using submodules to document the Iris commit that this builds against. Beyond mere documentation, this is also useful if you have some other, incompatible version of Iris installed but still want to compile this repo (say, for compiling an outdated version).

Things seem to work fine. If you just `clone && make`, it builds against the system version of Iris. You can do `make iris-local` to tell it to use the local version of Iris; this will initialize, clone and/or update the submodule and build Iris in there. If you want to switch back to the system-installed Iris, do `make iris-system`. Of course, before we merge this I should write a README explaining this (a README would be a good idea for this project anyway).

There's one problem: After initializing the submodule, `coqdep` in the outer repo will notice the `.v` files in the submodule and add them as dependencies. So even if you just initialize the submodule e.g. in order to update it to the latest commit (but you are otherwise using the system version), you need to remember to deinitialzie it again or your builds will start to fail because it can't find the `.vo` files it is looking for inside the submodule. Because of this effect on the dependencies (i.e., the `.v.d` files), both `iris-local` and `iris-system` also do a `make clean` in the outer repo -- which I guess makes sense anyway because you just switched Iris versions.

Our users don't have any problems with that, but I expect us to typically use a system-installed Iris -- so updating the submodule would mean doing the following: Initialize submodule, `cd` into it, update it, `cd` out of it, `git add && git commit` this change, deinitalize the submodule. It would be ncier if we could keep the submodule permanently initialized without using it, but I can't think of a way to do this. I guess I could write a little shellscript that does all these tasks (and some sanity checks like making sure we only go forward), so we'd do `./update-iris <SHA1 here>` and be done.

Cc @robbertkrebbers @jjourdan @zhangz @janno 
What do you think? Zhen, if this works here I'd also implement the same for `iris-atomic`. Janno, do you think it would make sense for GPS-Iris to also adapt this?

See merge request !1

.gitignore

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

.gitmodules

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

Makefile

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

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