README.md 1.09 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
5
6
7
8
# IRIS EXAMPLES

Some example verification demonstrating the use of Iris.

## Prerequisites

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/)
Ralf Jung's avatar
Ralf Jung committed
12
 - The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
Ralf Jung's avatar
Ralf Jung committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

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.

Alternatively, you can manually determine the required Iris commit by consulting
the `opam.pins` file.

## Building Instructions

Run `make` to build the full development.

## For Developers: How to update the Iris dependency

- 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-example) to install the new version of Iris.
- You may have to do "make clean" as Coq will likely complain about .vo file
  mismatches.