README.md 2.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
# The Iris tutorial @ POPL'18

Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5 6 7 8 9
This tutorial comes in two versions:

- The folder `exercises`: skeletons of the exercises with parts left `admit`ted.
- The folder `solutions`: the exercises together with their solutions.

## Dependencies

Robbert Krebbers's avatar
Robbert Krebbers committed
10 11
For the tutorial material you need to have the following dependencies installed:

Ralf Jung's avatar
Ralf Jung committed
12
- Coq 8.6.1 / 8.7.2 / 8.8.2
Ralf Jung's avatar
Ralf Jung committed
13
- Ssreflect 1.7.0
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17 18 19 20 21 22 23
- Coq-std++ 1.1
- Iris 3.1

*Note:* the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above.

## Installing Iris via opam

The easiest, and recommend, way of installing Iris and its dependencies is via
the OCaml package manager opam (1.2.2 or newer). You first have to add the Coq
Ralf Jung's avatar
Ralf Jung committed
24
opam repository if you have not already done so earlier:
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27

    opam repo add coq-released https://coq.inria.fr/opam/released

Ralf Jung's avatar
Ralf Jung committed
28
Then you can do `opam install coq-iris.3.1.0`.
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31 32 33

## Installing Iris from source

If you are unable to use opam, you can also build Iris from source. For this,
make sure to `git checkout` the correct versions, and run `make; make install`
Ralf Jung's avatar
Ralf Jung committed
34 35
for all of:

Ralf Jung's avatar
Ralf Jung committed
36
* ssreflect: <https://github.com/math-comp/math-comp/archive/mathcomp-1.7.0.tar.gz>
Ralf Jung's avatar
tweak  
Ralf Jung committed
37
  (`cd mathcomp/ssreflect` to only compile and install what is needed)
Ralf Jung's avatar
Ralf Jung committed
38
* std++: <https://gitlab.mpi-sws.org/iris/stdpp/repository/coq-stdpp-1.1.0/archive.tar.gz>
Ralf Jung's avatar
Ralf Jung committed
39
* Iris: <https://gitlab.mpi-sws.org/FP/iris-coq/repository/iris-3.1.0/archive.tar.gz>
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63

## Compiling the exercises

Run `make` to compile the exercises. You need to have exercise 3 compiled to
work on exercise 4 and 5.

## Documentation

The file `ProofMode.md` in the tutorial material (which can also be found in the
root of the Iris repository) contains a list of the Iris Proof Mode tactics.

If you would like to know more about Iris, we recommend to take a look at:

- http://iris-project.org/tutorial-material.html
  Lecture Notes on Iris: Higher-Order Concurrent Separation Logic
  Lars Birkedal and Aleš Bizjak
  Used for an MSc course on concurrent separation logic at Aarhus University

- https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf
  Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent
  Separation Logic
  Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars
  Birkedal, Derek Dreyer.
  A detailed description of the Iris logic and its model