Installing Coq for 3110

You need to install Coq 8.7.1 and an IDE.

Installing Coq 8.7.1. The easiest way to install Coq is to use OPAM. Simply do:

$ opam install coq.8.7.1

No version other than 8.7.1, not even slightly different, will do.

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. This is a full-featured editor made by the Microsoft Visual Studio team. It is available for all major systems, including Windows, OS X, and Linux. You can find it at https://code.visualstudio.com/. After installing VS Code, and after installing Coq 8.6.1, open VS Code and click on the bottom icon on the left-hand side to open the extension installer. Install VSCoq. (You might also want to install Prettify Symbols Mode, but it's not required.) VS Code and its Coq support are both relatively new, so there might be some rough edges that you encounter, but it's still the best choice for most people.

• 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 can be installed through OPAM with opam install coqide.8.7.1. But it has some OS package dependencies that can be difficult to get installed themselves. On the CS 3110 virtual machine, the dependencies can be satisfied by executing the following commands:

  • sudo apt-get update
  • sudo apt-get install libgtksourceview2.0-dev

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.