For the tenth class, we are going to dive into the StructTact library! This library contains the "structural tactics" that we read about for Tuesday's class, in Planning for Change. This is again implemented on top of Coq, so if you missed the artifact from two weeks ago, 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 StructTact README:
eval $(opam env)to sync your opam environment.
git clone https://github.com/uwplse/StructTact.gitto clone the StructTact repository.
cd StructTact && make && make installto build and install StructTact.
- Download this file, and open it and step through it in CoqIDE to make sure it works.
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.