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 from Part 1 for the course)
(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.1:
opam pin coq 8.12.1Coq 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.vsee also an HTML version of the coq files.