Software Installation

We'll use Coq V8.4, for various platforms:

Windows: Installation is straightforward, just grab this and run it. This will also install the coqide program, which you'd like to run after the installation.
Linux: is Coq's favorite place to run. You may simply run (on debian/Linux)
```
  # apt-get install coq
```
Or else you may grab the sources here and compile from scratch.
Macintosh: Grab the package here.

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

However, there is another popular IDE: Proof General, and it's more popular in the Coq community. We'll use proof general in this course.

The installation of proof general is simple:

Linux:

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

There are only a few commands you need to know to use ProofGeneral effectively:

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.