README.md 1.07 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6
# Repository Archived

This repository is archived.  For the current version of the Coq examples, see
[iris-examples](https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logatom).


7
# IRIS-ATOMIC
Zhen Zhang's avatar
Zhen Zhang committed
8 9 10

Atomicity related verification based on Iris logic.

11
## Prerequisites
Zhen Zhang's avatar
Zhen Zhang committed
12

13 14
This version is known to compile with:

Ralf Jung's avatar
Ralf Jung committed
15
 - Coq 8.8.2
Ralf Jung's avatar
Ralf Jung committed
16
 - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
17

Ralf Jung's avatar
Ralf Jung committed
18 19 20 21
## 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:
22

Ralf Jung's avatar
Ralf Jung committed
23 24 25 26 27
    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.
28

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

Ralf Jung's avatar
Ralf Jung committed
32 33 34
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`.