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
• Install Proof General
• Other IDEs
• Undergraduate Linux Cluster (ugclinux)

Install OPAM v2

• Establish a Unix development environment. If you took CS 3110 last semester, you’re already done. If not, on Mac, install MacPorts or Homebrew (not both). On Windows, install WSL; there are instructions on the CS 3110 website that will help.

• Install OPAM (version 2.0.x) through your Unix package manager.

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.

• Run these commands:

  $ opam update
  $ opam switch create coq-8.9.1 ocaml-base-compiler.4.09.0
  $ opam install utop
  $ opam pin add coq 8.9.1
  

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.

• You can double check that Coq is working by running coqtop. Here is a sample interaction:

  $ coqtop
  Welcome to Coq 8.9.1 (January 2020)
  
  Coq < Check 4160.
  4160
       : nat
  
  Coq < Quit.
  

Install Proof General

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

• Install Emacs. You’re going to want a recent version (e.g., 26.x, though even 24.x should suffice) with a GUI. Your package manager ought to have what you need. Note that if you strongly prefer Vim over Emacs, you can use Evil mode to get Vim keybindings.

  • On Linux: install Emacs through your package manager. You probably already have it.

  • On Mac: we recommend the Yamamoto Mitsuharu port, which is available through MacPorts and Homebrew—though any Cocoa port should be okay. The EmacsWiki has install instructions.

  • On WSL, run:

    $ sudo apt install emacs
    

    This will get you a text-mode Emacs that is perfectly usable. To get a GUI Emacs, you have to do just a little more work:

    • Install an X Windows Server. Two free and easy-to-install options are VcXsrv and Xming. In our limited testing, the graphics from VcXsrv seemed superior.

    • Launch the X Windows Server. The XLaunch icon it installed on your desktop is an easy way to do this. The default options it provides are good to begin; you can customize later as you see fit. Nothing will happen initially; the server is just running in the background waiting for a connection.

    • From WSL’s bash shell, run these commands:

      $ export DISPLAY=localhost:0
      $ export LIBGL_ALWAYS_INDIRECT=1
      $ emacs &
      

      You can put the two export commands in .bashrc to avoid having to type them every time. The second export is particular to VcXsrv. Emacs will launch. If the height of the frame that opens is abnormally small, try adding this to your .emacs file:

      (add-to-list 'default-frame-alist '(height . 24))
      

      (We’re not sure why this bug seems to exist on WSL. If anyone figures it out, please let us know.)

• You will need to learn at least a little Emacs right away. Launch Emacs with the command emacs. Do the built-in tutorial with C-h t. That is, Control-h followed by t. It will take maybe an hour, and it is time well spent.

• Install Proof General and Company Coq by following these instructions.

  • Tip: don’t miss the instructions there that tell you to add a line to enable Company Coq automatically.

  • On WSL: if you get an error about keys, run this command:

    $ gpg --homedir ~/.emacs.d/elpa/gnupg --receive-keys 066DAFCB81E42C40
    

    It’s needed because the Emacs available through WSL is a little out of date.

• You can double check that Proof General is working correctly as follows. Visit a new Coq file in Emacs with C-x C-f test.v. Enter this code: Check 4160. Press C-c C-n to compile it. You should get the output 4160 : nat in the Coq Response window. In a correctly configured GUI Emacs you will get ℕ instead of nat.

• Emacs is infinitely customizable. If you see any of the course staff using something that seems attractive, please just ask. We are happy to share with you what we use. Some of the course staff are fond of Spacemacs.

Other IDEs

• Visual Studio Code with the VSCoq 0.3.0 extension (by Maxime Dénès) might be the next-best choice to Proof General. At one time, this was a great choice. But it is an open-source project, and its original developer abandoned it; bugs accumulated. Quite recently, the Coq community has assumed development of the project. At this time, the course staff has little experience with this choice. But, in our limited testing, we found it worked okay.

• CoqIDE (pronounced cock-eyed) is an IDE produced by the Coq team itself. You should be able to install it through OPAM, though there are dependencies that you would also have to figure out how to install. It uses GUI technology that is likely to feel antiquated or awkward. Some students used it last year, but it provided a suboptimal experience that we do not recommend unless nothing else works.

• Coqoon is an older Eclipse plugin for Coq. It hasn’t been updated to be compatible with recent versions of Coq, so it’s not an option. We mention it here just to save you from spending time investigating it.

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 your_netid@ugclinux.cs.cornell.edu

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.

• On Mac, you can use XQuartz, which CS 3110 also quietly asked you to install—so you might already have it.

• On Windows, see above where we discuss VcXsrv and Xming.

With the server running, on your local terminal run

ssh -X your_netid@ugclinux.cs.cornell.edu

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.