CIS 500: Coq Resources

Running Coq on SEAS Systems

On any SEAS Linux machine, including the ones in the labs (Moore 100A, 100C, and 207), you should be able to start up CoqIDE by typing something like this at a command prompt:

         coqide Basics.v
      

Using CoqIDE

The CoqIDE user interface is pretty self-explanatory. Use the up/down buttons at the top of the window to send parts of your proof script to Coq for processing (down) or to retract parts that have already been sent so that you can edit them again (up).

Documentation

The main Coq page includes a comprehensive reference manual, an FAQ, and pointers to some other useful resources.

For those who wish to go deeper with Coq, the Coq'Art book Interactive Theorem Proving and Program Development, by Yves Bertot and Pierre Castéran is recommended, as is Adam Chlipala's Certified Programming with Dependent Types.

Installing Coq on your own machine

There is a few different ways to install Coq, depending on your system and your level of familiarity with terminal/editors etc UNIX tools, pick what works for you best.

Install CoqIDE through the packaged releases

Easy-install packages are available from the Coq download page. You should install the version specified in the Preface chapter of the Logical Foundations text.

Install Coq through OPAM

Alternatively you can install Coq through opam the OCaml package manager and use it with Proof General an Emacs IDE. This is a cross-platform way of installing Coq and in general, more eyes look at opam and proof-general releases than the easy-install packages, so it is a safe bet. First install opam . On MacOS you can use Homebrew by running

      brew install opam
      

If this installation fails, talk to your TA. Then in your terminal run the following commands in order. Don't forget to plug in the right Coq version from the Preface chapter of Logical Founcations.

      opam init
      eval $(opam env)
      opam pin add coq "Coq version"
      opam install coq
      

At this point you should see opam initialize itself successfully. Coq should be installed, but not necessarily in your system PATH. Try it out just to be sure

      coqc -v
      

If this works then everything is good with your Coq installation and you can skip to installing Proof General. If that did not work, then edit your "~/.bashrc" or "~/.bash_profile" and add the following line at the end of the file.

      export PATH=$PATH:$HOME/.opam/default/bin
      

Now in a new terminal window, try again running "coqc" and that should work this time, if not ask your TA for help.

Installing Proof-General

Next, to install your editor and IDE! First, download and install Emacs a general-purpose text editor with many features. Then, you want to setup MELPA for Emacs, a package manager. To do that edit the file "~/.emacs" and add the following lines at the end..

      (require 'package)
      (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
      (package-initialize)
      

Now open your Emacs editor and press Alt+x (M-x in Emacs talk) then write "package-install" then press Enter. It will say "Install package:" and expect you to write something. Write "proof-general" and hit "Enter". It should connect to the MELPA repository and download the proof-general package. We are almost done. Now, all we need to do is connect Proof General and your Coq installation. Open ~/.emacs and at the end, append the following lines then save and exit Emacs.

      ;; ========= OCaml path ==========
      (setq home-path (getenv "HOME"))
      (setq opam-bin-path (concat home-path "/.opam/default/bin"))
      (setenv "PATH" (concat (getenv "PATH") (concat ":" opam-bin-path ":/usr/local/bin")))
      (add-to-list 'exec-path "/usr/local/bin")
      (add-to-list 'exec-path opam-bin-path)
      

And that should be all! Now you have to learn basic Emacs usage hotkeys below and way more by doing an Emacs tutorial.

• C-x C-f: Open file for editting.
• C-x C-s: Save file.
• C-x C-c: Quit emacs
• C-g: Cancel this command I started
• C-x C-k: Close this file

Using ProofGeneral

There are only a few commands you need to know to use ProofGeneral effectively. They are:

• C-c C-n: send the next command to Coq.
• C-c C-u: undo (retract) the most recently executed command.
• C-c C-RET: submit everything up to the current cursor location to Coq for processing.
• C-c C-. : move the cursor to the end of the last command which has been processed by Coq.
• C-c . : toggle "electric terminator mode". When this mode is turned on, simply typing a period will send the current command to Coq (normally you have to type a period and then type C-c C-n).

Installing VSCoq

If that is not enough editors for you, how about yet another one, Visual Studio Code. Install it through the official installer, then through the Visual Studio Marketplace install the VSCoq plugin.