918 Bytes
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
2 3 4

Atomicity related verification based on Iris logic.

## Prerequisites
Zhen Zhang's avatar
Zhen Zhang committed

7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
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.