     START-INFO-DIR-ENTRY
     * ProofGeneral::Organize your proofs with Emacs!
     END-INFO-DIR-ENTRY

Proof General
*************

This file documents version 2.0 of Proof General, a generic Emacs interface for proof assistants.

Proof General 2.0 has been tested with XEmacs 20.4 and FSF GNU Emacs 20.2.  It is supplied ready customized for the proof assistants Coq, Lego, and Isabelle.

Introducing Proof General
*************************

A proof assistant is a computerized helper for developing mathematical proofs.

Proof General is a generic Emacs interface for proof assistants, developed at the LFCS in the University of Edinburgh.  It works best under XEmacs, but can also be used with FSF GNU Emacs.

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

Our aim is provide a powerful and configurable Emacs mode which helps user-interaction with interactive proof assistants.  Please help us with this aim!  Configure Proof General for your proof assistant, by adding features at the generic level wherever possible.  See Adapting Proof General to New Provers for more details, and send ideas, comments, patches, and code to proofgen@dcs.ed.ac.uk.

Quick start guide
=================

Proof General may have been installed for you already. If so, when you visit a proof script file for your proof assistant, 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 keys for the current mode.

The proof assistant is automatically started inside Emacs when you ask for some of the proof script to be processed.  To follow an example use of Proof General on a LEGO proof, see Walkthrough example in LEGO.

If Proof General has not already been installed, you should insert the line:

             (load "PROOFGENERAL/generic/proof-site.el")

into your ~/.emacs file, where PROOFGENERAL is the top-level directory that was created when Proof General was unpacked.

For more details on obtaining and installing Proof General, see Obtaining and Installing Proof General.

Features of Proof General
=========================

Why would you want to use Proof General?

Here is an outline of its main features.

  * Simplified communication
     The proof assistant's shell is normally hidden from the user. Communication takes place via two or 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 assistants. This means that the user only sees the output from the most recent proof step, rather than a screen full of output from the proof assistant.

     For more details, see Basic Script Management, see Script buffers and see Other buffers.

  * Script management
     Proof General colours proof script regions blue when they have already 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 Basic Script Management, see Script processing commands. and see Advanced Script Management.

  * Script editing mode
     Proof General provides useful facilities for editing proof scripts, including syntax hilighting 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 Script editing commands and see Script processing commands.

  * 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 Toolbar commands, see Proof assistant commands, and see Customizing Proof General.

Supported proof assistants
==========================

