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

12
13
- Coq 8.7.2 / 8.8.2
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17
18
19
20
21

*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
22
23
opam repository and the Iris development repository (if you have not already
done so earlier):
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25

    opam repo add coq-released https://coq.inria.fr/opam/released
26
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Robbert Krebbers's avatar
Robbert Krebbers committed
27

28
Then you can do `make build-dep` to install exactly the right version of Iris.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

## 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