Installing Coq for 3110

You need to install Coq 8.8.x and an IDE. As long as you followed the 3110 OCaml installation instructions to the letter at the beginning of the semester, you already very nearly done, because we snuck in the Coq installation as part of those.

Coq

Run:

$ opam install coq

More than likely, you will receive the message:

[NOTE] Package coq is already installed (current version is 8.8.1).

Which means you already have Coq installed.

IDE

Installing an IDE. There are three choices for an IDE: Visual Studio Code, Proof General, and coqide.

Visual Studio Code is our strong recommendation for most people. If you’re running the 3110 VM, it’s already installed, and there’s nothing more you need to do. On other platforms (including OS X), all you need to do is to open VS Code and click on the bottom icon on the left-hand side to open the extension installer. Install the VSCoq extension.
Proof General is the best Coq IDE, assuming you already know Emacs. Follow the installation instructions at https://proofgeneral.github.io/.
coqide is an IDE produced by the Coq team itself. It is more difficult to install and its look-and-feel is not as modern as VS Code. It is already installed on the 3110 VM. On other platforms, be aware that it has some OS package dependencies that can be difficult to get installed themselves.

Check that it’s working. Open a new file in your IDE, and save it with a name that ends in .v, for example, test.v. Put the following definition in your file:

Let x := 42.

(Note that everything there is important: the capitalization, the colon, and the period.) Now tell Coq to compile that definition:

In VS Code, go to View->Command Palette, type coq, find Step Forward, and note the key combination that appears. On Mac, for example, it is Control-Command-Down. Go back to your file and use that key combination.
In coqide, go to Navigation->Forward, look for Forward, and note the key combination that appears. On Mac, for example, it is Control-Down. Go back to your file and use that key combination.
In Proof General, type Control-c Control-n.

In each case, the definition you entered should be highlighted, and you should see output that says x is declared as a local definition or just x is defined.

Need help? The course staff is happy to help you out with any trouble you might have. It is far easier to diagnose problems in person, so we ask that you come to office hours rather than post on Piazza.