Previously I’ve used CoqIDE to interact with Coq, because I figured out it’d be tricky to set up Proof General. Proof General the Emacs interface to Coq and other interactive theorem provers. This time I decided to take the PG route and turns out it’s really easy if you’re using Homebrew! While at it, I also set up Ssreflect, which is an enhanced version of Coq with alternative standard library.

brew install emacs coq ssreflect

# Use --with-emacs to point to the Emacs you're using, so that the elisp
# files get compiled with the correct Emacs version.
brew install proof-general --with-emacs=/usr/local/bin/emacs

Next, do as Homebrew tells you and put these lines into your ~/.emacs:

(load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
(load-file "/usr/local/Cellar/ssreflect/1.5/share/ssreflect/pg-ssr.el")

Finally, customize Emacs variable coq-prog-name to the path of coqtop, i.e. /usr/local/bin/coqtop.

Spacemacs

This section was added 2016-02-27.

If you’re using Spacemacs, there’s now a very simple Coq layer available. It sets up Homebrew-installed Proof General, although it does not support Ssreflect.

First, clone the layer:

git clone https://github.com/olivierverdier/spacemacs-coq ~/.emacs.d/private/coq

Then, add coq to dotspacemacs-configuration-layers. You can edit your .spacemacs with SPC f e d and reload it with SPC f e R.