It doesn't matter if you're an Emacs militant or a pacifist!

Proof General will be useful to you if you use a proof assistant, and you'd like some of the following features:

A proof script is a sequence of commands sent to a proof assistant to construct a proof, usually stored in a file. Script management connects the editing of a proof script directly to an interactive proof process, maintaining consistency between the edit buffer and the state of the proof assistant.

Proof General colours a proof script to show the state in the proof assistant. Parts of a proof script that have been processed are displayed in blue and are "locked" -- they cannot be edited. Parts of the script currently being processed by the proof assistant are shown in red. Commands are provided to process new parts of the buffer, or undo already processed parts.

Take a look at this screenshot of Proof General to see script managament in action.

Script management in Proof General can work across many script files. When a script is visited in the editor, it is coloured to reflect whether the proof assistant has loaded it in this session.

Dependencies between script files is communicated from the proof assistant to Proof General. If you want to edit a file which has been loaded into the proof assistant already, Proof General will unlock the file and all the files which depend on it. This connects the editor with the theory dependency or make system of the proof assistant.

Proof by pointing allows you to click on a subterm of a goal to be proved, and apply an appropriate rule or tactic automatically.

Proof by pointing uses the interface to highlight subterms under the mouse, and Proof General uses the subterm structure to make it easy to cut and paste complicated subterms.

Proof General has a toolbar with buttons for starting a proof, manoeuvring in the proof script, restarting the prover and saving a proof.

Using the toolbar, you can replay proofs without knowing any low-level commands of the proof assistant or any Emacs hot-keys!

Syntax highlighting is an editing feature which decorates a file with different colours or fonts according to the syntax of some language (usually a programming language).

Proof General decorates proof scripts: proof commands are highlighted and different fonts may be used for definitions and assumptions, for example.

Tags are an editing feature which allow you to quickly locate the definition or declaration of a particular identifier.

Proof General is supplied with utilities to make tag indexes for Emacs. This makes it easy to quickly access definitions from a standard library, for example, and in large proof developments split across multiple files.

A pull-down menu gives easy access to definitions, declarations and proofs in the current buffer.

Sometimes you may want to run a proof assistant on a powerful remote machine. Proof General can communicate with a proof assistant running remotely, while your files and editor reside on your local machine.

Proof General is designed to be generic, so you can adapt it to a new proof assistant if you know a little bit of Emacs Lisp.

Adapting for a new proof assistant is mainly a matter of setting some variables with regular expressions to help parse output from the prover, and setting other variables with commands to send to the prover. To get the most from Proof General (proof-by-pointing, for example), it may be necessary to augment the output routines of the proof assistant.

Please feel free to download Proof General to customize it for a new system, and how you get on.

For more details of the above features, see the