CIS 500: Coq Resources

Running Coq on SEAS Systems

On any SEAS Linux machine, including the ones in the lab (Moore 100A), you should be able to start up CoqIDE by typing something like this:
         /mnt/eclipse/unsupported/linux/coq-latest/bin/coqide lec01.v
You can avoid typing this long string every time by adding something like
         export PATH=$PATH:/mnt/eclipse/unsupported/linux/coq-latest/bin
to your .bashrc file (if you use the bash shell -- users of other shells will need a different incantation). Then you can type just
         coqide lec01.v
to run Coq.

Using CoqIDE

The CoqIDE user interface is pretty self-explanatory. Use the up/down buttons at the top of the window to send parts of your proof script to Coq for processing (down) or to retract parts that have already been sent so that you can edit them again (up).


The main Coq page includes a comprehensive reference manual, an FAQ, and pointers to some other useful resources.

For those who wish to go deeper with Coq, the book Interactive Theorem Proving and Program Development, by Yves Bertot and Pierre Castéran is recommended.

Installing Coq on your own machine

Easy-install packages are available from the Coq download page. (At the moment, the link to the Windows installer of the most up-to-date version, 8.1pl1, seems to be missing, and there are no pre-built installers for OS X. It is fine to install the previous version, 8.1, instead.) Note that you'll need both Coq itself and some development environmnent -- either CoqIDE (try this first, since it is simpler to use, but may be tricky to install on some platforms) or Proof General.