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
(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
This section was added 2016-02-27.
First, clone the layer:
git clone https://github.com/olivierverdier/spacemacs-coq ~/.emacs.d/private/coq
dotspacemacs-configuration-layers. You can edit your
SPC f e d and reload it with
SPC f e R.