+
+ -
+ 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. 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 managament in action.
+
+
+
+ -
+ Proof General is designed for proof assistants which have a
+ command-line shell interpreter. When using Proof General, the proof
+ assistant's shell is hidden from the user. Communication takes
+ place via three buffers (Emacs text widgets). The script
+ buffer holds input, the commands to construct a proof. The
+ goals buffer displays the current list of subgoals to be
+ solved. The response buffer displays other output from the
+ proof assistant. By default, only two of these three buffers are
+ displayed at once. This means that the user only sees the output
+ from the most recent interaction, rather than a screen full of
+ output from the proof assistant.
+
+ 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.
+
+
+
+ -
+ Script management in Proof General can work across many script
+ files, integrating with the file handling of
+ the proof assistant. When a script is visited in the editor, it
+ is locked (coloured) to reflect whether the proof assistant has
+ loaded it in this session. When a file is unlocked, all of the
+ files which depend on it are automatically unlocked too.
+
+ 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 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 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.
+
+
+
+
+ -
+ Proof General has a toolbar with buttons for examining
+ the proof state, starting a proof, manoeuvring in the proof script,
+ restarting the prover, saving a proof, searching for a theorem,
+ issuing a command, interrupting the assistant, and getting help.
+
+ 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.
+
+
+
+
+ -
+ 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.
+
+
+
+ -
+ Proof General has a close integration with the
+ powerful
+ X-Symbol
+ package, which makes it easy to transparently use real symbols and
+ Greek letters in your proofs.
+
+ Instead of seeing "not P", you see "¬ P", instead
+ of "a * b", you see "a × b", etc.
+
+ (Those examples are simple so they will work on most browsers
+ without needing images, see the
+ screenshots for more examples.)
+
+
+
+
+ -
+ A pull-down menu gives easy
+ navigations to theorems, definitions, and declarations
+ proved 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.
+
+
+
+ -
+ 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.
+
+
+
+
+ -
+ Proof General is designed to be adaptable. Many aspects
+ of its behaviour can be easily customized (using dialogue boxes and
+ buttons, no text file editing!).
+
+ 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.
+
+
+