Installing Coq for Spacemacs

I had a very hard time getting Coq to work as expected on Spacemacs. I collected everything I found and made this little tutorial.

First of all we need to install Coq, though Opam. Debian-based users can do this with apt-get.

sudo apt-get install opam 
opam install coq

The next step is getting Proof General. Proof General is a generic front-end for proof assistants based on Emacs.

git clone ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG

The next step is installing company-coq with MELPA. Luckily, MELPA comes with the default Spacemacs installation. Just use M-x package-refresh-contents RET followed by M-x package-install RET company-coq RET to install and byte-compile company-coq and its dependencies (some of them will produce a few warnings; that’s OK).

Next, we have to download a Coq layer for Spacemacs. This will provide all the keybindings and configurations we need to start working.

Before dowloading the layer we need to change the dotspacemacs-configuration-layer-path in our .spacemacs dotfile. Find that line and change it like this:

dotspacemacs-configuration-layer-path '("~/.spacemacs.d/")

This informs Spacemacs that we will keep our configuration layers in this folder, so then Spacemacs knows how to reach them. Now we need to create the directory and clone the layer.

mkdir ~/.spacemacs.d
mkdir ~/.spacemacs.d/layers
cd ~/.spacemacs.d/layers
git clone
mv spacemacs-coq coq

We’re almost finished. Let’s go to the location of the layer we’ve just downloaded and open config.el. We need to change the proof-general-path:

(defvar proof-general-path "/home/yourname/.emacs.d/lisp/PG/generic/proof-site"
  "The path to proof general")

The thing is that this solution is unique to each user, you need to adapt the path to your own setup.

Finally, the last step (totally optional) will serve Evil users. If this is not configured, everytime you hit <ESC>, Emacs will autocomplete the current line.

(setq evil-want-abbrev-expand-on-insert-exit nil)

This should be added before Evil loads, that means, before dotspacemacs/user-init in your .spacemacs file. This was found here.