Coq / Proof General Setup

Opam

Coq / ssreflect

opam install coq.8.9.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

Proof General (or other editors)

I use emacs, and specifically spacemacs (though with “holy” emacs key bindings), so my preferred environment for interacting with Coq is Proof General, but you are welcome to (try to) use whatever you’d like. Be aware, however, that probably >99% of the Coq development that happens takes place in Emacs/Proof General… There is a dedicated IDE called CoqIDE (you can install via opam) – I’ve heard mixed things about it in the past. There is in-progress work on a VSCode plugin (there was one that bitrotted, and there is active work right now to fix it, so people who want to experiment can look at: https://github.com/coq-community/vscoq). For Vim, there is something called coq-au-vim, but it seems to be not very well maintained (e.g., not bothering to make minimal changes needed to support neovim), and I’m guessing many vim people are just happier using spacemacs (which by default uses evil mode, which is a pretty extensive vim emulation) and Proof General.

With that in mind, installing Proof General in Spacemacs just means adding the coq layer. This will also install company-coq, which despite the name, does a lot more than auto-completion: probably the most immediately noticeable is that it makes a lot of symbols prettier.

See http://develop.spacemacs.org/layers/+lang/coq/README.html for docs.

In Spacemacs, the key binding prefix is SPC m, and 90% of what you will do is SPC m ., which means “run prover to point”. You will also, eventually, probably find it convenient to run Print, Check, and Search via commands rather than by writing them down into the script. This isn’t necessary, but these all have key bindings as well.

If you are not using Spacemacs, you can install Proof General via melpa, see: https://proofgeneral.github.io/. Without Spacemacs, the same “run prover to point” is given the key binding C-c C-RET.

Anytime you edit within the evaluated region, the prover is stepped back to before the edits.