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.

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 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.