Installing Coq

You need OPAM v2, Coq 8.9.1, and an IDE. You can install them on your own machine. Or, you can install them on the CS department undergraduate Linux cluster, ugclinux.

Table of Contents:

Install OPAM v2

Install Coq v8.9.1

Coq is highly sensitive to version numbers. Version 8.9.1 is the only one that will be supported this semester. Note that it is not the most recent version.

Pinning v8.9.1, as the instructions above do, will ensure that OPAM does not try to upgrade it to a more recent version later in the semester. By putting it on its own switch, we ensure it doesn’t intefere with any other OCaml development you might do.

Install Proof General

You need a Coq IDE. We strongly recommend Proof General. Other choices are mentioned, below, but they are inferior.

Other IDEs

Undergraduate Linux Cluster (ugclinux)

The CS department runs a Linux cluster to which all affiliated CS majors should have access. (If you aren’t affiliated, we can probably still get you access anyway.) To access it, open a terminal and run:

$ ssh

OPAM v2 and Emacs are already installed on the cluster. You just need to install Coq and Proof General to your own account, following the instructions above. You will then be able to do all your Coq development on the cluster. To transfer files, you can put them in Git repos (which we recommended for assignments) or you can use the scp command to copy them between your local machine and ugclinux.

Off-campus: To connect to ugclinux from off campus, use the Cornell VPN.

Graphics: Emacs will launch a text interface, which is perfectly usable. It’s also possible to get graphics. First, install an X Windows Server on your own local machine.

With the server running, on your local terminal run

ssh -X

Note that’s the same command as before, but adding the -X flag. Now running emacs will open a graphical interface to Emacs. There could be significant lag, especially if (i) you are coming from off campus or (ii) there are other active users of ugclinux.