-
- -
- 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.
-
-
-