path: root/doc/ProofGeneral.texi

\def\fontdefs{\psfamily{bsf}{r}{c}{b}{b}{ri}{ri}{ro}{bo}\def\mainmagstep{1200}}
\input texinfo
@c
@c $Id$
@c
@c NB: the first line of this file uses a non-standard TeXinfo
@c hack to print in Serifa fonts.  It has no effect if you don't have
@c my hacked version of TeXinfo - da.
@c
@c 
@setfilename ProofGeneral.info
@settitle Proof General
@setchapternewpage odd
@paragraphindent 0
@c A flag for whether to include the front image in the
@c DVI file.  You can download the front image from
@c http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneralPortrait.eps.gz
@c then put it into this directory and 'make dvi' (pdf,ps)
@c will set the flag below automatically.
@set haveeps
@iftex
@afourpaper
@end iftex

@c
@c Some URLs.
@c FIXME: unfortunately, broken in buggy pdftexinfo.
@c so removed for now.
@set URLxsymbol  http://www.fmi.uni-passau.de/~wedler/x-symbol/
@set URLisamode  http://zermelo.dcs.ed.ac.uk/~isamode
@set URLpghome   http://zermelo.dcs.ed.ac.uk/home/proofgen
@set URLpglatestrpm  http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm
@set URLpglatesttar  http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz
@set URLpglatestdev  http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz
@c
@c

@c
@c IMPORTANT NOTE ABOUT THIS TEXINFO FILE:
@c I've tried keep full node lines *out* of this file because Emacs makes a
@c mess of updating them and they are a nuisance to do by hand.  
@c Instead, rely on makeinfo and friends to do the equivalent job.  
@c For this to work, we must follow each node
@c immediately with a section command, i.e.:
@c
@c  @node node-name
@c  <section-command>
@c
@c And each section with lower levels must have a menu command in
@c it.  Menu updating with Emacs is a bit better than node updating,
@c but tends to delete the first section of the file in XEmacs!
@c (it's better in FSF Emacs at the time of writing).
@c
@c
@c reminder about references: 
@c        @xref{node}  blah         start of sentence: See [ref]
@c        blah (@pxref{node}) blah  bla (see [ref]), best at end of sentence
@c        @ref{node}                without "see". Careful for info.


@set version 3.1
@set xemacsversion 21.1
@set fsfversion 20.5
@set last-update March 2000
@set rcsid $Id$

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

@c
@c MACROS
@c
@c define one here for a command with a key-binding?
@c
@c I like the idea, but it's maybe against the TeXinfo
@c style to fix together a command and its key-binding.
@c
@c merge functions and variables into concept index.
@c @syncodeindex fn cp
@c @syncodeindex vr cp

@c merge functions into variables index
@c @syncodeindex fn vr

@finalout
@titlepage
@title Proof General
@subtitle Organise your proofs with Emacs!
@subtitle Proof General @value{version}
@subtitle @value{last-update}

@c nested ifs fail here completely, WHY?
@iftex
@ifset haveeps
@c @vskip 1cm
@c The .eps file takes 8.4M!  A pity texi can't seem
@c to deal with gzipped files? (goes down to 1.7M).
@c But this still seems too much to put into the
@c PG distribution just for an image on the manual page,
@c so we take it out for now.
@c Ideally would like some way of generating eps from
@c the .jpg file.   
@image{ProofGeneralPortrait}
@end ifset
@end iftex
@author David Aspinall with H. Goguen, T. Kleymann and D. Sequeira
@page
@vskip 0pt plus 1filll
This manual and the program Proof General are
Copyright @copyright{} 1998-2000 Poof General team, LFCS Edinburgh.


@c
@c COPYING NOTICE
@c
@ignore
Permission is granted to process this file through TeX and print the
results, provided the printed document carries copying permission notice
identical to this one except for the removal of this paragraph (this
paragraph not being relevant to the printed manual).
@end ignore

@sp 2
Permission is granted to make and distribute verbatim copies of this
manual provided the copyright notice and this permission notice are
preserved on all copies.  
@sp 2

This manual documents Proof General, Version @value{version}, for use
with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion}
or later versions.

Version control: @code{@value{rcsid}}
@end titlepage

@page


@ifinfo
@node Top
@top Proof General

This file documents version @value{version} of @b{Proof General}, a
generic Emacs interface for proof assistants.

Proof General @value{version} has been tested with XEmacs
@value{xemacsversion} and FSF GNU Emacs @value{fsfversion}.  It is
supplied ready customized for the proof assistants Coq, Lego, 
Isabelle, and HOL.

@menu
* Preface::                     
* Introducing Proof General::   
* Basic Script Management::     
* Proof by Pointing::
* Advanced Script Management::  
* Support for other Packages::  
* Hints and Tips::
* Customizing Proof General::   
* LEGO Proof General::          
* Coq Proof General::           
* Isabelle Proof General::    
* HOL Proof General::
* Adapting Proof General to Other Provers::  
* Internals of Proof General::  
* Obtaining and Installing::  
* Known bugs and workarounds::  
* Plans and ideas::             
* References::                  
* Function Index::              
* Variable Index::              
* Keystroke Index::             
* Concept Index::               
@end menu
@end ifinfo

@node Preface
@unnumbered 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.

Proof General has a home page at
@uref{http://www.lfcs.informatics.ed.ac.uk/proofgen}.  
Visit this page for the latest version of this manual,
other documentation, system downloads, etc.


@menu
* Latest news for 3.1::                     
* News for 3.0::                     
* History::                     
* Credits::                     
@end menu


@node Latest news for 3.1
@unnumberedsec Latest news for 3.1
@cindex news

Proof General 3.1 is released as a bug-fix improvement over version 3.0.
There are some minor cosmetic improvements, but large changes have been
held back to ensure stability.  This release solves a few minor problems
which came to light since the final testing stages for 3.0.  It also
solves some compatibility problems, so now it works with various
versions of Emacs which we hadn't tested with before (non-mule FSF
Emacs, certain Japanese Emacs versions).

We're also pleased to announce HOL Proof General, a new instance of
Proof General for HOL98.  This is supplied as a "technology
demonstration" for HOL users in the hope that somebody from the HOL
community will volunteer to adopt it and become a maintainer and
developer.  (Otherwise, work on HOL Proof General will not continue).

Apart from that there are a few other small improvements.  Check the
CHANGES file in the distribution for full details.

The HOL98 support and most of the work on Proof General 3.1 was
undertaken by David Aspinall while he was visiting ETL, Osaka, Japan,
supported by the British Council and ETL.


@node News for 3.0
@unnumberedsec News for 3.0

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 support for scripting with multiple
files was improved so that it behaves reliably with Isabelle99; file
reading messages can be communicated in both directions now.  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.  We need a volunteer
from the Coq community to help to do this.

