Getting Started With Coq and Proof General
Today we’ll be talking about Coq. Coq is a dependently typed programming language and theorem proof assistant. Given that I’ve just now got the toolchain installed, I’m hardly qualified to say much more than that. However, I am qualified to talk about installing the toolchain, which is precisely what I intend to do.
To get started with Coq, you’ll need the usual things: a properly configured editor and the Coq compiler. Installing these isn’t terribly difficult. First, let’s install the compiler. If you’re running Ubuntu, this is quite simple:
$ sudo apt-get install coq
After this is done, you should have access to the compiler (
coqc) and the REPL (
$ which coqc /usr/bin/coqc $ which coqtop /usr/bin/coqtop $ coqc --version The Coq Proof Assistant, version 8.4pl4 (July 2014) compiled on Jul 27 2014 23:12:44 with OCaml 4.01.0
OK! Now for the (slightly) harder part: our properly configured editor. Here we have two choices: CoqIDE or Proof General. CoqIDE is a simple IDE that ships with Coq, so if you’re satisfied with this, then feel free to stop reading now: CoqIDE comes with Coq and should be already installed at this point!
However, if you want to be truly cool, you’ll opt for Proof General. Proof General is an Emacs plugin. Unfortunately, Proof General is not available in Melpa, so we get to install it manually. Fortunately for us, Proof General is in the repos, so if you’re running Ubuntu you can just
$ sudo apt-get install proofgeneral proofgeneral-doc
This will install Proof General, and set Emacs to load it up when you open a
.v file. (My condolences to all those who write Verilog and Coq on the same machine) However, some configuration remains to be done. First fire up emacs and execute:
M-x customize-group <enter> proof-general <enter>
Proof Assistants and ensure
Coq is selected. Now open up a
.v file and behold the glory!
Wait a minute, where’s my undo-tree? My rainbow-delimiters? My whitespace-mode? It’s not your imagination, Proof General has inexplicably ignored your fancy
.emacs config. This is all a bit irritating, but you can work around it by re-adding these things to the
(add-hook 'coq-mode-hook 'rainbow-delimiters-mode) (add-hook 'coq-mode-hook 'whitespace-mode) (add-hook 'coq-mode-hook 'undo-tree-mode)
This is a bit of a sorry state of affairs, and if anybody reading this knows a better way I’d love to hear it. For now, I got my shinies back, so it’ll do.
Regardless, Proof General should be ready to go at this point. We are ready to continue our journey down the rabbit hole into wonderland… See you all on the other side!