Next: Basic Script Management, Previous: Preface, Up: Top [Contents][Index]
Proof General is a generic Emacs interface for interactive proof assistants,1 developed at the LFCS in the University of Edinburgh.
You do not have to be an Emacs militant to use Proof General!
The interface is designed to be very easy to use. You develop your proof script2 in-place rather than line-by-line and later reassembling the pieces. Proof General keeps track of which proof steps have been processed by the prover, and prevents you editing them accidently. You can undo steps as usual.
The aim of Proof General is to provide a powerful and configurable interface for numerous interactive proof assistants. We target Proof General mainly at intermediate or expert users, so that the interface should be useful for large proof developments.
Please help us!
Send us comments, suggestsions, or (the best) patches to improve support for your chosen proof assistant. Contact us at https://github.com/ProofGeneral/PG/issues.
If your chosen proof assistant isn’t supported, read the accompanying Adapting Proof General manual to find out how to configure PG for a new prover.
If Proof General has not already been installed for you, you should unpack it and insert the line:
(load "proof-general-home/generic/proof-site.el")
into your ~/.emacs file, where proof-general-home is the top-level directory that was created when Proof General was unpacked.
For much more information, See Obtaining and Installing.
Once Proof General is correctly installed, the corresponding Proof General mode will be invoked automatically when you visit a proof script file for your proof assistant, for example:
Prover | Extensions | Mode |
LEGO | .l | lego-mode |
Coq | .v | coq-mode |
Isabelle | .thy | isar-mode |
Phox | .phx | phox-mode |
HOL98 | .sml | hol98-mode |
HOL Light | .ml | hol-light-mode |
ACL2 | .acl2 | acl2-mode |
Twelf | .elf | twelf-mode |
Plastic | .lf | plastic-mode |
Lambda-CLAM | .lcm | lclam-mode |
CCC | .ccc | ccc-mode |
PG-Shell | .pgsh | pgshell-mode |
(the exact list of Proof Assistants supported may vary according to the version of Proof General and its local configuration). You can also invoke the mode command directly, e.g., type M-x lego-mode, to turn a buffer into a lego script buffer.
You’ll find commands to process the proof script are available from the toolbar, menus, and keyboard. Type C-h m to get a list of the keyboard shortcuts for the current mode. The commands available should be easy to understand, but the rest of this manual describes them in some detail.
The proof assistant itself is started automatically inside Emacs as an "inferior" process when you ask for some of the proof script to be processed. You can start the proof assistant manually with the menu command "Start proof assistant".
To follow an example use of Proof General on a Isabelle proof, see Walkthrough example in Isabelle. If you know the syntax for proof scripts in another theorem prover, you can easily adapt the details given there.
Why would you want to use Proof General?
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: simplified interaction, script management, multiple file scripting, a script editing mode, proof by pointing, proof-tree visualization, toolbar and menus, syntax highlighting, real symbols, functions menu, tags, and finally, adaptability.
Here is an outline of some of these features. Look in the contents page or index of this manual to find out about the others!
Proof General does not commandeer the proof assistant shell: the user still has complete access to it if necessary.
For more details, see Summary of Proof General buffers and see Display customization.
For more details, see Basic Script Management, Script processing commands, and Advanced Script Management and Editing.
For more details, see Script editing commands, and Script processing commands.
The graphical proof-tree visualization is currently only supported for Coq. For more details, see Graphical Proof-Tree Visualization.
For more details, see Toolbar commands, Proof assistant commands, and Customizing Proof General.
Proof General comes ready-customized for several proof assistants, including these:
Proof General is designed to be generic, so if you know how to write regular expressions, you can make:
The exact list of Proof Assistants supported may vary according to the version of Proof General you have and its local configuration; only the standard instances documented in this manual are listed above.
Note that there is some variation between the features supported by different instances of Proof General. The main variation is proof by pointing, which is only supported in LEGO at the moment. For advanced features like this, some extensions to the output routines of the proof assistant are required, typically. If you like Proof General, please help us by asking the implementors of your favourite proof assistant to support Proof General as much as possible.
This manual assumes that you understand a little about using Emacs, for example, switching between buffers using C-x b and understanding that a key sequence like C-x b means "control with x, followed by b". A key sequence like M-z means "meta with z". (Meta may be labelled Alt on your keyboard).
The manual also assumes you have a basic understanding of your proof assistant and the language and files it uses for proof scripts. But even without this, Proof General is not useless: you can use the interface to replay proof scripts for any proof assistant without knowing how to start it up or issue commands, etc. This is the beauty of a common interface mechanism.
To get more from Proof General and adapt it to your liking, it helps to know a little bit about how Emacs lisp packages can be customized via the Customization mechanism. It’s really easy to use. For details, see How to customize. See (emacs)Customization, for documentation in Emacs.
To get the absolute most from Proof General, to improve it or to adapt it for new provers, you’ll need to know a little bit of Emacs lisp. Emacs is self-documenting, so you can begin from C-h and find out everything! Here are some useful commands:
info
describe-mode
describe-bindings
describe-function
describe-variable
This manual covers the user-level view and customization of Proof General. The accompanying Adapting Proof General manual considers adapting Proof General to new proof assistants, and documents some of the internals of Proof General.
Three appendices of this manual contain some details about obtaining and installing Proof General and some known bugs. The contents of these final chapters is also covered in the files INSTALL and BUGS contained in the distribution. Refer to those files for the latest information.
The manual concludes with some references and indexes. See the table of contents for full details.
A proof assistant is a computerized helper for developing mathematical proofs. For short, we sometimes call it a prover, although we always have in mind an interactive system rather than a fully automated theorem prover.
A proof script is a sequence of commands which constructs a proof, usually stored in a file.
Previous: Prerequisites for this manual, Up: Introducing Proof General [Contents][Index]