It doesn't matter if you're an Emacs militant or a pacifist!
Proof General is designed to be useful for novices and expert users alike.
It will be useful to you if you use a proof assistant, and
you'd like an interface with the following features:
script management,
multiple file scripting,
proof by pointing,
toolbar and menus,
syntax highlighting,
real symbols,
definitions menu,
tags,
and finally,
adaptability.
Are you convinced yet?
If not, read on…
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.
Dependencies between script files are either communicated from the proof assistant to Proof General, or maintained automatically by Proof General (based on the order in which files were processed).
Proof by pointing uses the interface to highlight subterms under the mouse, and sends messages asking the prover for hints to proceed. Proof General also uses the subterm structure to make it easy to cut and paste from complicated terms.
Using the toolbar, you can replay proofs without knowing any low-level commands of the proof assistant or any Emacs hot-keys!
Additionally, the toolbar commands and many more besides are available on menus; you don't need to know magical key presses for any features.
Proof General decorates proof scripts: proof commands are highlighted and different fonts may be used for definitions and assumptions, for example.
Most importantly, Proof General is generic, so you can adapt it to a new proof assistant with surprisingly little effort.
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. See this basic . To get the most from Proof General (proof by pointing, for example), it may be necessary to put some hooks in 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 (even) more details of the above features, see the