README.md 1.01 KB
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:

9
 - Coq 8.6.1 / 8.7.0
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
The easiest way to install the correct versions of the dependencies is through
opam.  Once you got opam set up, just run `make build-dep` to install the right
versions of the dependencies.  When the dependencies change (e.g., a newer
version of Iris is needed), just run `make build-dep` again.
17

Ralf Jung's avatar
Ralf Jung committed
18 19
Alternatively, you can manually determine the required Iris commit by consulting
the `opam.pins` file.
20

Ralf Jung's avatar
Ralf Jung committed
21
## Building Instructions
22

Ralf Jung's avatar
Ralf Jung committed
23
Run `make` to build the full development.
Zhen Zhang's avatar
Zhen Zhang committed
24

Ralf Jung's avatar
Ralf Jung committed
25
## For Developers: How to update the Iris dependency
Zhen Zhang's avatar
Zhen Zhang committed
26

Ralf Jung's avatar
Ralf Jung committed
27 28 29 30 31
- 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.