CIS 5000: Coq Resources

Coq Documentation

Although the course texts are intended to be self contained, 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.

Coq Development Environments

Option 1: VSCode and VSCoq (recommended)

The recommended option for working with Coq code is to use VSCode and connect to the Coq tools via a Docker container. For this setup, you need to take these steps:

Install your tools

1. Install/update Docker
2. Make sure that Docker is running
3. Install Visual Studio Code using the official installer. (Run it)
4. Install the Remote-Containers extension for VSCode.
5. Install the VSCoq extension for VSCode.

After setting up VSCode, you need to create a Coq project and tell VSCode to open it for processing in the Docker instance.

Configure a Coq Project

1. Create a new folder for your development. For instance, for the first part of the course, we use a directory called lf.
2. Create a subfolder in your project called .devcontainer and put the file devcontainer.json in this directory. (This file is what tells VSCode's Docker Plugin to use the Coq-configured environment.)
3. Create an appropriate _Coq_project file in the root folder of your project. For the `lf` project, its contents are:

             -Q . LF
   	  

   (The presence of a _Coq_project file triggers the VSCoq extension.)
4. In VSCode, use File > Open Folder to open the project. VSCode should detect the docker file and ask you whether you want to run the project in the container.

At this point, you should be able to create / open / visit a Coq file, e.g., Basics.v, and use the Coq interactive commands to step through the development. The VSCoq pages describe some handy shortcuts for stepping through your proof.

For more information about the Docker container, please see the au-fs22 GitHub Project.

You can also find the VSCode extensions by searching for them through the Visual Studio Marketplace in VSCode itself.

Option 2: Installing Coq on your own machine

There are 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.

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

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

Option 3: 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