     START-INFO-DIR-ENTRY
     * Proof General: (ProofGeneral). Organize your proofs with Emacs!
     END-INFO-DIR-ENTRY

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

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

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

Preface
*******

Welcome to Proof General!

This preface has some news about the current release, as well as some history about previous releases, and acknowledgements to those who have helped along the way.

Latest news
===========

Proof General 3.0 has many improvements over 2.x releases.

First, there are usability improvements.  The toolbar was somewhat impoverished before.  It now has twice as many buttons, and includes all of the useful functions used during proof which were previously hidden on the menu, or even only available as key-presses.  Key-bindings have been re-organized, users of previous versions may notice.  The menu has been redesigned and coordinated with the toolbar, and now gives easy access to more of the features of Proof General.  Previously several features were only likely to be discovered by those keen enough to read this manual!

Second, there are improvements, extensions, and bug fixes in the generic basis. Proofs which are unfinished and not explicitly closed by a ``save'' type command are supported by the core, if they are allowed by the prover.  The design of switching the active scripting buffer has been streamlined.  The management of the queue of commands waiting to be sent to the shell has been improved, so there are fewer unnecessary "Proof Process Busy!" messages.  The proof shell filter has been optimized to give hungry proof assistants a better share of CPU cycles. Proof-by-pointing has been resurrected; even though LEGO's implementation is incomplete, it seems worth maintaining the code in Proof General so that the implementors of other proof assistants are encouraged to provide support.  For one example, we can certainly hope for support in Coq, since the CtCoq proof-by-pointing code has been moved into the Coq kernel lately.  Somebody from the Coq community needs to help with this.

An important new feature in Proof General 3.0 is support for X-Symbol, which means that real logical symbols, Greek letters, etc can be displayed during proof development, instead of their ASCII approximations. This makes Proof General a more serious competitor to native graphical user interfaces.

Finally, Proof General has become much easier to adapt to new provers --- it fails gracefully (or not at all!) when particular configuration variables are unset, and provides more default settings which work out-of-the-box.  An example configuration for Isabelle is provided, which uses just 25 or so simple settings.

This manual has been updated and extended for Proof General 3.0. Amongst other improvements, it has a better description of how to add support for a new prover.

See the CHANGES file in the distribution for more information about the latest improvements in Proof General.  Developers should check the ChangeLog in the developer's release for detailed comments on internal changes.

Most of the work for Proof General 3.0 has been done by David Aspinall. Markus Wenzel helped with Isabelle support, and provided invaluable feedback and testing.  Pierre Courtieu took responsibility from Patrick Loiseleur for Coq support, although the improvements in both the Coq and LEGO code for this release were made by David Aspinall.  Markus Wenzel also provided support for his Isar language, a new proof language for Isabelle.  David von Oheimb helped to develop and debug the generic version of his X-Symbol patch which he originally provided for Isabelle.

A new instantiation of Proof General is being worked on for Plastic, a proof assistant being developed at the University of Durham.

Proof General has a home page at http://zermelo.dcs.ed.ac.uk/home/proofgen.  Visit this page for more news!

History
=======

It all started some time in 1994. There was no Emacs interface for LEGO. Back then, Emacs militants worked directly with the Emacs shell to interact with the LEGO system.

David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn't so difficult after all. In fact, Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles, called Isamode (http://www.dcs.ed.ac.uk/home/da/Isamode). Soon after, the package lego-mode was born. Users were able to develop proof scripts in one buffer. Support was provided to automatically send parts of the script to the proof process. The last official version with the name lego-mode (1.9) was released in May 1995.

The interface project really took off the ground in November 1996. Yves Bertot had been working on a sophisticated user interface for the Coq system (CtCoq) based on the generic environment Centaur. He visited the Edinburgh LEGO group for a week to transfer proof-by-pointing technology. Even though proof-by-pointing is an inherently structure-conscious algorithm, within a week, Yves Bertot, Dilip Sequeira and Thomas Kleymann managed to implement a first prototype of proof-by-pointing in the Emacs interface for LEGO [BKS97].

Perhaps we could reuse even more of the CtCoq system. It being a structure editor did no longer seem to be such an obstacle. Moreover, to conveniently use proof-by-pointing in actual developments, one would need better support for script management.

In 1997, Dilip Sequeira implemented script management in our Emacs interface for LEGO following the recipe in [BT98]. Inspired by the project CROAP, the implementation made some effort to be generic. A working prototype was demonstrated at UITP'97.

In October 1997, Healfdene Goguen ported lego-mode to Coq. Part of the generic code in the lego package was outsourced (and made more generic) in a new generic package called proof. Dilip Sequeira provided some LEGO-specific support for handling multiple files and wrote a few manual pages. The system was reasonably robust and we shipped out the package to friends.

In June 1998, David Aspinall reentered the picture by providing an instantiation for Isabelle. Actually, our previous version wasn't quite as generic as we had hoped. Whereas LEGO and Coq are similar systems in many ways, Isabelle was really a different beast. Fierce re-engineering and various usability improvements were provided by Aspinall and Kleymann to make it easier to instantiate to new proof systems. The major technical improvement was a truly generic extension of script management to work across multiple files.

It was time to come up with a better name than just proof mode. David Aspinall suggested Proof General and set about reorganizing the file structure to disentangle the Proof General project from LEGO at last.  He cooked up some images and bolted on a toolbar, so a naive user can replay proofs without knowing a proof assistant language or even Emacs hot-keys.  He also designed some web pages, and wrote most of this new manual.

Proof General 2.0 was the first official release of the improved program, made in December 1998.

