README.md 927 Bytes
Newer Older
1
# IRIS-ATOMIC
Zhen Zhang's avatar
Zhen Zhang committed
2 3 4

Atomicity related verification based on Iris logic.

5
## Prerequisites
Zhen Zhang's avatar
Zhen Zhang committed
6

7 8
This version is known to compile with:

Ralf Jung's avatar
Ralf Jung committed
9
 - Coq 8.6.1 / 8.7.1
Ralf Jung's avatar
Ralf Jung committed
10
 - Ssreflect 1.6.4
Ralf Jung's avatar
Ralf Jung committed
11
 - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
12

Ralf Jung's avatar
Ralf Jung committed
13 14 15 16
## Building from source

When building from source, we recommend to use opam (1.2.2 or newer) for
installing the dependencies.  This requires the following two repositories:
17

Ralf Jung's avatar
Ralf Jung committed
18 19 20 21 22
    opam repo add coq-released https://coq.inria.fr/opam/released
    opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git

Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
23

Ralf Jung's avatar
Ralf Jung committed
24 25
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
26

Ralf Jung's avatar
Ralf Jung committed
27 28 29
To update, do `git pull`.  After an update, the development may fail to compile
because of outdated dependencies.  To fix that, please run `opam update`
followed by `make build-dep`.