Proof General comes ready-customised for these proof assistants:

  * LEGO Proof General for LEGO Version 1.3.1

     All features of Proof General are supported. See LEGO Proof General for more details.

  * Coq Proof General for Coq Version 6.2

     All of features of Proof General are supported except multiple files. See Coq Proof General for more details.

  * Isabelle Proof General for Isabelle 98-1

     All features of Proof General are supported, except for an external tags program.  Isabelle Proof General handles theory files as well as ML (proof script files), and has an extensive theory file editing mode taken from Isamode (http://www.dcs.ed.ac.uk/home/da/Isamode). See Isabelle Proof General for more details.

Proof General is designed to be generic, so you can adapt it to other proof assistants if you know a little bit of Emacs Lisp.

  * Your Proof General for your favourite proof assistant

     See Adapting Proof General to New Provers for more details of how to do this.

Prerequisites for this manual
=============================

This manual assumes that 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 quite useless: you can still use the interface to replay proof scripts for any proof assistant without knowing how to start it up or issue commands, etc.

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.  See Easy customization and see Easy customization ((xemacs)) for details.

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

Basic Script Management
***********************

Proof scripts
=============

A proof script is a sequence of commands which construct a proof in a proof assistant.  Proof General is designed to work with text-based interactive proof assistants, where the mode of working is usually a dialogue between the human and the proof assistant.

Primitive interfaces for proof assistants simply present a shell-like view of this dialogue: the human repeatedly types commands to the shell until the proof is completed.  The system responds at each step, perhaps with a new list of subgoals to be solved, or perhaps with a failure report.  Proof General manages the dialogue to only show the human the information which is relevant at each step.

Often we want to keep a record of the proof commands used to prove a theorem, to build up a library of proved results.  An easy way to store a proof is to keep a text file which contains a proof script; the proof assitant usually provides facility to read a proof script from a file instead of the terminal.  Using the file, we can replay the proof script to prove the theorem again.

Using only a primitive shell interface, it can be tedious to construct proof scripts with cut-and-paste.  Proof General helps out by issuing commands directly from a proof script file, while it is being written and edited.  Proof General can also be used conveniently to replay a proof step-by-step, to see the progress at each stage.

Scripting is the process of building up a proof script file or replaying a proof.  When scripting, Proof General sends proof commands to the proof assistant one at a time, and prevents you from editing commands which have been successfully completed by the proof assistant. Regions of the proof script are analysed based on syntax and the behaviour of the proof assistant after each proof command.

Script buffers
==============

A script buffer is a buffer displaying a proof script.  Its Emacs mode is particular to the proof assistant you are using (but it inherits from proof-script mode).

A script buffer is divided into three regions: locked, queue and editing.  The proof commands in the script buffer can include a number of Goal-save sequences.

Locked, queue, and editing regions
----------------------------------

A script buffer is divided into three regions:

  * The locked region appears in blue (underlined on monochrome displays) and contains commands which have been sent to the proof process and verified. The commands in the locked region cannot be edited.

  * The queue region appears in pink (inverse video) and contains commands waiting to be sent to the proof process. Like those in the locked region, these commands can't be edited.

  * The editing region contains the commands the user is working on, and can be edited as normal Emacs text.

These three regions appear in the buffer in the order above; that is, the locked region is always at the start of the buffer, and the editing region always at the end. The queue region only exists if there is input waiting to be sent to the proof process.

Proof mode has two fundamental operations which transfer commands between these regions: assertion and retraction. Assertion corresponds to processing proof commands, and makes the locked region grow.  Retraction corresponds to undoing commands, and makes the locked region shrink.  See Script processing commands explains how to do assertion and retraction.

Goal-save sequences
-------------------

A proof script contains a sequence of commands used to prove one or more theorems.  Proof General assumes that for each proved theorem, a proof script contains a sequence of commands delimited by a pair of special commands, known as goal and save.  So a proof script has a series of proofs which look something like this (of course, the exact syntax will depend on the proof assistant you use):

        goal MYTHM is G
        ...
        save theorem MYTHM

Proof General recognizes the goal-save sequences in proof scripts.  The name MYTHM can appear in the menu for the proof script (see Support for function menus) to help quickly find a proof, and once a goal-save region has been fully processed by the proof assistant, it is treated as atomic when undoing proof steps.  This reflects the fact that most proof assistants discard the history of a proof once a it is completed or once a new proof is begun.

Active scripting buffer
-----------------------

You can edit as many script buffers as you want simultaneously, but only one buffer at a time can be used to process a proof script incrementally: this is the active scripting buffer.

The active scripting buffer has a special indicator: the word Scripting appears in its mode line.

Proof General will give an error message: Cannot have more than one active scripting buffer! if you attempt to use the script processing commands in a new script buffer when there is already an active scripting buffer which is only partly completed.  If you get this error message, you must choose either to assert the remainder of the active buffer, or to retract what has been proved so far, before you can start scripting in another buffer.

See Switching between proof scripts for more explanation of this.

Other buffers
=============

Proof General manages several kinds of buffers in Emacs.

  * The proof shell buffer is an Emacs shell buffer used to run your proof assistant.  Usually it is hidden from view (but see Working directly with the proof shell). Communication with the proof shell takes place via two or three intermediate buffers.

  * A script buffer, as we have explained, is a buffer for editing a proof script.  The active scripting buffer is the script buffer which is currently being used to send commands to the proof shell.

  * The goals buffer displays the list of subgoals to be solved for a proof in progress.  During a proof it is usually displayed together with the script buffer.

  * The response buffer displays other output from the proof assistant, for example error messages or informative messages. The response buffer is displayed whenever Proof General puts a new message in it.

Normally Proof General will automatically reveal and hide the goals and response buffers as necessary during scripting.  However there are ways to customize the way the buffers are displayed, see Display customization.

The menu Proof General -> Buffers provides a convenient way to display or switch to one of the four buffers: active scripting, goals, response, or shell.

Script editing commands
=======================

Script processing commands
==========================

 -- Command: proof-assert-next-command &optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command
     Process until the end of the next unprocessed command after point. If inside a comment, just process until the start of the comment. If you want something different, put it inside UNCLOSED-COMMENT-FUN. If IGNORE-PROOF-PROCESS-P is set, no commands will be added to the queue. Afterwards, move forward to near the next command afterwards, unless DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil, a space or newline will be inserted automatically.

 -- Command: proof-undo-last-successful-command &optional no-delete
     Undo last successful command at end of locked region. Unless optional NO-DELETE is set, the text is also deleted from the proof script.

 -- Command: proof-try-command &optional unclosed-comment-fun
     Process the command at point, but don't add it to the locked region. This will only happen if the command satisfies proof-state-preserving-p.

     Default action if inside a comment is just to go until the start of the comment. If you want something different, put it inside unclosed-comment-fun.

 -- Command: proof-retract-until-point &optional delete-region
     Sets up the proof process for retracting until point. In

             particular, it sets a flag for the filter process to call
             `proof-done-retracting' after the proof process has actually
             successfully reset its state. It optionally deletes the region in
             the proof script corresponding to the proof command sequence. If
             this function is invoked outside a locked region, the last
             successfully processed command is undone.

 -- Command: proof-process-buffer
     Process the current buffer and set point at the end of the buffer.

Why is C-c C-b useful?  Could just use the file to read it one go (will we have a command to do this other than via the process?). BUT it's nice because it stops exactly where a proof fails, so you can continue development from there.

Toolbar commands
================

Proof assistant commands
========================

 -- Command: proof-prf
     List proof state.

 -- Command: proof-ctxt
     List context.

 -- Command: proof-help
     Print help message giving syntax.

 -- Command: proof-execute-minibuffer-cmd
     Prompt for a command in the minibuffer and send it to proof assistant.

 -- Command: proof-interrupt-process
     Interrupt the proof assistant.  WARNING! This may confuse Proof General.

 -- Command: proof-execute-minibuffer-cmd
     Prompt for a command in the minibuffer and send it to proof assistant.

Walkthrough example in LEGO
===========================

Advanced Script Management
**************************

What we really mean by advanced is that Proof General supports large proof developments. These are typically spread across various files which depend on each other in some way. Proof General knows enough about the dependencies to allow script management across multiple files.

Switching between proof scripts
===============================

Basic modularity in large proof developments can be achieved by splitting proof scripts across various files. Let's assume that you are in the middle of a proof development. You are working on a soundness proof of Hoare Logic in a file called (The suffix may depend of the specific proof assistant you are using e.g, LEGO's proof script files have to end with .l.) HSound.l. It depends on a number of other files which develop underlying concepts e.g. syntax and semantics of expressions, assertions, imperative programs. You notice that the current lemma is too difficult to prove because you have forgotten to prove some more basic properties about determinism of the programming language. Or perhaps a previous definition is too cumbersome or even wrong.

At this stage, you would like to visit the appropriate file, say sos.l and retract to where changes are required. For further details on how to accomplish this, we refer to Retracting across files. Then, using script management, you want to develop some more basic theory in sos.l. Once this task has been completed (possibly involving retraction across even earlier files) and the new development has been asserted, you want to swich back to HSound.l and replay to the point you got stuck previously.

Some hours (or days) later you have completed the soundness proof and are ready to tackle new challenges. Perhaps, you want to prove a property that builds on soundness or you want to prove an orthogonal property such as completeness.

Proof General lets you do all of this while maintaining the consistency between proof script buffers and the state of the proof assistant. However, you cannot have more than one buffer where only a fraction of the proof script contains a locked region. Before you can employ script management in  another proof script buffer, you must either fully assert or retract the current script buffer.

View of processed files
=======================

Proof General is aware of all files that the proof assistant has processed or is currently processing. In fact, it relies on the proof assistant explicitly telling Proof General whenever it processes a new file which corresponds (For example, LEGO generates additional compiled (optimised) proof script files for efficiency.) to a file containing a proof script. For further technical details, see Handling multiple files.

If the current proof script buffer depends on background material from other files, proof assistants typically process these files automatically. If you visit such a file, the whole file is locked as having been processed in a single step. From the user's point of view, you can only retract but not assert in this buffer. Furthermore, retraction is only possible to the beginning of the buffer.

To be more precise, buffers are locked as soon the proof assistant notifies Proof General of processing a file different from the current proof script. Thus, if you visit the file while the proof assitant is still processing the file, it is already completely locked. If the proof assistant is not happy with the contents and complains with an error message, the buffer will still be marked as having been completely processed. Sorry. You need to visit the troublesome file, retract (which will always retract to the beginning of the file) and debug the problem e.g., by asserting all of the buffer under the supervision of Proof General, see Script processing commands.

In case you wondered, inconsistencies may arise when you have unsaved changes in a proof script buffer and the proof assistant suddenly decides to automatically process the corresponding file. The good news is that Proof General detects this problem and flashes up a warning in the response buffer. You might then want to visit the modified buffer, save it and retract to the beginning. Then you are back on track.

Retracting across files
=======================

Make sure that the current script buffer has either been completely asserted or retracted. Then you can retract proof scripts in a different file. Simply visit a file that has been processed earlier and retract in it, using the retraction commands from Script processing commands. Apart from removing parts of the locked region in this buffer, all files which depend on it will be retracted (and thus unlocked) automatically. Proof General reminds you that now is a good time to save any unmodified buffers.

Asserting across files
======================

Make sure that the current script buffer has either been completely asserted or retracted. Then you can assert proof scripts in a different file. Simply visit a file that contains no locked region and assert some command with the usual assertion commands, see Script processing commands. Proof General reminds you that now is a good time to save any unmodified buffers. This is particularly useful as assertion may cause the proof assistant to automatically process other files.

Working directly with the proof shell
=====================================

Occasionally you may want to review the dialogue of the entire session with the proof assistant, or check that it hasn't done something unexpected. Experienced users may also want to directly communicate with the proof assistant rather than sending commands via the minibuffer, see Proof assistant commands.

Although the proof shell is usually hidden from view, it is run in a buffer which provides the usual full editing and history facilities of Emacs shells (see the package comint.el distributed with your version of Emacs). You can switch to it using the menu:

       Proof-General -> Switch to buffers -> Proof Shell

Warning: you can probably cause confusion by typing in the shell buffer!  Proof General may lose track of the state of the proof assistant.

Proof General watches the output from the proof assistant to guess when a file is loaded or when a proof step is taken or undone, but it may not be guaranteed when the restricted interface is by-passed.  What happens depends on how complete the communication is between Proof General and the prover (which depends on the particular instantion of Proof General).

To resynchronise, you have two options. If you are lucky, it might suffice to

C-c C-z
     move the end of the locked region backwards to the end of the segment containing the point.

Otherwise, you will need to restart script management altogether, see Toolbar commands.

Support for other Packages
**************************

Support for function menus
==========================

The Emacs package fume-func is a provides the handy facility to make a menu from the names of entities declared in a buffer.  Proof General configures fume-func so that you can quickly jump to particular proofs in a script buffer.  (This is done with the configuration variables proof-goal-with-hole-regexp and proof-save-with-hole-regexp.)

If you want to use fume-func, you may need to enable it for yourself. It is distributed with XEmacs but by not enabled by default.  To enable it you should find the file func-menu.el and follow the instructions there.  At the time of writing, the current version of XEmacs is 20.4, supplied with function menu version 2.45, which suggests the following code for your .emacs file:

        (require 'func-menu)
        (define-key global-map 'f8 'function-menu)
        (add-hook 'find-file-hooks 'fume-add-menubar-entry t)
        (define-key global-map "\C-cl" 'fume-list-functions)
        (define-key global-map "\C-cg" 'fume-prompt-function-goto)
        (define-key global-map '(shift button3) 'mouse-function-menu)
        (define-key global-map '(meta  button1) 'fume-mouse-function-goto)

If you have another version of Emacs, you should check the fume-func.el file supplied with it.

Support for outline mode
========================

Proof General configures Emacs variables (outline-regexp and outline-heading-end-regexp) so that outline minor mode can be used on proof script files.  The headings taken for outlining are the "goal" statements at the start of goal-save sequences, see Goal-save sequences.

Use M-x outline-minor-mode to turn on outline minor mode. Functions for navigating, hiding, and revealing the proof script are available in menus.

See Outline Mode ((xemacs)) for more information about outline mode.

Support for tags
================

A "tags table" is a description of how a multi-file program is broken up into files.  It lists the names of the component files and the names and positions of the functions (or other named subunits) in each file. Grouping the related files makes it possible to search or replace through all the files with one command.  Recording the function names and positions makes possible the M-. command which finds the definition of a function by looking up which of the files it is in.

Some instantiations of Proof General (currently LEGO and Coq) are supplied with external programs for making tags tables.  Once a tag table has been made for your proof developments, you can use the Emacs tags mechanisms to find tags, and complete symbols from tags table.

One useful key binding you might want to make is to set the usual completion key M-tab to run tag-complete-symbol to use completion from names in the tag table.  To set this binding in Proof General script buffers, put this code in your .emacs file:

     (add-hook 'proof-mode-hook
       (lambda () (local-set-key '(meta tab) 'tag-complete-symbol)))

(Since this key binding interfers with a default binding that users may already have customized, Proof General doesn't do this automatically).

For more information on how to use tags, see Tags ((xemacs)).

Customizing Proof General
*************************

There are two kinds of customization for Proof General: it can be customized for a user's preferences using a particular proof assistant, or it can be customized by an Emacs expert to add a new proof assistant. Here we cover the user-level customization for Proof General.

We only consider settings for Proof General itself.  The support for a particular proof assistant can provide extra customization settings. See the chapters covering each assistant for details.

Easy customization
==================

Proof General uses the Emacs customization library extensively to provide a friendly interface.

You can access a menu of the customization settings for Proof General via the menu:

        Options -> Customize -> Emacs -> External -> Proof General

in XEmacs.

In FSF Emacs, use the menu:

        Help -> Customize -> Specific group

and type proof-general RET.

The complete set of customization settings will only be availabe after Proof General has been fully loaded.  Proof General is fully loaded when you visit a script file for the first time.

When visiting a script file, there is a more direct route to the settings:

        Proof-General -> Customize

Using the customize facility is straightforward.  You can select the setting to customize via the menus, or with M-x customize-variable.  When you have selected a setting, you are shown a buffer with its current value, and facility to edit it.  Once you have edited it, you can use the special buttons SET, SAVE and DONE.  You must use one of SET or SAVE to get any effect.  The SAVE button stores the setting in your .emacs file.

Notice that in the customize menus, variable names mentioned later may be abbreviated by omitting the "proof-" prefix.  Also, some of the option settings may have more descriptive names (for example, ON and OFF) than the low-level lisp values (non-nil, nil) which are mentioned in this chapter.

For more help, see Easy Customization (xemacs).

Display customization
=====================

If you are working on a workstation with a window system, you can use Emacs to manage several frames on the display, to keep the goals buffer displayed in a fixed place on your screen and in a certain font, for example.  A convenient way to do this is via special-display-regexps.

 -- Variable: proof-auto-delete-windows
     If non-nil, automatically remove windows when they are cleaned. For example, at the end of a proof the goals buffer window will be cleared; if this flag is set it will automatically be removed. If you want to fix the sizes of your windows you may want to set this variable to 'nil' to avoid windows being deleted automatically. If you use multiple frames, only the windows in the currently selected frame will be affected.

User options
============

Here are the remaining user options for Proof General.  These can be set via the customization system, via the old-fashioned M-x edit-options mechanism, or simply by adding setq's to your .emacs file.  The first approach is strongly recommended.

 -- User Option: proof-prog-name-ask
     If non-nil, query user which program to run for the inferior process.

 -- Variable: proof-rsh-command
     Shell command prefix to run a command on a remote host. For example,

             ssh bigjobs

     Would cause Proof General to issue the command 'ssh bigjobs isabelle' to start Isabelle remotely on our large compute server called 'bigjobs'.

     The protocol used should be configured so that no user interaction (passwords, or whatever) is required to get going.

The default value of proof-rsh-command is the empty string "".

 -- User Option: proof-toolbar-wanted
     Whether to use toolbar in proof mode.

 -- User Option: proof-toolbar-follow-mode
     Choice of how point moves with toolbar commands. One of the symbols: locked, follow, ignore.

     If locked, point sticks to the end of the locked region with toolbar commands.

     If follow, point moves just when needed to display the locked region end.

     If ignore, point is never moved after toolbar movement commands.

     The default is locked.

 -- User Option: proof-window-dedicated
     Whether response and goals buffers have dedicated windows. If t, windows displaying responses from the prover will not be switchable to display other windows.  This helps manage your display, but can sometimes be inconvenient, especially for experienced Emacs users.

 -- User Option: proof-strict-read-only
     Whether Proof General is strict about the read-only region in buffers. If non-nil, an error is given when an attempt is made to edit the read-only region.  If nil, Proof General is more relaxed (but may give you a reprimand!)

 -- Variable: proof-script-indent
     If non-nil, enable indentation code for proof scripts. Currently the indentation code can be rather slow for large scripts, and is critical on the setting of regular expressions for particular provers.  Enable it if it works for you.

The default for proof-script-indent is nil.

 -- User Option: proof-one-command-per-line
     If non-nil, format for newlines after each proof command in a script. This option is not fully-functional at the moment.

The default for proof-one-command-per-line is nil.

Changing faces
==============

The fonts and colours that Proof General uses are configurable.  If you alter these through the customize menus, only the particular kind of display in use (colour window system, monochrome window system, console, ...) will be affected.

 -- Face: proof-queue-face
     Face for commands in proof script waiting to be processed.

 -- Face: proof-locked-face
     Face for locked region of proof script (processed commands).

 -- Face: proof-declaration-name-face
     Face for declaration names in proof scripts. Exactly what uses this face depends on the proof assistant.

 -- Face: proof-tacticals-name-face
     Face for names of tacticals in proof scripts. Exactly what uses this face depends on the proof assistant.

 -- Face: proof-error-face
     Face for error messages from proof assistant.

 -- Face: proof-warning-face
     Face for warning messages. Could come either from proof assistant or Proof General itself.

The slightly bizarre name of the next face comes from the idea that while large amounts of output are being sent from the prover, some messages should be displayed to the user while the bulk of the output is hidden.  The messages which are displayed may have a special annotation to help Proof General recognize them, and this is an "eager" annotation in the sense that it should be processed as soon as it is observed by Proof General.

 -- Face: proof-eager-annotation-face
     Face for messages from proof assistant.

Tweaking configuration settings
===============================

This section is a note for advanced users.

Configuration settings are the per-prover customizations of Proof General.  These are not intended to be adjusted by the user.  But occasionally you may like to test changes to these settings to improve the way Proof General works.  You may want to do this when a proof assistant has a flexible proof script language in which one can define new tactics or even operations, and you want Proof General to recognize some of these which the default settings don't mention.  So please feel free to try adjusting the configuration settings and report to us if you find better default values than the ones we have provided.

The configuration settings appear in the customization group prover-config, or via the menu

         Proof-General -> Internals ->  Prover Config

One basic example of a setting you may like to tweak is:

 -- Variable: proof-assistant-home-page
     Web address for information on proof assistant

Most of the others are more complicated.  More details of the settings are given in see Adapting Proof General to New Provers.  To browse them, you can look through the customization groups prover-config, proof-script and proof-shell.  The group proof-script contains the configuration variables for scripting, and the group proof-shell contains those for interacting with the proof assistant.

Unfortunately, although you can use the customization mechanism to set and save these variables, saving them may have no effect because the default settings are often hard-wired into the proof assistant code. Ones we expect may need changing appear as proof assistant specific configurations.  For example, proof-assistant-home-page is set in the LEGO code from the value of the customization setting lego-www-home-page.  At present there is no easy way to save changes to other configuration variables across sessions, other than by editing the source code.  Please contact us if this proves to be a problem for any variable.

LEGO Proof General
******************

LEGO proof script mode is a mode derived from proof script mode for editing LEGO scripts. An important convention is that proof script buffers must start with a module declaration. If the proof script buffer's file name is fermat.l, then it must commence with a declaration of the form

     Module fermat;

If, in the development of the module fermat, you require material from other module e.g., lib_nat and galois, you need to specify this dependency as part of the module declaration:

     Module fermat Import lib_nat galois;

No need to worry too much about effeciency. When you retract back to a module declaration to add a new import item, LEGO does not actually retract the previously imported modules. Therefore, reasserting the extended module declaration really only processes the newly imported modules.

Using the LEGO Proof General, you never ever need to use administrative LEGO commands such as Forget, ForgetMark, KillRef, Load, Make, Reload and Undo again (And please, don't even think of including those in your LEGO proof script!). You can concentrate on your actual proof developments. Script management in Proof General will invoke the appropriate commands for you. Proving with LEGO has never been easier.

LEGO specific commands
======================

In addition to the commands provided by the generic Proof General, see the previous sections, the LEGO Proof General provides a few extensions. In proof scripts, there are some abbreviations for common commands:

C-c i
     intros

C-c I
     Intros

C-c R
     Refine

LEGO tags
=========

The LEGO Proof General provides the program legotags to generate tags for LEGO proof scripts. Invoking legotags *.l produces a file TAGS for all LEGO modules in the current directory. The LEGO library itself is shipped out with all its modules already being tagged. See Support for tags for further details.

LEGO customizations
===================

We refer to chapter Customizing Proof General for an introduction to the customisation mechanism. In addition to customizations at the generic level, for LEGO you can also customize:

 -- User Option: lego-tags
     The directory of the TAGS table for the LEGO library

The default for lego-tags is "/usr/lib/lego/lib_Type/".

 -- Variable: lego-help-menu-list
     List of menu items, as defined in `easy-menu-define' for LEGO specific help.

In Xemacs 20.4, LEGO script buffer are coloured (fontified as they say) by default. To automatically switch on fontification in FSF Emacs 20.2, you need to set

      (add-hook 'lego-mode-hooks 'turn-on-font-lock)

in your ~/.emacs file.

Coq Proof General
*****************

Coq specific commands
=====================

Coq customizations
==================

Isabelle Proof General
**********************

Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, http://www.dcs.ed.ac.uk/home/da/Isamode.  Detailed documentation for the theory file mode is included with Isamode, there are some notes on the special functions available and customization setttings below.

Theory files
============

Isabelle Proof General attempts to lock theory files as well as ML files when they are loaded.  Theory files are always completely locked or completely unlocked, because they are processed atomically.

Proof General attempts to load the theory file for a .ML file automatically before you start scripting.  This is tricky because Isabelle's theory loader assumes that .ML files are always read together with theory files.  At the moment Proof General uses an altered version of use_thy which doesn't load the top-level ML file in this case.

Compared to Isamode's theory editing mode, some of the functions and key bindings for interacting with Isabelle have been removed, and two new functions are available.

The key C-c C-b (isa-process-thy-file) will cause Isabelle to read the theory file being edited.  This causes the file and all its children (both theory and ML files) to be read.  Any top-level ML file associated with this theory file is also read.

The key C-c C-u (isa-retract-thy-file) will retract (unlock) the theory file being edited.  This unlocks the file and all its children (theory and ML files); no changes occur in Isabelle itself.

Isabelle specific commands
==========================

Switching to theory files
-------------------------

In Isabelle proofscript mode, C-c C-o (thy-find-other-file) finds and switches to the associated theory file, that is, the file with the same base name but extension .thy swapped for .ML.

The same function (and keybinding) switches back to an ML file from the theory file.

 -- Command: thy-find-other-file &optional samewindow
     Find associated .ML or .thy file. Finds and switch to the associated ML file (when editing a theory file) or theory file (when editing an ML file). If SAMEWINDOW is non-nil (interactively, with an optional argument) the other file replaces the one in the current window.

Isabelle customizations
=======================

Here are some of the user options specific to Isabelle.  You can set these with the customization mechanism as usual.

 -- Variable: isabelle-web-page
     URL of web page for Isabelle.

 -- User Option: thy-use-sml-mode
     If non-nil, invoke sml-mode inside "ML" section of theory files. This option is left-over from Isamode.  Really, it would be more useful if the script editing mode of Proof General itself could be based on sml-mode, but at the moment there is no way to do this.

 -- Variable: thy-indent-level
     Indentation level for Isabelle theory files.  An integer.

 -- User Option: thy-indent-level
     Indentation level for Isabelle theory files.  An integer.

 -- Variable: thy-sections
     Names of theory file sections and their templates. Each item in the list is a pair of a section name and a template. A template is either a string to insert or a function. Useful functions are:

            thy-insert-header, thy-insert-class, thy-insert-default-sort,
            thy-insert-const, thy-insert-rule

     The nil template does nothing. You can add extra sections to theory files by extending this variable.

 -- User Option: thy-template
     Template for theory files. Contains a default selection of sections in a traditional order. You can use the following format characters:

            %t --- replaced by theory name
            %p --- replaced by names of parents, separated by +'s

Adapting Proof General to New Provers
*************************************

Proof General has about 60 configuration variables which are set on a per-prover basis to configure the various features.  However, many of these variables occcur in pairs (typically regular expressions matching the start and end of some text), and you can begin by setting just a few variables to get the basic features working.

Skeleton example
================

Each proof assistant supported has its own subdirectory under PROOF-HOME-DIRECTORY, used to store a root elisp file and any other files needed to adapt the proof assistant for Proof General.

Here we show how a minimal configuration of Proof General works for Isabelle, without any special changes to Isabelle.

  * Make a directory called 'myassistant' under the Proof General home directory, to put the specific customization and associated files in.

  * Add a file myassistant.el to the new directory.

  * Edit proof-site.el to add a new entry to the PROOF-ASSISTANTS-TABLE variable.  The new entry should look like this:

     (myassistant "My New Assistant" "\\.myasst$")

     The first item is used to form the name of the internal variables for the new mode as well as the directory and file where it loads from.  The second is a string, naming the proof assistant. The third item is a regular expression to match names of proof script files for this assistant.  See the documentation of PROOF-ASSISTANTS-TABLE for more details.

  * Define the new modes in myassistant.el, by looking at the files for the currently supported assistants for example. Basically you need to define some modes using define-derived-mode and set the configuration variables.  You could begin by setting a minimum number of the variables, then adjust the settings via the customize menus, under Proof-General -> Internals.

Proof script settings
=====================

Proof shell settings
====================

Special annotations
-------------------

Internals of Proof General
**************************

Proof script mode
=================

Proof shell mode
================

Handling multiple files
=======================

Large proof developments are typically spread across multiple files. Many provers support such developments by keeping track of dependencies and automatically processing scripts. Proof General supports this mechanism. The user's point of view is explored further in Advanced Script Management. Here, we describe the more technical nitty gritty. This is what you need to know when you customise another proof assistant to work with Proof General.

The key idea is that we leave it to the specific proof assistant to worry about managing multiple files. But whenever the proof assistant processes or retracts a file it must clearly say so.

Proof General considers OUTPUT delimited by the the two regualar expressions proof-shell-eager-annotation-start and proof-shell-eager-annotation-end as being important. It displays the OUTPUT in the Response buffer and analyses their contents further. Among possibly other important messages characterised by these regular expressions, the prover must tell the interface whenver it processes a file and retracts across file boundaries.

proof-included-files-list
     records the file history. Whenever a new file is being processed, Proof General adds it to the front of the list. When the prover retracts across file boundaries, this list is resynchronised. It contains files in canonical truename format. See Truenames (lispref). You should not set this variable directly. The generic Proof General will modify proof-included-files-list itself. Instead, for a specific proof assistant you need to customise proof-shell-process-file. proof-shell-retract-files-regexp and proof-shell-compute-new-files-list.

proof-shell-process-file
     is either nil or a tuple of the form (REGEXP, FUNCTION). If REGEXP matches a substring of STR, then the function FUNCTION is invoked with input STR. It must return a script file name (with complete path) the system is currently processing. In practice, FUNCTION is likely to inspect the match data. See Match Data (lispref). Care has to be taken in case the prover only reports on compiled versions of files it is processing. In this case, FUNCTION needs to reconstruct the corresponding script file name. The new (true) file name is then automatically added to the front of proof-included-files-list by the generic code.

proof-shell-retract-files-regexp
     is a regular expression. It indicates that the prover has retracted across file boundaries. At this stage, Proof General's view of the processed files is out of date and needs to be updated with the help of the function proof-shell-compute-new-files-list.

proof-shell-compute-new-files-list
     Takes as argument the current output of the prover. It needs to return an up to date list of all processed files. Its output is then automatically stored in proof-included-files-list by the generic Proof General. In practice, this function is likely to inspect the previous (global) variable proof-included-files-list and the match data see Match Data (lispref) triggered by proof-shell-retract-files-regexp.

Credits and References
**********************

Credits
=======

LEGO Proof General was written by Thomas Kleymann and Dilip Sequeira.

Coq Proof General was written by Healfdene Goguen.

Isabelle Proof General was written by David Aspinall.

The generic base for Proof General was developed by all four of us.

Thomas Kleymann provided the impetus to develop a generic Emacs interface, following ideas used in Projet CROAP, and with the help of Yves Bertot.  David Aspinall provided the Proof General name and images.

An early version of this manual was prepared by Dilip Sequeira.  The present version was written by David Aspinall and Thomas Kleymann.

During the development of Proof General, the following people helped by providing feedback, testing, or code: Pascal Brisset, Rod Burstall, Paul Callaghan, Martin Hofmann, James McKinna, and Markus Wenzel.  Thanks to all of you!

References
==========

Script management as used in Proof General is described in the paper:

  * Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. To appear in Journal of Symbolic Computation.

Proof General has the beginnings of support for proof by pointing, as described in the document:

  * Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis RR-3286

Obtaining and Installing Proof General
**************************************

Proof General has its own home page (http://www.dcs.ed.ac.uk/home/proofgen) hosted at Edinburgh.  Visit this page for the latest news!

Obtaining Proof General
=======================

You can obtain Proof General from the URL

     http://www.dcs.ed.ac.uk/home/proofgen/download.html.

The distribution is available in three forms

  * A source tarball,
     http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz

  * A Linux RPM package (for any architecture),
     http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm

  * A developer's tarball,
     http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz

Both the tarball and the RPM package include the generic elisp code, code for LEGO, Coq, and Isabelle, installation instructions (reproduced below) and this documentation.

Installing Proof General from tarball
=====================================

Copy the distribution to some directory MYDIR. Unpack it there. For example:

     # cd MYDIR
     # gunzip ProofGeneral-VERSION.tar.gz
     # tar -xpf ProofGeneral-VERSION.tar

If you downloaded the version called LATEST, you'll find it unpacks to a numeric version number.

Proof General will now be in some subdirectory of MYDIR.  The name of the subdirectory will depend on the version number of Proof General. For example, it might be ProofGeneral-2.0.  It's convenient to link it to a fixed name:

     # ln -sf ProofGeneral-2.0 ProofGeneral

Now put this line in your .emacs file:

         (load-file "MYDIR/ProofGeneral/generic/proof-site.el")

This command will load proof-site which sets the Emacs load path for Proof General and add auto-loads and modes for the assistants below:

Prover   Extensions   Modes
Coq      .v    coq-mode
LEGO     .l    lego-mode
Isabelle   .thy,.ML   isa-mode

When you load a file with one of these extensions, the corresponding Proof General mode will be entered.  You can also invoke the mode command directly.

The default names for proof assistant binaries may work on your system. If not, you will need to set the appropriate variables.  The easiest way to do this (and most other customization of Proof General) is via the Customize mechanism, see the menu item:

       Proof-General -> Customize -> NAME OF ASSISTANT -> Prog Name

The Proof-General menu is available from script buffers after Proof General is loaded.  To load it manually, type

       M-x load-library RET proof RET

Notice that the customization mechanism is only available in Emacs 20.x and XEmacs.  If you cannot use customize, simply add a line like this:

       (setq isabelle-prog-name "/usr/bin/isabelle FOL")

to your .emacs file.

Installing Proof General from RPM package
=========================================

To install an RPM package you need to be root.  Then type

     # rpm -Uvh ProofGeneral-latest.noarch.rpm

Now add the line:

        (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el")

to your .emacs or the site-wide initialisation file site-start.el.

Notes for syssies
=================

Here are some more notes for installing Proof General in more complex ways.  Only attempt things in this section if you really understand what you're doing.

Byte compilation
----------------

Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibility problems (especially if you use more than one version of Emacs at the same time).

You can compile Proof General by typing make in the directory where you installed it.

Site-wide installation
----------------------

If you are installing Proof General site-wide, you can put the components in the standard directories of the filesystem if you prefer, providing the variables in proof-site.el are adjusted accordingly.  Make sure that the generic and assistant-specific elisp files are kept in subdirectories (coq, isa, lego) of proof-home-directory so that the autoload directory calculations are correct.

To prevent every user needing to edit their own .emacs files, you can put the load-file command to load proof-site.el into site-start.el or similar.  Consult the Emacs documention for more details if you don't know where to find this file.

Removing support for unwanted provers
-------------------------------------

You cannot run more than one instance of Proof General at a time: so if you're using Coq, visiting an .ML file will not load Isabelle Proof General, and the buffer remains in fundamental mode.  If there are some assistants supported that you never want to use, you can remove them from the variable proof-assistants in proof-site.el to solve this problem.

Via the Customize mechanism, see the menu:

       Options -> Customize -> Emacs -> External -> Proof General

or, after loading Proof General, in a proof script buffer

       Proof-General -> Customize

Known bugs and workarounds
**************************

We only mention a few important problems here.  The list is not a description of all bugs and may be out of date.

Please consult the file BUGS (http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS) in the distribution for more detailed and up-to-date information.

If you discover a problem which isn't mentioned in BUGS, please let us know by sending a note to proofgen@dcs.ed.ac.uk.

Bugs at the generic level
=========================

Undo in XEmacs
--------------

When proof-strict-read-only is non-nil, ordinary undo in script buffer can edit the "uneditable region" in XEmacs.  This doesn't happen in FSFmacs.  Test case: Insert some nonsense text after the locked region.  Kill the line. Process to the next command.  Press C-x u, nonsense text appears in locked region.

Workaround: be careful with undo.

Font locking and read-only in FSF Emacs
---------------------------------------

When proof-strict-read-only is set and font lock is switched on, spurious "Region read only" errors are given which break font lock.

Workaround: turn off proof-strict-read-only, font lock, or for the best of all possible worlds, switch to XEmacs.

Pressing keyboard quit C-g
--------------------------

Using C-g can leave script management in a mess.  The code is not properly protected from Emacs interrupts.

Workaround: Don't type C-g while script management is processing.  If you do, use proof-restart-scripting to restart the system.

One prover at a time
--------------------

You can't use more than one proof assistant at a time in the same Emacs session.  Attempting to load Proof General for a second prover will fail, leaving a buffer in fundamental mode instead of the Proof General mode for proof scripts.

Workaround: stick to one prover per Emacs session, make sure that the proof-assistants variables only enables Proof General for the provers you need.

Bugs specific to LEGO Proof General
===================================

Retraction and Discharge
------------------------

After a Discharge, retraction ought to only be possible back to the first declaration/definition which is discharged. However, LEGO Proof General does not know that Discharge has such a non-local effect. See Granularity of atomic command sequences for a proposal on how to fix this bug.

Workaround: retract back to the first declaration/definition which is discharged.

Retraction and proving
----------------------

Getting retracting right is tricky when working on proofs.

Definitions in a proof state
----------------------------

A thorny issues are local definitions in a proof state. LEGO cannot undo them explicitly.

Workaround: retract back to a command before a definition.

Normalisation in proofs
-----------------------

Normalisation commands such as Dnf, Hnf Normal cannot be undone in a proof state by Proof General.

Workaround: retract back to the start of the proof.

Not saving proofs.
------------------

After LEGO has issued a *** QED *** you may undo steps in the proof as long as you don't issue a Save command or start a new proof. The LEGO Proof General assumes that all proofs are terminated with a proper Save command.

Workaround: Always issue a Save command after completing a proof. If you forget one, you should retract to a point before the offending proof development.

Bugs specific to Coq Proof General
==================================

Hard-wired tactics
------------------

The collection of tactics which Proof General is aware of is hard-wired. Thus, user-defined tactics cannot be retracted.

Workaround: You may need to retract to the start of the proof.

Sections
--------

The Coq Proof General does not know about Coq's section mechansim.

Bugs specific to Isabelle Proof General
=======================================

Scripting lanugage limitations
------------------------------

Since Isabelle uses ML as a top-level language for writing proof-scripts, Proof General may have difficulty understanding scripts which stray too far away from the standard functions, tactics, and tacticals.  You will usually notice when a function, or whatever, doesn't get highlighted as you might expect.  This probably has no detrimental impact on the interface unless you use your own variants of the goal or qed forms.

Workaround: Restrict yourself to standard proof script functions, or customize some of the variables from isa.el and isa-syntax.el appropriately.

Plans and ideas
***************

This section contains some tentative plans and ideas for improving Proof General.  Please send us contributions to this wish list, or better still, offers to implement something from it!

Granularity of atomic command sequences
=======================================

This is a proposal by Thomas Kleymann for generalising the way Proof General handles sequences of proof commands see Goal-save sequences, particularly to make retraction more flexible.

The locked region of a script buffer contains the initial segment of the proof script which has been processed successfully. It consists of atomic sequences of commands (ACS). Retraction is supported to the beginning of every ACS. By default, every command is an ACS. But the granularity of atomicity can be adjusted for different proof assistants. This is essential when arbitrary retraction is not supported. Usually, after a theorem has been proved, one may only retract to the start of the goal. One needs to mark the proof of the theorem as an ACS.

proof-atomic-sequents-list
     is a list of instructions for setting up ACSs. Each instruction is a list of the form (END START &optional FORGET-COMMAND). END is a regular expression to recognise the last command in an ACS. START is a function. Its input is the last command of an ACS. Its output is a regular expression to recognise the first command of the ACS. It is evaluated once and the output is successively matched against previously processed commands until a match occurs (or the beginning of the current buffer is reached). The region determined by (START,END) is locked as an ACS. Optionally, the ACS is annotated with the actual command to retract the ACS. This is computed by applying FORGET-COMMAND to the first and last command of the ACS.

Browser mode for script files and theories
==========================================

This is a proposal by David Aspinall for a browser window.

A browser window should provide support for browsing script files and theories.  We should be able to inspect data in varying levels of detail, perhaps using outlining mechanisms.  For theories, it would be nice to query the running proof assistant.  This may require support from the assistant in the form of output which has been specially marked-up with an SGML like syntax, for example.

A browser would be useful to:

  * Provide impoverished proof assistants with a browser

  * Extend the uniform interface of Proof General to theory browsing

  * Interact closely with proof script-writing

The last point is the most important. We should be able to integrate a search mechanism for proofs of similar theorems, theorems containing particular constants, etc.