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
There are several good IDEs of varying levels of sophistication that you can use for developing Coq code.
Please post on the course discussion site if you encounter difficulties setting up your Coq development environment.
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. The procedure for this setup is described in the Preface chapter of Logical Foundations.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 Logical Foundations.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 runningbrew install opamIf 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 coqAt 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 -vIf 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/binNow 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