Software Foundations in Coq
This page contains useful materials for the Coq Boot Camp and lectures on
Software Foundations in Coq.
Hints on Using Coq for OPLSS 2013
These notes are intended to help you get a working and useful version of Coq 8.4
running on your laptop or other personal machine prior to the boot camp.
If you find errors here or have suggestions that might be useful for others,
let me know (by mail to
email@example.com) and I'll update this page.
What you'll need
A working Coq installation contains several pieces:
- the Coq compiler (
- the read-eval-print loop (
- the standard libraries
- some form of integrated development environment (IDE); see more details below
- miscellaneous other tools
- the Reference Manual and
Standard Library documentation.
Choosing an IDE
To use Coq effectively, you must have a working IDE for it.
There are two in common use:
Both of these IDE's work by running a
- Proof General (PG) is a generic IDE
proof assistants that runs under Emacs. If you are
already an emacs user (or want to become one), I strongly recommend this option, because
it is reliable and easy to install.
- CoqIDE is
a standalone tool designed specifically for use with Coq, and is part of the standard source release (and some
binary releases). It is based on GTK and implemented in Ocaml. CoqIDE is a reasonable option
if you don't know (or you dislike) emacs, but it is less reliable and can be hard to build and install.
coqtop process in the background, so this
must be installed successfully in any case.
Most of the required pieces can be obtained from the
official Coq Download page.
The most recent stable release of Coq is version 8.4pl2.
For the version of the Software Foundations textbook we will use,
any variant of Coq version 8.4 should work (but Windows/CoqIDE users
see note below). Versions below 8.4 will not work.
Proof General can be downloaded from here;
you should use the most recent stable version, which is 4.2.
Some platform-specific notes on installation follow:
- linux. Use a package manager if you can: e.g.,
there are 8.4pl2 versions of Coq (with and without CoqIDE) on
Debian/testing, and an 8.4pl1 (apparently without CoqIDE) on gentoo.
Otherwise, you'll need to compile from source
from the Download page.
Once you have the necessary prerequisites installed, this is usually straightforward
except for CoqIDE, which often has build problems.
- MacOS. You should use
coqide-8.4pl2.dmg from the
Download page if you can,
but the binaries it installs do not work for me under MacOS 10.7 (better results
have been reported under MacOS 10.8). An earlier version that does
work for me under 10.7 is here: coqide-8.4.dmg.
Macports claims to have an 8.4pl2 package available including CoqIDE.
If you don't need CoqIDE, the
coq-8.4.dmg file from the
Download page should work,
or you can build from source (again, building CoqIDE from source is often problematic),
or fetch from homebrew (which has 8.4pl2, but without CoqIDE).
- Windows. The
installer on the Download page reportedly works.
If you are using CoqIDE, make sure you install 8.4pl2; earlier 8.4 versions have serious bugs that
make CoqIDE almost usable. If you want to use PG instead of CoqIDE,
you may need to add the Coq bin directory to your path.
Although both CoqIDE and PG come with lots of fancy features, you really only need support for four
It is essential that at least the first three of these commands be bound to keyboard shortcuts,
as you will use them constantly when working on Coq script files. While both IDE's support such
shortcuts, they can be tricky to get right on Macs and (for CoqIDE) on some linux window managers.
CoqIDE users should plan on needing to edit their
- Execute one tactic step forward.
- Undo one tactic step backward.
- "Goto" the cursor position, executing forward or undoing backward as necessary.
- Interrupt the current command or tactic (important when the underlying
slow or unresponsive).
.coqide.keys file directly,
as described in the documentation;
this page may also be useful.
- PG: In my experience, 3-pane mode doesn't work too reliably; using just 2 panes is generally fine.
Use the Coq pull-down menu to toggle the pane mode.
- PG: To handle the fairly large Coq files in Software Foundations, you'll need to increase the
"undo limit" by putting adding something like
'(coq-default-undo-limit 10000) to your
- CoqIDE: Be warned that the autosave feature (enabled by default) has often been unreliable
in the past, and the IDE crashes fairly often. Use explicit saves, early and often!
Exercises worked during the boot camp or suggested as especially
good homework targets:
- boolean functions
- pigeonhole principle