Class 14: Coq Plugin Development

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.

Installation Instructions

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.

During class, we will again divide up into groups. We will then do the exercises in the plugin tutorial. 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.