For the eighth class, we are going to dive into the implementation of the Iris Proof Mode! This is implemented on top of Coq, so if you missed last week's artifact, I recommend installing it and playing around with it first.
Installation can be finicky, so please install the artifact before class using the instructions below. If you have any trouble, please post your questions in this thread. You can also drop any installation tips you have in that thread.
Please follow these instructions, which are adapted from the Iris contribution guide:
opam switch 4.12.0in the terminal to configure your environment to use the right Coq version from last class.
eval $(opam env)in the terminal to sync your opam environment.
opam repo add coq-released https://coq.inria.fr/opam/releasedin the terminal to add the release repository.
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.gitin the terminal to add the Iris development version.
git clone https://gitlab.mpi-sws.org/iris/iris.gitin the terminal to clone the Iris repository.
- Change directories to the Iris directory (
cd iris) and then run
make builddepto build dependencies.
make -jNto build Iris, where N is the number of CPU cores your computer has (for me, this was
make installfinish the installation.
If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked.
You can find the exercise we will do together in class below.