Tools for formal reasoning on the Department's computer systems
Various tools for formal reasoning, and their related
dependencies, have been installed under the
directory /home/group/formal/ in the Department's
computer systems.
To get the programs into your path, enter the following line in a shell prompt:
. /home/group/formal/use.sh
You can also add the line to your ~/.bash_profile to
make it executed automatically upon login.
To make the Emacs libraries usable, evaluate the following expression in GNU Emacs:
(load-file "/home/group/formal/use.el")
You can evaluate the expression either by typing M-: in
emacs, or by adding the line to your ~/.emacs file.
The installed software includes:
- Coq 8.2pl1
-
- Links
- Hints
- Use the command rlwrap coqtop to get command-line editing and history. Even better, use Proof General (see below) under Emacs.
- Proof General 3.7.1
-
- Links
- Hints
-
After you have loaded the file
use.elin Emacs, Proof General should be automatically active for all files whose filename ends in.v. For starters, edit or open a Coq script that contains some commands. Make surecoq-modeis active. Type C-c C-n (i.e. Control-c followed by Control-n), and you should see in another buffer the result of Coq executing that command. Type C-c C-n to move forward, and C-c C-u to go backward. For more navigation commands, see Section 2.6 of the user manual.
- Ott 0.10.17
- Ssreflect 1.2
-
- Links
- Hints
- The ssrcoq binary is available, but you don't need to use it: you can just use Coq as normal, and import the ssreflect library with Require ssreflect. The language extension will be loaded automatically.
- Objective Caml 3.11.1