Commit 7c6793f3 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ci' into 'master'

Iris as submodule; CI support

This adds Iris as a submodule, matching the structure in Furthermore, it sets up the CI so after pushing, the repo is built against the given Iris version (with a cache to avoid needless rebuilding of Iris).

@zhangz if you have any unpushed changes, please push them. This branch moves all files to a subfolder `theories/`, so it will conflict with any other change.

See merge request !2
parents 8d5768cb 541920fb
Pipeline #2965 passed with stages
in 2 minutes and 39 seconds
...@@ -10,4 +10,5 @@ ...@@ -10,4 +10,5 @@
*.bak *.bak
Makefile.coq Makefile.coq
.coq-native/ .coq-native/
image: coq:8.5
- iris
- iris-atomic
stage: iris
- coq
- 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'
- master
- ci
stage: iris-atomic
- coq
- 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'
- master
- ci
[submodule "iris"]
path = iris
url =
# Makefile originally taken from coq-club %: Makefile.coq phony
+@make -f Makefile.coq $@
%: Makefile.coq
+make -f Makefile.coq $@
all: Makefile.coq all: Makefile.coq
+make -f Makefile.coq all +@make -f Makefile.coq all
clean: Makefile.coq clean: Makefile.coq
+make -f Makefile.coq clean +@make -f Makefile.coq clean
rm -f Makefile.coq rm -f Makefile.coq
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq 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: ; _CoqProject: ;
Makefile: ; Makefile: ;
.PHONY: all clean phony: ;
.PHONY: all clean phony iris-local iris-system
iris-atomic # IRIS-ATOMIC
Atomicity related verification based on Iris logic. 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]( 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.
-Q . iris_atomic -Q theories iris_atomic
atomic.v -Q iris-enabled iris
sync.v theories/atomic.v
atomic_incr.v theories/sync.v
simple_sync.v theories/atomic_incr.v
flat.v theories/simple_sync.v
atomic_sync.v theories/flat.v
treiber.v theories/atomic_sync.v
misc.v theories/treiber.v
evmap.v theories/misc.v
peritem.v theories/evmap.v
atomic_pcas.v theories/peritem.v
Subproject commit 6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment