Class 8: Reflections on Reflection

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.

Installation Instructions

Please follow these instructions, which are adapted from the Iris contribution guide:

1. Run opam switch 4.12.0 in the terminal to configure your environment to use the right Coq version from last class.
2. Run eval $(opam env) in the terminal to sync your opam environment.
3. Run opam repo add coq-released https://coq.inria.fr/opam/released in the terminal to add the release repository.
4. Run opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git in the terminal to add the Iris development version.
5. Run git clone https://gitlab.mpi-sws.org/iris/iris.git in the terminal to clone the Iris repository.
6. Change directories to the Iris directory (cd iris) and then run make builddep to build dependencies.
7. Run make -jN to build Iris, where N is the number of CPU cores your computer has (for me, this was make -j8).
8. Run make install finish 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.

During class, we will again divide up into groups, matching people who already have experience with people who are totally new to this. We will then do the exercise in this file. You can do this on your own if you cannot make it to class, or enter a Zoom breakout if you're remote. Let me know if you can't attend, but would like me to find you a partner or make an exception.

There is a discussion question at the bottom of the file. This is the only graded part. Please have your group post your answers in this thread, following the directions from the file.