Version 2.1 was released in August 1999.  It was used at the Types Summer School held in Giens, France in September 1999 (see http://www-sop.inria.fr/types-project/types-sum-school.html). About 50 students learning Coq, Isabelle, and LEGO used Proof General for all three systems.  This experience provided invaluable feedback and encouragement to make the improvements now in Proof General 3.0.

Credits
=======

The main developers of Proof General are

  * David Aspinall,

  * Healfdene Goguen,

  * Thomas Kleymann and

  * Dilip Sequeira.

LEGO Proof General (the successor of lego-mode) was crafted by Thomas Kleymann and Dilip Sequeira. It is presently maintained by David Aspinall and Paul Callaghan <P.C.Callaghan@durham.ac.uk>. Coq Proof General was crafted by Healfdene Goguen, with later contributions from Patrick Loiseleur. It is now maintained by Pierre Courtieu <courtieu@lri.fr>. Isabelle Proof General was crafted and is being maintained by David Aspinall <da@dcs.ed.ac.uk>.  It has benefited greatly from tweaks and suggestions by Markus Wenzel, who crafted and maintains Isabelle/Isar Proof General.  Markus also added Proof General support inside Isabelle.  David von Oheimb supplied the original patches for X-Symbol support.

The generic base for Proof General was developed by Kleymann, Sequeira, Goguen and Aspinall (in order of appearance). It follows some of the ideas used in Project CROAP (http://www.inria.fr/croap/). The project to implement a proof mode for LEGO was initiated in 1994 and coordinated until October 1998 by Thomas Kleymann, becoming generic along the way.  In October 1998, the project became Proof General and has been managed by David Aspinall since then.

This manual was written by David Aspinall and Thomas Kleymann.  Some words found their way here from the user documentation of LEGO mode, prepared by Dilip Sequeira.  Healfdene Goguen supplied some text for Coq Proof General.  The extensive revision of this manual for Proof General 3.0 has been made by David Aspinall.

The Proof General project has benefited from funding by EPSRC (Applications of a Type Theory Based Proof Assistant), the EC (Types for Proofs and Programs) and the support of the LFCS.

For testing and feedback for previous versions of Proof General, thanks go to Pascal Brisset, Rod Burstall, Martin Hofmann, and James McKinna.

During the development of Proof General 3.0, many people helped provide testing and other feedback, including the Proof General maintainers, Paul Callaghan, Pierre Courtieu, and Markus Wenzel, and other folk who helpfully tested and reported on pre-releases, including Matt Fairtlough, Tobias Nipkow, Leonor Prensa-Nieto, and David von Oheimb. Thanks to all of you!

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

Proof General is a generic Emacs interface for interactive proof assistants, (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.) 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 (A proof script is a sequence of commands which constructs a proof, usually stored in a file.) 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 main aim of Proof General is to provide a powerful and configurable Emacs mode to help user-interaction with numerous interactive proof assistants.  Please help us with this aim!  Configure Proof General for your own proof assistant, by adding features at the generic level of Proof General wherever possible.  See Adapting Proof General to Other 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, the corresponding Proof General mode will be invoked automatically:

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

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 also start the proof assistant directly with the menu command "Start proof assistant".

To follow an example use of Proof General on a LEGO proof, see Walkthrough example in LEGO.  If you know the syntax for proof scripts in another theorem prover, you can easily adapt the details given there.

If Proof General has not already been installed, you should 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.

See Obtaining and Installing, if you need more information.

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, 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 Summary of Proof General buffers and see 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 Basic Script Management, Script processing commands, and 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 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, 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.

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

Proof General comes ready-customized for these proof assistants:

  * LEGO Proof General for LEGO Version 1.3.1

     See LEGO Proof General, for more details.

  * Coq Proof General for Coq Version 6.3

     See Coq Proof General, for more details.

  * Isabelle Proof General for Isabelle99

     See Isabelle Proof General, for more details.

  * Isabelle/Isar Proof General for Isabelle99

     See Isabelle Proof General, and documentation suplied with Isabelle 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 Adapting Proof General to Other Provers.

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.

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-x followed by b".

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 Easy customization ((xemacs)), for documentation in XEmacs.

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

Organization of this manual
===========================

About half of this manual covers the user-level view and customization of Proof General.  The other half considers adapting Proof General to new proof assistants, and documents some of the internals of Proof General.

Three final appendices contain some details about obtaining and installing Proof General, some known bugs, and some future plans.  The contents of these final chapters is also covered in the files INSTALL, BUGS, and TODO, contained in the distribution.

The manual concludes with some references and indexes.  See the table of contents for full details.

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

This chapter is an introduction to using the script management facilities of Proof General.  We begin with a quick walkthrough example, then describe the concepts and functions in more detail.

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

Here's a short example in LEGO to see how script management is used. The file you are asked to type below is included in the distribution as lego/example.l.  If you're not using LEGO, substitute some lines from a simple proof for your proof assistant, or consult the example file provided with Proof General.

First, find a new file by doing C-x C-f and typing as the filename example.l.  This should load LEGO Proof General and the toolbar and Proof General menus will appear.  This walkthrough is keyboard based, although you could easily use the toolbar and menu functions instead.

Now turn on electric terminator minor mode by typing C-c ; and enter:

     Module example Import lib_logic;

Electric terminator minor mode sends commands to the proof assistant as you type them.  The command should now be lit in pink (or inverse video if you don't have a colour display).  As LEGO imports each module, a line will appear in the minibuffer showing the creation of context marks. Eventually the command should turn blue, indicating that LEGO has successfully processed it. Then type (on a new line if you like):

     Goal bland_commutes: {A,B:Prop} (and A B) -> (and B A);

The goal should be echoed in the goals buffer.

     Intros;

Whoops! That was the wrong command. Press C-c C-u to pretend that didn't happen.

     intros; andI;

A proof summary will appear in the goals buffer.

     Refine H; intros; Immed; Refine H; intros; Immed;

finishes the Goal.

     Save bland_commutes;

Moving the mouse pointer over the locked region now reveals that the entire proof has been aggregated into a single segment. Suppose we decide to call the goal something more sensible. Moving the cursor up into the locked region, somewhere between Goal and Save, we enter C-c C-RET.  The segment is transferred back into the editing region. Now we correct the goal name, move the cursor to the end of the buffer, and type C-c C-RET.  Proof General queues the commands for processing and executes them.

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

A proof script is a sequence of commands which constructs definitions, declarations and proofs 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 assistant usually provides facilities 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-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
----------------------------------

The three regions that a script buffer can be divided into are:

  * The locked region, which 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, which 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, which 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 processed by the proof process.

Proof General has two fundamental operations which transfer commands between these regions: assertion (or processing) and retraction (or undoing).

Assertion causes commands from the editing region to be transferred to the queue region and sent one by one to the proof process. If the command is accepted, it is transferred to the locked region, but if an error occurs it is signalled to the user, and the offending command is transferred back to the editing region together with any remaining commands in the queue.

Assertion corresponds to processing proof commands, and makes the locked region grow.

Retraction causes commands to be transferred from the locked region to the editing region (again via the queue region) and the appropriate 'undo' commands to be sent to the proof process.

Retraction corresponds to undoing commands, and makes the locked region shrink.  For details of the commands available for doing assertion and retraction, see Script processing commands.

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

A proof script contains a sequence of commands used to prove one or more theorems.

As commands in a proof script are transferred to the locked region, they are aggregated into segments which constitute the smallest units which can be undone. Typically a segment consists of a declaration or definition, or all the text from a goal command to the corresponding save command, or the individual commands in the proof of an unfinished goal.  As the mouse moves over the the region, the segment containing the pointer will be highlighted.

Proof General therefore assumes that the proof script has a series of proofs which look something like this:

        goal MYTHM is G
        ...
        save theorem MYTHM

interspersed with comments, definitions, and the like.  Of course, the exact syntax and terminology will depend on the proof assistant you use.

The name MYTHM can appear in a menu for the proof script to help quickly find a proof (see Support for function menus).

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.

When you use a scripting command, it will automatically turn a buffer into the active scripting mode.  You can also do this by hand, via the menu command 'Toggle Scripting' or the key C-c C-s.

C-c C-s
     proof-toggle-active-scripting

When active scripting mode is turned on, several things may happen to get ready for scripting (exactly what happens depends on which proof assistant you are using and some user settings).  First, the proof assistant is started if it is not already running.  Second, a command is sent to the proof assistant to change directory to the directory of the current buffer.  If the current buffer corresponds to a file, this is the directory the file lives in.  This is in case any scripting commands refer to files in the same directory as the script.  The third thing that may happen is that you are prompted to save some unsaved buffers. This is in case any scripting commands may read in files which you are editing.  Finally, some proof assistants may automatically read in files which the current file depends on implicitly.  In Isabelle, for example, there is an implicit dependency between a .ML script file and a .thy theory file which defines its theory.

If you have a partly processed scripting buffer and use C-c C-s, or you attempt to use script processing in a new buffer, Proof General will ask you if you want to retract what has been proved so far, Scripting incomplete in buffer myproof.l, retract? or if you want to process the remainder of the active buffer, Completely process buffer myproof.l instead? before you can start scripting in a new buffer.  If you refuse to do either, Proof General will give an error message: Cannot have more than one active scripting buffer!.

To turn off active scripting, the buffer must be completely processed (all blue), or completely unprocessed.  There are two reasons for this. First, it would be confusing if it were possible to split parts of a proof arbitrarily between different buffers; the dependency between the commands would be lost and it would be tricky to replay the proof. Second, we want to interface with file management in the proof assistant.  Proof General assumes that a proof assistant may have a notion of which files have been processed, but that it will only record files that have been completely processed.  For more explanation of the handling of multiple files, see Switching between proof scripts.

 -- Command: proof-toggle-active-scripting &optional arg
     Toggle active scripting mode in the current buffer.

     With ARG, turn on scripting iff ARG is positive.

Summary of Proof General buffers
================================

Proof General manages several kinds of buffers in Emacs.  Here is a summary of the different kinds of buffers you will use when developing proofs.

  * The proof shell buffer is an Emacs shell buffer used to run your proof assistant.  Usually it is hidden from view (but see Escaping script management). 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 goals buffer has facility for proof-by-pointing.

  * 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
=======================

Proof General provides a few functions for editing proof scripts.  The generic functions mainly consist of commands to navigate within the script.  Specific proof assistant code may add more to these basics.

Indentation is controlled by the user option proof-script-indent (see User options).  When indentation is enabled, Proof General will indent lines of proof script with the usual Emacs functions, particularly TAB, indent-for-tab-command. Unfortunately, indentation in Proof General 3.0 is somewhat slow.  Therefore with large proof scripts, we recommend proof-script-indent is turned off.

Here are the commands for moving around in a proof script, with their default key-bindings:

C-c C-a
     proof-goto-command-start

C-c C-e
     proof-goto-command-end

C-c C-.
     proof-goto-end-of-locked

 -- Command: proof-goto-command-start
     Move point to start of current (or final) command of the script.

 -- Command: proof-goto-command-end
     Set point to next proof-terminal-char.

The variable proof-terminal-char is a prover-specific character to terminate proof commands.  LEGO and Isabelle use a semicolon, ;. Coq employs a full-stop ..

 -- Command: proof-goto-end-of-locked &optional switch
     Jump to the end of the locked region, maybe switching to script buffer.

     If interactive or SWITCH is non-nil, switch to script buffer first.

During the course of a large proof, it may be useful to copy previous commands.  As you move the mouse over previous portions of the script, you'll notice that each proof command is highlighted individually. (Once a goal...save sequence is ``closed'', the whole sequence is highlighted).  There is a useful mouse binding for copying the highlighted command under the mouse:

C-button1
     proof-mouse-track-insert

 -- Command: proof-mouse-track-insert event
     Copy highlighted command under the mouse to point.  Ignore comments.

     If there is no command under the mouse, behaves like mouse-track-insert.

Read the documentation in Emacs to find out about the normal behaviour of proof-mouse-track-insert, if you don't already know what it does.

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

Here are the commands for asserting and retracting portions of the proof script, together with their default key-bindings.  Sometimes assertion and retraction commands can only be issued when the queue is empty.  You will get an error message Proof Process Busy! if you try to assert or retract when the queue is being processed. (In fact, this is an unnecessary restriction imposed by the original design of Proof General.  There is nothing to stop future versions of Proof General allowing the queue region to be extended or shrunk, whilst the prover is processing it.  Proof General 3.0 already relaxes the original design, by allowing successive assertion commands without complaining.)

C-c C-n
     proof-assert-next-command-interactive

C-c C-u
     proof-undo-last-successful-command

C-c C-RET
     proof-goto-point

C-c C-b
     proof-process-buffer

C-c C-r
     proof-retract-buffer

C-c TERMINATOR-CHARACTER
     proof-electric-terminator-toggle

The last command, proof-electric-terminator-toggle, is triggered using the character which terminates proof commands for your proof assistant's script language.  For LEGO and Isabelle, use C-c ;, for Coq, use C-c ..  This not really a script processing command. Instead, if enabled, it causes subsequent key presses of ; or . to automatically activate proof-assert-next-command-interactive for convenience.

Rather than use a file command inside the proof assistant to read a proof script, a good reason to use C-c C-b (proof-process-buffer) is that with a faulty proof script (e.g., a script you are adapting to prove a different theorem), Proof General will stop exactly where the proof script fails, showing you the error message and the last processed command.  So you can easily continue development from exactly the right place in the script.

Here is the full set of script processing commands.

 -- Command: proof-assert-next-command-interactive
     Process until the end of the next unprocessed command after point.

     If inside a comment, just process until the start of the comment.

 -- Command: proof-undo-last-successful-command
     Undo last successful command at end of locked region.

 -- Command: proof-goto-point
     Assert or retract to the command at current position.

     Calls proof-assert-until-point or proof-retract-until-point as appropriate.

 -- Command: proof-process-buffer
     Process the current buffer, and maybe move point to the end.

 -- Command: proof-retract-buffer
     Retract the current buffer, and maybe move point to the start.

 -- Command: proof-electric-terminator-toggle arg
     Toggle proof-electric-terminator-enable. With ARG, turn on iff ARG>0.

     This function simply uses customize-set-variable to set the variable. It was constructed with the macro proof-customize-toggle.

 -- Command: proof-assert-until-point-interactive
     Process the region from the end of the locked-region until point.

     Default action if inside a comment is just process as far as the start of the comment.

 -- Command: proof-retract-until-point-interactive &optional delete-region
     Tell the proof process to retract until point.

     If invoked outside a locked region, undo the last successfully processed command.  If called with a prefix argument (DELETE-REGION non-nil), also delete the retracted region from the proof-script.

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

There are several commands for interacting with the proof assistant away from a proof script.  Here are the key-bindings and functions.

C-c C-p
     proof-prf

C-c C-t
     proof-ctxt

C-c C-h
     proof-help

C-c C-f
     proof-find-theorems

C-c C-c
     proof-interrupt-process

C-c C-v
     proof-minibuffer-cmd

 -- Command: proof-prf
     Show the current proof state.

     Issues a command to the assistant based on proof-showproof-command.

 -- Command: proof-ctxt
     Show the current context.

     Issues a command to the assistant based on proof-context-command.

 -- Command: proof-help
     Show a help or information message from the proof assistant.

     Typically, a list of syntax of commands available. Issues a command to the assistant based on proof-info-command.

 -- Command: proof-find-theorems arg
     Search for items containing given constants.

     Issues a command based on ARG to the assistant, using proof-find-theorems-command. The user is prompted for an argument.

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

     This sends an interrupt signal to the proof assistant, if Proof General thinks it is busy.

     This command is risky because when an interrupt is trapped in the proof assistant, we don't know whether the last command succeeded or not.  The assumption is that it didn't, which should be true most of the time, and all of the time if the proof assistant has a careful handling of interrupt signals.

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

     The command isn't added to the locked region.

     If proof-state-preserving-p is configured, it is used as a check that the command will be safe to execute, in other words, that it won't ruin synchronization.  If when applied to the command it returns false, then an error message is given.

     This command risks spoiling synchronization if the test proof-state-preserving-p is not configured, or if it is only an approximate test.

As if the last two commands weren't risky enough, there's also a command which explicitly adjusts the end of the locked region, to be used in extreme circumstances only.  See Escaping script management.

There are a few commands for stopping, starting, and restarting the proof assistant process which have menu entries but no key-bindings. As with any Emacs command, you can invoke these with M-x.

Here's a tip: if you accidently kill one of the Proof General special buffers (goals or response), exiting the proof assistant and restarting it will solve the problem.

 -- Command: proof-shell-start
     Initialise a shell-like buffer for a proof assistant.

     Also generates goal and response buffers. Does nothing if proof assistant is already running.

 -- Command: proof-shell-restart
     Clear script buffers and send proof-shell-restart-cmd.

     All locked regions are cleared and the active scripting buffer deactivated.

     If the proof shell is busy, an interrupt is sent with proof-interrupt-process and we wait until the process is ready.

     The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process.

     It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing.  (One way of caching is via object files, used by Lego and Coq).

 -- Command: proof-shell-exit
     Query the user and exit the proof process.

     This simply kills the proof-shell-buffer relying on the hook function proof-shell-kill-function to do the hard work.

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

The toolbar provides a selection of functions for asserting and retracting portions of the script, issuing non-scripting commands, and inserting "goal" and "save" type commands.  The latter functions are not available on keys, but are available from the from the menu, or via M-x, as well as the toolbar.

 -- Command: proof-issue-goal arg
     Write a goal command in the script, prompting for the goal.

     Issues a command based on ARG to the assistant, using proof-goal-command. The user is prompted for an argument.

 -- Command: proof-issue-save arg
     Write a save/qed command in the script, prompting for the theorem name.

     Issues a command based on ARG to the assistant, using proof-save-command. The user is prompted for an argument.

Proof by Pointing
*****************

This chapter describes what you can do from inside the goals buffer, providing support for these features exists for your proof assistant. As of Proof General 3.0, it only exists for LEGO.  If you would like to see proof by pointing support for Proof General in another proof assistant, please petition the developers of that proof assistant to provide it!

Goals buffer commands
=====================

When you are developing a proof, the input focus (Emacs cursor) is usually on the script buffer.  Therefore Proof General binds mouse buttons for commands in the goals buffer, to avoid the need to move the cursor between buffers.

The mouse bindings are these:

button2
     pbp-button-action

C-button2
     proof-undo-and-delete-last-successful-command

button3
     pbp-yank-subterm

Where button2 indicates the middle mouse button, and button3 indicates the right hand mouse button.

The idea is that you can automatically construct parts of a proof by clicking.  Using the middle mouse button asks the proof assistant to try to do a step in the proof, based on where you click.  If you don't like the command which was inserted into the script, you can use the control key with the middle button to undo the step, and delete it from your script.

Note that proof-by-pointing may construct several commands in one go. These are sent back to the proof assistant altogether and appear as a single step in the proof script.  However, if the proof is later replayed (without using PBP), the proof-by-pointing constructions will be considered as separate proof commands, as usual.

 -- Command: pbp-button-action event
     Construct a proof-by-pointing command based on the mouse-click EVENT.

     This function should be bound to a mouse button in the Proof General goals buffer.

     The EVENT is used to find the smallest subterm around a point.  A position code for the subterm is sent to the proof assistant, to ask it to construct an appropriate proof command.  The command which is constructed will be inserted at the end of the locked region in the proof script buffer, and immediately sent back to the proof assistant. If it succeeds, the locked region will be extended to cover the proof-by-pointing command, just as for any proof command the user types by hand.

 -- Command: proof-undo-and-delete-last-successful-command
     Undo and delete last successful command at end of locked region.

     Handy for proof by pointing, in case the last proof-by-pointing command took the proof in a direction you don't like.

Proof-by-pointing uses markup describing the term structure of the concrete syntax output by the proof assistant.  This markup is useful in itself: it allows you to explore the structure of a term using the mouse (the smallest subexpression that the mouse is over is highlighted), and easily copy subterms from the output to a proof script.

The right-hand mouse button provides this convenient way to copy subterms from the goals buffer, using the function pbp-yank-subterm.

 -- Command: pbp-yank-subterm event
     Copy the subterm indicated by the mouse-click EVENT.

     This function should be bound to a mouse button in the Proof General goals buffer.

     The EVENT is used to find the smallest subterm around a point.  The subterm is copied to the kill-ring, and immediately yanked (copied) into the current buffer at the current cursor position.

     In case the current buffer is the goals buffer itself, the yank is not performed.  Then the subterm can be retrieved later by an explicit yank.

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

If you are working with large proof developments, you may want to know about the advanced script management features of Proof General covered in this chapter.

Large proof developments 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.

With large developments particularly, users may occasionally need to escape from script management, in case Proof General loses synchronization with the proof assistant.  Proof General provides you with several escape mechanisms if you want to do this.

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. 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 switch 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 tries to be aware of all files that the proof assistant has processed or is currently processing.  In the best case, it relies on the proof assistant explicitly telling it 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.

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.

Unlike a script buffer that has been processed step-by-step via Proof General, automatically loaded script buffers do not pass through a ``red'' phase to indicate that they are currently being processed.  This is a limitation of the present implementation.  Proof General locks a buffer as soon as it sees the appropriate message from the proof assistant.  Different proof assistants may use different messages: either early locking when processing a file begins (e.g. LEGO) or late locking when processing a file ends (e.g. Isabelle).

With early locking, you may find that a script which has only been partly processed (due to an error or interrupt, for example), is wrongly completely locked by Proof General.  Visit the file and retract back to the start to fix this.

With late locking, there is the chance that you can break synchronization by editing a file as it is being read by the proof assistant, and saving it before processing finishes.

In fact, there is a general problem of editing files which may be processed by the proof assistant automatically.  Synchronization can be broken whenever you have unsaved changes in a proof script buffer and the proof assistant processes the corresponding file.  (Of course, this problem is familiar from program development using separate editors and compilers).  The good news is that Proof General can detect the problem and flashes up a warning in the response buffer.  You can then 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 (Proof General enforces this).  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 see 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.

Automatic multiple file handling
================================

To make it easier to adapt Proof General for a proof assistant, there is another possibility for multiple file support --- that it is provided automatically by Proof General and not integrated with the file-management system of the proof assistant.

In this case, Proof General assumes that the only files processed are the ones it has sent to the proof assistant itself.  Moreover, it (conservatively) assumes that there is a linear dependency between files in the order they were processed.

If you only have automatic multiple file handling, you'll find that any files loaded directly by the proof assistant are not locked when you visit them in Proof General.  Moreover, if you retract a file it may retract more than is strictly necessary (because it assumes a linear dependency).

For further technical details of the ways multiple file scripting is configured, see Handling multiple files.

Escaping script management
==========================

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 -> Buffers -> 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.  Output from the assistant is only fully monitored when Proof General is in control of the shell.

When in control, 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.  What happens when you type in the shell buffer directly depends on how complete the communication is between Proof General and the prover (which depends on the particular instantiation of Proof General).

If synchronization is lost, you have two options to resynchronize. If you are lucky, it might suffice to use the key:

C-c C-z
     proof-frob-locked-end

This command is disabled by default, to protect novices using it accidently.

If proof-frob-locked-end does not work, you will need to restart script management altogether (see Proof assistant commands).

 -- Command: proof-frob-locked-end
     Move the end of the locked region backwards to regain synchronization.

     Only for use by consenting adults.

     This command can be used to repair synchronization in case something goes wrong and you want to tell Proof General that the proof assistant has processed less of your script than Proof General thinks.

     You should only use it to move the locked region to the end of a proof command.

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

Proof General makes some configuration for other Emacs packages which provide various useful facilities.  Sometimes this configuration is purely at the proof assistant specific level (and so not necessarily available), and sometimes it is made using Proof General settings.

When adding support for a new proof assistant, we suggest that these other packages are supported, as a convention.

The packages currently supported are font-lock, x-symbol, func-menu, outline-mode, and etags.

Apart from these designated packages, many other packages in Emacs will be useful when using Proof General, even though they need no specific configuration for Proof General.  It is worth taking time to explore the Emacs manual to find out about them.  One that we highlight in particular is abbrev-mode.

Syntax highlighting
===================

Proof script buffers are decorated (or fontified) with colours, bold and italic fonts, etc, according to the syntax of the proof language and the settings for font-lock-keywords made by the proof assistant specific portion of Proof General.  Moreover, Proof General usually decorates the output from the proof assistant, also using font-lock.

In XEmacs, fontification is automatically turned on. To automatically switch on fontification in FSF GNU Emacs 20.4, you may need to engage M-x global-font-lock-mode.  The old mechanism of adding hooks to the mode hooks (lego-mode-hooks, coq-mode-hooks, etc) is no longer recommended; it should not be needed in latest Emacs versions which have more flexible customization.

Fontification for output is controlled by a separate switch in Proof General. Set proof-output-fontify-enable to nil if you don't want the output from your proof assistant to be fontified according to the setting of font-lock-keywords in the proof assistant specific portion of Proof General. See User options.

X-Symbol support
================

The X-Symbol package displays characters from a variety of fonts in Emacs buffers, automatically converting between codes for special characters and tokens which are character sequences stored in files.

Proof General uses X-Symbol to allow interaction between the user and the proof assistant to use tokens, yet appear to be using special characters.  So proof scripts and proofs can be processed with real mathematical symbols, Greek letters, etc.

You will be able to enable X-Symbol support if you have installed the X-Symbol package and support has been provided in Proof General for a token language for your proof assistant. The X-Symbol package is available from http://www.fmi.uni-passau.de/~wedler/x-symbol/.

See Configuring X-Symbol, for notes about how to configure a proof assistant to use X-Symbol in Proof General.

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

The Emacs package func-menu (formerly called fume-func) is a handy facility to make a menu from the names of entities declared in a buffer.  Proof General configures func-menu 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 function menu, you can simply select "Function menu" from the Proof General menu, or type M-x function-menu.

Although the package is distributed with XEmacs, it is not enabled by default every time you visit a buffer.  To enable it by default (i.e. avoid typing M-x function-menu), you should find the file func-menu.el and follow the instructions there.

FSF Emacs 20.4 does not have the function menu library built in, but you may be able to download it from the elisp archives.  A similar mode which is supported is imenu, also in XEmacs.  Proof General would be grateful if anyone can send patches for using imenu as an alternative to function menu.

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. If you want to use outline to hide parts of the proof script in the locked region, you need to disable proof-strict-read-only.

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

An Emacs "tags table" is a description of how a multi-file system 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 (legotags and coqtags) for making tags tables.  For example, invoking coqtags *.v produces a file TAGS for all files *.v in the current directory. Invoking coqtags `find . -name \*.v` produces a file TAGS for all files ending in .v in the current directory structure. 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 interferes 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)).

Using abbreviations
===================

A very useful package of Emacs supports automatic expansions of abbreviations as you type, see Abbrevs ((xemacs)).

Proof General has no special support for abbreviations, we just mention it here to encourage its use.  For example, the proof assistant Coq has many command strings that are long, such as ``Reflexivity,'' ``Inductive,'' ``Definition'' and ``Discriminate.''  Here is the Coq Proof General author's suggested abbreviations for Coq:

     "assn" 0 "Assumption"
     "ax" 0 "Axiom"
     "coern" 0 "Coercion"
     "cofixpt" 0 "CoFixpt"
     "coindv" 0 "CoInductive"
     "constr" 0 "Constructor"
     "contradn" 0 "Contradiction"
     "defn" 0 "Definition"
     "discr" 0 "Discriminate"
     "extrn" 0 "Extraction"
     "fixpt" 0 "Fixpoint"
     "genz" 0 "Generalize"
     "hypo" 0 "Hypothesis"
     "immed" 0 "Immediate"
     "indn" 0 "Induction"
     "indv" 0 "Inductive"
     "injn" 0 "Injection"
     "intn" 0 "Intuition"
     "invn" 0 "Inversion"
     "pmtr" 0 "Parameter"
     "refly" 0 "Reflexivity"
     "rmk" 0 "Remark"
     "specz" 0 "Specialize"
     "symy" 0 "Symmetry"
     "thm" 0 "Theorem"
     "transpt" 0 "Transparent"
     "transy" 0 "Transitivity"
     "trivial" 0 "Trivial"
     "varl" 0 "Variable"

The above list was taken from the file that Emacs saves between sessions.  The easiest way to configure abbreviations is as you write, by using the key presses C-x a g (add-global-abbrev) or C-x a i g (inverse-add-global-abbrev).  To enable expansion of abbreviations, the Abbrev minor mode, type M-x abbrev-mode RET.  See the Emacs manual for more details.

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 a developer to add support for a new proof assistant.  Here we cover the user-level customization for Proof General, see Adapting Proof General to Other Provers, for how to configure for a new proof assistant.

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.

Basic options
=============

Proof General has some basic on/off options which you can toggle directly from the menu:

        Proof-General -> Options

The effect of changing one of these options will be seen immediately (or in the next proof step).  The window-control options on this menu are described shortly.  See Display customization.

To save these options, use the usual Emacs save options command, for XEmacs on the menu:

        Options -> Save Options

or M-x customize-save-customized.

The options on this sub-menu are also available in the complete user customization options group for Proof General.

How to customize
================

Proof General uses the Emacs customization library to provide a friendly interface.  You can access all the customization settings for Proof General via the menu:

        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.  In XEmacs, the menu item Options -> Save Options saves all settings you have edited.

A technical note.  In the customize menus, the variable names mentioned later in this chapter may be abbreviated --- the "proof-" or similar prefixes are omitted.  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.  These features make customize rather more friendly than raw lisp.

You can also access the customize settings for Proof General from other (non-script) buffers.  In XEmacs, the menu path is:

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

in XEmacs.  In FSF GNU Emacs, use the menu:

        Help -> Customize -> Top-level Customization Group

and select the External and then Proof-General groups.

The complete set of customization settings will only be available after Proof General has been fully loaded.  Proof General is fully loaded when you visit a script file for the first time, or if you type M-x load-library RET proof RET.

For more help with customize, see Easy Customization (xemacs).

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

By default, Proof General displays two buffers during scripting, in a split window on the display.  One buffer is the script buffer.  The other buffer is either the goals buffer (e.g. *isabelle-goals*) or the response buffer (*isabelle-response*).  Proof General switches between these last two automatically.

Proof General allows several ways to customize this default display model.

If your screen is large enough, you may prefer to display all three of the interaction buffers at once.  This is useful, for example, to see output from the proof-find-theorems command at the same time as the subgoal list.  Set the user option proof-dont-switch-windows to make Proof General keep both the goals and response buffer displayed.

 -- User Option: proof-dont-switch-windows
     Whether response and goals buffers have dedicated windows.

     If non-nil, Emacs windows displaying messages from the prover will not be switchable to display other windows.

     This option can help manage your display.

     Setting this option triggers a three-buffer mode of interaction where the goals buffer and response buffer are both displayed, rather than the two-buffer mode where they are switched between.  It also prevents Emacs automatically resizing windows between proof steps.

     If you use several frames (the same Emacs in several windows on the screen), you can force a frame to stick to showing the goals or response buffer.

     For single frame use this option may be inconvenient for experienced Emacs users.

     The default value is nil.

Sometimes during script management, there is no response from the proof assistant to some command.  In this case you might like the empty response window to be hidden so you have more room to see the proof script.  The setting proof-delete-empty-windows helps you do this.

 -- User Option: proof-delete-empty-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 automatically deleted.

     The default value is nil.

This option only has an effect when you have set proof-dont-switch-windows.

If you are working on a machine 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 the user option

 -- User Option: proof-multiple-frames-enable
     Whether response and goals buffers have separate frames.

     If non-nil, Emacs will make separate frames (screen windows) for the goals and response buffers, by altering the Emacs variable special-display-regexps.

     The default value is nil.

Multiple frames work best when proof-delete-empty-windows is off and proof-dont-switch-windows is on.

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

Here is the complete set of user options for Proof General, apart from the three display options mentioned above.

User options can be set via the customization system already mentioned, 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.

Unless mentioned, all of these settings can be changed dynamically, without needing to restart Emacs to see the effect.  But you must use customize to be sure that Proof General reconfigures itself properly.

 -- User Option: proof-splash-enable
     If non-nil, display a splash screen when Proof General is loaded.

     The default value is t.

 -- User Option: proof-electric-terminator-enable
     If non-nil, use electric terminator mode.

     If electric terminator mode is enabled, pressing a terminator will automatically issue proof-assert-next-command for convenience, to send the command straight to the proof process.  If the command you want to send already has a terminator character, you don't need to delete the terminator character first.  Just press the terminator somewhere nearby.  Electric!

     The default value is nil.

 -- User Option: proof-toolbar-enable
     If non-nil, display Proof General toolbar for script buffers.

     NB: the toolbar is only available with XEmacs.

     The default value is t.

 -- User Option: proof-x-symbol-enable
     Whether to use x-symbol in Proof General buffers.

     If you activate this variable, whether or not you get x-symbol support depends on whether your proof assistant supports it and whether X-Symbol is installed in your Emacs.

     The default value is nil.

 -- User Option: proof-output-fontify-enable
     Whether to fontify output from the proof assistant.

     If non-nil, output from the proof assistant will be highlighted in the goals and response buffers. (This is providing font-lock-keywords have been set for the buffer modes).

     The default value is t.

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

     If you change proof-strict-read-only during a session, you must use the "Restart" button (or M-x proof-shell-restart) before you can see the effect in buffers.

     The default value for proof-strict-read-only depends on which version of Emacs you are using.  In FSF Emacs, strict read only is buggy when it used in conjunction with font-lock, so it is disabled by default.

     The default value is strict.

 -- User Option: proof-toolbar-use-button-enablers
     If non-nil, toolbars buttons may be enabled/disabled automatically.

     Toolbar buttons can be automatically enabled/disabled according to the context.  Set this variable to nil if you don't like this feature or if you find it unreliable.

     Notes: * Toolbar enablers are only available with XEmacs 21 and later. * With this variable nil, buttons do nothing when they would otherwise be disabled. * If you change this variable it will only be noticed when you next start Proof General.

     The default value is t.

 -- User Option: proof-query-file-save-when-activating-scripting
     If non-nil, query user to save files when activating scripting.

     Often, activating scripting or executing the first scripting command of a proof script will cause the proof assistant to load some files needed by the current proof script.  If this option is non-nil, the user will be prompted to save some unsaved buffers in case any of them corresponds to a file which may be loaded by the proof assistant.

     You can turn this option off if the save queries are annoying, but be warned that with some proof assistants this may risk processing files which are out of date with respect to the loaded buffers!

     The default value is t.

 -- User Option: 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 value 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 value is nil.

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

     The default value is nil.

 -- User Option: proof-prog-name-guess
     If non-nil, use proof-guess-command-line to guess proof-prog-name.

     This option is compatible with proof-prog-name-ask. No effect if proof-guess-command-line is nil.

     The default value is nil.

 -- User Option: proof-tidy-response
     Non-nil indicates that the response buffer should be cleared often.

     The response buffer can be set either to accumulate output, or to clear frequently.

     With this variable non-nil, the response buffer is kept tidy by clearing it often, typically between successive commands (just like the goals buffer).

     Otherwise the response buffer will accumulate output from the prover.

     The default value is t.

 -- User Option: proof-show-debug-messages
     Whether to display debugging messages in the response buffer.

     If non-nil, debugging messages are displayed in the response giving information about what Proof General is doing. To avoid erasing the messages shortly after they're printed, you should set proof-tidy-response to nil.

     The default value is nil.

 -- User Option: proof-follow-mode
     Choice of how point moves with script processing commands.

     One of the symbols: 'locked, 'follow, 'ignore. If 'locked, point sticks to the end of the locked region. If 'follow, point moves just when needed to display the locked region end. If 'ignore, point is never moved after movement commands.

     The default value is locked.

 -- User Option: proof-auto-action-when-deactivating-scripting
     If 'retract or 'process, do that when deactivating scripting.

     With this option set to 'retract or 'process, when scripting is turned off in a partly processed buffer, the buffer will be retracted or processed automatically.

     With this option unset (nil), the user is questioned instead.

     Proof General insists that only one script buffer can be partly processed: all others have to be completely processed or completely unprocessed.  This is to make sure that handling of multiple files makes sense within the proof assistant.

     NB: A buffer is completely processed when all non-whitespace is locked (coloured blue); a buffer is completely unprocessed when there is no locked region.

     The default value is nil.

 -- User Option: proof-script-command-separator
     String separating commands in proof scripts.

     For example, if a proof assistant prefers one command per line, then this string should be set to a newline.  Otherwise it should be set to a space.

     The default value is " ".

 -- User Option: 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 is "".

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

The fonts and colours that Proof General uses are configurable.  If you alter faces through the customize menus (or the command M-x customize-face), only the particular kind of display in use (colour window system, monochrome window system, console, ...) will be affected.  This means you can keep separate default settings for each different display environment where you use Proof General.

As well as the faces listed below, Proof General may use the regular font-lock- faces (eg font-lock-keyword-face, font-lock-variable-name-face, etc) for fontifying the proof script or proof assistant output.  These can be altered to your taste just as easily, but note that changes will affect all other modes which use them!

 -- 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-error-face
     Face for error messages from proof assistant.

 -- Face: proof-warning-face
     Face for warning messages.

     Warning messages can come from proof assistant or from Proof General itself.

 -- Face: proof-debug-message-face
     Face for debugging messages from Proof General.

 -- 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-eager-annotation-face
     Face for important messages from proof assistant.

The slightly bizarre name of the last 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.

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.

     Used for Proof General's help menu.

Most of the others are more complicated.  For more details of the settings, see Adapting Proof General to Other 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 practical effect because the default settings are mostly 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.  (In future versions of Proof General, we plan to make all settings editable in Customize, by shadowing the settings as prover specific ones).

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 efficiency. 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 (as discussed in 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
=========

You might want to ask your local system administrator to tag the directories lib_Prop, lib_Type and lib_TYPE of the LEGO library. See Support for tags, for further details on tags.

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 value is "/usr/lib/lego/lib_Type/".

 -- Variable: lego-www-home-page
     Lego home page URL.

 -- Variable: lego-help-menu-list
     List of menu items for LEGO specific help.

     See the documentation of easy-menu-define

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

Coq Proof General is an instantiation of Proof General for the Coq proof assistant.  It supports most of the generic features of Proof General, but does not have integrated file management or proof-by-pointing yet.

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

Coq Proof General supplies the following key-bindings:

C-c I
     Inserts ``Intros '' into proof buffer.

C-c a
     Inserts ``Apply '' into proof buffer.

C-c s
     Inserts ``Section '' into proof buffer

C-c e
     Closes the current section by inserting ``End <section-name>.''. (this should work well with nested sections).

Editing multiple proofs
=======================

Coq allows the user to enter top-level commands while editing a proof script.  For example, if the user realizes that the current proof will fail without an additional axiom, he or she can add that axiom to the system while in the middle of the proof.  Similarly, the user can nest lemmas, beginning a new lemma while in the middle of an earlier one, and as the lemmas are proved or their proofs aborted they are popped off a stack.

Coq Proof General supports this feature of Coq.  Top-level commands entered while in a proof are promoted immediately above the outermost active proof.  If new lemmas are started, Coq Proof General lets the user work on the proof of the new lemma, and when the lemma is finished the full proof of that lemma is promoted.  This is supported to any nesting depth that Coq allows.

Special note: this feature is disabled in version 3.0 because the implementation was unreliable.

User-loaded tactics
===================

Another feature that Coq allows is the extension of the grammar of the proof assistant by new tactic commands.  This feature interacts with the proof script management of Proof General, because Proof General needs to know when a tactic is called that alters the proof state.

Unfortunately, Coq Proof General does not currently support tactic extension in Coq.  When the user tries to retract across an extended tactic in a script, the algorithm for calculating how far to undo does not recognize the extension, and so the proof buffer and Coq are not synchronized.

Until this feature is incorporated into Coq Proof General, the user can use C-c C-v to resynchronize.  For example, if the user does C-c C-u to move the point back past one extended tactic, he or she can type C-c C-v ``Undo 1.''  This then undoes the tactic that the proof mode failed to recognize.

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

Isabelle Proof General supports all of the generic features of Proof General, including integration with Isabelle's theory loader for proper automatic multiple file handling.

Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, see 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 settings below.

Note that in ``classic'' Isabelle, .thy files contain definitions and declarations for a theory, while .ML contain proof scripts. So most of Proof General's functions only make sense in .ML files, and there is no toolbar and only a short menu for .thy files.  Also note that Proof General does not understand full ML syntax(!), so you should only use the scripting commands on .ML files which contain proof commands (no ML functions, structures, etc).

There is no specific documentation here for the Isabelle/Isar instance of Proof General.  With Isar, .thy files contain proofs as well as theory definitions, and so they support the toolbar and usual scripting functions of Proof General.  To load the Isabelle/Isar instance of Proof General, you can set PROOFGENERAL_ASSISTANTS=isar in the shell before starting Emacs, to make sure ordinary Isabelle theory file mode isn't loaded instead.

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

As well as locking ML files, Isabelle Proof General locks theory files when they are loaded.  Theory files are always completely locked or completely unlocked, because they are processed atomically.

Proof General tries to load the theory file for a .ML file automatically before you start scripting.  This relies on new support especially for Proof General built into Isabelle99's theory loader.

However, because scripting cannot begin until the theory is loaded, and it should not begin if an error occurs during loading the theory, Proof General blocks waiting for the theory loader to finish.  If you have a theory file which takes a long time to load, you might want to load it directly, from the .thy buffer.  Extra commands are provided in theory mode for this:

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 not read, in contrast with the use_thy command of Isabelle.

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.

 -- Command: isa-process-thy-file file
     Process the theory file FILE.  If interactive, use buffer-file-name.

 -- Command: isa-retract-thy-file file
     Retract the theory file FILE. If interactive, use buffer-file-name.

     To prevent inconsistencies, scripting is deactivated before doing this. So if scripting is active in an ML file which is not completely processed, you will be asked to retract the file or process the remainder of it. (If you process the rest of it it may subsequently be unlocked anyway).

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

In Isabelle proof script 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 key-binding) 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 as usual with the customization mechanism.

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

     The default value is nil.

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

     The default value is 2.

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

 -- Variable: 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 + characters.

Adapting Proof General to Other Provers
***************************************

Proof General has about 80 configuration variables which are set on a per-prover basis to configure the various features.  It may sound like a lot but don't worry!  Many of the variables occur in pairs (typically regular expressions matching the start and end of some text), and you can begin by setting just a fraction of the variables to get the basic features of script management working.  The bare minimum for a working prototype is about 20 simple settings.

For more advanced features you may need (or want) to write some Emacs Lisp.  If you're adding new functionality please consider making it generic for different proof assistants, if appropriate.  When writing your modes, please follow the Emacs Lisp conventions see Style Tips (lispref).

The configuration variables are declared in the file generic/proof-config.el.  The details in the central part of this chapter are based on the contents of that file, beginning in Menus and user-level commands, and continuing until Global constants. The final sections cover the details of configuring for multiple files and for supporting the other Emacs packages mentioned in Support for other Packages.  The last section mentions which functions you are allowed to use if you write additional Elisp code interfacing to Proof General.

In the first three sections we describe the general mechanisms for instantiating Proof General.

Overview of adding a new prover
===============================

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 is how to go about adding support for a new prover.

 1. Make a directory called myassistant/ under the Proof General home directory proof-home-directory, to put the specific customization and associated files in.

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

 3. Edit proof-site.el to add a new entry to the proof-assistants-table variable.  The new entry should look like this:

              (myassistant "My Proof 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-assistant-table for more details.

 4. Define the new Proof General modes in myassistant.el, by setting configuration variables to customize the behaviour of the generic modes.

 -- User Option: proof-assistant-table
     Proof General's table of supported proof assistants.

     Extend this table to add a new proof assistant. Each entry is a list of the form

              (SYMBOL NAME AUTOMODE-REGEXP)

     The NAME is a string, naming the proof assistant. The SYMBOL is used to form the name of the mode for the assistant, SYMBOL-mode, run when files with AUTOMODE-REGEXP are visited.  SYMBOL is also used to form the name of the directory and elisp file for the mode, which will be

              PROOF-HOME-DIRECTORY/SYMBOL/SYMBOL.el

     where PROOF-HOME-DIRECTORY is the value of the variable proof-home-directory.

     The default value is ((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (plastic "Plastic" "\\.lf$")).

The final step of the description above is where the work lies.  There are two basic methods.  You can write some Emacs lisp functions and define the modes using the macro define-derived-mode.  Or you can use the new easy configuration mechanism of Proof General 3.0 described in the next section, which calls define-derived-mode for you. You still need to know which configuration variables should be set, and how to set them.  The documentation below (and inside Emacs) should help with that, but the best way to begin is by using an existing Proof General instance as an example.

Demonstration instance and easy configuration
=============================================

Proof General is supplied with a demonstration instance for Isabelle which configures the basic features.  This is a whittled down version of Isabelle Proof General, which you can use as a template to get support for a new assistant going.  Check the directory demoisa for the two files demoisa.el and demoisa-easy.el.

The file demoisa.el follows the scheme described in Major modes used by Proof General.  It uses the Emacs Lisp macro define-derived-mode to define the four modes for a Proof General instance, by inheriting from the generic code.  Settings which configure Proof General are made by functions called from within each mode, as appropriate.

The file demoisa-easy.el uses a new simplified mechanism to achieve (virtually) the same result.  It uses the macro proof-easy-config defined in proof-easy-configl.el to make all of the settings for the Proof General instance in one go, defining the derived modes automatically using a regular naming scheme.  No lisp code is used in this file except the call to this macro.  The minor difference in the end result is that all the variables are set at once, rather than inside each mode.  But since the configuration variables are all global variables anyway, this makes no real difference.

The macro proof-easy-config is called like this:

        (proof-easy-config MYPROVER "MYPROVER"
             CONFIG_1 VAL_1
             ...
             CONFIG_N VAL_N)

The main body of the macro call is like the body of a setq.  It contains pairs of variables and value settings.  The first argument to the macro is a symbol defining the mode root, the second argument is a string defining the mode name.  These should be the same as the first part of the entry in proof-assistant-table for your prover. See Overview of adding a new prover.  After the call to proof-easy-config, the new modes MYPROVER-mode, MYPROVER-shell-mode, MYPROVER-response-mode, and MYPROVER-goals-mode will be defined.  The configuration variables in the body will be set immediately.

Even Emacs Lisp experts may prefer the simplified mechanism.  If you want to set some buffer-local variables in your Proof General modes, or invoke supporting lisp code, this can easily be done by adding functions to the appropriate mode hooks after the proof-easy-config call. For example, to add extra settings for the shell mode for demoisa, we could do this:

        (defun demoisa-shell-extra-config ()
           EXTRA CONFIGURATION ...
         )
        (add-hook 'demoisa-shell-mode-hook 'demoisa-shell-extra-config)

The function to do extra configuration demoisa-shell-extra-config is then called as the final step when demoisa-shell-mode is entered (be wary, this will be after the generic proof-shell-config-done is called, so it will be too late to set normal configuration variables which may be examined by proof-shell-config-done).

Major modes used by Proof General
=================================

There are four major modes used by Proof General, one for each type of buffer it handles.  The buffer types are: script, shell, response and goals.  Each of these has a generic mode, respectively: proof-mode, proof-shell-mode, proof-response-mode, and proof-pbp-mode.

The pattern for defining the major mode for an instance of Proof General is to use define-derived-mode to define a specific mode to inherit from each generic one, like this:

     (define-derived-mode myass-shell-mode proof-shell-mode
        "MyAss shell" nil
        (myass-shell-config)
        (proof-shell-config-done))

Where myass-shell-config is a function which sets the configuration variables for the shell (see Proof shell settings).

It's important that your mode invokes one of the functions proof-config-done, proof-shell-config-done, proof-response-config-done, or proof-goals-config-done once they've set their configuration variables.  These functions finalize the configuration of the mode.

For each mode, there is a configuration variable which names it so that Proof General can set buffers to the proper mode, or find buffers in that mode.  These are documented below, and set like this:

       (setq proof-mode-for-script 'myass-mode)

where myass-mode is your major mode for scripts, derived from proof-mode.  You must set these variables before the proof shell is started; one way to do this is inside a function which is called from the hook pre-shell-start-hook.  See the file demoisa.el for details of how to do this.

 -- Variable: proof-mode-for-script
     Mode for proof script buffers.

     This is used by Proof General to find out which buffers contain proof scripts. Suggestion: this can be set in the script mode configuration.

 -- Variable: proof-mode-for-shell
     Mode for proof shell buffers.

     Usually customised for specific prover. Suggestion: this can be set a function called by pre-shell-start-hook.

 -- Variable: proof-mode-for-response
     Mode for proof response buffer.

     Usually customised for specific prover. Suggestion: this can be set a function called by pre-shell-start-hook.

 -- Variable: proof-mode-for-pbp
     Mode for proof state display buffers.

     Usually customised for specific prover. Suggestion: this can be set a function called by pre-shell-start-hook.

Menus and user-level commands
=============================

The following variables should be set in the script mode before proof-config-done is called.  These make some settings for the commands and menus available in Proof General.

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

     Used for Proof General's help menu.

 -- Variable: proof-context-command
     Command to display the context in proof assistant.

 -- Variable: proof-info-command
     Command to ask for help or information in the proof assistant.

 -- Variable: proof-showproof-command
     Command to display proof state in proof assistant.

 -- Variable: proof-goal-command
     Command to set a goal in the proof assistant.  String or fn.

     If a string, the format character %s will be replaced by the goal string. If a function, it should return the command string to insert.

 -- Variable: proof-save-command
     Command to save a proved theorem in the proof assistant.  String or fn.

     If a string, the format character %s will be replaced by the theorem name. If a function, it should return the command string to insert.

 -- Variable: proof-find-theorems-command
     Command to search for a theorem containing a given constant. String or fn.

     If a string, the format character %s will be replaced by the constant name. If a function, it should return the command string to insert.

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

The following variables should be set in the script mode before proof-config-done is called.  These configure the mode for the script buffer.

 -- Variable: proof-terminal-char
     Character which terminates a command in a script buffer.

     You must set this variable in script mode configuration.

 -- Variable: proof-comment-start
     String which starts a comment in the proof assistant command language.

     The script buffer's comment-start is set to this string plus a space. Moreover, comments are ignored during script management, and not sent to the proof process.

     You should set this variable for reliable working of Proof General, as well as proof-comment-end.

 -- Variable: proof-comment-end
     String which ends a comment in the proof assistant command language.

     The script buffer's comment-end is set to this string plus a space. See also proof-comment-start.

     You should set this variable for reliable working of Proof General,

 -- Variable: proof-case-fold-search
     Value for case-fold-search when recognizing portions of proof scripts.

     The default value is 'nil'.  If your prover has a case insensitive input syntax, proof-case-fold-search should be set to 't' instead. NB: This setting is not used for matching output from the prover.

 -- Variable: proof-save-command-regexp
     Matches a save command.

 -- Variable: proof-save-with-hole-regexp
     Regexp which matches a command to save a named theorem.

     Match number 2 should be the name of the theorem saved. Used for setting names of goal..save regions and for default function-menu configuration in proof-script-find-next-entity.

 -- Variable: proof-goal-command-regexp
     Matches a goal command in the proof script.   Must be set.

 -- Variable: proof-goal-with-hole-regexp
     Regexp which matches a command used to issue and name a goal.

     Match number 2 should be the name of the goal issued. Used for setting names of goal..save regions and for default function-menu configuration in proof-script-find-next-entity.

 -- Variable: proof-non-undoables-regexp
     Regular expression matching commands which are not undoable.

     Used in default functions proof-generic-state-preserving-p and proof-generic-count-undos.  If you don't use those, May be left as nil.

 -- Variable: proof-ignore-for-undo-count
     Matcher for script commands to be ignored in undo count.

     May be left as nil, in which case it will be set to proof-non-undoables-regexp. Used in default function proof-generic-count-undos.

 -- Variable: proof-script-next-entity-regexps
     Regular expressions to help find definitions and proofs in a script.

     This is the list of the form

             (ANYENTITY-REGEXP
              DISCRIMINATOR-REGEXP  ... DISCRIMINATOR-REGEXP)

     The idea is that ANYENTITY-REGEXP matches any named entity in the proof script, on a line where the name appears.  This is assumed to be the start or the end of the entity.  The discriminators then test which kind of entity has been found, to get its name.  A DISCRIMINATOR-REGEXP has one of the forms

            (REGEXP MATCHNO)
            (REGEXP MATCHNO 'backward BACKREGEXP)
            (REGEXP MATCHNO 'forward FORWARDREGEXP)

     If REGEXP matches the string captured by ANYENTITY-REGEXP, then MATCHNO is the match number for the substring which names the entity.

     If 'backward BACKREGEXP is present, then the start of the entity is found by searching backwards for BACKREGEXP.

     Conversely, if 'forward FORWARDREGEXP is found, then the end of the entity is found by searching forwards for FORWARDREGEXP.

     Otherwise, the start and end of the entity will be the region matched by ANYENTITY-REGEXP.

     This mechanism allows fairly complex parsing of the buffer, in particular, it allows for goal..save regions which are named only at the end.  However, it does not parse strings, comments, or parentheses.

     This variable may not need to be set: a default value which should work for goal..saves is calculated from proof-goal-with-hole-regexp, proof-goal-command-regexp, and proof-save-with-hole-regexp.

 -- Variable: proof-script-find-next-entity-fn
     Name of function to find next interesting entity in a script buffer.

     This is used to configure func-menu.  The default value is proof-script-find-next-entity, which searches for the next entity based on fume-function-name-regexp which by default is set from proof-script-next-entity-regexps.

     The function should move point forward in a buffer, and return a cons cell of the name and the beginning of the entity's region.

     Note that proof-script-next-entity-regexps is set to a default value from proof-goal-with-hole-regexp and proof-save-with-hole-regexp in the function proof-config-done, so you may not need to worry about any of this.  See whether function menu does something sensible by default.

 -- Variable: proof-goal-command-p
     A function to test: is this really a goal command?

 -- Variable: proof-completed-proof-behaviour
     Indicates how Proof General treats commands beyond the end of a proof.

     Normally goal...save regions are "closed", i.e. made atomic for undo. But once a proof has been completed, there may be a delay before the "save" command appears --- or it may not appear at all.  Unless nested proofs are supported, this can spoil the undo-behaviour in script management since once a new goal arrives the old undo history may be lost in the prover.  So we allow Proof General to close off the goal..[save] region in more flexible ways. The possibilities are:

                  nil  -  nothing special; close only when a save arrives
            'closeany  -  close as soon as the next command arrives, save or not
           'closegoal  -  close when the next "goal" command arrives
              'extend  -  keep extending the closed region until a save or goal.

     If your proof assistant allows nested goals, it will be wrong to close off the portion of proof so far, so this variable should be set to nil. There is no built-in understanding of the undo behaviour of nested proofs; instead there is some support for un-nesting nested proofs in the proof-lift-global mechanism.  (Of course, this is risky in case of nested contexts!)

 -- Variable: proof-lift-global
     Function which lifts local lemmas from inside goals out to top level.

     This function takes the local goalsave span as an argument. Leave this set this at nil if the proof assistant does not support nested goals, or if you don't want to write a function to do move them around.

 -- Variable: proof-count-undos-fn
     Function to calculate a command to issue undos to reach a target span.

     The function takes a span as an argument, and should return a string which is the command to undo to the target span.  The target is guaranteed to be within the current (open) proof. This is an important function for script management. The default setting proof-generic-count-undos is based on the settings proof-non-undoables-regexp and proof-non-undoables-regexp.

 -- Function: proof-generic-count-undos span
     Count number of undos in a span, return command needed to undo that far.

     Command is set using proof-undo-n-times-cmd.

     A default value for proof-count-undos-fn.

     For this function to work properly, you must configure proof-undo-n-times-cmd and proof-ignore-for-undo-count.

 -- Variable: proof-find-and-forget-fn
     Function that returns a command to forget back to before its argument span.

     This setting is used to for retraction (undoing) in proof scripts.

     It should undo the effect of all settings between its target span up to (proof-locked-end).  This may involve forgetting a number of definitions, declarations, or whatever.

     The special string proof-no-command means there is nothing to do.

     Important: the generic implementation proof-generic-find-and-forget does nothing, it always returns proof-no-command.

     This is an important function for script management. Study one of the existing instantiations for examples of how to write it, or leave it set to the default function proof-generic-find-and-forget (which see).

 -- Function: proof-generic-find-and-forget span
     Calculate a forget/undo command to forget back to SPAN.

     This is a long-range forget: we know that there is no open goal at the moment, so forgetting involves unbinding declarations, etc, rather than undoing proof steps.

     CURRENTLY UNIMPLEMENTED: just returns proof-no-command. Check the lego-find-and-forget or coq-find-and-forget functions for examples of how to write this function.

     In the next release of Proof General, there will be a generic implementation of this.

 -- Variable: proof-goal-hyp-fn
     Function which returns cons cell if point is at a goal/hypothesis.

     This is used to parse the proofstate output to mark it up for proof-by-pointing.  It should return a cons or nil.  First element of the cons is a symbol, 'goal' or 'hyp'.  The second element is a string: the goal or hypothesis itself.

     If you leave this variable unset, no proof-by-pointing markup will be attempted.

 -- Variable: proof-kill-goal-command
     Command to kill the currently open goal.

     You must set this (perhaps to a no-op) for script management to work.

 -- Variable: proof-global-p
     Whether a command is a global declaration.  Predicate on strings or nil.

     This is used to handle nested goals allowed by some provers, by recognizing global declarations as candidates for rearranging the proof script.

     May be left as nil to disable this function.

 -- Variable: proof-state-preserving-p
     A predicate, non-nil if its argument (a command) preserves the proof state.

     If set, used by proof-minibuffer-cmd to filter out scripting commands which should be entered directly into the script itself.

     The default setting for this function, proof-generic-state-preserving-p tests by negating the match on proof-non-undoables-regexp.

 -- Function: proof-generic-state-preserving-p cmd
     Is CMD state preserving?  Match on proof-non-undoables-regexp.

 -- Variable: proof-activate-scripting-hook
     Hook run when a buffer is switched into scripting mode.

     The current buffer will be the newly active scripting buffer.

     This hook may be useful for synchronizing with the proof assistant, for example, to switch to a new theory (in case that isn't already done by commands in the proof script).

     When functions in this hook are called, the variable activated-interactively will be non-nil if proof-activate-scripting was called interactively (rather than as a side-effect of some other action). If a hook function sends commands to the proof process, it should wait for them to complete (so the queue is cleared for scripting commands), unless activated-interactively is set.

 -- Variable: proof-stack-to-indent
     Prover-specific code for indentation.

 -- Variable: proof-parse-indent
     Proof-assistant specific function for parsing.

     Invoked in proof-parse-to-point. Must be a function taking two arguments, a character (the current character) and a stack reflecting indentation, and must return a stack. The stack is a list of the form (c . p) where c is a character representing the type of indentation and p records the column for indentation. The generic proof-parse-to-point function supports parentheses and commands. It represents these with the characters ?(, ?[ and proof-terminal-char.

See Handling multiple files, for more details about the final setting in this group.

 -- Variable: proof-auto-multiple-files
     Whether to use automatic multiple file management.

     If non-nil, Proof General will automatically retract a script file whenever another one is retracted which it depends on.  It assumes a simple linear dependency between files in the order which they were processed.

     If your proof assistant has no management of file dependencies, or one which depends on a simple linear context, you may be able to use this setting to good effect.  If the proof assistant has more complex file dependencies then you should configure it to communicate with Proof General about the dependencies rather than using this setting.

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

The variables in this section concern the proof shell mode, and are the largest group.  They are split into several subgroups.  The first subgroup are commands invoked at various points.  The second subgroup of variables are concerned with matching the output from the proof assistant.  The final subgroup contains various hooks which you can set to add lisp customization to Proof General in various points (some of them are also used internally for behaviour you may wish to adjust).

Variables for configuring the proof shell are put into the customize group proof-shell.

These should be set in the shell mode configuration, before proof-shell-config-done is called.

To understand the way the proof assistant runs inside Emacs, you may want to refer to the comint.el (Command interpreter) package distributed with Emacs.  This package controls several shell-like modes available in Emacs, including the proof-shell-mode and all specific shell modes derived from it.

Commands
--------

 -- Variable: proof-prog-name
     System command to run the proof assistant in the proof shell.

     Suggestion: this can be set in proof-pre-shell-start-hook from a variable which is in the proof assistant's customization group.  This allows different proof assistants to coexist (albeit in separate Emacs sessions).

 -- Variable: proof-shell-init-cmd
     The command for initially configuring the proof process.

     This command is sent to the process as soon as it starts up, perhaps in order to configure it for Proof General or to print a welcome message. Note that it is sent before Proof General's synchronization mechanism is engaged (in case the command engages it).  It is better to configure the proof assistant via command line options if possible.

 -- Variable: proof-shell-restart-cmd
     A command for re-initialising the proof process.

     The proof-terminal-char is added on to the end.

 -- Variable: proof-shell-quit-cmd
     A command to quit the proof process.  If nil, send EOF instead.

     The proof-terminal-char is added on to the end.

 -- Variable: proof-shell-quit-timeout
     The number of seconds to wait after sending proof-shell-quit-cmd.

     After this timeout, the proof shell will be killed off more rudely. If your proof assistant takes a long time to clean up (for example writing persistent databases out or the like), you may need to bump up this value.

 -- Variable: proof-shell-cd-cmd
     Command to the proof assistant to change the working directory.

     The format character %s is replaced with the directory, and the proof-terminal-char is added on to the end.

     This is used to define the function proof-cd which changes to the value of (default-directory) for script buffers. For files, the value of (default-directory) is simply the directory the file resides in.

     NB: By default, proof-cd is called from proof-activate-scripting-hook, so that the prover switches to the directory of a proof script every time scripting begins.

See Handling multiple files, for more details about the final two settings in this group,

 -- Variable: proof-shell-inform-file-processed-cmd
     Command to the proof assistant to tell it that a file has been processed.

     The format character %s is replaced by a complete filename for a script file which has been fully processed interactively with Proof General.

     This is used to interface with the proof assistant's internal management of multiple files, so the proof assistant is kept aware of which files have been processed.  Specifically, when scripting is deactivated in a completed buffer, it is added to Proof General's list of processed files, and the prover is told about it by issuing this command.

     If this is set to nil, no command is issued.

     See also: proof-shell-inform-file-retracted-cmd, proof-shell-process-file, proof-shell-compute-new-files-list.

 -- Variable: proof-shell-inform-file-retracted-cmd
     Command to the proof assistant to tell it that a file has been retracted.

     The format character %s is replaced by a complete filename for a script file which Proof General wants the prover to consider as not completely processed.

     This is used to interface with the proof assistant's internal management of multiple files, so the proof assistant is kept aware of which files have been processed.  Specifically, when scripting is activated, the file is removed from Proof General's list of processed files, and the prover is told about it by issuing this command.  The action may cause the prover in turn to suggest to Proof General that files depending on this one are also unlocked.

     If this is set to nil, no command is issued.

     See also: proof-shell-inform-file-processed-cmd, proof-shell-process-file, proof-shell-compute-new-files-list.

Settings for matching output from proof process
-----------------------------------------------

 -- Variable: proof-shell-wakeup-char
     A special character which terminates an annotated prompt.

     Set to nil if proof assistant does not support annotated prompts.

 -- Variable: proof-shell-first-special-char
     First special character.

     Codes above this character can have special meaning to Proof General, and are stripped from the prover's output strings. Leave unset if no special characters are being used.

 -- Variable: proof-shell-prompt-pattern
     Proof shell's value for comint-prompt-pattern, which see.

     This pattern is just for interaction in comint (shell buffer). You don't really need to set it.

 -- Variable: proof-shell-annotated-prompt-regexp
     Regexp matching a (possibly annotated) prompt pattern.

     Output is grabbed between pairs of lines matching this regexp. To help matching you may be able to annotate the proof assistant prompt with a special character not appearing in ordinary output. The special character should appear in this regexp, and should be the value of proof-shell-wakeup-char.

 -- Variable: proof-shell-abort-goal-regexp
     Regexp matching output from an aborted proof.

 -- Variable: proof-shell-error-regexp
     Regexp matching an error report from the proof assistant.

     We assume that an error message corresponds to a failure in the last proof command executed.  So don't match mere warning messages with this regexp.  Moreover, an error message should not be matched as an eager annotation (see proof-shell-eager-annotation-start) otherwise it will be lost.

     Error messages are considered to begin from proof-shell-error-regexp and continue until the next prompt.

     The engine matches interrupts before errors, see proof-shell-interrupt-regexp.

     It is safe to leave this variable unset (as nil).

 -- Variable: proof-shell-interrupt-regexp
     Regexp matching output indicating the assistant was interrupted.

     We assume that an interrupt message corresponds to a failure in the last proof command executed.  So don't match mere warning messages with this regexp.  Moreover, an interrupt message should not be matched as an eager annotation (see proof-shell-eager-annotation-start) otherwise it will be lost.

     The engine matches interrupts before errors, see proof-shell-error-regexp.

     It is safe to leave this variable unset (as nil).

 -- Variable: proof-shell-proof-completed-regexp
     Regexp matching output indicating a finished proof.

     Match number 1 should be the response text.

     This is used to enable the QED function (save a proof) and to control what output appears in the response buffer at the end of a proof.

 -- Variable: proof-shell-clear-response-regexp
     Regexp matching output telling Proof General to clear the response buffer.

     This feature is useful to give the prover more control over what output is shown to the user.  Set to nil to disable.

 -- Variable: proof-shell-start-goals-regexp
     Regexp matching the start of the proof state output.

     This is an important setting.  Output between proof-shell-start-goals-regexp and proof-shell-end-goals-regexp will be pasted into the goals buffer and possibly analysed further for proof-by-pointing markup.

 -- Variable: proof-shell-end-goals-regexp
     Regexp matching the end of the proof state output, or nil.

     If nil, just use the rest of the output following proof-shell-start-goals-regexp.

 -- Variable: proof-shell-eager-annotation-start
     Eager annotation field start.  A regular expression or nil.

     An eager annotation indicates to Proof General that some following output should be displayed immediately and not accumulated for parsing later. It's nice to recognize warnings or file-reading messages with this regexp.

     See also proof-shell-eager-annotation-start-length, proof-shell-eager-annotation-end.

     Set to nil to disable this feature.

 -- Variable: proof-shell-eager-annotation-end
     Eager annotation field end.  A regular expression or nil.

     An eager annotation indicates to Emacs that some following output should be displayed immediately and not accumulated for parsing.

     The default value is "\n" to match up to the end of the line.

 -- Variable: proof-shell-assumption-regexp
     A regular expression matching the name of assumptions.

     At the moment, this setting is not used in the generic Proof General.

     In the future it will be used for a generic implementation for proof-goal-hyp-fn, used to help parse the goals buffer to annotate it for proof by pointing.

Hooks and function variables
----------------------------

 -- Variable: proof-pre-shell-start-hook
     Hooks run before proof shell is started.

     Suggestion: set this to a function which configures just these proof shell variables:

             proof-prog-name
             proof-mode-for-shell
             proof-mode-for-response
             proof-mode-for-pbp

     This is the bare minimum needed to get a shell buffer and its friends configured in the function proof-shell-start.

 -- Variable: proof-shell-insert-hook
     Hooks run by proof-shell-insert before inserting a command.

     Can be used to configure the proof assistant to the interface in various ways -- for example, to observe or alter the commands sent to the prover, or to sneak in extra commands to configure the prover.

     This hook is called inside a save-excursion with the proof-shell-buffer current, just before inserting and sending the text in the variable string.  The hook can massage string or insert additional text directly into the proof-shell-buffer. Before sending string, it will be stripped of carriage returns.

     Additionally, the hook can examine the variable action.  It will be a symbol, set to the callback command which is executed in the proof shell filter once string has been processed.  The action variable suggests what class of command is about to be inserted:

           'proof-done-invisible       A non-scripting command
           'proof-done-advancing       A "forward" scripting command
           'proof-done-retracting      A "backward" scripting command

     Caveats: You should be very careful about setting this hook.  Proof General relies on a careful synchronization with the process between inputs and outputs.  It expects to see a prompt for each input it sends from the queue.  If you add extra input here and it causes more prompts than expected, things will break!  Extending the variable string may be safer than inserting text directly, since it is stripped of carriage returns before being sent.

     Example uses: LEGO uses this hook for setting the pretty printer width if the window width has changed; Plastic uses it to remove literate-style markup from string. The x-symbol support uses this hook to convert special characters into tokens for the proof assistant.

 -- Variable: proof-shell-handle-error-or-interrupt-hook
     Run after an error or interrupt has been reported in the response buffer.

     Hook functions may inspect proof-shell-error-or-interrupt-seen to determine whether the cause was an error or interrupt.

 -- Variable: proof-shell-process-output-system-specific
     Set this variable to handle system specific output.

     Errors, start of proofs, abortions of proofs and completions of proofs are recognised in the function proof-shell-process-output. All other output from the proof engine is simply reported to the user in the RESPONSE buffer.

     To catch further special cases, set this variable to a pair of functions '(condf . actf). Both are given (cmd string) as arguments. cmd is a string containing the currently processed command. string is the response from the proof system. To change the behaviour of proof-shell-process-output, (condf cmd string) must return a non-nil value. Then (actf cmd string) is invoked. See the documentation of proof-shell-process-output for the required output format.

See Handling multiple files, for more details about the final three settings in this section.

 -- Variable: proof-shell-process-file
     A pair (REGEXP . FUNCTION) to match a processed file name.

     If REGEXP matches output, then the function FUNCTION is invoked on the output string chunk. It must return the name of a script file (with complete path) that the system has successfully processed. In practice, FUNCTION is likely to inspect the match data.  If it returns the empty string, the file name of the scripting buffer is used instead.  If it returns nil, no action is taken.

     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 added to the front of proof-included-files-list.

 -- Variable: proof-shell-retract-files-regexp
     Matches a message that the prover has retracted a file.

     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.

 -- Variable: proof-shell-compute-new-files-list
     Function to update proof-included-files list.

     It needs to return an up to date list of all processed files. Its output is stored in proof-included-files-list. Its input is the string of which proof-shell-retract-files-regexp matched a substring. In practice, this function is likely to inspect the previous (global) variable proof-included-files-list and the match data triggered by proof-shell-retract-files-regexp.

Goals buffer settings
=====================

The goals buffer settings allow configuration of Proof General for proof by pointing or similar features.

 -- Variable: pbp-change-goal
     Command to change to the goal %s

 -- Variable: pbp-goal-command
     Command informing the prover that pbp-button-action has been

     requested on a goal.

 -- Variable: pbp-hyp-command
     Command informing the prover that pbp-button-action has been

     requested on an assumption.

 -- Variable: pbp-error-regexp
     Regexp indicating that the proof process has identified an error.

 -- Variable: proof-shell-result-start
     Regexp matching start of an output from the prover after pbp commands.

     In particular, after a pbp-goal-command or a pbp-hyp-command.

 -- Variable: proof-shell-result-end
     Regexp matching end of output from the prover after pbp commands.

     In particular, after a pbp-goal-command or a pbp-hyp-command.

 -- Variable: proof-shell-start-char
     Starting special for a subterm markup.

     Subsequent characters with values below proof-shell-first-special-char are assumed to be subterm position indicators.  Subterm markups should be finished with proof-shell-end-char.

 -- Variable: proof-shell-end-char
     Finishing special for a subterm markup.

     See documentation of proof-shell-start-char.

 -- Variable: proof-shell-goal-char
     Mark for goal.

     This setting is also used to see if proof-by-pointing features are configured.  If it is unset, some of the code for parsing the is disabled.

 -- Variable: proof-shell-field-char
     Annotated field end

Splash screen settings
======================

The splash screen can be configured, in a rather limited way.

 -- Variable: proof-splash-time
     Minimum number of seconds to display splash screen for.

     The splash screen may be displayed for a couple of seconds longer than this, depending on how long it takes the machine to initialise Proof General.

 -- Variable: proof-splash-contents
     Evaluated to configure splash screen displayed when entering Proof General.

     A list of the screen contents.  If an element is a string or an image specifier, it is displayed centred on the window on its own line. If it is nil, a new line is inserted.

 -- Variable: proof-splash-extensions
     Prover specific extensions of splash screen.

     These are evaluated and appended to proof-splash-contents.

Global constants
================

The settings here are internal constants used by Proof General. You don't need to configure these for your proof assistant unless you want to modify or extend the defaults.

 -- Variable: proof-general-name
     Proof General name used internally and in menu titles.

 -- User Option: proof-general-home-page
     Web address for Proof General

     The default value is "http://www.dcs.ed.ac.uk/home/proofgen".

 -- Variable: proof-universal-keys
     List of key-bindings made for the script, goals and response buffer.

     Elements of the list are tuples (k . f) where k is a key-binding (vector) and f the designated function.

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

Documentation for the configuration settings mentioned here appears in the previous sections, this section is intended to help explain the use of those settings.

Proof General maintains a list proof-included-files-list of files which it thinks have been processed by the proof assistant.  When a file which is on this list is visited in Emacs, it will be coloured entirely blue to indicate that it has been processed.  No editing of the file will be allowed (unless proof-strict-read-only allows it).

 -- Variable: proof-included-files-list
     List of files currently included in proof process.

     This list contains files in canonical truename format (see file-truename).

     Whenever a new file is being processed, it gets added to this list via the proof-shell-process-file configuration settings. When the prover retracts a file, this list is resynchronised via the proof-shell-retract-files-regexp and proof-shell-compute-new-files-list configuration settings.

     Only files which have been fully processed should be included here. Proof General itself will automatically add the filenames of a script buffer which has been completely read when scripting is deactivated. It will automatically remove the filename of a script buffer which is completely unread when scripting is deactivated.

     NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant should only output a processed message when a file has been successfully read.

The way that proof-included-files-list is maintained is the key to multiple file management.  (But you should not set this variable directly, it is managed via the configuration settings).

There is a range of strategies for managing multiple files.  Ideally, file dependencies should be managed by the proof assistant.  Proof General will use the prover's low-level commands to process a whole file and its requirements non-interactively, without going through script management.  So that the user knows which files have been processed, the proof assistant should issue messages which Proof General can recognize (``file foo has been processed'') --- see proof-shell-process-file.  When the user wants to edit a file which has been processed, the file must be retracted (unlocked).  The proof assistant should provide a command corresponding to this action, which undoes a given file and all its dependencies.  As each file is undone, a message should be issued which Proof General can recognize (``file foo has been undone'') -- see proof-shell-retract-files-regexp.  (The function proof-shell-compute-new-files-list should be set to calculate the new value for proof-included-files-list after a retract message has been seen).

As well as this communication from the assistant to Proof General about processed or retracted files, Proof General can communicate the other way: it will tell the proof assistant when it has processed or retracted a file via script management.  This is because during script management, the proof assistant may not be aware that it is actually dealing with a file of proof commands (rather than just terminal input).

Proof General will provide this information in two special instances. First, when scripting is turned off in a file that has been completely processed, Proof General will tell the proof assistant using proof-shell-inform-file-processed-cmd.  Second, when scripting is turned on in a file which is completely processed, Proof General will tell the proof assistant to reconsider: the file should not be considered completely processed yet.  This uses the setting proof-shell-inform-file-retracted-cmd.  This second case might lead to a series of messages from the prover telling Proof General to unlock files which depend on the present one, again via proof-shell-retract-files-regexp.

What we have described so far is the ideal case, but it may require some support from the proof assistant to set up (for example, if file-level undo is not normally supported, or the messages during file processing are not suitable).  Moreover, some proof assistants may not have file handling with dependencies, or may have a particularly simple case of a linear context: each file depends on all the ones processed before it. Proof General allows you a shortcut to get automatic management of multiple files in these cases by setting the flag proof-auto-multiple-files.  This setting is probably an approximation to the right thing for any proof assistant.  More files than necessary will be retracted if the prover has a tree-like file dependency rather than a linear one.

Finally, we should mention how Proof General recognizes file processing messages from the proof assistant.  Proof General considers OUTPUT delimited by the the two regular 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 the contents further. Among other important messages characterised by these regular expressions (warnings, errors, or information), the prover can tell the interface whenever it processes or retracts a file.

To summarize, the settings for multiple file management that may be customized are as follows. To recognize file-processing, proof-shell-process-file.  To recognize messages about file undoing, proof-shell-retract-files-regexp and proof-shell-compute-new-files-list.   See Hooks and function variables.  To tell the prover about files handled with script management, use proof-shell-inform-file-processed-cmd and proof-shell-inform-file-retracted-cmd.  See Proof shell commands.  Finally, set the flag proof-auto-multiple-files for a automatic approximation to multiple file handling. See Proof script settings.

Configuring Font Lock
=====================

Support for Font Lock in Proof General was mentioned earlier (see Syntax highlighting).  To configure Font Lock for a new proof assistant, you need to set the variable font-lock-keywords in each of the mode functions you want highlighting for.  Proof General will automatically install these settings, and enable Font Lock minor mode (for syntax highlighting as you type) in script buffers.

To understand its format, check the documentation of font-lock-keywords inside Emacs.

Proof General has a special hack for simplifying font lock settings proof-font-lock-zap-commas, but it is recommended to restrict to using the font-lock-keywords setting if possible.

 -- Variable: proof-font-lock-zap-commas
     If non-nil, enable a font-lock hack which unfontifies commas.

     If you fontify variables inside lists like [a,b,c] by matching on the brackets [ and ], you may take objection to the commas being coloured as well.  In that case, enable this hack which will magically restore the commas to the default font for you.

     The hack is rather painful and forces immediate fontification of files on loading (no lazy, caching locking).  It is unreliable under FSF Emacs, to boot.

     LEGO and Coq enable it by tradition.

Configuring X-Symbol
====================

The X-Symbol package was mentioned earlier (see X-Symbol support). To configure X-Symbol for Proof General, you must understand a little bit of how X-Symbol works: read the documentation that is supplied with it.

The basic task is to set up a token language for your proof assistant.  If your assistant is stored in the subdirectory MYPROVER, the token language will be called MYPROVER and be defined in a file x-symbol-MYPROVER.el which is automatically loaded by X-Symbol.  The name of the token language mode will be MYPROVERsym.

Proof General will check that the file x-symbol-MYPROVER.el exists and set up X-Symbol to load it.  The token language file must define a number of standard settings, and X-Symbol will give warnings if any of them are missing.

Apart from the token language file, there are several settings for X-Symbol which you can set in the usual configuration file MYPROVER.el.  These settings are optional.

 -- Variable: proof-xsym-activate-command
     Command to activate token input/output for X-Symbol.

     If non-nil, this command is sent to the proof assistant when X-Symbol support is activated.

 -- Variable: proof-xsym-deactivate-command
     Command to deactivate token input/output for X-Symbol.

     If non-nil, this command is sent to the proof assistant when X-Symbol support is deactivated.

We expect tokens to be used uniformly, so that along with each script mode buffer, the response buffer and goals buffer also invoke X-Symbol to display special characters in the same token language.  This happens automatically.  If you want additional modes to use X-Symbol with the token language for your proof assistant, you can set proof-xsym-extra-modes.

 -- Variable: proof-xsym-extra-modes
     List of additional mode names to use X-Symbol with Proof General tokens.

     These modes will have X-Symbol enabled for the proof assistant token language, in addition to the four modes for Proof General (script, shell, response, pbp).

     Set this variable if you want additional modes to also display tokens (for example, editing documentation or source code files).

Writing more lisp code
======================

You may want to add some extra features to your instance of Proof General which are not supported in the generic core.  To do this, you can use the settings described above, plus a small number of fundamental functions in Proof General which you can consider as exported in the generic interface.  Be careful using more functions than are mentioned here because the internals of Proof General may change between versions.

The recommended functions you may invoke are these:

  * Any of the interactive commands (i.e. anything you can invoke with M-x, including all key-bindings)

  * The function proof-shell-invisible-command documented below.

This function proof-shell-invisible-command is a useful utility for sending a single command to the process.  You should use this to implement user-level or internal functions rather than attempting to directly manipulate the proof action list, or insert into the shell buffer.

 -- Function: proof-shell-invisible-command cmd &optional wait
     Send CMD to the proof process.  Add terminal string if necessary.

     By default, let the command be processed asynchronously. But if optional WAIT command is non-nil, wait for processing to finish before and after sending the command. If WAIT is an integer, wait for that many seconds afterwards.

There are two handy macros to help you define functions which invoke proof-shell-invisible-command.

 -- Macro: proof-define-assistant-command
     Define command FN to send string BODY to proof assistant, based on CMDVAR.

     BODY defaults to CMDVAR, a variable.

 -- Macro: proof-define-assistant-command-witharg
     Define command FN to prompt for string CMDVAR to proof assistant.

     CMDVAR is a function or string.  Automatically has history.

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

This chapter sketches some of the internal functions and variables of Proof General, to help developers who wish to understand or modify the code.

Most of the documentation below is generated automatically from the comments in the code.  Because Emacs lisp is interpreted and self-documenting, the best way to find your way around the source is inside Emacs once Proof General is loaded.  Read the source files, and use functions such as C-h v and C-h f.

The code is split into files.  The following sections document the important files, kept in the generic/ subdirectory.

Spans
=====

Spans are an abstraction of XEmacs extents used to help bridge the gulf between FSF GNU Emacs and XEmacs.  In FSF GNU Emacs, spans are implemented using overlays.

See the files span-extent.el and span-overlay.el for the implementation of the common interface in each case.

Proof General site configuration
================================

The file proof-site.el contains the initial configuration for Proof General for the site (or user) and the choice of provers.

The first part of the configuration is to set proof-home-directory to the directory that proof-site.el is located in, or to the variable of the environment variable PROOFGENERAL_HOME if that is set.

 -- Variable: proof-home-directory
     Directory where Proof General is installed. Ends with slash.

     Default value taken from environment variable PROOFGENERAL_HOME if set, otherwise based on where the file proof-site.el was loaded from. You can use customize to set this variable.

Further directory variables allow the files of Proof General to be split up and installed across a system if need be, rather than under the proof-home-directory root.

 -- Variable: proof-images-directory
     Where Proof General image files are installed. Ends with slash.

 -- Variable: proof-info-directory
     Where Proof General Info files are installed. Ends with slash.

After defining these settings, we define a mode stub for each proof assistant enabled.  The mode stub will autoload Proof General for the right proof assistant when a file is visited with the corresponding extension.  The proof assistants enabled are the ones listed in the proof-assistants setting.

 -- User Option: proof-assistants
     Choice of proof assistants to use with Proof General.

     A list of symbols chosen from: 'demoisa 'isar 'isa 'lego 'coq 'plastic. Each proof assistant defines its own instance of Proof General, providing session control, script management, etc.  Proof General will be started automatically for the assistants chosen here. To avoid accidently invoking a proof assistant you don't have, only select the proof assistants you (or your site) may need.

     You can select which proof assistants you want by setting this variable before proof-site.el is loaded, or by setting the environment variable PROOFGENERAL_ASSISTANTS to the symbols you want, for example "lego isa".  Or you can edit the file proof-site.el itself.

     Note: to change proof assistant, you must start a new Emacs session.

     The default value is (demoisa isar isa lego coq plastic).

The file proof-site.el also defines a version variable.

 -- Variable: proof-general-version
     Version string identifying Proof General release.

User option conventions
=======================

The file proof-config.el defines the configuration variables for Proof General, including user options.  See Adapting Proof General to Other Provers, for details of its contents.  Here we mention some conventions for declaring user options.

User options are declared using defcustom as usual, but have `*' as the first character of their docstrings (standard Emacs convention).  Also, they live in the customize group proof-user-options.

If changing a user option setting amounts to more than just setting a variable (it may have some dynamic effect), we set the custom-set property for the variable to the function proof-set-value which does an ordinary set-default to set the variable, and then calls a function with the same name as the variable, to do whatever is necessary according to the new value for the variable.

There are several settings which can be switched on or off by the user, which use this proof-set-value mechanism.  They are controlled by boolean variables with names like proof-FOO-enable, and appear at the start of the customize group proof-user-options. They should be edited by the user through the customization mechanism, and set in the code using customize-set-variable.

In proof.el there is a handy macro, proof-customize-toggle, which constructs an interactive function for toggling boolean customize settings.  We can use this to make an interactive function proof-FOO-toggle to put on a menu or bind to a key, for example.

This general scheme is followed as far as possible, to give uniform behaviour and appearance for boolean user options, as well as interfacing properly with the customize mechanism.

 -- Function: proof-set-value sym value
     Set a customize variable using set-default and a function.

     We first call set-default to set SYM to VALUE. Then if there is a function SYM (i.e. with the same name as the variable SYM), it is called to take some dynamic action for the new setting.

 -- Macro: proof-customize-toggle
     Make a function for toggling a boolean customize setting VAR.

     The toggle function uses customize-set-variable to change the variable.

Global variables
================

Global variables are defined in proof.el.  The same file defines a few utility functions and some triggers to load in the other files.

 -- Variable: proof-script-buffer
     The currently active scripting buffer or nil if none.

 -- Variable: proof-shell-buffer
     Process buffer where the proof assistant is run.

 -- Variable: proof-response-buffer
     The response buffer.

 -- Variable: proof-goals-buffer
     The goals buffer (also known as the pbp buffer).

 -- Variable: proof-buffer-type
     Symbol indicating the type of this buffer: 'script, 'shell, 'pbp, or 'response.

 -- Variable: proof-included-files-list
     List of files currently included in proof process.

     This list contains files in canonical truename format (see file-truename).

     Whenever a new file is being processed, it gets added to this list via the proof-shell-process-file configuration settings. When the prover retracts a file, this list is resynchronised via the proof-shell-retract-files-regexp and proof-shell-compute-new-files-list configuration settings.

     Only files which have been fully processed should be included here. Proof General itself will automatically add the filenames of a script buffer which has been completely read when scripting is deactivated. It will automatically remove the filename of a script buffer which is completely unread when scripting is deactivated.

     NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant should only output a processed message when a file has been successfully read.

 -- Variable: proof-shell-proof-completed
     Flag indicating that a completed proof has just been observed.

     If non-nil, the value counts the commands from the last command of the proof (starting from 1).

 -- Variable: proof-shell-error-or-interrupt-seen
     Flag indicating that an error or interrupt has just occurred.

     Set to 'error or 'interrupt if one was observed from the proof assistant during the last group of commands.

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

The file proof-script.el contains the main code for proof script mode, as well as definitions of menus, key-bindings, and user-level functions.

Proof scripts have two important variables for the locked and queue regions.  These variables are local to each script buffer (although we only really need one queue span in total rather than one per buffer).

 -- Variable: proof-locked-span
     The locked span of the buffer.

     Each script buffer has its own locked span, which may be detached from the buffer. Proof General allows buffers in other modes also to be locked; these also have a non-nil value for this variable.

 -- Variable: proof-queue-span
     The queue span of the buffer.  May be detached if inactive or empty.

Various utility functions manipulate and examine the spans.  An important one is proof-init-segmentation.

 -- Function: proof-init-segmentation
     Initialise the queue and locked spans in a proof script buffer.

     Allocate spans if need be.  The spans are detached from the buffer, so the regions are made empty by this function.

For locking files loaded by a proof assistant, we use the next function.

 -- Function: proof-complete-buffer-atomic buffer
     Make sure BUFFER is marked as completely processed, completing with a single step.

     If buffer already contains a locked region, only the remainder of the buffer is closed off atomically.

     This works for buffers which are not in proof scripting mode too, to allow other files loaded by proof assistants to be marked read-only.

Atomic locking is instigated by the next function, which uses the variables proof-included-files-list documented earlier (see Handling multiple files and see Global variables).

 -- Function: proof-register-possibly-new-processed-file file &optional informprover
     Register a possibly new FILE as having been processed by the prover.

     If INFORMPROVER is non-nil, the proof assistant will be told about this, to co-ordinate with its internal file-management.  (Otherwise we assume that it is a message from the proof assistant which triggers this call).

     No action is taken if the file is already registered.

     A warning message is issued if the register request came from the proof assistant and Emacs has a modified buffer visiting the file.

An important pair of functions activate and deactivate scripting for the current buffer.  A change in the state of active scripting can trigger various actions, such as starting up the proof assistant, or altering proof-included-files-list.

 -- Command: proof-activate-scripting &optional nosaves queuemode
     Ready prover and activate scripting for the current script buffer.

     The current buffer is prepared for scripting. No changes are necessary if it is already in Scripting minor mode. Otherwise, it will become the new active scripting buffer, provided scripting can be switched off in the previous active scripting buffer with proof-deactivate-scripting.

     Activating a new script buffer may be a good time to ask if the user wants to save some buffers; this is done if the user option proof-query-file-save-when-activating-scripting is set and provided the optional argument NOSAVES is non-nil.

     The optional argument QUEUEMODE relaxes the test for a busy proof shell to allow one which has mode QUEUEMODE. In all other cases, a proof shell busy error is given.

     Finally, the hooks proof-activate-scripting-hook are run. This can be a useful place to configure the proof assistant for scripting in a particular file, for example, loading the correct theory, or whatever.  If the hooks issue commands to the proof assistant (via proof-shell-invisible-command) which result in an error, the activation is considered to have failed and an error is given.

 -- Command: proof-deactivate-scripting &optional forcedaction
     Deactivate scripting for the active scripting buffer.

     Set proof-script-buffer to nil and turn off the modeline indicator. No action if there is no active scripting buffer.

     We make sure that the active scripting buffer either has no locked region or a full locked region (everything in it has been processed). If this is not already the case, we question the user whether to retract or assert, or automatically take the action indicated in the user option proof-auto-action-when-deactivating-scripting.

     If the scripting buffer is (or has become) fully processed, and it is associated with a file, it is registered on proof-included-files-list.  Conversely, if it is (or has become) empty, we make sure that it is not registered.  This is to be certain that the included files list behaves as we might expect with respect to the active scripting buffer, in an attempt to harmonize mixed scripting and file reading in the prover.

     This function either succeeds, fails because the user refused to process or retract a partly finished buffer, or gives an error message because retraction or processing failed.  If this function succeeds, then proof-script-buffer is nil afterwards.

     The optional argument FORCEDACTION overrides the user option proof-auto-action-when-deactivating-scripting and prevents questioning the user.  It is used to make a value for the kill-buffer-hook for scripting buffers, so that when a scripting buffer is killed it is always retracted.

The next function is the main one used for parsing the proof script buffer.

 -- Function: proof-segment-up-to pos &optional next-command-end
     Create a list of (type, int, string) tuples from end of queue/locked region to POS.

     Each tuple denotes the command and the position of its terminator, type is one of 'comment, or 'cmd. 'unclosed-comment may be consed onto the start if the segment finishes with an unclosed comment. If optional NEXT-COMMAND-END is non-nil, we contine past POS until the next command end.

The function proof-semis-to-vanillas is used to convert a parsed region of the script into a series of commands to be sent to the proof assistant.

 -- Function: proof-semis-to-vanillas semis &optional callback-fn
     Convert a sequence of terminator positions to a set of vanilla extents.

     Proof terminator positions SEMIS has the form returned by the function proof-segment-up-to. Set the callback to CALLBACK-FN or 'proof-done-advancing by default.

The function proof-assert-until-point is the main one used to process commands in the script buffer.  It's actually used to implement the assert-until-point, electric terminator keypress, and find-next-terminator behaviours.  In different cases we want different things, but usually the information (i.e. are we inside a comment) isn't available until we've actually run proof-segment-up-to (point), hence all the different options when we've done so.

 -- Function: proof-assert-until-point &optional unclosed-comment-fun ignore-proof-process-p
     Process the region from the end of the locked-region until point.

     Default action if inside a comment is just process as far as 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 and the buffer will not be activated for scripting.

proof-assert-next-command is a variant of this function.

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

The main command for retracting parts of a script is proof-retract-until-point.

 -- Function: proof-retract-until-point &optional delete-region
     Set up the proof process for retracting until point.

     In particular, set a flag for the filter process to call proof-done-retracting after the proof process has successfully reset its state. If DELETE-REGION is non-nil, delete the region in the proof script corresponding to the proof command sequence. If invoked outside a locked region, undo the last successfully processed command.

To clean up when scripting is stopped, a script buffer is killed, or the proof assistant exits, we use the functions proof-restart-buffers and proof-script-remove-all-spans-and-deactivate.

 -- Function: proof-restart-buffers buffers
     Remove all extents in BUFFERS and maybe reset proof-script-buffer.

     No effect on a buffer which is nil or killed.  If one of the buffers is the current scripting buffer, then proof-script-buffer will deactivated.

 -- Function: proof-script-remove-all-spans-and-deactivate
     Remove all spans from scripting buffers via proof-restart-buffers.

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

The proof shell mode code is in the file proof-shell.el.  Proof shell mode is defined to inherit from comint-mode using define-derived-mode near the end of the file.  The bulk of the code in the file is concerned with sending code to and from the shell, and processing output for the associated buffers (goals and response).

Good process handling is a tricky issue.  Proof General attempts to manage the process strictly, by maintaining a queue of commands to send to the process.  Once a command has been processed, another one is popped off the queue and sent.

There are several important internal variables which control interaction with the process.

 -- Variable: proof-shell-busy
     A lock indicating that the proof shell is processing.

     When this is non-nil, proof-shell-ready-prover will give an error.

 -- Variable: proof-marker
     Marker in proof shell buffer pointing to previous command input.

 -- Variable: proof-action-list
     A list of

            (SPAN COMMAND ACTION)

     triples, which is a queue of things to do. See the functions proof-start-queue and proof-exec-loop.

 -- Variable: proof-analyse-using-stack
     Choice of syntax tree encoding for terms.

     If nil, prover is expected to make no optimisations. If non-nil, the pretty printer of the prover only reports local changes. For LEGO 1.3.1 use nil, for Coq 6.2, use t.

The function proof-shell-start is used to initialise a shell buffer and the associated buffers.

 -- Command: proof-shell-start
     Initialise a shell-like buffer for a proof assistant.

     Also generates goal and response buffers. Does nothing if proof assistant is already running.

The function proof-shell-kill-function performs the converse function of shutting things down; it is used as a hook function for kill-buffer-hook.  Then no harm occurs if the user kills the shell directly, or if it is done more cautiously via proof-shell-exit.  The function proof-shell-restart allows a less drastic way of restarting scripting, other than killing and restarting the process.

 -- Function: proof-shell-kill-function
     Function run when a proof-shell buffer is killed.

     Attempt to shut down the proof process nicely and clear up all the locked regions and state variables. Value for kill-buffer-hook in shell buffer. Also called by proof-shell-bail-out if the process is exited by hand (or exits by itself).

 -- Command: proof-shell-exit
     Query the user and exit the proof process.

     This simply kills the proof-shell-buffer relying on the hook function proof-shell-kill-function to do the hard work.

 -- Function: proof-shell-bail-out process event
     Value for the process sentinel for the proof assistant process.

     If the proof assistant dies, run proof-shell-kill-function to cleanup and remove the associated buffers.  The shell buffer is left around so the user may discover what killed the process.

 -- Command: proof-shell-restart
     Clear script buffers and send proof-shell-restart-cmd.

     All locked regions are cleared and the active scripting buffer deactivated.

     If the proof shell is busy, an interrupt is sent with proof-interrupt-process and we wait until the process is ready.

     The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process.

     It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing.  (One way of caching is via object files, used by Lego and Coq).

Input to the shell
------------------

Input to the proof shell via the queue region is managed by the functions proof-start-queue and proof-shell-exec-loop.

 -- Function: proof-start-queue start end alist
     Begin processing a queue of commands in ALIST.

     If START is non-nil, START and END are buffer positions in the active scripting buffer for the queue region.

     This function calls proof-append-alist.

 -- Function: proof-append-alist alist &optional queuemode
     Chop off the vacuous prefix of the command queue ALIST and queue it.

     For each proof-no-command item at the head of the list, invoke its callback and remove it from the list.

     Append the result onto proof-action-list, and if the proof shell isn't already busy, grab the lock with QUEUEMODE and start processing the queue.

     If the proof shell is busy when this function is called, then QUEUEMODE must match the mode of the queue currently being processed.

 -- Function: proof-shell-exec-loop
     Process the proof-action-list.

     proof-action-list contains a list of (SPAN COMMAND ACTION) triples.

     If this function is called with a non-empty proof-action-list, the head of the list is the previously executed command which succeeded. We execute (ACTION SPAN) on the first item, then (ACTION SPAN) on any following items which have proof-no-command as their cmd components. If a there is a next command after that, send it to the process.  If the action list becomes empty, unlock the process and remove the queue region.

     The return value is non-nil if the action list is now empty.

Input is actually inserted into the shell buffer and sent to the process by the low-level function proof-shell-insert.

 -- Function: proof-shell-insert string action
     Insert STRING at the end of the proof shell, call comint-send-input.

     First call proof-shell-insert-hook.  The argument ACTION may be examined by the hook to determine how to process the STRING variable.

     Then strip STRING of carriage returns before inserting it and updating proof-marker to point to the end of the newly inserted text.

     Do not use this function directly, or output will be lost.  It is only used in proof-append-alist when we start processing a queue, and in proof-shell-exec-loop, to process the next item.

When Proof General is processing a queue of commands, the lock is managed using a couple of utility functions.  You should not need to use these directly.

 -- Function: proof-grab-lock &optional queuemode
     Grab the proof shell lock, starting the proof assistant if need be.

     Runs proof-state-change-hook to notify state change. Clears the proof-shell-error-or-interrupt-seen flag. If QUEUEMODE is supplied, set the lock to that value.

 -- Function: proof-release-lock &optional err-or-int
     Release the proof shell lock, with error or interrupt flag ERR-OR-INT.

     Clear proof-shell-busy, and set proof-shell-error-or-interrupt-seen to err-or-int.

Output from the shell
---------------------

Two main functions deal with output, proof-shell-process-output and proof-shell-process-urgent-message.  In effect we consider the output to be two streams intermingled: the "urgent" messages which have "eager" annotations, as well as the ordinary ruminations from the prover.

The idea is to conceal as much irrelevant information from the user as possible; only the remaining output between prompts and after the last urgent message will be a candidate for the goal or response buffer. The variable proof-shell-urgent-message-marker tracks the last urgent message seen.

 -- Function: proof-shell-process-output cmd string
     Process shell output (resulting from CMD) by matching on STRING.

     CMD is the first part of the proof-action-list that lead to this output.  The result of this function is a pair (SYMBOL NEWSTRING).

     Here is where we recognizes interrupts, abortions of proofs, errors, completions of proofs, and proof step hints (proof by pointing results). They are checked for in this order, using

            proof-shell-interrupt-regexp
            proof-shell-error-regexp
            proof-shell-abort-goal-regexp
            proof-shell-proof-completed-regexp
            proof-shell-result-start

     All other output from the proof engine will be reported to the user in the response buffer by setting proof-shell-delayed-output to a cons cell of ('insert . TEXT) where TEXT is the text string to be inserted.

     Order of testing is: interrupt, abort, error, completion.

     To extend this function, set proof-shell-process-output-system-specific.

     The "aborted" case is intended for killing off an open proof during retraction.  Typically it the error message caused by a proof-kill-goal-command.  It simply inserts the word "Aborted" into the response buffer.  So it is expected to be the result of a retraction, rather than the indication that one should be made.

     This function can return one of 4 things as the symbol: 'error, 'interrupt, 'loopback, or nil. 'loopback means this was output from pbp, and should be inserted into the script buffer and sent back to the proof assistant.

 -- Variable: proof-shell-urgent-message-marker
     Marker in proof shell buffer pointing to end of last urgent message.

 -- Function: proof-shell-process-urgent-message message
     Analyse urgent MESSAGE for various cases.

     Cases are: included file, retracted file, cleared response buffer, or if none of these apply, display it. MESSAGE should be a string annotated with proof-shell-eager-annotation-start, proof-shell-eager-annotation-end.

The main processing point which triggers other actions is proof-shell-filter.

 -- Function: proof-shell-filter str
     Filter for the proof assistant shell-process.

     A function for comint-output-filter-functions.

     Deal with output and issue new input from the queue.

     Handle urgent messages first.  As many as possible are processed, using the function proof-shell-process-urgent-messages.

     Otherwise wait until an annotated prompt appears in the input. If proof-shell-wakeup-char is set, wait until we see that in the output chunk STR.  This optimizes the filter a little bit.

     If a prompt is seen, run proof-shell-process-output on the output between the new prompt and the last input (position of proof-marker) or the last urgent message (position of proof-shell-urgent-message-marker), whichever is later. For example, in this case:

           PROMPT> INPUT
           OUTPUT-1
           URGENT-MESSAGE
           OUTPUT-2
           PROMPT>

     proof-marker is set after INPUT by proof-shell-insert and proof-shell-urgent-message-marker is set after URGENT-MESSAGE. Only OUTPUT-2 will be processed.  For this reason, error messages and interrupt messages should not be considered urgent messages.

     Output is processed using proof-shell-filter-process-output.

     The first time that a prompt is seen, proof-marker is initialised to the end of the prompt.  This should correspond with initializing the process.  The ordinary output before the first prompt is ignored (urgent messages, however, are always processed; hence their name).

 -- Function: proof-shell-filter-process-output string
     Subroutine of proof-shell-filter to process output STRING.

     Appropriate action is taken depending on the what proof-shell-process-output returns: maybe handle an interrupt, an error, or deal with ordinary output which is a candidate for the goal or response buffer.  Ordinary output is only displayed when the proof action list becomes empty, to avoid a confusing rapidly changing output.

     After processing the current output, the last step undertaken by the filter is to send the next command from the queue.

Debugging
=========

To debug Proof General, it may be helpful to set the configuration variable proof-show-debug-messages.

 -- User Option: proof-show-debug-messages
     Whether to display debugging messages in the response buffer.

     If non-nil, debugging messages are displayed in the response giving information about what Proof General is doing. To avoid erasing the messages shortly after they're printed, you should set proof-tidy-response to nil.

     The default value is nil.

For more information about debugging Emacs lisp, consult the Emacs Lisp Reference Manual.  I recommend using the source-level debugger edebug.

Obtaining and Installing
************************

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

STOP PRESS: the Proof General web pages are temporarily being hosted at zermelo.dcs.ed.ac.uk.  The canonical address used to be www.dcs.ed.ac.uk, and it may one day revert to this.

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

You can obtain Proof General from the URL

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

The distribution is available in three forms

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

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

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

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

The developer's tarball contains our full source tree, including all of the elisp and documentation, along with our low-level list of things to do, sources for the images, some make files used to generate the release itself from our CVS repository, and some test files.  Developers interested in accessing our CVS repository directly should contact proofgen@dcs.ed.ac.uk.

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")

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.

Setting the names of binaries
=============================

The load-file command you have added will load proof-site which sets the Emacs load path for Proof General and add auto-loads and modes for the supported assistants.

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.

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 with the same .elc files.  Furthermore, we develop Proof General with source files so may miss problems with the byte compiled versions.  If you discover problems using the byte-compiled .elc files which aren't present using the source .el files, please report them to us.

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, see Proof General site configuration.  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 documentation 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 adjust the variable proof-assistants in proof-site.el to remove the extra autoloads.  This is advisable in case the extensions clash with other Emacs modes, for example sml-mode for .ML files, or Verilog mode for .v files.

See Proof General site configuration, to find out how to disable support for provers you don't use.

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

We mention some of the known problems with Proof General here.  The list was written for Proof General 2.0.  It is not a description of all bugs and may be out of date.
 Please consult the file BUGS (http://zermelo.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 the script buffer can edit the "uneditable region" in XEmacs.  This doesn't happen in FSF GNU Emacs.  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 GNU 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-shell-restart to restart the system.

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.

Definitions in a proof state
............................

A thorny issue 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.

Non-writable directories
------------------------

If LEGO 1.3.1 attempts to write a (object) file in a non-writable directory, it forgets the protocol mechanism on how to interact with Proof General and gets stuck.

Workaround: Directly enter Configure AnnotateOn; in the Proof Shell to recover.

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

Coq Proof General does not know about Coq's Section mechanism.

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

Here are some bugs and problems specific to Isabelle Proof General.

Clash with sml-mode
-------------------

Since Isabelle proof scripts are not differentiated from .ML files, Proof General may compete with sml-mode (if you use it) for controlling these buffers.  To ensure Proof General wins, load it last.

Workaround: use another extension for real ML files, e.g. .sml, and disable .ML from entering sml-mode.

Indentation
-----------

Isabelle Proof General doesn't support Proof General's indentation code to indent proof scripts.  In any case, Proof General's indentation code is somewhat broken.

Workaround: indent your script by hand.

Scripting language 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, or include nested structure with semicolons within a top-level phrase.  You will usually notice when a function, or whatever, doesn't get highlighted as you might expect, or when only part of a top-level phrase gets parsed as a command and Proof General gets ``stuck''.  Sometimes you will be able to fix things by changing the script.  Generally 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.

Interaction with theory database
--------------------------------

Isabelle Proof General uses some support from Isabelle to remove and reload theories from the theory database.  To maintain consistency, Isabelle is rather conservative.  So re-asserting a retracted file will often re-load it, even if it has not changed.  (This is because the file may have implicit dependencies on things in the global ML environment not made apparent by the theory structure). This may lead to seemingly unnecessary repetition of time-consuming proofs, so be careful not to retract more than you need!

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, an offer to implement something from it!

Proof by pointing and similar features
======================================

This is a note by David Aspinall about proof by pointing and similar features.

Proof General already supports proof by pointing, and experimental support is provided in LEGO.  We would like to extend this support to other proof assistants.  Unfortunately, proof by pointing requires rather heavy support from the proof assistant.  There are two aspects to the support:

  * term structure mark-up

  * proof by pointing command generation

Term structure mark-up is useful in itself: it allows the user to explore the structure of a term using the mouse (the smallest subexpression that the mouse is over is highlighted), and easily copy subterms from the output to a proof script.

Command generation for proof by pointing is usually specific to a particular logic in use, if we hope to generate a good proof command unambiguously for any particular click. However, Proof General could easily be generalised to offer the user a context-sensitive choice of next commands to apply, which may be more useful in practice, and a worthy addition to Proof General.

Implementors of new proof assistants should be encouraged to consider supporting term-structure mark up from the start.  Command generation should be something that the logic-implementor can specify in some way.

Of the supported provers, we can certainly hope for proof-by-pointing support from Coq, since the CtCoq proof-by-pointing code has been moved into the Coq kernel lately.  I hope the Coq community can encourage somebody to do this.

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 should be able to be adjusted.

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. At present, support for goal-save sequences Goal-save sequences, has been hard wired. No other ACS are currently supported. We propose the following to overcome this deficiency:

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, starting with the command matched by END, 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.

     For convenience one might also want to allow START to be the symbol t as a convenient short-hand for '(lambda (str) ".") which always matches.

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.

References
**********

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

  * [BT98] Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7), pp. 161-194, February 1998.

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

  * [BKS97] 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