Skip to content
Snippets Groups Projects
Commit 9a515ecb authored by Ralf Jung's avatar Ralf Jung
Browse files

add iris as submodule

parent e8ca86e2
No related branches found
No related tags found
No related merge requests found
...@@ -9,4 +9,5 @@ ...@@ -9,4 +9,5 @@
*~ *~
*.bak *.bak
.coq-native/ .coq-native/
iris-project
Makefile.coq Makefile.coq
[submodule "iris"]
path = iris
url = https://gitlab.mpi-sws.org/FP/iris-coq.git
# Makefile originally taken from coq-club # Makefile originally taken from coq-club
%: Makefile.coq phony %: Makefile.coq phony
...@@ -13,10 +14,18 @@ clean: Makefile.coq ...@@ -13,10 +14,18 @@ clean: 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 -s iris iris-enabled
+make -C iris -f Makefile
iris-system: clean
rm -f iris-enabled
_CoqProject: ; _CoqProject: ;
Makefile: ; Makefile: ;
phony: ; phony: ;
.PHONY: all clean phony .PHONY: all clean phony iris-local iris-system
# 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.
-Q . lrust -Q theories lrust
adequacy.v -Q iris-enabled iris
derived.v theories/adequacy.v
heap.v theories/derived.v
lang.v theories/heap.v
lifting.v theories/lang.v
memcpy.v theories/lifting.v
notation.v theories/memcpy.v
proofmode.v theories/notation.v
races.v theories/proofmode.v
tactics.v theories/races.v
wp_tactics.v theories/tactics.v
lifetime.v theories/wp_tactics.v
type.v theories/lifetime.v
type_incl.v theories/type.v
perm.v theories/type_incl.v
perm_incl.v theories/perm.v
typing.v theories/perm_incl.v
theories/typing.v
Subproject commit bb5e21f21fd1b5be820005eb53750f84270ab4ec
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment