diff --git a/.gitignore b/.gitignore
index 94f871e19869a0a36905b13a1abb6fc776d6f664..5aced84bb89b21f466d23c469a2b724d16c4de74 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,4 +10,5 @@
 *.bak
 Makefile.coq
 .coq-native/
+iris-enabled
 
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000000000000000000000000000000000000..941d913e2ae27c2842dff9d29ab0cb6547e03ba1
--- /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 6c554b2751754c364a05e7cad9ad4634c68da0a4..51cf12d0852549f11dde463406570900ee31d326 100644
--- a/Makefile
+++ b/Makefile
@@ -1,20 +1,28 @@
-# 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 -nsf 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
diff --git a/README.md b/README.md
index 4c10b5ae8f960748a46613edd714f9104804f322..a83b6ccd6dd243b1bda8752055ae6cc1df4e9c68 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,26 @@
-iris-atomic
-====
+# IRIS-ATOMIC
 
 Atomicity related verification based on Iris logic.
 
-Build
---------
+## Prerequisites
 
-Please make sure Iris dependency version is same as noted in `IRIS_VERSION`
+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 3d0e6a317f40b1e2f8d92c79b3e4b2e94f02cf07..c4cb0c01e8d471adeefb112fcde3ecb193086f91 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,12 +1,13 @@
--Q . iris_atomic
-atomic.v
-sync.v
-atomic_incr.v
-simple_sync.v
-flat.v
-atomic_sync.v
-treiber.v
-misc.v
-evmap.v
-peritem.v
-atomic_pcas.v
+-Q theories iris_atomic
+-Q iris-enabled iris
+theories/atomic.v
+theories/sync.v
+theories/atomic_incr.v
+theories/simple_sync.v
+theories/flat.v
+theories/atomic_sync.v
+theories/treiber.v
+theories/misc.v
+theories/evmap.v
+theories/peritem.v
+theories/atomic_pcas.v
diff --git a/iris b/iris
new file mode 160000
index 0000000000000000000000000000000000000000..6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838
--- /dev/null
+++ b/iris
@@ -0,0 +1 @@
+Subproject commit 6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838
diff --git a/atomic.v b/theories/atomic.v
similarity index 100%
rename from atomic.v
rename to theories/atomic.v
diff --git a/atomic_incr.v b/theories/atomic_incr.v
similarity index 100%
rename from atomic_incr.v
rename to theories/atomic_incr.v
diff --git a/atomic_pcas.v b/theories/atomic_pcas.v
similarity index 100%
rename from atomic_pcas.v
rename to theories/atomic_pcas.v
diff --git a/atomic_sync.v b/theories/atomic_sync.v
similarity index 100%
rename from atomic_sync.v
rename to theories/atomic_sync.v
diff --git a/evmap.v b/theories/evmap.v
similarity index 100%
rename from evmap.v
rename to theories/evmap.v
diff --git a/flat.v b/theories/flat.v
similarity index 100%
rename from flat.v
rename to theories/flat.v
diff --git a/misc.v b/theories/misc.v
similarity index 100%
rename from misc.v
rename to theories/misc.v
diff --git a/peritem.v b/theories/peritem.v
similarity index 100%
rename from peritem.v
rename to theories/peritem.v
diff --git a/simple_sync.v b/theories/simple_sync.v
similarity index 100%
rename from simple_sync.v
rename to theories/simple_sync.v
diff --git a/sync.v b/theories/sync.v
similarity index 100%
rename from sync.v
rename to theories/sync.v
diff --git a/treiber.v b/theories/treiber.v
similarity index 100%
rename from treiber.v
rename to theories/treiber.v