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

12
- Coq 8.10.1 / 8.11.0
Ralf Jung's avatar
Ralf Jung committed
13
- [Iris](https://gitlab.mpi-sws.org/iris/iris) 3.3.0
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17

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

Ralf Jung's avatar
Ralf Jung committed
18
19
20
21
For a tutorial that works with Coq 8.6, and that can be installed without opam,
please check out the
[version of this tutorial for Iris 3.1](https://gitlab.mpi-sws.org/iris/tutorial-popl18/tree/iris-3.1.0).

Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
## Installing Iris via opam

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

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

32
Then you can do `make build-dep` to install exactly the right version of Iris.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
38
39
40

## Compiling the exercises

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

## Documentation

Robbert Krebbers's avatar
Robbert Krebbers committed
41
The files [`proof_mode.md`] and [`heap_lang.md`] in the Iris repository contain a
Ralf Jung's avatar
Ralf Jung committed
42
43
44
list of the Iris Proof Mode tactics as well as the specialized tactics for
reasoning about HeapLang programs.

Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
[`proof_mode.md`]: https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/proof_mode.md
[`heap_lang.md`]: https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/heap_lang.md
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60

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
Ralf Jung's avatar
Ralf Jung committed
61
62
63
64
65
66
67
68

## Generating the exercises

If you want to contribute to the tutorial, note that the files in `exercises/`
are generated from the corresponding files in `solutions/`. Run `make exercises`
to re-generate those files. This requires `gawk` to be installed (which should
usually be available on Linux but might have to be installed separately on
macOS).
Ralf Jung's avatar
Ralf Jung committed
69
70
71

The syntax for the solution files is as follows:
```
72
(* SOLUTION *) Proof.
Ralf Jung's avatar
Ralf Jung committed
73
  solution here.
74
Qed.
Ralf Jung's avatar
Ralf Jung committed
75
76
77
```
is replaced by
```
78
Proof.
Ralf Jung's avatar
Ralf Jung committed
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
  (* exercise *)
Admitted.
```
and the more powerful
```
(* BEGIN SOLUTION *)
  solution here.
(* END SOLUTION BEGIN TEMPLATE
  exercise template here.
END TEMPLATE *)
```
is replaced by
```
  exercise template here.
```