For the fourteenth class, we are going to play with a tutorial on Coq plugins---the way the tool for paper this week was implemented, and the way the paper we'll read next week is implemented too. Coq has a rich plugin system that gives you access to lots of internal tools, but still doesn't sacrifice the overall correctness of the automation you build. So you can use Coq's plugin system to build really rich and powerful automation without sacrificing correctness, all in OCaml---though it can be a bit hard, since you have to learn a lot about Coq's internal APIs.
To make this easier, I and the Coq developers together designed a number of Coq plugin tutorials a few years ago. For this class, I've adapted one of those tutorials to make it more relevant to show you what it's like to write Coq commands that define new terms. This is relevant to both this week's paper and next week's paper!
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.
Clone this tutorial plugin from Github. If you have any trouble, please post your questions in this thread. Please also drop any installation tips you have in that thread.
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.