Installing Coq

You need to install Coq 8.8.1 or 8.8.2. Follow the instructions on the Coq website. For those who have taken CS 3110: note that you can install Coq natively on Windows; you don’t have to run inside the 3110 VM.

You also need to install an IDE. We recommend either CoqIDE or Proof General; we also mention Visual Studio Code and Eclipse, below:

• CoqIDE is a special-purpose IDE produced by the Coq team itself that you can install at the same time you install Coq. Compared to Proof General, CoqIDE is a lean, special-purpose tool with a gentler learning curve. CoqIDE is also likely to be easier to install. If you don’t want to use Emacs, CoqIDE is our recommendation.

• Proof General is highly recommended. Although it will take time to install and to master, it will ultimately make you highly productive: it offers powerful features for auto-completion, auto-compilation, searching for theorems, browsing documentation, and more. The catch is that you have to use the Emacs editor. Don’t let that discourage you! If you’ve never learned Emacs before, now is a good time to invest the effort. (If you prefer Vim, see the instructions regarding Spacemacs below.)

  • First, install Emacs. You’re going to want a recent version (e.g., 26.1) with a GUI. The details of how to do this vary depending on your OS. OS X and Windows both have Emacs ports available. If you’re running on Linux, your package manager ought to have what you need.

  • Second, if you’ve never used Emacs before, do its built-in tutorial. Start Emacs and type C-h t, that is, Ctrl-h followed by t. There are also many other tutorials available on websites. Don’t feel like you need to learn all the keystrokes the tutorial teaches all at once: over time, you’ll figure out which you need the most. The Emacs Reference Card might be useful to print out and keep nearby as you acclimate.

  • Third, install Proof General. Now anytime you open a Coq file (.v), Emacs will have Coq and Proof General menus, as well as a toolbar. You’ll want to start learning the keyboard shortcuts for common navigation commands, such as Next Step, Goto Point, and Undo Step.

  • Fourth, install Company-Coq. Feel free to do the Company-Coq tutorial (M-x company-coq-tutorial), although some of it might make more sense after we get a couple weeks or more into the course.

  • Finally, as you start doing assignments in the course, you might want to begin exploring the “Proof-General -> Quick Options” menu and the first section of the “Coq” menu to see what customizations to the interface might work best for you. Here are two that we recommend trying out right away: (i) “Coq -> Electric Terminator” or “Double Hit Electric Terminator”, which will automatically send your most recent command to Coq; and (ii) “Coq -> 3 Windows Mode Layout -> hybrid” (and the other options), which will give you various options for where the Goals and Response windows appear. “Proof-General -> Quick Option -> Display -> Multiple Windows” will give you even more flexibility.

  Optionally, you could augment Emacs with Spacemacs, which is a curated Emacs configuration that provides Vim-like modal editing and key bindings. The Spacemacs README provides more information, including detailed installation instructions. The Vim Migration guide will help Vim users adapt. After installing Spacemacs, follow these instructions to enable Coq:

  • Clone the Coq layer:

     git clone https://github.com/olivierverdier/spacemacs-coq ~/.emacs.d/private/coq
    

  • Start Emacs, then press SPC f e d (that is, press space, f, e, then d) to edit your .spacemacs file. Add coq to the list of dotspacemacs-configuration-layers list. You might also want to uncomment some of the layers suggested in the template of this file, especially auto-completion, spell-checking, and syntax-checking. Save the file and then press SPC f e R to reload the configuration. Now Proof General will start automatically on opening .v files. You can use : company-coq-tutorial RET to work through the Company Coq tutorial.

• Visual Studio Code with the VSCoq extension was good enough for the little bit of Coq we did in CS 3110, and it would probably get you through CS 4160. But, development of VSCoq seems to have been abandoned as of mid-2017, and unresolved issues are beginning to accumulate. Its current stability and functionality might cause you difficulty and make you less productive. So, we recommend switching to either CoqIDE or Proof General.

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