coq Getting started with coq Install Coq on MacOS

Example

You can install the whole bundle by downloading the dmg package from here.

The bundle contains a CoqIDE that can be used for writing your proofs or you can use coqtop command to run the interpreter on your terminal

Installation of Coq on MacOS is easy using homebrew as well

brew install coq

or if you use MacPorts

sudo port install coq

There is no good vi support for Coq. You can use Proof General within emacs which has a good usability.

To install Proof General remove old versions of Proof General clone the new version from GitHub

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

Then add the following to your .emacs:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

Make sure that the emacs you are running the actual Emacs. If you face version mismatch problems you might have to run makefile again specifying Emacs path explicitly

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs