Commit fc4ae5bc authored by Ralf Jung's avatar Ralf Jung

Update README

parent cbe5e59a
Pipeline #3318 passed with stage
in 14 minutes and 6 seconds
...@@ -6,25 +6,26 @@ Atomicity related verification based on Iris logic. ...@@ -6,25 +6,26 @@ Atomicity related verification based on Iris logic.
This version is known to compile with: This version is known to compile with:
- Coq 8.5pl2 - Coq 8.5pl3
- Ssreflect 1.6 - Ssreflect 1.6
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
You will furthermore need an up-to-date version of The easiest way to install the correct versions of the dependencies is through
[Iris](https://gitlab.mpi-sws.org/FP/iris-coq/). Run `git submodule status` to opam. Once you got opam set up, just run `make build-dep` to install the right
see which git commit of Iris is known to work. You can pick between using a versions of the dependencies. When the dependencies change (e.g., a newer
system-installed Iris (from Coq's `user-contrib`) or a version of Iris locally version of Iris is needed), just run `make build-dep` again.
compiled for lambda-Rust.
## Building Instructions Alternatively, you can manually determine the required Iris commit by consulting
the `opam.pins` file.
To use the system-installed Iris (which is the default), run `make iris-system`. ## Building Instructions
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. Run `make` to build the full development.
## Update local dependency by tracking Iris `master` ## For Developers: How to update the Iris dependency
git submodule update --remote - Do the change in Iris, push it.
- In iris-atomic, change opam.pins to point to the new commit.
- Run "make build-dep" (in iris-atomic) to install the new version of Iris.
- You may have to do "make clean" as Coq will likely complain about .vo file
mismatches.
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