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.

Linux

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

Windows

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

OS/X

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 https://raw.githubusercontent.com/Homebrew/install/master/install)"

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.