An important new feature in Proof General 3.0 is support for
@uref{http://www.fmi.uni-passau.de/~wedler/x-symbol/,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 @code{CHANGES} file in the distribution for more information
about the latest improvements in Proof General.  Developers should check
the @code{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, especially for the improvements to multiple file
handling.  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
@emph{Plastic}, a proof assistant being developed at the University of
Durham.



@node History
@unnumberedsec History
@cindex @code{lego-mode}
@cindex 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 @uref{http://zermelo.dcs.ed.ac.uk/~isamode,Isamode}. Soon
after, the package @code{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 @code{lego-mode} (1.9) was released in May 1995.


@cindex proof by pointing 
@cindex CtCoq
@cindex Centaur
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].

@cindex structure editor
@cindex script management

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.

@cindex generic
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 @code{lego-mode} to Coq. Part
of the generic code in the @code{lego} package was outsourced (and made
more generic) in a new package called @code{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 @code{proof}
mode. David Aspinall suggested @emph{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 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
@uref{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.

@c Why not adapt Proof General to your favourite proof assitant?



@node Credits
@unnumberedsec Credits
@cindex @code{lego-mode}
@cindex maintenance

The main developers of Proof General have been:

@itemize @bullet
@item @b{David Aspinall},
@item @b{Healfdene Goguen},
@item @b{Thomas Kleymann} and
@item @b{Dilip Sequeira}.
@end itemize

LEGO Proof General (the successor of @code{lego-mode}) was crafted by
Thomas Kleymann and Dilip Sequeira. 
@c
It is presently maintained by David Aspinall and
Paul Callaghan @i{<P.C.Callaghan@@durham.ac.uk>}. 
@c
Coq Proof General was crafted by Healfdene Goguen, with
later contributions from Patrick Loiseleur.
It is now maintained by Pierre Courtieu @i{<courtieu@@lri.fr>}.
@c
Isabelle Proof General was crafted and is being maintained by David
Aspinall @i{<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 @uref{http://www.inria.fr/croap/,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.  Since Proof General 2.0, this manual has been maintained
and improved by David Aspinall.  Pierre Courtieu wrote the section on
file variables.

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.  Version 3.1 was
prepared whilst David Aspinall was visiting ETL, Japan, supported by the
British Council.

For testing and feedback for older versions of Proof General, thanks go
to Rod Burstall, Martin Hofmann, and James McKinna, as well as some
those who continued to help with the latest 3.x series.

@c FIXME HERE!
During the development of Proof General 3.x releases, 
many people helped provide testing and other feedback, 
including the Proof General maintainers,
Paul Callaghan, Pierre Courtieu, and Markus Wenzel, and other folk who
tested pre-releases or sent bug reports, including 
Pascal Brisset,
Martin Buechi,
Matt Fairtlough, 
Kim Hyung Ho,
John Longley, 
Tobias Nipkow, 
Leonor Prensa-Nieto, 
David von Oheimb,
and 
Randy Pollack.  Thanks to all of you!




@c
@c CHAPTER: Introduction
@c
@node Introducing Proof General
@chapter Introducing Proof General
@cindex proof assistant
@cindex Proof General

@c would like the logo on the title page really but
@c it doesn't seem to work there for html.
@ifhtml
<IMG SRC="ProofGeneral.jpg" ALT="[ Proof General logo ]" >
@end ifhtml

@dfn{Proof General} is a generic Emacs interface for interactive proof
assistants,@footnote{A @dfn{proof assistant} is a computerized helper for
developing mathematical proofs.  For short, we sometimes call it a
@dfn{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@footnote{A @dfn{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 aim of Proof General is to provide a powerful and configurable
interface for numerous interactive proof assistants.  We target Proof
General mainly at intermediate or expert users, so that the interface
should be useful for large proof developments.  Please help us!
Configure Proof General for your own proof assistant, by adding features
at the generic level of Proof General wherever possible.  @xref{Adapting
Proof General to Other Provers}, for more details, and send ideas,
comments, patches, and code to @code{proofgen@@dcs.ed.ac.uk}.

@menu
* Quick start guide::           
* Features of Proof General::   
* Supported proof assistants::  
* Prerequisites for this manual::
* Organization of this manual::
@end menu




@node Quick start guide
@section 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: 
@multitable @columnfractions .3 .3 .4
@item       @b{Prover}    @tab @b{Extensions} @tab @b{Mode}
@item       LEGO          @tab @file{.l}      @tab @code{lego-mode}
@item       Coq           @tab @file{.v}      @tab @code{coq-mode}
@item       Isabelle      @tab @file{.thy},@file{.ML} @tab @code{isa-mode}
@item       Isabelle/Isar @tab @file{.thy}    @tab @code{isar-mode}
@item       HOL98         @tab @file{.sml}    @tab @code{hol98-mode}
@end multitable
You can also invoke the mode command directly, e.g., type 
@kbd{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 @kbd{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, 
@pxref{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:
@lisp
        (load "@var{proof-general-home}/generic/proof-site.el")
@end lisp
into your @file{~/.emacs} file, where @var{proof-general-home} is the
top-level directory that was created when Proof General was unpacked.

@xref{Obtaining and Installing}, if you need more
information.


@node Features of Proof General
@section Features of Proof General
@cindex Features
@cindex Why use Proof General?

Why would you want to use Proof General?

@c FIXME: would like to keep this synched with web page, really.
@c but web page needs extra markup.

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!

@itemize @bullet
@item @i{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 @dfn{script
buffer} holds input, the commands to construct a proof.  The @dfn{goals
buffer} displays the current list of subgoals to be solved.  The
@dfn{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, @pxref{Summary of Proof General buffers}
and @pxref{Display customization}.


@item @i{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 @emph{asserting} or
@emph{retracting} parts of a proof script, which alters the coloured
regions.

For more details, @pxref{Basic Script Management},
@ref{Script processing commands},
and @ref{Advanced Script Management}.
@item @i{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, @pxref{Script editing commands},
and @ref{Script processing commands}.
@item @i{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, @pxref{Toolbar commands}, @ref{Proof assistant
commands}, and @ref{Customizing Proof General}.

@item @i{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.
@c Proof General expects to parse
@c term-structure annotations on the output syntax of the prover.
@c It uses these to construct a message to the prover indicating
@c where the user has clicked, and the proof assistant can
@c response with a suggested tactic.
@end itemize


@node Supported proof assistants
@section Supported proof assistants

Proof General comes ready-customized for these proof assistants:

@c FLAG VERSIONS HERE
@itemize @bullet
@item 
@b{LEGO Proof General} for LEGO Version 1.3.1@*
@xref{LEGO Proof General}, for more details.
@item 
@b{Coq Proof General} for Coq Version 6.3@*
@xref{Coq Proof General}, for more details.
@item 
@b{Isabelle Proof General} for Isabelle99@*
@xref{Isabelle Proof General}, for more details.
@item 
@b{Isabelle/Isar Proof General} for Isabelle99@*
@xref{Isabelle Proof General}, and documentation suplied with
Isabelle for more details.
@item 
@b{HOL Proof General} for HOL98@*
@xref{HOL Proof General}, for more details.
@end itemize
Proof General is designed to be generic, so if you know how
to write regular expressions, you can make:
@itemize @bullet
@item
@b{Your Proof General} for your favourite proof assistant.@*
For more details of how to make Proof General work
with another proof assistant,
@pxref{Adapting Proof General to Other Provers}.
@end itemize
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.

@node Prerequisites for this manual
@section Prerequisites for this manual

This manual assumes that you understand a little about using Emacs, for
example, switching between buffers using @kbd{C-x b} and understanding
that a key sequence like @kbd{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 @emph{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,
@pxref{How to customize}.  @inforef{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 @kbd{C-h} and find out
everything!  Here are some useful commands:

@table @asis
@item @kbd{C-h i}
@code{info}
@item @kbd{C-h m} 
@code{describe-mode}
@item @kbd{C-h b} 
@code{describe-bindings}
@item @kbd{C-h f} 
@code{describe-function}
@item @kbd{C-h v} 
@code{describe-variable}
@end table


@node Organization of this manual
@section 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
@file{INSTALL}, @file{BUGS}, and @file{TODO}, contained in the
distribution.

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







@c
@c CHAPTER: Basic Script Management
@c
@node Basic Script Management
@chapter 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.

@menu
* Walkthrough example in LEGO::  
* Proof scripts::               
* Script buffers::              
* Summary of Proof General buffers::               
* Script editing commands::     
* Script processing commands::  
* Toolbar commands::            
* Proof assistant commands::    
@end menu

@node Walkthrough example in LEGO
@section 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
@file{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.

This walkthrough is keyboard based, but you could easily use the toolbar
and menu functions instead.  The best way to learn Emacs key bindings is
by using the menus.  You'll find the keys named below listed on the
menus.

@itemize @bullet
@item
First, find a new file by @kbd{C-x C-f} and typing as the filename
@file{example.l}.  This should load LEGO Proof General and the toolbar
and Proof General menus will appear.  You should have an empty buffer
displayed.
@end itemize

The notation @kbd{C-x C-f} means control key with `x' followed by
control key with `f'.  This is a standard notation for Emacs key
bindings, used throughout this manual.  This function also
appears on the @code{File} menu of Emacs.  The remaining commands
used will be on the @code{Proof-General} menu.

If you're not using LEGO, you must choose a different file extension,
appropriately for your proof assistant.  If you don't know what to use,
see the previous chapter for the list of supported assistants and file
extensions.

@itemize @bullet
@item
Turn on @dfn{electric terminator} by typing @kbd{C-c ;} and
enter:
@lisp
Module example Import lib_logic;
@end lisp
This first command defines a file header and tells LEGO to use logic; 
these steps are usually not necessary in other proof assistants.
@end itemize

Electric terminator sends commands to the proof assistant as you type
them.  The exact key binding is based on the terminator used for your
proof assistant, but you can always check the menu if you're not sure.

Electric terminator mode is popular, but not enabled by default because
of the principle of least surprise.  You can customize Proof General to
enable it everytime if you want, @xref{Customizing Proof General}.  In
XEmacs, this is particularly easy: just use the menu item @code{Options
-> Save Options} to save some common options while using Proof General.

The @code{Module} 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.

@itemize @bullet
@item
Next type (on a new line if you like):
@lisp
Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);
@end lisp
@end itemize

The goal should be displayed in the goals buffer.

@itemize @bullet
@item 
Now type:
@lisp
Intros;
@end lisp
@end itemize
This will update the goals buffer.

But whoops! That was the wrong command.

@itemize @bullet
@item
Press @kbd{C-c C-BS} to pretend that didn't happen.
@end itemize
Note: @kbd{BS} means the backspace key.  This key press sends an undo
command to LEGO, and deletes the @code{Intros;} command from the proof
script.  If you just want to undo without deleting, you can type
@kbd{C-c C-u} instead, or use the toolbar navigation button.

@itemize @bullet
@item
Instead, let's try:
@lisp
intros; andI;
@end lisp
We've used the conjunction-introduction rule.

To finish off, use these commands:
@lisp
Refine H; intros; Immed; Refine H; intros; Immed;
@end lisp
@end itemize
Now you should see LEGO display the QED message.

@itemize @bullet
@item
Finally, type:
@lisp
Save bland_commutes;
@end lisp
@end itemize

This last command closes the proof and saves the proved theorem.

Moving the mouse pointer over the locked region now reveals that the
entire proof has been aggregated into a single segment. This reflects
the fact that LEGO has thrown away the history of the proof, so if we
want to undo now, the whole proof must be retracted.

@itemize  @bullet
@item 
Suppose we decide to call the goal something more sensible. Move the
cursor up into the locked region, somewhere between @samp{Goal} and
@samp{Save}, enter @kbd{C-c C-RET}.  
@end itemize

You see that the locked segment for the whole proof is now unlocked (and
uncoloured): it is transferred back into the editing region.

The command @kbd{C-c C-RET} moves the end of the locked region to the
cursor position, sending undoing commands or proof commands as
necessary.

@itemize @bullet
@item 
Now correct the goal name, for example:
@lisp
Goal and_commutes: @{A,B:Prop@} (and A B) -> (and B A);
@end lisp
Move the cursor to the end of the buffer, and
type @kbd{C-c C-RET} again.  
@end itemize

Proof General queues the commands for processing and executes them one
by one.  You should see the proof turn pink, then quickly command by
command it is turned blue.  The progress of pink to blue can be
much slower with long and complicated proofs!



@node Proof scripts
@section Proof scripts
@cindex proof script
@cindex scripting

A @dfn{proof script} is a sequence of commands which constructs
definitions, declarations, theories, and proofs in a proof
assistant. Proof General is designed to work with text-based
@i{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 @dfn{shell}
(command interpreter) 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
show the human only 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; proof
assistants usually provide facilities to read a proof script from a file
instead of the terminal.  Using the file, we can @dfn{replay} the proof
script to prove the theorem again.
@c Re-playing a proof script is a non-interactive procedure,
@c since it is supposed to succeed.

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.
@c developing them in proof script files.

@dfn{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,
to keep synchronization.  Regions of the proof script are analysed
based on their syntax and the behaviour of the proof assistant after each
proof command.


@node Script buffers
@section Script buffers
@cindex script buffer
@cindex proof script mode

A @dfn{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 @dfn{proof-mode}).


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

@menu
* Locked queue and editing regions::  
* Goal-save sequences::         
* Active scripting buffer::     
@end menu


@node Locked queue and editing regions
@subsection Locked, queue, and editing regions
@cindex Locked region
@cindex Queue region
@cindex Editing region
@cindex blue text
@cindex pink text


The three regions that a script buffer is divided into are: @c 

@itemize @bullet
@item The @emph{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.

@item The @emph{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.

@item The @emph{editing} region, which contains the commands the user is working
on, and can be edited as normal Emacs text.
@end itemize

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: @emph{assertion} (or processing) and
@emph{retraction} (or undoing).

@cindex Assertion
@strong{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.

@cindex Retraction
@strong{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,
@xref{Script processing commands}.


@node Goal-save sequences
@subsection Goal-save sequences
@cindex goal
@cindex save
@cindex 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 @dfn{goal} command to the
corresponding @dfn{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:
@lisp
   goal @var{mythm} is @var{G}
   @dots{}
   save theorem @var{mythm}
@end lisp
interspersed with comments, definitions, and the like.  Of course, the
exact syntax and terminology will depend on the proof assistant you use.

The name @var{mythm} can appear in a menu for the proof script to help
quickly find a proof (@pxref{Support for function menus}).

@c Proof General recognizes the goal-save sequences in proof scripts.
@c once a goal-save region has been fully processed by the proof assistant,
@c it is treated as atomic when undoing proof steps.  This reflects the
@c fact that most proof assistants discard the history of a proof once a it
@c is completed or once a new proof is begun.


@node Active scripting buffer
@subsection Active scripting buffer
@cindex 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 @dfn{active scripting buffer}.

The active scripting buffer has a special indicator: the word
@code{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 @kbd{C-c C-s}.

@table @asis
@item @kbd{C-c C-s}
@code{proof-toggle-active-scripting}
@end table

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 @code{.ML} script
file and a @code{.thy} theory file which defines its theory.

If you have a partly processed scripting buffer and use @kbd{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,
@code{Scripting incomplete in buffer myproof.l, retract?}
or if you want to process the remainder of the active buffer, 
@code{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: 
@code{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 certainly 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.@footnote{Some proof assistants provide some level of support for
switching between multiple concurrent proofs, but Proof General does not
use this.  Generally the exact context for such proofs is hard to define
to easily split them into multiple files.}  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 @i{completely}
processed.  For more explanation of the handling of multiple files,
@xref{Switching between proof scripts}.

@c TEXI DOCSTRING MAGIC: proof-toggle-active-scripting
@deffn Command proof-toggle-active-scripting &optional arg
Toggle active scripting mode in the current buffer.@*
With @var{arg}, turn on scripting iff @var{arg} is positive.
@end deffn




@node Summary of Proof General buffers
@section Summary of Proof General buffers
@cindex shell buffer
@cindex goals buffer
@cindex response buffer
@cindex proof by pointing

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.

@itemize @bullet
@item The @dfn{proof shell buffer} is an Emacs shell buffer
 used to run your proof assistant.  Usually it is hidden from view
 (but @pxref{Escaping script management}).
 Communication with the proof shell takes place via two or three
 intermediate buffers.
@item  A @dfn{script buffer}, as we have explained, is a buffer for editing a
 proof script.  The @dfn{active scripting buffer} is the script buffer
 which is currently being used to send commands to the proof shell.
@item The @dfn{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 @dfn{proof-by-pointing}.
@item The @dfn{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.
@end itemize

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 (@pxref{Display
customization}).

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

@c When
@c Proof General sees an error in the shell buffer, it will highlight the
@c error and display the buffer automatically.


@c This facility was not added:
@c
@c Optionally, the goals buffer and script buffer can be identified
@c @pxref{Identify goals and response}.  The disadvantage of this is that
@c the goals display can be replaced by other messages, so you must ask for
@c it to be refreshed.  The advantage is that it is simpler to deal with
@c fewer Emacs buffers.



@node Script editing commands
@section 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.

@findex indent-for-tab-command
@vindex proof-script-indent
Indentation is controlled by the user option @code{proof-script-indent}
(@pxref{User options}).  When indentation is enabled, Proof General
will indent lines of proof script with the usual Emacs functions,
particularly @kbd{TAB}, @code{indent-for-tab-command}.
@c FIXME: remove when indentation is fixed.
Unfortunately, indentation in Proof General @value{version} is somewhat
slow.  Therefore with large proof scripts, we recommend
@code{proof-script-indent} is turned off.

Here are the commands for moving around in a proof script,
with their default key-bindings:
@kindex C-c C-a
@kindex C-c C-e
@kindex C-c C-.
@table @kbd
@item C-c C-a
@code{proof-goto-command-start}
@item C-c C-e
@code{proof-goto-command-end}
@item C-c C-.
@code{proof-goto-end-of-locked}
@end table

@c TEXI DOCSTRING MAGIC: proof-goto-command-start
@deffn Command proof-goto-command-start 
Move point to start of current (or final) command of the script.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-goto-command-end
@deffn Command proof-goto-command-end 
Set point to next @samp{@code{proof-terminal-char}}.
@end deffn

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

@c TEXI DOCSTRING MAGIC: proof-goto-end-of-locked
@deffn Command proof-goto-end-of-locked &optional switch
Jump to the end of the locked region, maybe switching to script buffer.@*
If interactive or @var{switch} is non-nil, switch to script buffer first.
@end deffn

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:

@kindex C-button1
@table @kbd
@item C-button1 
@code{proof-mouse-track-insert}
@end table

@c TEXI DOCSTRING MAGIC: proof-mouse-track-insert


@deffn 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 @code{mouse-track-insert}.
@end deffn
Read the documentation in Emacs to find out about the normal behaviour
of @code{proof-mouse-track-insert}, if you don't already know what it
does.


@node Script processing commands
@section Script processing commands
@kindex C-c C-n
@kindex C-c C-u
@kindex C-c C-BS
@kindex C-c C-b
@kindex C-c C-r
@kindex C-c C-RET

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 @code{Proof Process Busy!} if you try to
assert or retract when the queue is being processed.@footnote{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.}

@table @kbd
@item C-c C-n
@code{proof-assert-next-command-interactive}
@item C-c C-u
@code{proof-undo-last-successful-command}
@item C-c C-BS
@code{proof-undo-and-delete-successful-command}
@item C-c C-RET
@code{proof-goto-point}
@item C-c C-b
@code{proof-process-buffer}
@item C-c C-r
@code{proof-retract-buffer}
@item C-c @var{terminator-character}
@code{proof-electric-terminator-toggle}
@end table

The last command, @code{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 @kbd{C-c ;},
for Coq, use @kbd{C-c .}.  This not really a script processing
command. Instead, if enabled, it causes subsequent key presses of
@kbd{;} or @kbd{.} to automatically activate
@code{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 @kbd{C-c C-b}
(@code{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.

@c TEXI DOCSTRING MAGIC: proof-assert-next-command-interactive
@deffn 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.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-undo-last-successful-command
@deffn Command proof-undo-last-successful-command 
Undo last successful command at end of locked region.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-undo-and-delete-last-successful-command
@deffn Command proof-undo-and-delete-last-successful-command 
Undo and delete last successful command at end of locked region.@*
Useful if you typed completely the wrong command.
Also handy for proof by pointing, in case the last proof-by-pointing
command took the proof in a direction you don't like.

Notice that the deleted command is put into the Emacs kill ring, so
you can use the usual @samp{yank} and similar commands to retrieve the
deleted text.
@end deffn


@c TEXI DOCSTRING MAGIC: proof-goto-point
@deffn Command proof-goto-point 
Assert or retract to the command at current position.@*
Calls @code{proof-assert-until-point} or @code{proof-retract-until-point} as
appropriate.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-process-buffer
@deffn Command proof-process-buffer 
Process the current buffer, and maybe move point to the end.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-retract-buffer
@deffn Command proof-retract-buffer 
Retract the current buffer, and maybe move point to the start.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-electric-terminator-toggle
@deffn Command proof-electric-terminator-toggle arg
Toggle @code{proof-electric-terminator-enable}. With @var{arg}, turn on iff ARG>0.@*
This function simply uses @code{customize-set-variable} to set the variable.
It was constructed with the macro @code{proof-customize-toggle}.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-assert-until-point-interactive

@deffn 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.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-retract-until-point-interactive


@deffn 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 (@var{delete-region} non-nil), also
delete the retracted region from the proof-script.
@end deffn
@node Proof assistant commands
@section Proof assistant commands
@kindex C-c C-p
@kindex C-c C-h
@kindex C-c C-c
@kindex C-c C-v
@kindex C-c C-f
@kindex C-c C-t

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

@table @kbd
@item C-c C-p
@code{proof-prf}
@item C-c C-t
@code{proof-ctxt}
@item C-c C-h
@code{proof-help}
@item C-c C-f
@code{proof-find-theorems}
@item C-c C-c
@code{proof-interrupt-process}
@item C-c C-v
@code{proof-minibuffer-cmd}
@end table

@c TEXI DOCSTRING MAGIC: proof-prf
@deffn Command proof-prf 
Show the current proof state.@*
Issues a command to the assistant based on @code{proof-showproof-command}.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-ctxt
@deffn Command proof-ctxt 
Show the current context.@*
Issues a command to the assistant based on @code{proof-context-command}.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-help
@deffn 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 @code{proof-info-command}.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-find-theorems
@deffn Command proof-find-theorems arg
Search for items containing given constants.@*
Issues a command based on @var{arg} to the assistant, using @code{proof-find-theorems-command}.
The user is prompted for an argument.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-interrupt-process
@deffn 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.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-minibuffer-cmd
@deffn 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 @samp{@code{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
@samp{@code{proof-state-preserving-p}} is not configured, or if it is
only an approximate test.
@end deffn

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.  @xref{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 @kbd{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.

@c TEXI DOCSTRING MAGIC: proof-shell-start
@deffn 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.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-shell-restart
@deffn Command proof-shell-restart 
Clear script buffers and send @code{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
@code{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).
@end deffn

@c TEXI DOCSTRING MAGIC: proof-shell-exit
@deffn Command proof-shell-exit 
Query the user and exit the proof process.

This simply kills the @code{proof-shell-buffer} relying on the hook function
@code{proof-shell-kill-function} to do the hard work.
@end deffn



@node Toolbar commands
@section 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
@kbd{M-x}, as well as the toolbar.

@c TEXI DOCSTRING MAGIC: proof-issue-goal
@deffn Command proof-issue-goal arg
Write a goal command in the script, prompting for the goal.@*
Issues a command based on @var{arg} to the assistant, using @code{proof-goal-command}.
The user is prompted for an argument.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-issue-save
@deffn Command proof-issue-save arg
Write a save/qed command in the script, prompting for the theorem name.@*
Issues a command based on @var{arg} to the assistant, using @code{proof-save-command}.
The user is prompted for an argument.
@end deffn




@c
@c CHAPTER: Proof by Pointing
@c 
@node Proof by Pointing
@chapter 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!

@menu
* Goals buffer commands::
@end menu

@node Goals buffer commands
@section 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:

@table @kbd
@item button2
@code{pbp-button-action}
@item C-button2
@code{proof-undo-and-delete-last-successful-command}
@item button3
@code{pbp-yank-subterm}
@end table

Where @kbd{button2} indicates the middle mouse button, and @kbd{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.

@c TEXI DOCSTRING MAGIC: pbp-button-action

@deffn Command pbp-button-action event
Construct a proof-by-pointing command based on the mouse-click @var{event}.@*
This function should be bound to a mouse button in the Proof General
goals buffer.

The @var{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.
@end deffn

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
@code{pbp-yank-subterm}.

@c TEXI DOCSTRING MAGIC: pbp-yank-subterm

@deffn Command pbp-yank-subterm event
Copy the subterm indicated by the mouse-click @var{event}.@*
This function should be bound to a mouse button in the Proof General
goals buffer.

The @var{event} is used to find the smallest subterm around a point.  The
subterm is copied to the @code{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.
@end deffn
@c Proof General expects to parse
@c term-structure annotations on the output syntax of the prover.
@c It uses these to construct a message to the prover indicating
@c where the user has clicked, and the proof assistant can
@c response with a suggested tactic.





@c
@c CHAPTER: Advanced Script Management
@c
@node Advanced Script Management
@chapter Advanced Script Management
@cindex Multiple Files

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.

@menu
* Switching between proof scripts::  
* View of processed files ::    
* Retracting across files::     
* Asserting across files::      
* Automatic multiple file handling::
* Escaping script management::
@end menu

@node Switching between proof scripts
@section Switching between proof scripts
@cindex 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@footnote{The suffix may depend of
the specific proof assistant you are using e.g, LEGO's proof script
files have to end with @file{.l}.} @file{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
@file{sos.l} and retract to where changes are required. Then, using
script management, you want to develop some more basic theory in
@file{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 @file{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.

@node View of processed files 
@section  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@footnote{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 @emph{beginning} of the buffer.
@c This isn't strictly true, is it?  We lock off buffers atomically,
@c but spans in them to start with stay there.  (Only meaningful
@c for reading currently active scripting file)

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 @emph{early locking} when processing a file begins (e.g. LEGO) or
@emph{late locking} when processing a file ends (e.g. Isabelle).

With @emph{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 @emph{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.



@c only true for LEGO!
@c If the proof assistant is not happy with the script and
@c complains with an error message, the buffer will still be marked as
@c having been completely processed. Sorry. You need to visit the
@c troublesome file, retract (which will always retract to the beginning of 
@c the file) and debug the problem e.g., by asserting all of the buffer
@c under the supervision of Proof General, see @ref{Script processing
@c commands}. 


@node Retracting across files
@section Retracting across files
@cindex Retraction

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 @pxref{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.

@node Asserting across files
@section Asserting across files
@cindex Assertion

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, @pxref{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.


@node Automatic multiple file handling
@section 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 @emph{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, @pxref{Handling multiple files}.



@node Escaping script management
@section Escaping script management
@cindex Shell

Occasionally you may want to review the dialogue of the entire session
with the proof assistant, or check that it hasn't done something
unexpected.  Experienced users may also want to directly communicate
with the proof assistant rather than sending commands via the
minibuffer, @pxref{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 @file{comint.el} distributed with your
version of Emacs). You can switch to it using the menu:

@lisp
  Proof-General -> Buffers -> Shell
@end lisp

@b{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:

@table @kbd
@item C-c C-z
@code{proof-frob-locked-end}
@end table

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

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

@c TEXI DOCSTRING MAGIC: proof-frob-locked-end
@deffn 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.
@end deffn


@node Support for other Packages
@chapter 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 
@code{font-lock}, 
@code{x-symbol},
@code{func-menu},
@code{outline-mode},
and @code{etags}.


@menu
* Syntax highlighting::         
* X-Symbol support::
* Support for function menus::  
* Support for outline mode::    
* Support for tags::            
@end menu

@node Syntax highlighting
@section Syntax highlighting
@vindex lego-mode-hooks
@vindex coq-mode-hooks
@vindex isa-mode-hooks
@cindex font lock 
@cindex colour
@c Proof General specifics  

Proof script buffers are decorated (or @i{fontified}) with colours, bold
and italic fonts, etc, according to the syntax of the proof language and
the settings for @code{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
@code{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
@code{M-x global-font-lock-mode}.  The old mechanism of adding hooks to
the mode hooks (@code{lego-mode-hooks}, @code{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 @code{proof-output-fontify-enable} to @code{nil} if you
don't want the output from your proof assistant to be fontified
according to the setting of @code{font-lock-keywords} in the proof
assistant specific portion of Proof General. @xref{User options}.



@node X-Symbol support
@section X-Symbol support
@cindex real symbols
@cindex X-Symbols
@cindex Greek letters
@cindex logical symbols
@cindex mathematical symbols

The X-Symbol package displays characters from a variety of fonts in
Emacs buffers, automatically converting between codes for special
characters and @i{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
@uref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}.

Notice that for proper symbol support, the proof assistant needs to have
a special @i{token language}, or a special character set, to use
symbols.  In this case, the proof assistant will output, and accept as
input, tokens like @code{\longrightarrow}, which display as the
corresponding symbols.  However, for proof assistants which do not have
such token support, we can use "fake" symbol support quite effectively,
displaying ordinary character sequences such as @code{-->} with symbols.
The only problem with this hack is that it can cause surprising results,
for example, using symbols for the greek letters can be confusing
when words like @code{philosophy} appear!

@xref{Configuring X-Symbol}, for notes about how to configure
a proof assistant to use X-Symbol in Proof General.


@node Support for function menus
@section Support for function menus
@vindex proof-goal-with-hole-regexp
@cindex func-menu
@cindex fume-func

The Emacs package @code{func-menu} (formerly called @code{fume-func}) is
a handy facility to make a menu from the names of entities declared in a
buffer.  Proof General configures @code{func-menu} so that you can
quickly jump to particular proofs in a script buffer.  (This is done
with the configuration variables @code{proof-goal-with-hole-regexp} and
@code{proof-save-with-hole-regexp}.)
@c , @pxref{Proof script mode} for further details.

If you want to use function menu, you can simply select "Function menu"
from the Proof General menu, or type @kbd{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 @code{M-x function-menu}), you should find the file
@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 @code{imenu}, also in XEmacs.  Proof General would
be grateful if anyone can send patches for using @code{imenu}
as an alternative to function menu.


@node Support for outline mode
@section Support for outline mode
@cindex outline mode

Proof General configures Emacs variables (@code{outline-regexp} and
@code{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, 
@pxref{Goal-save sequences}. If you want to use @code{outline} to hide 
parts of the proof script in the @emph{locked} region, you need to disable
@code{proof-strict-read-only}.

Use @kbd{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 @inforef{Outline Mode, ,(xemacs)} for more information about
outline mode.


@node Support for tags
@section Support for tags
@cindex 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 @kbd{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 (@file{legotags} and @file{coqtags}) for
making tags tables.  For example, invoking @samp{coqtags *.v} produces a file
@file{TAGS} for all files @samp{*.v} in the current directory. Invoking @samp{coqtags `find . -name \*.v`} produces a file
@file{TAGS} for all files ending in @samp{.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 @kbd{M-tab} to run @code{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 @file{.emacs} file:
@lisp
(add-hook 'proof-mode-hook
  (lambda () (local-set-key '(meta tab) 'tag-complete-symbol)))
@end lisp
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, @inforef{Tags, ,(xemacs)}.



@node Hints and Tips
@chapter Hints and Tips

Apart from the packages officially supported in Proof General, many
other features of Emacs are 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.

Here we provide some hints and tips for a couple of Emacs features which
users have found valuable with Proof General.  Further contributions to
this chapter are welcomed!

@menu
* Using file variables::
* Using abbreviations::
@end menu


@node Using file variables
@section Using file variables
@cindex file variables

A very convenient way to customize file-specific variables is to use the
File Variables (@inforef{File Variables, ,xemacs}). This feature of
Emacs allows to specify the values to use for certain Emacs variables
when a file is loaded. Those values are written as a list at the end of
the file.

For example, in projects involving multiple directories, it is often
useful to set the variables @code{proof-prog-name} and
@code{compile-command} for each file. Here is an example for Coq users:
for the file @file{.../dir/bar/foo.v}, if you want Coq to be started
with the path @code{.../dir/theories/} added in the libraries path
(@code{"-I"} option), you can put at the end of @file{foo.v}:
@lisp

(* 
 Local Variables: 
 coq-prog-name: "coqtop -emacs -full -I ../theories"
 End:
*)
@end lisp

That way the good command is called when the scripting starts in
@file{foo.v}. Notice that the command argument @code{"-I ../theories"}
is specific to the file @file{foo.v}, and thus if you set it via the
configuration tool, you will need to do it each time you load this
file. On the contrary with this method, Emacs will do this operation
automatically.

Extending the previous example, if the makefile for @file{foo.v} is
located in directory @file{.../dir/}, you can add the right compile
command:

@lisp
(* 
 Local Variables: 
 coq-prog-name: "coqtop -emacs -full -I ../theories"
 compile-command: "make -C .. -k bar/foo.vo" 
 End:
*)
@end lisp

And then the right call to make will be done if you use the @kbd{M-x
compile} command. Notice that the lines are commented in order to be
ignored by the proof assistant. It is possible to use this mechanism for
any other buffer local variable. Read (@inforef{File Variables,
,xemacs}.



@node Using abbreviations
@section Using abbreviations

A very useful package of Emacs supports automatic expansions of
abbreviations as you type, @inforef{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:
@lisp
"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"
@end lisp

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 @kbd{C-x a g} (@code{add-global-abbrev}) or
@kbd{C-x a i g} (@code{inverse-add-global-abbrev}).  To enable expansion
of abbreviations, the @code{Abbrev} minor mode, type @kbd{M-x
abbrev-mode RET}.  See the Emacs manual for more details.






@node Customizing Proof General
@chapter Customizing Proof General
@cindex Customization


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 @ref{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.


@menu
* Basic options::
* How to customize::          
* Display customization::       
* User options::                
* Changing faces::              
* Tweaking configuration settings::  
@end menu

@node Basic options
@section Basic options

Proof General has some basic on/off options which you can toggle
directly from the menu:
@lisp
   Proof-General -> Options
@end lisp
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.  @xref{Display customization}.

To save these options, use the usual Emacs save options command,
for XEmacs on the menu:
@lisp
   Options -> Save Options
@end lisp
or @code{M-x customize-save-customized}.

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

@node How to customize
@section How to customize
@cindex Using Customize
@cindex Emacs customization library 

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:
@lisp
   Proof-General -> Customize
@end lisp

Using the customize facility is straightforward.  You can select the
setting to customize via the menus, or with @code{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 @var{set}, @var{save} and
@var{done}.  You must use one of @var{set} or @var{save} to get any
effect.  The @var{save} button stores the setting in your @file{.emacs}
file.  In XEmacs, the menu item @code{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 "@code{proof}-" or
similar prefixes are omitted.  Also, some of the option settings may
have more descriptive names (for example, @var{on} and @var{off}) than
the low-level lisp values (non-@code{nil}, @code{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:
@lisp
   Options -> Customize -> Emacs -> External -> Proof General
@end lisp
in XEmacs.  In FSF GNU Emacs, use the menu:
@lisp
   Help -> Customize -> Top-level Customization Group
@end lisp
and select the @code{External} and then @code{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 @kbd{M-x
load-library RET proof RET}.

For more help with customize, see @inforef{Easy Customization, ,xemacs}.



@node Display customization
@section Display customization
@cindex display customization
@cindex multiple windows
@cindex buffer display customization
@cindex frames
@cindex multiple frames
@cindex three-buffer interaction

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. @code{*isabelle-goals*})
or the response buffer (@code{*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 @code{proof-find-theorems} command at the same time as
the subgoal list.  Set the user option @code{proof-dont-switch-windows} to
make Proof General keep both the goals and response buffer displayed.

@c TEXI DOCSTRING MAGIC: proof-dont-switch-windows
@defopt 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 @code{nil}.
@end defopt

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 @code{proof-delete-empty-windows} helps you do this.

@c TEXI DOCSTRING MAGIC: proof-delete-empty-windows
@defopt 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 @code{'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 @code{nil}.
@end defopt
This option only has an effect when you have set
@code{proof-dont-switch-windows}.

If you are working on a machine with a window system, you can use Emacs
to manage several @i{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
@c TEXI DOCSTRING MAGIC: proof-multiple-frames-enable

@defopt 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
@samp{@code{special-display-regexps}}.

The default value is @code{nil}.
@end defopt
Multiple frames work best when @code{proof-delete-empty-windows} is off
and @code{proof-dont-switch-windows} is on.


@node User options
@section User options
@c Index entries for each option 'concept'
@cindex User options
@cindex Strict read-only
@cindex Query program name
@cindex Dedicated windows
@cindex Remote host
@cindex Toolbar follow mode
@cindex Toolbar disabling
@cindex Toolbar button enablers
@cindex Proof script indentation
@cindex Indentation
@cindex Remote shell
@cindex Running proof assistant remotely
@c @cindex formatting proof script

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 @code{M-x edit-options} mechanism, or simply by
adding @code{setq}'s to your @file{.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.

@c TEXI DOCSTRING MAGIC: proof-splash-enable
@defopt proof-splash-enable 
If non-nil, display a splash screen when Proof General is loaded.

The default value is @code{t}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-electric-terminator-enable
@defopt proof-electric-terminator-enable 
If non-nil, use electric terminator mode.@*
If electric terminator mode is enabled, pressing a terminator will 
automatically issue @samp{@code{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 @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-toolbar-enable
@defopt 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 @code{t}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-x-symbol-enable
@defopt 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 @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-output-fontify-enable
@defopt 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 @code{font-lock-keywords} have been set for the 
buffer modes).

The default value is @code{t}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-strict-read-only
@defopt 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 @code{proof-strict-read-only} during a session, you must 
use the "Restart" button (or M-x @code{proof-shell-restart}) before
you can see the effect in buffers.

The default value for @code{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 @code{strict}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-toolbar-use-button-enablers
@defopt 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 @code{t}.
@end defopt

@c This one removed: proof-auto-retract

@c TEXI DOCSTRING MAGIC: proof-query-file-save-when-activating-scripting
@defopt 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 @code{t}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-script-indent
@defopt 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 @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-one-command-per-line
@defopt 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 @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-prog-name-ask
@defopt proof-prog-name-ask 
If non-nil, query user which program to run for the inferior process.

The default value is @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-prog-name-guess
@defopt proof-prog-name-guess 
If non-nil, use @samp{@code{proof-guess-command-line}} to guess @code{proof-prog-name}.@*
This option is compatible with @code{proof-prog-name-ask}.
No effect if @code{proof-guess-command-line} is nil.

The default value is @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-tidy-response
@defopt 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 @code{t}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-show-debug-messages
@defopt 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 @samp{@code{proof-tidy-response}} to nil.

The default value is @code{nil}.
@end defopt


@c ******* NON-BOOLEANS *******

@c TEXI DOCSTRING MAGIC: proof-follow-mode
@defopt proof-follow-mode 
Choice of how point moves with script processing commands.@*
One of the symbols: @code{'locked}, @code{'follow}, @code{'ignore}.
If @code{'locked}, point sticks to the end of the locked region.
If @code{'follow}, point moves just when needed to display the locked region end.
If @code{'ignore}, point is never moved after movement commands.

The default value is @code{locked}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-auto-action-when-deactivating-scripting
@defopt proof-auto-action-when-deactivating-scripting 
If @code{'retract} or @code{'process}, do that when deactivating scripting.

With this option set to @code{'retract} or @code{'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 @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-script-command-separator
@defopt 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 @code{" "}.
@end defopt

@c TEXI DOCSTRING MAGIC: proof-rsh-command
@defopt proof-rsh-command 
Shell command prefix to run a command on a remote host.  @*
For example,
@lisp
   ssh bigjobs
@end lisp
Would cause Proof General to issue the command @samp{ssh bigjobs isabelle}
to start Isabelle remotely on our large compute server called @samp{bigjobs}.

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

The default value is @code{""}.
@end defopt




@node Changing faces
@section Changing faces

The fonts and colours that Proof General uses are configurable.  If you
alter faces through the customize menus (or the command @kbd{M-x
customize-face}), only the particular kind of display in use (colour
window system, monochrome window system, console, @dots{}) 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
@code{font-lock-} faces (eg @code{font-lock-keyword-face},
@code{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!


@c TEXI DOCSTRING MAGIC: proof-queue-face
@deffn Face proof-queue-face 
Face for commands in proof script waiting to be processed.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-locked-face
@deffn Face proof-locked-face 
Face for locked region of proof script (processed commands).
@end deffn

@c TEXI DOCSTRING MAGIC: proof-error-face
@deffn Face proof-error-face 
Face for error messages from proof assistant.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-warning-face
@deffn Face proof-warning-face 
Face for warning messages.@*
Warning messages can come from proof assistant or from Proof General itself.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-debug-message-face
@deffn Face proof-debug-message-face 
Face for debugging messages from Proof General.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-declaration-name-face
@deffn Face proof-declaration-name-face 
Face for declaration names in proof scripts.@*
Exactly what uses this face depends on the proof assistant.
@end deffn


@c TEXI DOCSTRING MAGIC: proof-tacticals-name-face
@deffn Face proof-tacticals-name-face 
Face for names of tacticals in proof scripts.@*
Exactly what uses this face depends on the proof assistant.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-eager-annotation-face
@deffn Face proof-eager-annotation-face 
Face for important messages from proof assistant.
@end deffn

@c Maybe this detail of explanation belongs in the internals,
@c with just a hint here.
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.




@node Tweaking configuration settings
@section 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
@code{prover-config}, or via the menu
@lisp
    Proof-General -> Internals ->  Prover Config
@end lisp

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

@c TEXI DOCSTRING MAGIC: proof-assistant-home-page
@defvar proof-assistant-home-page 
Web address for information on proof assistant.@*
Used for Proof General's help menu.
@end defvar

Most of the others are more complicated.  For more details of the settings,
see @ref{Adapting Proof General to Other Provers}.  To browse
them, you can look through the customization groups
@code{prover-config}, @code{proof-script} and @code{proof-shell}.  The
group @code{proof-script} contains the configuration variables for
scripting, and the group @code{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,
@code{proof-assistant-home-page} is set in the LEGO code from the value
of the customization setting @code{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).
@c Please contact us if this proves to be a problem for any variable.




@c
@c  CHAPTER: LEGO Proof General
@c 
@node LEGO Proof General
@chapter LEGO Proof General
@cindex 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 @emph{must} start with a module declaration. If the proof script
buffer's file name is @file{fermat.l}, then it must commence with a
declaration of the form

@lisp
Module fermat;
@end lisp

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

@lisp
Module fermat Import lib_nat galois;
@end lisp

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 @samp{Forget}, @samp{ForgetMark}, @samp{KillRef},
@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again
@footnote{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.

@menu
* LEGO specific commands::      
* LEGO tags::                   
* LEGO customizations::         
@end menu


@node LEGO specific commands
@section 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:

@kindex C-c i
@kindex C-c I 
@kindex C-c R 
@table @kbd
@item C-c i   
intros
@item C-c I   
Intros
@item C-c R   
Refine
@end table

@node LEGO tags
@section LEGO tags

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



@node LEGO customizations
@section LEGO customizations

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

@c TEXI DOCSTRING MAGIC: lego-tags
@defopt lego-tags 
The directory of the @var{tags} table for the @var{lego} library

The default value is @code{"/usr/lib/lego/lib_Type/"}.
@end defopt

@c TEXI DOCSTRING MAGIC: lego-www-home-page
@defvar lego-www-home-page 
Lego home page URL.
@end defvar

@c TEXI DOCSTRING MAGIC: lego-help-menu-list
@defvar lego-help-menu-list 
List of menu items for @var{lego} specific help.

See the documentation of @samp{@code{easy-menu-define}} 
@end defvar

@c We don't worry about the following for now. These are too obscure.
@c lego-indent
@c lego-test-all-name

@c We also don't document any of the internal variables which have been
@c set to configure the generic Proof General and which the user should
@c not tamper with


@node Coq Proof General
@chapter 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.

@menu
* Coq-specific commands::
* Editing multiple proofs::
* User-loaded tactics::
@end menu


@node Coq-specific commands
@section Coq-specific commands
@kindex C-c I 
@kindex C-c a
@kindex C-c s
@kindex C-c e

Coq Proof General supplies the following key-bindings:
@table @kbd
@item C-c I   
Inserts ``Intros '' into proof buffer.
@item C-c a
Inserts ``Apply '' into proof buffer.
@item C-c s
Inserts ``Section '' into proof buffer
@item C-c e
Closes the current section by inserting ``End <section-name>.''. (this
should work well with nested sections).
@end table

@node Editing multiple proofs
@section 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.

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

@node User-loaded tactics
@section 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 Proof General failed to
recognize.







@c Sorry, there is currently very little specific documentation written for
@c Coq Proof General. If any Coq user would like to contribute, please send
@c a message to @code{proofgen@@dcs.ed.ac.uk}.

@c Type @kbd{C-h C-m} to get a list of all Coq specific commands and
@c browse the customize menus to find out what customization
@c options there are for Coq.



@c
@c  CHAPTER: Isabelle Proof General
@c

@node Isabelle Proof General
@chapter Isabelle Proof General
@cindex 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
@uref{http://zermelo.dcs.ed.ac.uk/~isamode}.  Detailed documentation
for the theory file mode is included with @code{Isamode}, there are some
notes on the special functions available and customization settings
below.

Note that in ``classic'' Isabelle, @file{.thy} files contain definitions
and declarations for a theory, while @file{.ML} contain proof scripts.
So most of Proof General's functions only make sense in @file{.ML}
files, and there is no toolbar and only a short menu for @file{.thy}
files.  

There is no specific documentation here for the Isabelle/Isar instance
of Proof General.  With Isabelle/Isar, @file{.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
@code{PROOFGENERAL_ASSISTANTS=isar} in the shell before starting Emacs,
to make sure ordinary Isabelle theory file mode isn't loaded instead.


@menu
* ML files::
* Theory files::                
* Isabelle specific commands::  
* Isabelle customizations::     
@end menu


@node ML files
@section ML files
@cindex ML files (in Isabelle)
@cindex Isabelle proof scripts

In Isabelle, ML files are used to hold proof scripts, as well as
definitions of tactics, proof procedures, etc.  So ML files are the
normal domain of Proof General.  But there are some things to be wary
of.

Proof General does not understand full ML syntax(!), so ideally you
should only use Proof General's scripting commands on @file{.ML} files
which contain proof commands (no ML functions, structures, etc).

If you do use files with Proof General which declare functions,
structures, etc, you should be okay provided your code doesn't include
non top-level semi-colons (which will confuse Proof General's simplistic
parser), and provided all value declarations (and other non proof-steps)
occur outside proofs.  This is because within proofs, Proof General
considers every ML command to be a proof step which is undoable.

For example, do this:
@lisp
   structure S = struct
     val x = 3
     val y = 4
   end;
@end lisp
instead of this:
@lisp
   structure S = struct
     val x = 3;
     val y = 4;
   end
@end lisp
In the second case, just the first binding in the structure body will be
sent to Isabelle and Proof General will wait indefinitely.

And do this:
@lisp
    val intros1 = REPEAT (resolve_tac [impI,allI] 1);
    Goal "Q(x) --> (ALL x. P(x) --> P(x))";
    br impI 1;
    by intros1;
    ba 1;
    qed "mythm";
@end lisp
instead of this:
@lisp
    Goal "Q(x) --> (ALL x. P(x) --> P(x))";
    br impI 1;
    val intros1 = REPEAT (resolve_tac [impI,allI] 1);
    by intros1;
    ba 1;
    qed "mythm";
@end lisp
In the last case, when you undo, Proof General wrongly considers the
@code{val} declaration to be a proof step, and it will issue an
@code{undo} to Isabelle to undo it.  This leads to a loss of
synchronization.  To fix things when this happens, simply retract to
some point before the @code{Goal} command and fix your script.

Having ML as a top-level, Isabelle even lets you redefine the entire
proof command language, which will certainly confuse Proof General!
Stick to using the standard functions, tactics, and tacticals and there
should be no problems.  (In fact, there should be no problems provided
you don't use your own "goal" or "qed" forms, which Proof General
recognizes.  As the example above shows, Proof General makes no
attempt to recognize arbitrary tactic applications).


@node Theory files
@section Theory files
@cindex Theory files (in Isabelle)
@cindex ML files (in Isabelle)

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 @file{.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 @strong{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 @file{.thy} buffer.  Extra commands are
provided in theory mode for this:

@c FIXME: should say something about this:
@c This can cause confusion in the theory loader later,
@c especially with @code{update()}.  To be safe, try to use just the Proof
@c General interface, and report any repeatable problems to
@c @code{isabelle@dcs.ed.ac.uk}.

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

The key @kbd{C-c C-b} (@code{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 @emph{not} read, in contrast
with the @code{use_thy} command of Isabelle.

The key @kbd{C-c C-u} (@code{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.

@c TEXI DOCSTRING MAGIC: isa-process-thy-file
@deffn Command isa-process-thy-file file
Process the theory file @var{file}.  If interactive, use @code{buffer-file-name}.
@end deffn

@c TEXI DOCSTRING MAGIC: isa-retract-thy-file
@deffn Command isa-retract-thy-file file
Retract the theory file @var{file}. If interactive, use @code{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.
@end deffn


@node Isabelle specific commands
@section Isabelle specific commands

@cindex Switching to theory files
@kindex C-c C-o

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

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


@c TEXI DOCSTRING MAGIC: thy-find-other-file
@deffn 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 @var{samewindow} is non-nil (interactively, with an optional argument)
the other file replaces the one in the current window.
@end deffn


@node Isabelle customizations
@section Isabelle customizations

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

@c TEXI DOCSTRING MAGIC: isabelle-web-page
@defvar isabelle-web-page 
URL of web page for Isabelle.
@end defvar


@c @unnumberedsubsec Theory file editing customization

@c TEXI DOCSTRING MAGIC: thy-use-sml-mode
@defopt thy-use-sml-mode 
If non-nil, invoke @code{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 @code{sml-mode}, but at the moment there is no way to do this.

The default value is @code{nil}.
@end defopt

@c TEXI DOCSTRING MAGIC: thy-indent-level
@defopt thy-indent-level 
Indentation level for Isabelle theory files.  An integer.

The default value is @code{2}.
@end defopt

@c TEXI DOCSTRING MAGIC: thy-sections
@defvar 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:
@lisp
  @code{thy-insert-header}, @code{thy-insert-class}, @code{thy-insert-default-sort},
  @code{thy-insert-const}, @code{thy-insert-rule}.
@end lisp
The nil template does nothing.
You can add extra sections to theory files by extending this variable.
@end defvar

@c TEXI DOCSTRING MAGIC: thy-template
@defvar thy-template 
Template for theory files.@*
Contains a default selection of sections in a traditional order.
You can use the following format characters:

@samp{%t} --- replaced by theory name.

@samp{%p} --- replaced by names of parents, separated by @samp{+} characters.
@end defvar

@c ideal for above:
@c @defopt thy-template
@c Template for theory files.
@c Contains a default selection of sections in a traditional order.
@c You can use the following format characters:
@c   @code{%t}  -- replaced by theory name
@c   @code{%p}  -- replaced by names of parents, separated by @code{+}'s
@c @end defopt



@c
@c  CHAPTER: HOL Proof General
@c

@node HOL Proof General
@chapter HOL Proof General
@cindex HOL Proof General

HOL Proof General is a "technology demonstration" of Proof General for
HOL98.  This means that only a basic instantiation has been provided,
and that it is not yet supported as a maintained instantiation of Proof
General.  Hopefully somebody from the HOL community is willing to adopt
HOL Proof General and support and improve it.  Please volunteer!  It
needn't be a large or heavy committment.

HOL Proof General may work with variants of HOL other than HOL98, but is
untested.  Probably a few of the settings would need to be changed in a
simple way, to cope with small differences in output between the
systems.  (Please let us know if you modify the HOL98 version for
another variant of HOL).

HOL Proof General has basic script management support, with a little bit
of decoration of scripts and output.  It does not rely on a modified
version of HOL, so the pattern matching may be fragile in certain cases.
Support for multiple files deduces dependencies automatically, so there
is no interaction with the HOL make system yet.

Note that HOL proof scripts often use batch-oriented single step tactic
proofs, but Proof General does not (yet) offer an easy way to edit these
kind of proofs.  They will replay simply as a single step proof and you
will need to convert from the interactive to batch form as usual if you
wish to obtain batch proofs.   Also note that Proof General does not
contain an SML parser, so are problems if you write complex ML in
proof scripts. @xref{ML files}, for the same issue with Isabelle.





@node Adapting Proof General to Other Provers
@chapter 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 @inforef{Style
Tips, ,lispref}.

The configuration variables are declared in the file
@file{generic/proof-config.el}.  The details in the central part of this
chapter are based on the contents of that file, beginning in @ref{Menus
and user-level commands}, and continuing until @ref{Global constants}.
The final sections cover the details of configuring for multiple files
and for supporting the other Emacs packages mentioned in @ref{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.



@menu
* Overview of adding a new prover::            
* Demonstration instance and easy configuration::
* Major modes used by Proof General::  
* Menus and user-level commands::  
* Proof script settings::       
* Proof shell settings::        
* Goals buffer settings::  
* Splash screen settings::      
* Global constants::            
* Handling multiple files::     
* Configuring Font Lock::
* Configuring X-Symbol::
* Writing more lisp code::
@end menu


@node Overview of adding a new prover
@section Overview of adding a new prover

Each proof assistant supported has its own subdirectory under
@code{proof-home-directory}, used to store a root elisp file and any
other files needed to adapt the proof assistant for Proof General.

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

Here is how to go about adding support for a new prover.

@enumerate
@item Make a directory called @file{myassistant/} under the Proof General home
directory @code{proof-home-directory}, to put the specific customization
and associated files in.
@item Add a file @file{myassistant.el} to the new directory.
@item Edit @file{proof-site.el} to add a new entry to the
  @code{proof-assistants-table} variable.  The new entry should look
like this:
@lisp
    (myassistant "My Proof Assistant" "\\.myasst$")
@end lisp    
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 @code{proof-assistant-table} for
more details.
@item Define the new Proof General modes in @file{myassistant.el}, 
 by setting configuration variables to customize the
 behaviour of the generic modes.  
@end enumerate

@c You could begin by setting a minimum number of the variables, then
@c adjust the settings via the customize menus, under Proof-General ->
@c Internals.

@c TEXI DOCSTRING MAGIC: proof-assistant-table
@defopt 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
@lisp
    (@var{symbol} @var{name} @var{automode-regexp})
@end lisp
The @var{name} is a string, naming the proof assistant.
The @var{symbol} is used to form the name of the mode for the
assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp}
are visited.  @var{symbol} is also used to form the name of the
directory and elisp file for the mode, which will be
@lisp
    @var{proof-home-directory}/@var{symbol}/@var{symbol}.el
@end lisp
where @samp{PROOF-HOME-DIRECTORY} is the value of the
variable @code{proof-home-directory}.

The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (plastic "Plastic" "\\.lf$") (hol98 "HOL" "\\.sml$"))}.
@end defopt


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 @code{define-derived-mode}.  Or you can
use the new easy configuration mechanism of Proof General 3.0 described
in the next section, which calls @code{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.


@node Demonstration instance and easy configuration
@section 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 @file{demoisa} for the
two files @file{demoisa.el} and @file{demoisa-easy.el}.

The file @file{demoisa.el} follows the scheme described in @ref{Major
modes used by Proof General}.  It uses the Emacs Lisp macro
@code{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 @file{demoisa-easy.el} uses a new simplified mechanism to
achieve (virtually) the same result.  It uses the macro
@code{proof-easy-config} defined in @file{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 @code{proof-easy-config} is called like this:
@lisp
   (proof-easy-config @var{myprover} "@var{MyProver}"
        @var{config_1} @var{val_1}
        ...
        @var{config_n} @var{val_n})
@end lisp
The main body of the macro call is like the body of a @code{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 @code{proof-assistant-table} for your prover.
@xref{Overview of adding a new prover}.  After the call to
@code{proof-easy-config}, the new modes @code{@var{myprover}-mode},
@code{@var{myprover}-shell-mode}, @code{@var{myprover}-response-mode},
and @code{@var{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 @code{proof-easy-config} call.
For example, to add extra settings for the shell mode for
@code{demoisa}, we could do this:
@lisp
   (defun demoisa-shell-extra-config ()
      @var{extra configuration ...}
    )
   (add-hook 'demoisa-shell-mode-hook 'demoisa-shell-extra-config)
@end lisp
The function to do extra configuration @code{demoisa-shell-extra-config}
is then called as the final step when @code{demoisa-shell-mode} is
entered (be wary, this will be after the generic
@code{proof-shell-config-done} is called, so it will be too late to set
normal configuration variables which may be examined by
@code{proof-shell-config-done}).


@node Major modes used by Proof General
@section 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:
@code{proof-mode}, @code{proof-shell-mode}, @code{proof-response-mode},
and @code{proof-pbp-mode}.

The pattern for defining the major mode for an instance of Proof General
is to use @code{define-derived-mode} to define a specific mode to inherit from
each generic one, like this:
@lisp
(define-derived-mode myass-shell-mode proof-shell-mode
   "MyAss shell" nil
   (myass-shell-config)
   (proof-shell-config-done))
@end lisp
Where @code{myass-shell-config} is a function which sets the
configuration variables for the shell (@pxref{Proof shell settings}).

It's important that your mode invokes one of the functions
 @code{proof-config-done},
 @code{proof-shell-config-done}, 
 @code{proof-response-config-done}, or
 @code{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:
@lisp
  (setq proof-mode-for-script 'myass-mode)
@end lisp
where @code{myass-mode} is your major mode for scripts, derived from
@code{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 @code{pre-shell-start-hook}.  See the file @file{demoisa.el}
for details of how to do this.

@c TEXI DOCSTRING MAGIC: proof-mode-for-script
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-mode-for-shell
@defvar proof-mode-for-shell 
Mode for proof shell buffers.@*
Usually customised for specific prover.
Suggestion: this can be set a function called by @samp{pre-shell-start-hook}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-mode-for-response
@defvar proof-mode-for-response 
Mode for proof response buffer.@*
Usually customised for specific prover.
Suggestion: this can be set a function called by @samp{pre-shell-start-hook}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-mode-for-pbp
@defvar proof-mode-for-pbp 
Mode for proof state display buffers.@*
Usually customised for specific prover.
Suggestion: this can be set a function called by @samp{pre-shell-start-hook}.
@end defvar

@node Menus and user-level commands
@section Menus and user-level commands

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

@c TEXI DOCSTRING MAGIC: proof-assistant-home-page
@defvar proof-assistant-home-page 
Web address for information on proof assistant.@*
Used for Proof General's help menu.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-context-command
@defvar proof-context-command 
Command to display the context in proof assistant.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-info-command
@defvar proof-info-command 
Command to ask for help or information in the proof assistant.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-showproof-command
@defvar proof-showproof-command 
Command to display proof state in proof assistant.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goal-command
@defvar proof-goal-command 
Command to set a goal in the proof assistant.  String or fn.@*
If a string, the format character @samp{%s} will be replaced by the
goal string. 
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-save-command
@defvar proof-save-command 
Command to save a proved theorem in the proof assistant.  String or fn.@*
If a string, the format character @samp{%s} will be replaced by the
theorem name. 
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-find-theorems-command
@defvar proof-find-theorems-command 
Command to search for a theorem containing a given constant. String or fn.@*
If a string, the format character @samp{%s} will be replaced by the
constant name.
If a function, it should return the command string to insert.
@end defvar



@c defgroup proof-script
@node Proof script settings
@section Proof script settings

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

@c TEXI DOCSTRING MAGIC: proof-terminal-char
@defvar proof-terminal-char 
Character which terminates a command in a script buffer.@*
You must set this variable in script mode configuration.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-comment-start
@defvar proof-comment-start 
String which starts a comment in the proof assistant command language.@*
The script buffer's @code{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 @samp{@code{proof-comment-end}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-comment-end
@defvar proof-comment-end 
String which ends a comment in the proof assistant command language.@*
The script buffer's @code{comment-end} is set to this string plus a space.
See also @samp{@code{proof-comment-start}}.

You should set this variable for reliable working of Proof General,
@end defvar
@c TEXI DOCSTRING MAGIC: proof-case-fold-search
@defvar proof-case-fold-search 
Value for @code{case-fold-search} when recognizing portions of proof scripts.@*
The default value is @code{'nil'}.  If your prover has a case @strong{insensitive}
input syntax, @code{proof-case-fold-search} should be set to @code{'t'} instead.  
NB: This setting is not used for matching output from the prover.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-save-command-regexp
@defvar proof-save-command-regexp 
Matches a save command.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp
@defvar 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
@code{function-menu} configuration in @code{proof-script-find-next-entity}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goal-command-regexp
@defvar proof-goal-command-regexp 
Matches a goal command in the proof script.   Must be set.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp
@defvar 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
@code{function-menu} configuration in @code{proof-script-find-next-entity}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-non-undoables-regexp
@defvar proof-non-undoables-regexp 
Regular expression matching commands which are @strong{not} undoable.@*
Used in default functions @samp{@code{proof-generic-state-preserving-p}} 
and @samp{@code{proof-generic-count-undos}}.  If you don't use those,
May be left as nil.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-ignore-for-undo-count
@defvar 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
@samp{@code{proof-non-undoables-regexp}}.
Used in default function @samp{@code{proof-generic-count-undos}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps
@defvar proof-script-next-entity-regexps 
Regular expressions to help find definitions and proofs in a script.@*
This is the list of the form
@lisp
   (@var{anyentity-regexp}
    @var{discriminator-regexp}  ... @var{discriminator-regexp})
@end lisp
The idea is that @var{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
@var{discriminator-regexp} has one of the forms
@lisp
  (@var{regexp} @var{matchno}) 
  (@var{regexp} @var{matchno} @code{'backward} @var{backregexp}) 
  (@var{regexp} @var{matchno} @code{'forward} @var{forwardregexp})
@end lisp
If @var{regexp} matches the string captured by @var{anyentity-regexp}, then
@var{matchno} is the match number for the substring which names the entity.

If @code{'backward} @var{backregexp} is present, then the start of the entity
is found by searching backwards for @var{backregexp}.

Conversely, if @code{'forward} @var{forwardregexp} is found, then the end of
the entity is found by searching forwards for @var{forwardregexp}.

Otherwise, the start and end of the entity will be the region matched
by @var{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 @code{proof-goal-with-hole-regexp},
@code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-find-next-entity-fn
@defvar proof-script-find-next-entity-fn 
Name of function to find next interesting entity in a script buffer.@*
This is used to configure @code{func-menu}.  The default value is
@code{proof-script-find-next-entity}, which searches for the next entity
based on fume-function-name-regexp which by default is set from
@code{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 @code{proof-script-next-entity-regexps} is set to a default value
from @code{proof-goal-with-hole-regexp} and @code{proof-save-with-hole-regexp} in
the function @code{proof-config-done}, so you may not need to worry about any
of this.  See whether function menu does something sensible by
default.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-goal-command-p

@defvar proof-goal-command-p 
A function to test: is this really a goal command?
@end defvar
@c TEXI DOCSTRING MAGIC: proof-completed-proof-behaviour
@defvar 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:
@lisp
        nil  -  nothing special; close only when a save arrives
  @code{'closeany}  -  close as soon as the next command arrives, save or not
 @code{'closegoal}  -  close when the next "goal" command arrives
    @code{'extend}  -  keep extending the closed region until a save or goal.
@end lisp
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 @code{proof-lift-global} mechanism.  (Of course, this is risky in case of
nested contexts!)
@end defvar
 
@c TEXI DOCSTRING MAGIC: proof-lift-global
@defvar 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 @samp{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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-count-undos-fn
@defvar 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 @samp{@code{proof-generic-count-undos}} is based on the
settings @samp{@code{proof-non-undoables-regexp}} and
@samp{@code{proof-non-undoables-regexp}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-generic-count-undos
@defun proof-generic-count-undos span
Count number of undos in a span, return command needed to undo that far.@*
Command is set using @samp{@code{proof-undo-n-times-cmd}}.

A default value for @samp{@code{proof-count-undos-fn}}.

For this function to work properly, you must configure
@samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}.
@end defun
@c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn
@defvar 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 (@code{proof-locked-end}).  This may involve forgetting a number
of definitions, declarations, or whatever.

The special string @code{proof-no-command} means there is nothing to do.

Important: the generic implementation @samp{@code{proof-generic-find-and-forget}}
does nothing, it always returns @samp{@code{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 @samp{@code{proof-generic-find-and-forget}}
(which see).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-generic-find-and-forget

@defun proof-generic-find-and-forget span
Calculate a forget/undo command to forget back to @var{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.

@var{currently} @var{unimplemented}: just returns @code{proof-no-command}.
Check the @code{lego-find-and-forget} or @code{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.
@end defun
@c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn
@defvar 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, @code{'goal'} or @code{'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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-kill-goal-command
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-global-p
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-state-preserving-p
@defvar proof-state-preserving-p 
A predicate, non-nil if its argument (a command) preserves the proof state.@*
If set, used by @code{proof-minibuffer-cmd} to filter out scripting
commands which should be entered directly into the script itself.

The default setting for this function, @samp{@code{proof-generic-state-preserving-p}}
tests by negating the match on @samp{@code{proof-non-undoables-regexp}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-generic-state-preserving-p

@defun proof-generic-state-preserving-p cmd
Is @var{cmd} state preserving?  Match on @code{proof-non-undoables-regexp}.
@end defun
@c TEXI DOCSTRING MAGIC: proof-activate-scripting-hook
@defvar 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
@samp{activated-interactively} will be non-nil if 
@code{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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-stack-to-indent
@defvar proof-stack-to-indent 
Prover-specific code for indentation.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-parse-indent
@defvar proof-parse-indent 
Proof-assistant specific function for parsing.@*
Invoked in @samp{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 @samp{c} is a character
representing the type of indentation and @samp{p} records the column for
indentation. The generic @samp{proof-parse-to-point} function supports
parentheses and commands. It represents these with the characters
@samp{?(}, @samp{?[} and @samp{@code{proof-terminal-char}}. 
@end defvar

@xref{Handling multiple files}, for more details about the final
setting in this group.

@c TEXI DOCSTRING MAGIC: proof-auto-multiple-files
@defvar 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.
@end defvar



@node Proof shell settings
@section 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 @code{proof-shell}.

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

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

@menu
* Proof shell commands::        
* Settings for matching output from proof process::  
* Hooks and other settings::  
@end menu

@node Proof shell commands
@subsection Commands

@c TEXI DOCSTRING MAGIC: proof-prog-name
@defvar proof-prog-name 
System command to run the proof assistant in the proof shell.@*
Suggestion: this can be set in @code{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).
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-init-cmd
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd
@defvar proof-shell-restart-cmd 
A command for re-initialising the proof process.@*
The @code{proof-terminal-char} is added on to the end.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd
@defvar proof-shell-quit-cmd 
A command to quit the proof process.  If nil, send EOF instead.@*
The @code{proof-terminal-char} is added on to the end.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-quit-timeout
@defvar proof-shell-quit-timeout 
The number of seconds to wait after sending @code{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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd
@defvar proof-shell-cd-cmd 
Command to the proof assistant to change the working directory.@*
The format character @samp{%s} is replaced with the directory, and the
@code{proof-terminal-char} is added on to the end.  The escape sequences
in @samp{@code{proof-shell-filename-escapes}} are applied to the filename.

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

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

@xref{Handling multiple files},
for more details about the final two settings in this group,


@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-processed-cmd
@defvar proof-shell-inform-file-processed-cmd 
Command to the proof assistant to tell it that a file has been processed.@*
The format character @samp{%s} is replaced by a complete filename for a
script file which has been fully processed interactively with
Proof General.  The escape sequences in @samp{@code{proof-shell-filename-escapes}} 
are applied to the filename.

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: @code{proof-shell-inform-file-retracted-cmd}, 
@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd
@defvar proof-shell-inform-file-retracted-cmd 
Command to the proof assistant to tell it that a file has been retracted.@*
The format character @samp{%s} is replaced by a complete filename for a
script file which Proof General wants the prover to consider
as not completely processed. The escape sequences
in @samp{@code{proof-shell-filename-escapes}} are applied to the filename.

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: @code{proof-shell-inform-file-processed-cmd}, 
@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
@end defvar


@node Settings for matching output from proof process
@subsection Settings for matching output from proof process
@c TEXI DOCSTRING MAGIC: proof-shell-wakeup-char
@defvar proof-shell-wakeup-char 
A special character which terminates an annotated prompt.@*
Set to nil if proof assistant does not support annotated prompts.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-first-special-char
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-prompt-pattern
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp
@defvar 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 @code{proof-shell-wakeup-char}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-abort-goal-regexp
@defvar proof-shell-abort-goal-regexp 
Regexp matching output from an aborted proof.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-error-regexp
@defvar 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 @code{proof-shell-eager-annotation-start}) otherwise it
will be lost.

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

The engine matches interrupts before errors, see @code{proof-shell-interrupt-regexp}.

It is safe to leave this variable unset (as nil).
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp
@defvar 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 @code{proof-shell-eager-annotation-start}) otherwise it
will be lost.

The engine matches interrupts before errors, see @code{proof-shell-error-regexp}.

It is safe to leave this variable unset (as nil).
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp
@defvar proof-shell-start-goals-regexp 
Regexp matching the start of the proof state output.@*
This is an important setting.  Output between @samp{@code{proof-shell-start-goals-regexp}}
and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer
and possibly analysed further for proof-by-pointing markup.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp
@defvar 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 @code{proof-shell-start-goals-regexp}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start
@defvar 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 @samp{@code{proof-shell-eager-annotation-start-length}},
@samp{@code{proof-shell-eager-annotation-end}}.

Set to nil to disable this feature.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp
@defvar 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 @samp{@code{proof-goal-hyp-fn}},
used to help parse the goals buffer to annotate it for proof by pointing.
@end defvar


@node Hooks and other settings
@subsection Hooks and other settings

@c TEXI DOCSTRING MAGIC: proof-shell-filename-escapes
@defvar proof-shell-filename-escapes 
A list of escapes that are applied to %s for filenames.@*
A list of cons cells, car of which is string to be replaced
by the cdr.
For example, when directories are sent to Isabelle, HOL, and Coq,
they appear inside ML strings and the backslash character and
quote characters must be escaped.  The setting
@lisp
  '(("@var{\\\\}" . "@var{\\\\}")
    ("\"" . "\\\""))
@end lisp
achieves this.   This does not apply to @var{lego}, which does not
need backslash escapes and does not allow filenames with
quote characters.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type
@defvar proof-shell-process-connection-type 
The value of @code{process-connection-type} for the proof shell.@*
Set non-nil for ptys, nil for pipes.
The default (and preferred) option is to use pty communication.
However there is a long-standing backslash/long line problem with
Solaris which gives a mess of ^G characters when some input is sent
which has a  in the 256th position.   
So we select pipes by default if it seems like we're on Solaris.
We do not force pipes everywhere because this risks loss of data.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-pre-shell-start-hook
@defvar 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: 
@lisp
   @code{proof-prog-name}
   @code{proof-mode-for-shell}
   @code{proof-mode-for-response}
   @code{proof-mode-for-pbp}
@end lisp
This is the bare minimum needed to get a shell buffer and
its friends configured in the function @code{proof-shell-start}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-insert-hook
@defvar proof-shell-insert-hook 
Hooks run by @code{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 @code{save-excursion} with the @code{proof-shell-buffer} 
current, just before inserting and sending the text in the 
variable @samp{string}.  The hook can massage @samp{string} or insert additional 
text directly into the @code{proof-shell-buffer}.  
Before sending @samp{string}, it will be stripped of carriage returns.

Additionally, the hook can examine the variable @samp{action}.  It will be
a symbol, set to the callback command which is executed in the proof
shell filter once @samp{string} has been processed.  The @samp{action} variable
suggests what class of command is about to be inserted:
@lisp
 @code{'proof-done-invisible}       A non-scripting command
 @code{'proof-done-advancing}       A "forward" scripting command
 @code{'proof-done-retracting}      A "backward" scripting command
@end lisp
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
@samp{string} may be safer than inserting text directly, since it is
stripped of carriage returns before being sent.

Example uses:
@var{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 @samp{string}. 
The x-symbol support uses this hook to convert special characters
into tokens for the proof assistant.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook
@defvar proof-shell-handle-error-or-interrupt-hook 
Run after an error or interrupt has been reported in the response buffer.@*
Hook functions may inspect @samp{@code{proof-shell-error-or-interrupt-seen}} to 
determine whether the cause was an error or interrupt.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook
@defvar proof-shell-pre-interrupt-hook 
Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@*
This hook is added to allow customization for Poly/ML and other
systems where the system queries the user before returning to
the top level.  For Poly/ML it can be used to send the string "f",
for example.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-process-output-system-specific
@defvar 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 @samp{@code{proof-shell-process-output}}.
All other output from the proof engine is simply reported to the
user in the @var{response} buffer.

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


@xref{Handling multiple files}, for more details about the final three
settings in this section.

@vindex proof-included-files-list
@c TEXI DOCSTRING MAGIC: proof-shell-process-file
@defvar proof-shell-process-file 
A pair (@var{regexp} . @var{function}) to match a processed file name.

If @var{regexp} matches output, then the function @var{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, @var{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, @var{function} needs to
reconstruct the corresponding script file name. The new (true) file
name is added to the front of @samp{@code{proof-included-files-list}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp
@defvar 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
@samp{@code{proof-shell-compute-new-files-list}}.
@end defvar
@vindex proof-included-files-list
@c TEXI DOCSTRING MAGIC: proof-shell-compute-new-files-list
@defvar proof-shell-compute-new-files-list 
Function to update @samp{proof-included-files list}.

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




@node Goals buffer settings
@section Goals buffer settings

The goals buffer settings allow configuration of Proof General for proof
by pointing or similar features.
@c At the moment these settings are disabled.

@c TEXI DOCSTRING MAGIC: pbp-change-goal
@defvar pbp-change-goal 
Command to change to the goal @samp{%s}
@end defvar
@c TEXI DOCSTRING MAGIC: pbp-goal-command
@defvar pbp-goal-command 
Command informing the prover that @samp{@code{pbp-button-action}} has been@*
requested on a goal.
@end defvar
@c TEXI DOCSTRING MAGIC: pbp-hyp-command
@defvar pbp-hyp-command 
Command informing the prover that @samp{@code{pbp-button-action}} has been@*
requested on an assumption.
@end defvar
@c TEXI DOCSTRING MAGIC: pbp-error-regexp
@defvar pbp-error-regexp 
Regexp indicating that the proof process has identified an error.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-result-start
@defvar proof-shell-result-start 
Regexp matching start of an output from the prover after pbp commands.@*
In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-result-end
@defvar proof-shell-result-end 
Regexp matching end of output from the prover after pbp commands.@*
In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-start-char
@defvar proof-shell-start-char 
Starting special for a subterm markup.@*
Subsequent characters with values @strong{below} @code{proof-shell-first-special-char}
are assumed to be subterm position indicators.  Subterm markups should
be finished with @code{proof-shell-end-char}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-end-char
@defvar proof-shell-end-char 
Finishing special for a subterm markup.@*
See documentation of @code{proof-shell-start-char}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-goal-char
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-field-char
@defvar proof-shell-field-char 
Annotated field end
@end defvar


@node Splash screen settings
@section Splash screen settings

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

@c TEXI DOCSTRING MAGIC: proof-splash-time
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-splash-contents
@defvar 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.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-splash-extensions
@defvar proof-splash-extensions 
Prover specific extensions of splash screen.@*
These are evaluated and appended to @samp{@code{proof-splash-contents}}.
@end defvar






@node Global constants
@section 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.

@c TEXI DOCSTRING MAGIC: proof-general-name
@defvar proof-general-name 
Proof General name used internally and in menu titles.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-general-home-page
@defopt proof-general-home-page 
Web address for Proof General

The default value is @code{"http://www.lfcs.informatics.ed.ac.uk/proofgen"}.
@end defopt
@c TEXI DOCSTRING MAGIC: proof-universal-keys
@defvar proof-universal-keys 
List of key-bindings made for the script, goals and response buffer. @*
Elements of the list are tuples @samp{(k . f)} 
where @samp{k} is a @code{key-binding} (vector) and @samp{f} the designated function.
@end defvar



@node Handling multiple files
@section Handling multiple files
@cindex 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 @ref{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 @code{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 @code{proof-strict-read-only} allows it).


@c TEXI DOCSTRING MAGIC: proof-included-files-list
@defvar proof-included-files-list 
List of files currently included in proof process.@*
This list contains files in canonical truename format
(see @samp{@code{file-truename}}).

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

Only files which have been @strong{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.
@end defvar

The way that @code{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).

@vindex proof-shell-process-file
@vindex proof-shell-retract-files-regexp
@vindex proof-shell-compute-new-files-list

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 @code{foo} has been processed'') --- see
@code{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 @code{foo} has been undone'') -- see
@code{proof-shell-retract-files-regexp}.  (The function
@code{proof-shell-compute-new-files-list} should be set to calculate the
new value for @code{proof-included-files-list} after a retract message
has been seen).


@c The key idea is that we leave it to the specific proof assistant to
@c worry about managing multiple files, as far as possible.  Whenever the
@c proof assistant processes or retracts a file it must clearly say so, so
@c that Proof General can register this.

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
@code{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
@code{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
@code{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
@code{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.

@vindex proof-shell-eager-annotation-start
@vindex proof-shell-eager-annotation-end
Finally, we should mention how Proof General recognizes file processing
messages from the proof assistant.  Proof General considers @var{output}
delimited by the the two regular expressions
@code{proof-shell-eager-annotation-start} and
@code{proof-shell-eager-annotation-end} as being important. It displays
the @var{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,
@code{proof-shell-process-file}.  To recognize messages about file
undoing, @code{proof-shell-retract-files-regexp} and
@code{proof-shell-compute-new-files-list}.  @xref{Hooks and other
settings}.  To tell the prover about files handled with script
management, use
 @code{proof-shell-inform-file-processed-cmd} and
 @code{proof-shell-inform-file-retracted-cmd}.  @xref{Proof shell
 commands}.  Finally, set the flag @code{proof-auto-multiple-files} 
for a automatic approximation to multiple file handling.
@xref{Proof script settings}.


@node Configuring Font Lock
@section Configuring Font Lock
@cindex font lock

Support for Font Lock in Proof General was mentioned earlier
(@pxref{Syntax highlighting}).  To configure Font Lock for a new proof
assistant, you need to set the variable @code{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.

@c nope: too big. TEXI DOCSTRING MAGIC: font-lock-keywords
To understand its format, check the documentation of
@code{font-lock-keywords} inside Emacs.

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


@c TEXI DOCSTRING MAGIC: proof-font-lock-zap-commas
@defvar 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 @samp{[} and @samp{]}, 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.

@var{lego} and Coq enable it by tradition.
@end defvar




@node Configuring X-Symbol
@section Configuring X-Symbol
@cindex X-Symbol

The X-Symbol package was mentioned earlier (@pxref{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 @i{token language} for your proof
assistant.  If your assistant is stored in the subdirectory
@var{myprover}, the token language will be called @var{myprover} and be
defined in a file @file{x-symbol-@var{myprover}.el} which is
automatically loaded by X-Symbol.  The name of the token language mode
will be @code{@var{myprover}sym}.

Proof General will check that the file @file{x-symbol-@var{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
@file{@var{myprover}.el}.  These settings are optional.

@c There's also proof-xsym-font-lock-keywords, but I don't 
@c really know what this setting is good for.

@c TEXI DOCSTRING MAGIC: proof-xsym-activate-command
@defvar 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.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-xsym-deactivate-command
@defvar 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.
@end defvar

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
@code{proof-xsym-extra-modes}.

@c TEXI DOCSTRING MAGIC: proof-xsym-extra-modes
@defvar 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).
@end defvar



@node Writing more lisp code
@section 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:

@itemize @bullet
@item Any of the interactive commands (i.e. anything you
 can invoke with @kbd{M-x}, including all key-bindings)
@item The function @code{proof-shell-invisible-command} documented below.
@end itemize

This function @code{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.

@c TEXI DOCSTRING MAGIC: proof-shell-invisible-command
@defun proof-shell-invisible-command cmd &optional wait
Send @var{cmd} to the proof process.  Add terminal string if necessary.@*
By default, let the command be processed asynchronously.
But if optional @var{wait} command is non-nil, wait for processing to finish
before and after sending the command.
If @var{wait} is an integer, wait for that many seconds afterwards.
@end defun

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

@c TEXI DOCSTRING MAGIC: proof-define-assistant-command
@deffn Macro proof-define-assistant-command 
Define command FN to send string @var{body} to proof assistant, based on @var{cmdvar}.@*
@var{body} defaults to @var{cmdvar}, a variable.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-define-assistant-command-witharg
@deffn Macro proof-define-assistant-command-witharg 
Define command FN to prompt for string @var{cmdvar} to proof assistant.@*
@var{cmdvar} is a function or string.  Automatically has history.
@end deffn




@node Internals of Proof General
@chapter 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 @kbd{C-h v} and @kbd{C-h f}.

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

@menu
* Spans::                       
* User option conventions::
* Proof General site configuration::  
* Global variables::            
* Proof script mode::           
* Proof shell mode::            
* Debugging::
@end menu



@node Spans
@section Spans
@cindex spans
@cindex extents
@cindex overlays

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

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

@node Proof General site configuration
@section Proof General site configuration
@cindex installation directories
@cindex site configuration

The file @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
@code{proof-home-directory} to the directory that @file{proof-site.el}
is located in, or to the variable of the environment variable
@code{PROOFGENERAL_HOME} if that is set.

@c TEXI DOCSTRING MAGIC: proof-home-directory
@defvar proof-home-directory 
Directory where Proof General is installed. Ends with slash.@*
Default value taken from environment variable @samp{PROOFGENERAL_HOME} if set, 
otherwise based on where the file @samp{proof-site.el} was loaded from.
You can use customize to set this variable.
@end defvar

@c They're no longer options.
@c The default value for @code{proof-home-directory} mentioned above is the
@c one for the author's system, it won't be the same for you!

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
@code{proof-home-directory} root.

@c TEXI DOCSTRING MAGIC: proof-images-directory
@defvar proof-images-directory 
Where Proof General image files are installed. Ends with slash.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-info-directory
@defvar proof-info-directory 
Where Proof General Info files are installed. Ends with slash.
@end defvar



@cindex mode stub
After defining these settings, we define a @dfn{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 @code{proof-assistants} setting.

@c TEXI DOCSTRING MAGIC: proof-assistants
@defopt proof-assistants 
Choice of proof assistants to use with Proof General.@*
A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'plastic} @code{'hol98}.
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 @samp{proof-site.el} is loaded, or by setting
the environment variable @samp{PROOFGENERAL_ASSISTANTS} to the
symbols you want, for example "lego isa".  Or you can
edit the file @samp{proof-site.el} itself.

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

The default value is @code{(demoisa isar isa lego coq plastic hol98)}.
@end defopt

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

@c TEXI DOCSTRING MAGIC: proof-general-version
@defvar proof-general-version 
Version string identifying Proof General release.
@end defvar



@node User option conventions
@section User option conventions
@cindex conventions
@cindex user options

The file @file{proof-config.el} defines the configuration variables for
Proof General, including user options.  @xref{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 @code{defcustom} as usual, but have
`@code{*}' as the first character of their docstrings (standard Emacs
convention).  Also, they live in the customize group
@code{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 @code{custom-set}
property for the variable to the function @code{proof-set-value} which
does an ordinary @code{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 @code{proof-set-value} mechanism.  They are controlled by
boolean variables with names like @code{proof-@var{foo}-enable}, and
appear at the start of the customize group @code{proof-user-options}.
They should be edited by the user through the customization mechanism,
and set in the code using @code{customize-set-variable}.

In @code{proof.el} there is a handy macro,
@code{proof-customize-toggle}, which constructs an interactive function
for toggling boolean customize settings.  We can use this to make an
interactive function @code{proof-@var{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 @code{customize} mechanism.

@c TEXI DOCSTRING MAGIC: proof-set-value
@defun proof-set-value sym value
Set a customize variable using @code{set-default} and a function.@*
We first call @samp{@code{set-default}} to set @var{sym} to @var{value}.
Then if there is a function @var{sym} (i.e. with the same name as the
variable @var{sym}), it is called to take some dynamic action for the new
setting.
@end defun

@c TEXI DOCSTRING MAGIC: proof-customize-toggle
@deffn Macro proof-customize-toggle 
Make a function for toggling a boolean customize setting VAR.@*
The toggle function uses @code{customize-set-variable} to change the variable.
@end deffn
@node Global variables
@section Global variables

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

@c TEXI DOCSTRING MAGIC: proof-script-buffer
@defvar proof-script-buffer 
The currently active scripting buffer or nil if none.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-buffer
@defvar proof-shell-buffer 
Process buffer where the proof assistant is run.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-response-buffer


@defvar proof-response-buffer 
The response buffer.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goals-buffer
@defvar proof-goals-buffer 
The goals buffer (also known as the pbp buffer).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-buffer-type
@defvar proof-buffer-type 
Symbol indicating the type of this buffer: @code{'script}, @code{'shell}, @code{'pbp}, or @code{'response}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-included-files-list
@defvar proof-included-files-list 
List of files currently included in proof process.@*
This list contains files in canonical truename format
(see @samp{@code{file-truename}}).

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

Only files which have been @strong{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.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed
@defvar 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).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-error-or-interrupt-seen
@defvar proof-shell-error-or-interrupt-seen 
Flag indicating that an error or interrupt has just occurred.@*
Set to @code{'error} or @code{'interrupt} if one was observed from the proof 
assistant during the last group of commands.
@end defvar


@node Proof script mode
@section Proof script mode

The file @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).

@c TEXI DOCSTRING MAGIC: proof-locked-span
@defvar 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.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-queue-span
@defvar proof-queue-span 
The queue span of the buffer.  May be detached if inactive or empty.
@end defvar

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

@c TEXI DOCSTRING MAGIC: proof-init-segmentation
@defun 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.
@end defun

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

@c TEXI DOCSTRING MAGIC: proof-complete-buffer-atomic
@defun proof-complete-buffer-atomic buffer
Make sure @var{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.
@end defun

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

@c TEXI DOCSTRING MAGIC: proof-register-possibly-new-processed-file
@defun proof-register-possibly-new-processed-file file &optional informprover
Register a possibly new @var{file} as having been processed by the prover.@*
If @var{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.
@end defun

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
@code{proof-included-files-list}.

@c TEXI DOCSTRING MAGIC: proof-activate-scripting
@deffn 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 @samp{@code{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 @samp{@code{proof-query-file-save-when-activating-scripting}} is set
and provided the optional argument @var{nosaves} is non-nil.

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

Finally, the hooks @samp{@code{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 @samp{@code{proof-shell-invisible-command}})
which result in an error, the activation is considered to
have failed and an error is given.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-deactivate-scripting
@deffn Command proof-deactivate-scripting &optional forcedaction
Deactivate scripting for the active scripting buffer.

Set @code{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 @samp{@code{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
@samp{@code{proof-included-files-list}}.  Conversely, if it is (or has become)
empty, we make sure that it is @strong{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 @code{proof-script-buffer} is nil afterwards.

The optional argument @var{forcedaction} overrides the user option
@samp{@code{proof-auto-action-when-deactivating-scripting}} and prevents
questioning the user.  It is used to make a value for
the @code{kill-buffer-hook} for scripting buffers, so that when
a scripting buffer is killed it is always retracted.
@end deffn

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

@c TEXI DOCSTRING MAGIC: proof-segment-up-to
@defun proof-segment-up-to pos &optional next-command-end
Create a list of (type, int, string) tuples from end of queue/locked region to @var{pos}.@*
Each tuple denotes the command and the position of its terminator,
type is one of @code{'comment}, or @code{'cmd}. @code{'unclosed-comment} may be consed onto
the start if the segment finishes with an unclosed comment.
If optional @var{next-command-end} is non-nil, we contine past @var{pos} until
the next command end.
@end defun

The function @code{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.

@c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas
@defun proof-semis-to-vanillas semis &optional callback-fn
Convert a sequence of terminator positions to a set of vanilla extents.@*
Proof terminator positions @var{semis} has the form returned by
the function @code{proof-segment-up-to}.
Set the callback to @var{callback-fn} or @code{'proof-done-advancing} by default.
@end defun

The function @code{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 @code{proof-segment-up-to (point)},
hence all the different options when we've done so.

@c TEXI DOCSTRING MAGIC: proof-assert-until-point
@defun 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
@var{unclosed-comment-fun}. If @var{ignore-proof-process-p} is set, no commands
will be added to the queue and the buffer will not be activated for
scripting.
@end defun

@code{proof-assert-next-command} is a variant of this function.

@c TEXI DOCSTRING MAGIC: proof-assert-next-command
@deffn 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 @var{unclosed-comment-fun}. 
If @var{ignore-proof-process-p} is set, no commands will be added to the queue.
Afterwards, move forward to near the next command afterwards, unless
@var{dont-move-forward} is non-nil.  If @var{for-new-command} is non-nil,
a space or newline will be inserted automatically.
@end deffn

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

@c TEXI DOCSTRING MAGIC: proof-retract-until-point
@defun 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 
@samp{@code{proof-done-retracting}} after the proof process has successfully 
reset its state.
If @var{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.
@end defun

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

@c TEXI DOCSTRING MAGIC: proof-restart-buffers
@defun proof-restart-buffers buffers
Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@*
No effect on a buffer which is nil or killed.  If one of the buffers
is the current scripting buffer, then @code{proof-script-buffer} 
will deactivated.
@end defun

@c TEXI DOCSTRING MAGIC: proof-script-remove-all-spans-and-deactivate
@defun proof-script-remove-all-spans-and-deactivate 
Remove all spans from scripting buffers via @code{proof-restart-buffers}.
@end defun


@c
@c SECTION: Proof Shell Mode
@c
@node Proof shell mode
@section Proof shell mode
@cindex proof shell mode
@cindex comint-mode

The proof shell mode code is in the file @file{proof-shell.el}.  Proof
shell mode is defined to inherit from @code{comint-mode} using
@code{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.

@c TEXI DOCSTRING MAGIC: proof-shell-busy
@defvar proof-shell-busy 
A lock indicating that the proof shell is processing.@*
When this is non-nil, @code{proof-shell-ready-prover} will give
an error.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-marker
@defvar proof-marker 
Marker in proof shell buffer pointing to previous command input.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-action-list
@defvar proof-action-list 
A list of@*
@lisp
  (@var{span} @var{command} @var{action})
@end lisp
triples, which is a queue of things to do.
See the functions @samp{@code{proof-start-queue}} and @samp{proof-exec-loop}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-analyse-using-stack
@defvar 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 @var{lego} 1.3.1 use @samp{nil}, for Coq 6.2, use @samp{t}.
@end defvar


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

@c TEXI DOCSTRING MAGIC: proof-shell-start
@deffn 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.
@end deffn

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

@c TEXI DOCSTRING MAGIC: proof-shell-kill-function
@defun 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 @code{kill-buffer-hook} in shell buffer.
Also called by @code{proof-shell-bail-out} if the process is
exited by hand (or exits by itself).
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-exit
@deffn Command proof-shell-exit 
Query the user and exit the proof process.

This simply kills the @code{proof-shell-buffer} relying on the hook function
@code{proof-shell-kill-function} to do the hard work.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-shell-bail-out
@defun proof-shell-bail-out process event
Value for the process sentinel for the proof assistant process.@*
If the proof assistant dies, run @code{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.
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-restart
@deffn Command proof-shell-restart 
Clear script buffers and send @code{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
@code{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).
@end deffn

@c
@c INPUT
@c
@subsection Input to the shell

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

@c TEXI DOCSTRING MAGIC: proof-start-queue
@defun proof-start-queue start end alist
Begin processing a queue of commands in @var{alist}.@*
If @var{start} is non-nil, @var{start} and @var{end} are buffer positions in the
active scripting buffer for the queue region.

This function calls @samp{@code{proof-append-alist}}.
@end defun

@c TEXI DOCSTRING MAGIC: proof-append-alist

@defun proof-append-alist alist &optional queuemode
Chop off the vacuous prefix of the command queue @var{alist} and queue it.@*
For each @samp{@code{proof-no-command}} item at the head of the list, invoke its 
callback and remove it from the list.

Append the result onto @samp{@code{proof-action-list}}, and if the proof 
shell isn't already busy, grab the lock with @var{queuemode} and
start processing the queue.

If the proof shell is busy when this function is called,
then @var{queuemode} must match the mode of the queue currently
being processed.
@end defun
@vindex proof-action-list
@c TEXI DOCSTRING MAGIC: proof-shell-exec-loop
@defun proof-shell-exec-loop 
Process the @code{proof-action-list}.

@samp{@code{proof-action-list}} contains a list of (@var{span} @var{command} @var{action}) triples.

If this function is called with a non-empty @code{proof-action-list}, the
head of the list is the previously executed command which succeeded.
We execute (@var{action} @var{span}) on the first item, then (@var{action} @var{span}) on any
following items which have @code{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.
@end defun

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

@c TEXI DOCSTRING MAGIC: proof-shell-insert
@defun proof-shell-insert string action
Insert @var{string} at the end of the proof shell, call @code{comint-send-input}.

First call @code{proof-shell-insert-hook}.  The argument @var{action} may be
examined by the hook to determine how to process the @var{string} variable.

Then strip @var{string} of carriage returns before inserting it and updating
@code{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 @code{proof-append-alist} when we start processing a queue, and in
@code{proof-shell-exec-loop}, to process the next item.
@end defun


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.


@c TEXI DOCSTRING MAGIC: proof-grab-lock

@defun proof-grab-lock &optional queuemode
Grab the proof shell lock, starting the proof assistant if need be.@*
Runs @code{proof-state-change-hook} to notify state change.
Clears the @code{proof-shell-error-or-interrupt-seen} flag.
If @var{queuemode} is supplied, set the lock to that value.
@end defun
@c TEXI DOCSTRING MAGIC: proof-release-lock







@defun proof-release-lock &optional err-or-int
Release the proof shell lock, with error or interrupt flag @var{err-or-int}.@*
Clear @code{proof-shell-busy}, and set @code{proof-shell-error-or-interrupt-seen}
to err-or-int.
@end defun
@c
@c OUTPUT
@c
@subsection Output from the shell

Two main functions deal with output, @code{proof-shell-process-output}
and @code{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 @code{proof-shell-urgent-message-marker} tracks
the last urgent message seen.

@vindex proof-action-list
@c TEXI DOCSTRING MAGIC: proof-shell-process-output
@defun proof-shell-process-output cmd string
Process shell output (resulting from @var{cmd}) by matching on @var{string}.@*
@var{cmd} is the first part of the @code{proof-action-list} that lead to this
output.  The result of this function is a pair (@var{symbol} @var{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
@lisp
  @code{proof-shell-interrupt-regexp}
  @code{proof-shell-error-regexp}
  @code{proof-shell-abort-goal-regexp}
  @code{proof-shell-proof-completed-regexp}
  @code{proof-shell-result-start}
@end lisp
All other output from the proof engine will be reported to the user in
the response buffer by setting @code{proof-shell-delayed-output} to a cons
cell of ('insert . @var{text}) where @var{text} is the text string to be inserted.

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

To extend this function, set @code{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
@code{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: @code{'error},
@code{'interrupt}, @code{'loopback}, or nil. @code{'loopback} means this was output from
pbp, and should be inserted into the script buffer and sent back to
the proof assistant.
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker
@defvar proof-shell-urgent-message-marker 
Marker in proof shell buffer pointing to end of last urgent message.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message
@defun proof-shell-process-urgent-message message
Analyse urgent @var{message} for various cases.@*
Cases are: included file, retracted file, cleared response buffer, or
if none of these apply, display it.
@var{message} should be a string annotated with 
@code{proof-shell-eager-annotation-start}, @code{proof-shell-eager-annotation-end}.
@end defun

The main processing point which triggers other actions is
@code{proof-shell-filter}.

@c TEXI DOCSTRING MAGIC: proof-shell-filter
@defun proof-shell-filter str
Filter for the proof assistant shell-process.@*
A function for @code{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 @samp{@code{proof-shell-process-urgent-messages}}.

Otherwise wait until an annotated prompt appears in the input.  
If @code{proof-shell-wakeup-char} is set, wait until we see that in the
output chunk @var{str}.  This optimizes the filter a little bit.

If a prompt is seen, run @code{proof-shell-process-output} on the output
between the new prompt and the last input (position of @code{proof-marker})
or the last urgent message (position of
@code{proof-shell-urgent-message-marker}), whichever is later.  
For example, in this case:
@lisp
 PROMPT> @var{input}
 @var{output-1}
 @var{urgent-message}
 @var{output-2}
 PROMPT>
@end lisp
@code{proof-marker} is set after @var{input} by @code{proof-shell-insert} and
@code{proof-shell-urgent-message-marker} is set after @var{urgent-message}.
Only @var{output-2} will be processed.  For this reason, error
messages and interrupt messages should @strong{not} be considered
urgent messages.

Output is processed using @code{proof-shell-filter-process-output}.

The first time that a prompt is seen, @code{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).
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-filter-process-output
@defun proof-shell-filter-process-output string
Subroutine of @code{proof-shell-filter} to process output @var{string}.

Appropriate action is taken depending on the what
@code{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.
@end defun






@c
@c SECTION: Debugging
@c
@node Debugging
@section Debugging
@cindex debugging

To debug Proof General, it may be helpful to set the
configuration variable @code{proof-show-debug-messages}.

@c TEXI DOCSTRING MAGIC: proof-show-debug-messages
@defopt 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 @samp{@code{proof-tidy-response}} to nil.

The default value is @code{nil}.
@end defopt

For more information about debugging Emacs lisp, consult the Emacs Lisp
Reference Manual.  I recommend using the source-level debugger
@code{edebug}.














@c
@c
@c APPENDIX: Obtaining and Installing
@c
@c
@node Obtaining and Installing
@appendix Obtaining and Installing

Proof General has its own
@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen,home page} hosted at
Edinburgh.  Visit this page for the latest news!

STOP PRESS: the Proof General web pages are temporarily being hosted at
@uref{zermelo.dcs.ed.ac.uk}.  The canonical address used to be
@uref{www.dcs.ed.ac.uk}, and it may one day revert to this.

@menu
* Obtaining Proof General::     
* Installing Proof General from tarball::  
* Installing Proof General from RPM package::  
* Setting the names of binaries::
* Notes for syssies::           
@end menu


@node Obtaining Proof General
@section Obtaining Proof General

You can obtain Proof General from the URL
@example
@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen}.
@end example

The distribution is available in three forms
@itemize @bullet
@item A source tarball, @*
@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz}
@item A Linux RPM package (for any architecture), @*
@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm}
@item A developer's tarball, @*
@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz}
@end itemize

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
@code{proofgen@@dcs.ed.ac.uk}.

@c was Installing Proof General from @file{.tar.gz}
@node Installing Proof General from tarball
@section Installing Proof General from tarball

Copy the distribution to some directory @var{mydir}.
Unpack it there. For example:
@example
# cd @var{mydir}
# gunzip ProofGeneral-@var{version}.tar.gz
# tar -xpf ProofGeneral-@var{version}.tar
@end example
If you downloaded the version called @var{latest}, you'll find it
unpacks to a numeric version number.

Proof General will now be in some subdirectory of @var{mydir}.  The name
of the subdirectory will depend on the version number of Proof General.
For example, it might be @file{ProofGeneral-2.0}.  It's convenient to
link it to a fixed name:
@example
# ln -sf ProofGeneral-2.0 ProofGeneral
@end example
Now put this line in your @file{.emacs} file:
@lisp
    (load-file "@var{mydir}/ProofGeneral/generic/proof-site.el")
@end lisp

@node Installing Proof General from RPM package
@section Installing Proof General from RPM package

To install an RPM package you need to be root.  Then type
@example
# rpm -Uvh ProofGeneral-latest.noarch.rpm
@end example

Now add the line:
@lisp
   (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el")
@end lisp
to your @file{.emacs} or the site-wide initialisation file
@file{site-start.el}.

@node Setting the names of binaries
@section Setting the names of binaries

The @code{load-file} command you have added will load @file{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:
@example
  Proof-General -> Customize -> @var{Name of Assistant} -> Prog Name
@end example
The Proof-General menu is available from script buffers after Proof
General is loaded.  To load it manually, type
@lisp
  M-x load-library RET proof RET
@end lisp

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:
@lisp
  (setq isabelle-prog-name "/usr/bin/isabelle FOL")
@end lisp
to your @file{.emacs} file.



@node Notes for syssies
@section 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.

@unnumberedsubsec 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 @code{.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 @code{.elc} files which aren't present using the source
@code{.el} files, please report them to us.

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


@unnumberedsubsec 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 @file{proof-site.el} are adjusted
accordingly, see @ref{Proof General site configuration}.  Make sure that
the @file{generic/} and assistant-specific elisp files are kept in
subdirectories (@file{coq/}, @file{isa.}, @file{lego.}) of
@code{proof-home-directory} so that the autoload directory calculations
are correct.

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

@unnumberedsubsec 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 @file{.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 @code{proof-assistants} in @file{proof-site.el} to remove the
extra autoloads.  This is advisable in case the extensions clash with
other Emacs modes, for example @code{sml-mode} for @file{.ML} files, or
Verilog mode for @file{.v} files.  

See @ref{Proof General site configuration}, to find out how to disable
support for provers you don't use.

@c Via the Customize mechanism, see the menu:
@c @example
@c   Options -> Customize -> Emacs -> External -> Proof General
@c @end example
@c or, after loading Proof General, in a proof script buffer
@c @example
@c   Proof-General -> Customize
@c @end example



@c
@c
@c APPENDIX: Known bugs and workarounds
@c
@c
@node Known bugs and workarounds
@appendix 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
@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}}
in the distribution for more detailed and up-to-date information.  @* 

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

@menu
* Bugs at the generic level::   
* Bugs specific to LEGO Proof General::  
* Bugs specific to Coq Proof General::  
* Bugs specific to Isabelle Proof General::  
@end menu

@node Bugs at the generic level
@section Bugs at the generic level

@subsection Undo in XEmacs

When @code{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
@kbd{C-x u}, nonsense text appears in locked region.

@strong{Workaround:} be careful with undo.

@subsection Font locking and read-only in FSF GNU Emacs

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

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


@subsection  Pressing keyboard quit @kbd{C-g}

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

@strong{Workaround:} Don't type @kbd{C-g} while script management is
processing.  If you do, use @code{proof-shell-restart} to restart
the system.

@c da: Removed 11.12.98: since PG handles this gracefully now,
@c I no longer consider it a bug really.
@c @subsection One prover at a time
@c You can't use more than one proof assistant at a time in the same Emacs
@c session.  Attempting to load Proof General for a second prover will
@c fail, leaving a buffer in fundamental mode instead of the Proof General
@c mode for proof scripts.

@c @strong{Workaround:} stick to one prover per Emacs session, make sure
@c that the @code{proof-assistants} variable only enables Proof General
@c for the provers you need.


@node Bugs specific to LEGO Proof General
@section Bugs specific to LEGO Proof General

@menu
* Retraction and Discharge::    
* Non writable directories::    
@end menu

@node Retraction and Discharge
@subsection Retraction and Discharge

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

@strong{Workaround:} retract back to the first declaration/definition
which is discharged.

@subsubsection Definitions in a proof state 
A thorny issue are local definitions in a proof state. LEGO cannot undo
them explicitly.

@strong{Workaround:} retract back to a command before a definition.

@subsubsection Normalisation in proofs
Normalisation commands such as @samp{Dnf}, @samp{Hnf} @samp{Normal}
cannot be undone in a proof state by Proof General.

@strong{Workaround:} retract back to the start of the proof.

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

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

@node Non writable directories
@subsection 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. 

@strong{Workaround:} Directly enter @kbd{Configure AnnotateOn;} in the 
Proof Shell to recover.

@node Bugs specific to Coq Proof General
@section Bugs specific to Coq Proof General

@subsection Hard-wired tactics

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

@strong{Workaround:} You may need to retract to the start of the proof.

@subsection Sections

Coq Proof General does not know about Coq's Section mechanism.
Problems similar to LEGO's discharge.
See @ref{Granularity of atomic command sequences}, for a proposal
on how to fix this bug.

@c 
@c Isabelle Bugs
@c
@node Bugs specific to Isabelle Proof General
@section Bugs specific to Isabelle Proof General

Here are some bugs and problems specific to Isabelle Proof General.

@subsection Clash with @code{sml-mode}

Since Isabelle proof scripts are not differentiated from @file{.ML}
files, Proof General may compete with @code{sml-mode} (if you use it)
for controlling these buffers.  To ensure Proof General wins, load it
last.

@strong{Workaround:} use another extension for real ML files, e.g.
@code{.sml}, and disable @code{.ML} from entering @code{sml-mode}.

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

@strong{Workaround:} indent your script by hand.



@subsection 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 @code{goal} or
@code{qed} forms.

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

@subsection 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!

@c
@c
@c APPENDIX: Plans and ideas
@c
@c
@node Plans and ideas
@appendix Plans and ideas

This appendix contains some tentative plans and ideas for improving Proof
General.  

This appendix is no longer extended: instead we keep a list of Proof
General projects on the web, and forthcoming plans and ideas in the
@file{TODO} and @file{todo} files included in the ordinary and
developers distributions, respectively.  Once the items mentioned below
are implemented, they will be removed from here.

Please send us contributions to our wish lists, or better still, an
offer to implement something from them!

@menu
* Proof by pointing and similar features::
* Granularity of atomic command sequences::  
* Browser mode for script files and theories::  
@end menu

@node Proof by pointing and similar features
@section Proof by pointing and similar features
@cindex proof by pointing

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:
@itemize @bullet
@item term structure mark-up
@item proof by pointing command generation
@end itemize
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.


@node Granularity of atomic command sequences
@section Granularity of atomic command sequences
@c @cindex Granularity of Atomic Sequences
@c @cindex Retraction
@c @cindex Goal
@cindex ACS (Atomic Command Sequence)

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

The blue 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 @ref{Goal-save sequences}, has
been hard wired. No other ACS are currently supported. We propose the
following to overcome this deficiency:

@vtable @code
@item proof-atomic-sequents-list
is a list of instructions for setting up ACSs. Each instruction is a
list of the form @code{(@var{end} @var{start} &optional
@var{forget-command})}. @var{end} is a regular expression to recognise
the last command in an ACS. @var{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 @var{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 (@var{start},@var{end}) is locked as an ACS. Optionally,
the ACS is annotated with the actual command to retract the ACS. This is 
computed by applying @var{forget-command} to the first and last command
of the ACS.

For convenience one might also want to allow @var{start} to be the
symbol @samp{t} as a convenient short-hand for @code{'(lambda (str)
".")} which always matches.
@end vtable

@node Browser mode for script files and theories
@section 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:
@itemize @bullet
@item Provide impoverished proof assistants with a browser
@item Extend the uniform interface of Proof General to theory browsing 
@item Interact closely with proof script writing
@end itemize
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.


@node References
@unnumbered References

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

@itemize @bullet
@item @b{[BT98]}
Yves Bertot and Laurent Th@'ery. @i{A generic approach to building
user interfaces for theorem provers}. Journal of
Symbolic Computation, 25(7), pp. 161-194, February 1998.
@end itemize

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

@itemize @bullet
@item @b{[BKS97]}
Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. @i{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 
@end itemize




@node Function Index
@unnumbered Function and Command Index
@printindex fn

@node Variable Index
@unnumbered Variable and User Option Index
@printindex vr

@node Keystroke Index
@unnumbered Keystroke Index
@printindex ky

@node Concept Index
@unnumbered Concept Index
@printindex cp

@page
@contents
@bye