From 889f7c78ca03661b5a236e2f38174524e72ccbd5 Mon Sep 17 00:00:00 2001 From: Ralf Jung <post@ralfj.de> Date: Mon, 7 Nov 2016 15:28:25 +0100 Subject: [PATCH] use submodules to document matching Iris version --- .gitignore | 1 + .gitmodules | 3 +++ Makefile | 22 +++++++++++++------- README.md | 27 ++++++++++++++++++++----- _CoqProject | 25 ++++++++++++----------- iris | 1 + atomic.v => theories/atomic.v | 0 atomic_incr.v => theories/atomic_incr.v | 0 atomic_pcas.v => theories/atomic_pcas.v | 0 atomic_sync.v => theories/atomic_sync.v | 0 evmap.v => theories/evmap.v | 0 flat.v => theories/flat.v | 0 misc.v => theories/misc.v | 0 peritem.v => theories/peritem.v | 0 simple_sync.v => theories/simple_sync.v | 0 sync.v => theories/sync.v | 0 treiber.v => theories/treiber.v | 0 17 files changed, 55 insertions(+), 24 deletions(-) create mode 100644 .gitmodules create mode 160000 iris rename atomic.v => theories/atomic.v (100%) rename atomic_incr.v => theories/atomic_incr.v (100%) rename atomic_pcas.v => theories/atomic_pcas.v (100%) rename atomic_sync.v => theories/atomic_sync.v (100%) rename evmap.v => theories/evmap.v (100%) rename flat.v => theories/flat.v (100%) rename misc.v => theories/misc.v (100%) rename peritem.v => theories/peritem.v (100%) rename simple_sync.v => theories/simple_sync.v (100%) rename sync.v => theories/sync.v (100%) rename treiber.v => theories/treiber.v (100%) diff --git a/.gitignore b/.gitignore index 94f871e..5aced84 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 0000000..941d913 --- /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 6c554b2..51cf12d 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 4c10b5a..a83b6cc 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 3d0e6a3..c4cb0c0 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 0000000..6cb76aa --- /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 -- GitLab