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
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 https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG cd ~/.emacs.d/lisp/PG make
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:
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 https://github.com/olivierverdier/spacemacs-coq.git 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
(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.