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 (coqtop):

$ 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 apt-get it:

$ 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>

Expand 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 coq-mode-hook:

(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!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: