Software Installation

We'll use Coq V8.4pl3, take a look at the Coq download page.

The official IDE to edit Coq source code is "CoqIde", which comes with Coq. It's great and you may try it.

There is another popular IDE (my favorite): Proof General, and it's more popular in the Coq community. You may try it.

The installation of proof general is simple:

Linux:

  # apt-get install proofgeneral
  # apt-get install proofgeneral-coq

Windows: there is a pre-built version hacked by us based on GNU emacs. You should uncompress this archive and put it at (important!):
```
  d:\emacs-23.1
```
And it also assumes the Coq executable is at "C:\program files\Coq\bin", if that's not the case, change the file "d:\emacs-23.1\bin\coq-emacs.bat" accordingly.

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).

Run Proof General. Visit the file Basics.v. And happy hacking.