Organize your proofs!
It doesn't matter if you're an Emacs militant or a pacifist!
The aim of Proof General is to provide powerful and configurable interfaces which help user-interaction with proof assistants. Proof General targets power users rather than novices, but is designed to be useful to both. Proof General leads to an environment for serious proof engineering of interactively-constructed proofs.
Proof General is used by many people for organizing large proof developments, and also for teaching interactive proof. They enjoy the following features:
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. Bodies of completed proofs in the locked region can be hidden from view to help browsing. Proof General has commands for processing new parts of the buffer, or undoing already processed parts.
Take a look at these screenshots of Proof General to see script management in action.
Despite this more friendly communication model, Proof General does not commandeer the proof assistant shell: the user still has complete access to it if necessary.
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).
Using hidden markup in the concrete syntax, Proof General allows the user to explore the structure of complex terms output by the prover. This provides nifty features for cutting-and-pasting subterms, querying the type of a subterm, looking up the definition of an identifier, and so on.
Proof by pointing uses this markup to allow the prover to suggest steps in a proof, guided by the user's gestures in displayed goals. For example, clicking on a hypothesis inserts a proof step into the script to solve a goal using that hypothesis, and executes it.
[Subterm markup is only fully supported by LEGO at the moment, with an experimental implementation of proof by pointing. Isabelle highlights only variables. If you would like to see these features better supported in your favourite proof assistant, please canvas the implementor to add subterm-markup support.]
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.
Alternatively or additionally, you can use Proof General's own Unicode Tokens mode which provides a presentation view on the source text by rendering sequences of characters using symbols, fonts and positioning information (see the screenshots for examples.)
Many facilities are provided for editing proof scripts. The completion mechanism of Emacs can be used to help type keywords and identifier names. The outline mode of Emacs allows hiding of parts of proof scripts; a further special proof hiding facility is provided to hide the body of completed proofs. Navigation in the script is supported by a pull-down menu which gives easy access to the theorems, definitions, and declarations in the current buffer.
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 example instance. 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 tell us how you get on.
For (even) more details of Proof General's features, see the manuals and papers on the documentation page.