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.