# ProofGeneral 3.7

ProofGeneral is a powerful frontend for proof assistants based on Emacs.

- LICENSE TYPE:
- GPL (GNU General Public License)
- USER RATING:
- DEVELOPED BY:
**ProofGeneral Team**- HOMEPAGE:
- proofgeneral.inf.ed.ac.uk
- CATEGORY:
- ROOT \ Science and Engineering \ Mathematics

ProofGeneral is a powerful frontend for proof assistants based on Emacs. It is generic in that it supports a variety of proof assistants (among others, Isabelle, Lego, and PhoX) and provides for them script management, a simplified interaction model, subterm higlighting and more.

·

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

·

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.

·

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.

·

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.

·

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!

·

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.

·

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.

·

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.

· A proof assistant, for example: Coq; Isabelle/Isar; LEGO; PhoX (see links for versions).

· Version 21.4.1, 22.1.1 or 23.X beta version of GNU Emacs or version 21.4.20 or 21.5.beta28 of XEmacs. GNU Emacs is the preferred option.

**Here are some key features of "ProofGeneral":**·

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

·

__Simplified interaction model__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.

·

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

·

__Subterm highlighting and proof by pointing__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.

·

__Toolbar and menus__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!

·

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

·

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

·

__Proof-script editing facilities__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.

·

__Remote proof assistant__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__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.

·

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

**What's New**in This Release:· A proof assistant, for example: Coq; Isabelle/Isar; LEGO; PhoX (see links for versions).

· Version 21.4.1, 22.1.1 or 23.X beta version of GNU Emacs or version 21.4.20 or 21.5.beta28 of XEmacs. GNU Emacs is the preferred option.

Last updated on March 29th, 2008

#### Add your review!

SUBMIT