Separation Logic Course

Installation instructions

You might already have Coq 8.12 installed from Part 1 of the course. In that case, go to step 4 directly and check that you can step through the files in coqide.

Install opam (if you don't have it already)
(optional) If you want to keep untouched an existing version of Coq, create a new opam switch:
```
opam switch create mpri-2-36-1-part2 4.10.0
```
Install Coq 8.12:
```
opam pin coq 8.12.2
```
Coq editor: use emacs with proof general if you want and know what you're doing, other otherwise install coqide with the following command. (If you run into problems try installing the package libgtksourceview2.0-dev first)
```
opam install coqide
```

Download and build the class's material:

wget https://chargueraud.org/teach/verif/slf.tar.gz
tar xvf slf.tar.gz
cd slf/
make -j

You should now be able to start proving:

coqide SLFPreface.v

see also an HTML version of the coq files.