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

Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
7
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.

Tej Chajed's avatar
Tej Chajed committed
8
The slides for the tutorial's lecture component are at [talks/iris-popl21-tutorial.pdf](talks/iris-popl21-tutorial.pdf).
Ralf Jung's avatar
Ralf Jung committed
9
You can also watch the [recording of this talk from POPL'21](https://www.youtube.com/watch?v=LjXaffBpMag).
Tej Chajed's avatar
Tej Chajed committed
10
11
12

The Coq demo source is in [demo.v](talks/demo/demo.v).

Ralf Jung's avatar
Ralf Jung committed
13
14
The tutorial material is based on the earlier [POPL 2018 tutorial](https://gitlab.mpi-sws.org/iris/tutorial-popl18/) by Robbert Krebbers and Jacques-Henri Jourdan.

Ralf Jung's avatar
Ralf Jung committed
15
16
17
18
19
## Chat

For help with this tutorial, you can join the [POPL2021 Tutorial channel](https://mattermost.mpi-sws.org/iris/channels/popl2021-tutorial) on the MPI-SWS Mattermost.
To log in, you need to [create an MPI-SWS GitLab account](https://gitlab.mpi-sws.org/users/sign_up), either by logging in via GitHub or by registering a new account.

Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
## Dependencies

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

Ralf Jung's avatar
Ralf Jung committed
24
- Coq 8.14.1 / 8.15.1
Ralf Jung's avatar
Ralf Jung committed
25
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
Robbert Krebbers's avatar
Robbert Krebbers committed
26

Ralf Jung's avatar
Ralf Jung committed
27
28
*Note:* the tutorial material will not work with earlier or later versions of
Iris, it is important to install the exact versions as described below.
Ralf Jung's avatar
Ralf Jung committed
29

30
### Installing Iris via opam
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32

The easiest, and recommend, way of installing Iris and its dependencies is via
33
34
35
36
the OCaml package manager opam (2.0.0 or newer). After
[installing opam](https://opam.ocaml.org/doc/Install.html), you first have to
add the Coq opam repository and the Iris development repository (if you have not
already done so earlier):
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38

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

41
42
Once you have opam set up, `cd` into a clone of this repository and run `make
build-dep` to install the right versions of the dependencies.
43
44
45
46

To update, do `git pull`.  After an update, the development may fail to compile
because of outdated dependencies.  To fix that, please run `opam update`
followed by `make build-dep`.
Robbert Krebbers's avatar
Robbert Krebbers committed
47

48
49
50
51
52
53
54
55
56
57
58
59
### Installing Iris without opam (not recommended)

You can also install Iris without opam, but this will increase the risk of build
failures due to incompatibilities.  Assuming you already have an appropriate
version of Coq installed, you need to install both std++ and Iris:

* Clone [std++](https://gitlab.mpi-sws.org/iris/stdpp/), then run `make -jN && make install`
  (where `N` is the number of CPU cores you wish to use for the build).
* Clone [Iris](https://gitlab.mpi-sws.org/iris/iris/), then run `make -jN && make install`.

We usually make sure that the latest commits of std++, Iris, and the tutorial
work together, but sometimes they can be temporarily broken.  The versions
Tej Chajed's avatar
Tej Chajed committed
60
installed via opam are always guaranteed to work.
61

Ralf Jung's avatar
Ralf Jung committed
62
63
64
65
66
67
## Working on the exercises

To work on the exercises, simply edit the files in the `exercises/` folder. Some
proofs in these files are admitted and marked as `(* exercise *)`; your task is
to complete those proofs all the way to a `Qed`.

68
69
After you are done with a file, run `make` (with your working directory being
the repository root, where the `Makefile` is located) to compile and check the
70
exercises. You need to have exercise 3 compiled to work on exercise 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

Ralf Jung's avatar
Ralf Jung committed
72
73
If you are stuck, you can find solutions in the corresponding file in the
`solutions/` folder.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76

## Documentation

Robbert Krebbers's avatar
Robbert Krebbers committed
77
The files [`proof_mode.md`] and [`heap_lang.md`] in the Iris repository contain a
Ralf Jung's avatar
Ralf Jung committed
78
79
80
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
81
82
[`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
83
84
85

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

Ralf Jung's avatar
Ralf Jung committed
86
87
- [Lecture Notes on Iris: Higher-Order Concurrent Separation Logic](http://iris-project.org/tutorial-material.html)<br>
  Lars Birkedal and Aleš Bizjak<br>
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
  Used for an MSc course on concurrent separation logic at Aarhus University

Ralf Jung's avatar
Ralf Jung committed
90
91
- [Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic](https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf)<br>
  Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer<br>
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  A detailed description of the Iris logic and its model
Ralf Jung's avatar
Ralf Jung committed
93
94
95
96
97

## 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`
98
99
100
to re-generate those files. This requires `gawk` to be installed (which should
usually be available on Linux, and on macOS can be installed with `brew install
gawk`).
Ralf Jung's avatar
Ralf Jung committed
101
102
103

The syntax for the solution files is as follows:
```
104
(* SOLUTION *) Proof.
Ralf Jung's avatar
Ralf Jung committed
105
  solution here.
106
Qed.
Ralf Jung's avatar
Ralf Jung committed
107
108
109
```
is replaced by
```
110
Proof.
Ralf Jung's avatar
Ralf Jung committed
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
  (* 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.
```