Running Coq on SEAS Systems
On any SEAS Linux machine, including the ones in the labs (Moore
100A, 100C, and 207), you should be able to start up CoqIDE by typing something
like this at a command prompt:
coqide Basics.v
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).
Documentation
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. You should install version 8.3.
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
for emacs.
Using ProofGeneral
There are only a few commands you need to know to use ProofGeneral
effectively. They are:
- C-c C-n: send the next command to Coq.
- C-c C-u: undo (retract) the most recently executed
command.
- C-c C-RET: submit everything up to the current cursor
location to Coq for processing.
- C-c C-. : move the cursor to the end of the last command
which has been processed by Coq.
- C-c . : toggle "electric terminator mode". When this mode
is turned on, simply typing a period will send the current
command to Coq (normally you have to type a period and then type
C-c C-n).
