README.md 1.17 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

The easiest way to install the correct versions of the dependencies is through
Ralf Jung's avatar
Ralf Jung committed
15
opam.  You will need the Coq and Iris opam repositories:
Ralf Jung's avatar
Ralf Jung committed
16

Ralf Jung's avatar
Ralf Jung committed
17 18 19 20 21
    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.
Ralf Jung's avatar
Ralf Jung committed
22 23 24 25 26 27 28

## Building Instructions

Run `make` to build the full development.

## For Developers: How to update the Iris dependency

Ralf Jung's avatar
Ralf Jung committed
29 30 31 32 33 34
* Do the change in Iris, push it.
* Wait for CI to publish a new Iris version on the opam archive, then run
  `opam update iris-dev`.
* In iris-examples, change the `opam` file to depend on the new version.
* Run `make build-dep` (in iris-examples) to install the new version of Iris.
  You may have to do `make clean` as Coq will likely complain about .vo file
Ralf Jung's avatar
Ralf Jung committed
35
  mismatches.