EECS 762 Blog

Notes

Immediately after class I found the notes that I lost. They were, um, on my computer. Forgot to refresh an editor window. Regardless, I just pushed updated notes that include what I presented today.

Class Notes

I have the notes that I’m using in class available on the class website. Follow the Formatted Lecture Notes link to get a formatted version. If you want to download the unprocessed markdown file I use in Marp you can get that at Unformatted Lecture Notes. Both links will usually get updated before class. Note that the unformatted notes are zipped. gh-pages trys to turn anything with an md extension into an html file.

Welcome

Welcome to the EECS 762 blog. I will post information about projects, lectures and music here. Please check here often when projects are due as I will post late-breaking information including hints and corrections. Please see the course homepage for lecture topics, project postings and exam information as well as course administrative details.

To prepare for the course you should install Rocq and download the first two books, Logical Foundations and Programming Language Foundations, from the Software Foundations book series. We will start off with a quick review and jump quickly into IMP verification.

If you are not familiar with Rocq and IMP already, you can still be successful in the course. We will work together on projects in class early in the semester. This joint work will help you come up to speed quickly.

Rocq Installation

Some notes on installing Rocq from Will Thomas, my TA last semester:

1. Use a Unix-esque environment (WSL for Windows, default for macOS and Linux)
2. Use opam and follow the install instructions. In particular, I would suggest using the shell script.
3. Once you have opam installed (and properly initialized), just run opam install coq.9.0.0

FAQs

1. What is WSL? WSL is the Windows Subsystem for Linux. It gives you all the benefits of a Linux programming environment, from your Windows machine. Here are some WSL install Docs.
2. Do I need to use WSL? Not necessarily… but opam support for Windows natively is very new and relatively buggy. You might find yourself up against cases of “sorry you just can’t do that on Windows with opam currently”
3. Okay I have this WSL thing, what do I do? Enter the WSL Linux environment with the command:

wsl

Navigate to some folder you care about putting the Rocq code in:

cd ~/Rocq/2025/lf       # navigate to folder
code .                  # Launches vscode

From there, make sure you have the right Rocq extension installed (see below)

Proving with Rocq

Use VSCode… alternatives exist, but they are not well-supported or have hardly any features. In particular, I use the coq-lsp vscode extension. Others also have great success with vsrocq. Both will involve you using opam to install a language server. Thus, the importance of using opam.

Still having trouble?

Try searching online, it might be a common issue with a fix. Otherwise, come to office hours.