1. Introducing Proof General

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 script(2) 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 accidentally. 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, suggestions, 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.

1.1 Installing Proof General

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 section Obtaining and Installing.

1.2 Quick start guide

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:

(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 coq-mode, to turn a buffer into a Coq 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 section Walkthrough example in Isabelle. If you know the syntax for proof scripts in another theorem prover, you can easily adapt the details given there.

1.3 Features of Proof General

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!

• Simplified interaction
  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). Communication takes place via three buffers. 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. This means that the user normally only sees the output from the most recent interaction, rather than a screen full of output from the proof assistant.

  Proof General does not commandeer the proof assistant shell: the user still has complete access to it if necessary.

  For more details, see section Summary of Proof General buffers and see section Display customization.

• Script management
  Proof General colours proof script regions blue when they have been processed by the prover, and colours regions red when the prover is currently processing them. The appearance of Emacs buffers always matches the proof assistant’s state. Coloured parts of the buffer cannot be edited. Proof General has functions for asserting or retracting parts of a proof script, which alters the coloured regions.

  For more details, see section Basic Script Management, Script processing commands, and Advanced Script Management and Editing.

• Script editing mode
  Proof General provides useful facilities for editing proof scripts, including syntax highlighting and a menu to jump to particular goals, definitions, or declarations. Special editing functions send lines of proof script to the proof assistant, or undo previous proof steps.

  For more details, see section Script editing commands, and Script processing commands.

• Proof-tree visualization
  In cooperation with the external program Prooftree (available from the Prooftree website), Proof General can display proof trees graphically and provide visual information about the proof status of different branches in a proof. The proof-tree display provides additional means for inspecting the proof tree and thus helps against loosing track in proofs.

  The graphical proof-tree visualization is currently only supported for Coq. For more details, see section Graphical Proof-Tree Visualization.

• Toolbar and menus
  A script buffer has a toolbar with navigation buttons for processing parts of the proof script. A menu provides further functions for operations in the proof assistant, as well as customization of Proof General.

  For more details, see section Toolbar commands, Proof assistant commands, and Customizing Proof General.

• Proof by pointing
  Proof General has support for proof-by-pointing and similar features. Proof by pointing allows you to click on a subterm of a goal to be proved, and automatically apply an appropriate proof rule or tactic. Proof by pointing is specific to the proof assistant (and logic) in use; therefore it is configured mainly on the proof assistant side. If you would like to see proof by pointing support for Proof General in a particular proof assistant, petition the developers of the proof assistant to provide it.

1.4 Supported proof assistants

Proof General comes ready-customized for several proof assistants, including these:

• Coq Proof General for Coq Version 8.2
  See section Coq Proof General, for more details.
• EasyCrypt Proof General for EasyCrypt
  See section EasyCrypt Proof General, for mode details.
• Shell Proof General for shell scripts (not really a proof assistant!)
  See section Shell Proof General, for more details.

Proof General is designed to be generic, so if you know how to write regular expressions, you can make:

• Your Proof General for your favourite proof assistant.
  For more details of how to make Proof General work with another proof assistant, see the accompanying manual Adapting Proof General.

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 has been supported only in LEGO so far. 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.

1.5 Prerequisites for this manual

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 section 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:

C-h i

info

C-h m

describe-mode

C-h b

describe-bindings

C-h f

describe-function

C-h v

describe-variable

1.6 Organization of this manual

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.

This document was generated on April 20, 2024 using texi2html 1.82.