Installation of Coq

The version of Coq we use is 8.4 (not version 8.5). For installation questions on Linux, contact Robbert. For installation questions on OS/X, contact Kristoffer. For installation questions on Windows contact Kent.


Debian and Ubuntu users are recommended to use apt-get to install Coq.


Windows users are recommended to use the installer, which is available at the Coq download page.


If you have not already, install the HomeBrew package manager by pasting the following into Terminal and following the instructions presented.

ruby -e "$(curl -fsSL"

Run brew update, followed by brew install coq proof-general. Again, follow any instructions presented. In case you miss them, they can be recovered with brew info coq and brew info proof-general. In short, add

(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
(load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")

to your .emacs, and you are all set.