File: ProofGeneral.texi

package info (click to toggle)
proofgeneral 4.5-3
links: PTS, VCS
area: main
in suites: sid, trixie
size: 5,172 kB
sloc: lisp: 33,783; makefile: 388; sh: 118; perl: 109
file content (6046 lines) | stat: -rw-r--r-- 238,330 bytes
\input texinfo
@c
@c $Id$
@c
@c
@c TODO:  
@c   Theorem dependencies, history in script and response,
@c   identifier info commands


@c
@c 
@setfilename ProofGeneral.info
@settitle Proof General
@setchapternewpage odd
@paragraphindent 0
@iftex
@afourpaper
@end iftex

@c
@c Some URLs.
@c FIXME: unfortunately, broken in buggy pdftexinfo.
@c so removed for now.
@set URLxsymbol  http://x-symbol.sourceforge.net
@set URLisamode  http://proofgeneral.inf.ed.ac.uk/~isamode
@set URLpghome   https://proofgeneral.github.io
@set URLpglatestrpm  http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.noarch.rpm
@set URLpglatesttar  http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.tar.gz
@set URLpglatestdev  http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz
@c
@c

@c
@c IMPORTANT NOTES 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
@c LINE BREAKS: For html generated from this to look good, it is
@c important that there are lots of line breaks/blank lines, esp
@c after @enddefn's and similar.  Otherwise text flows on the same
@c paragraph but gets coloured wrongly with Netscape's handling of 
@c style sheets.
@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.
@c

@set version 4.5
@set emacsversion 25.2
@set last-update July 2022
@set rcsid $Id$

@dircategory Theorem proving
@direntry
* ProofGeneral: (ProofGeneral). Organize your proofs with Emacs!
@end direntry

@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 Organize your proofs!
@sp 1
@subtitle User Manual for Proof General @value{version}
@subtitle @value{last-update}
@subtitle @b{proofgeneral.github.io}

@iftex
@vskip 1cm
@image{ProofGeneral-image}
@end iftex
@author D. Aspinall, P. Courtieu, E. Martin-Dorel, C. Pit--Claudel,
@author T. Kleymann, H. Goguen, D. Sequeira, M. Wenzel
@page
@vskip 0pt plus 1filll
This manual and the program Proof General are
Copyright @copyright{} 1998-2011 Proof 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 GNU Emacs @value{emacsversion} or
later versions (subject to Emacs API changes).  Proof General is
distributed under the terms of the GNU General Public License (GPL),
version 3 or later;
please check the accompanying file @file{COPYING} for more details.

@sp 1

Visit Proof General on the web at @code{https://proofgeneral.github.io}

@sp 1

@c (commented; dates from CVS) @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 GNU Emacs
@value{emacsversion} on Linux.  It is supplied ready to use for the proof
assistants Coq, EasyCrypt, and PhoX.

@menu
* Preface::                     
* Introducing Proof General::   
* Basic Script Management::     
* Advanced Script Management and Editing::  
* Unicode symbols and special layout support::
* Support for other Packages::  
* Subterm Activation and Proof by Pointing::
* Graphical Proof-Tree Visualization::
* Customizing Proof General::   
* Hints and Tips::
* Coq Proof General::           
* EasyCrypt Proof General::
* Shell Proof General::
@c * PhoX Proof General::
* Obtaining and Installing::  
* Bugs and Enhancements::
* References::                  
* History of Proof General::
* 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, future plans,
and acknowledgements to those who have helped along the way.
The appendix @ref{History of Proof General} contains old
news about previous releases, and notes on the development
of Proof General.

Proof General has a home page at
@uref{https://proofgeneral.github.io}.  
Visit this page for the latest version of this manual,
other documentation, system downloads, etc.


@menu
* News for Version 4.5::
* News for Version 4.4::
* News for Version 4.3::
* News for Version 4.2::
* News for Version 4.1::
* News for Version 4.0::
* Future::
* Credits::                     
@end menu

@node News for Version 4.5
@unnumberedsec News for Version 4.5
@cindex news

Proof-General is now distributed under the GPLv3+ license.

This release contains several bugfixes and many new features (see the
CHANGES file or the Git changelog for more details).

The support of the following systems have been added: EasyCrypt,
qrhl-tool.

The old code for the support of the following systems have been
removed: Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam,
Isabelle, HOL98.

@node News for Version 4.4
@unnumberedsec News for Version 4.4
@cindex news

Proof General 4.4 is the first release since PG has moved to
@uref{https://github.com/ProofGeneral/PG, GitHub}.

This release contains several bugfixes and improvements (see the Git
ChangeLog for more details) and supports both Coq 8.4 and Coq 8.5.

@node News for Version 4.3
@unnumberedsec News for Version 4.3
@cindex news

In Proof General version 4.3, the multiple file handling for Coq
has been improved. It now supports asynchronous and parallel
compilation of required modules. 

The proof tree display now supports the newest features of Coq
8.4. Proof General version 4.3 is compatible with Prooftree
version 0.11 (or better).


@node News for Version 4.2
@unnumberedsec News for Version 4.2
@cindex news

Proof General version 4.2 adds the usual round of compatibility fixes,
to support newer versions of Emacs and Coq.  It also contains some
updates to support HOL Light in a primitive fashion.

It also contains a new mechanism to display proof trees, provided by
Hendrik Tews and using a bespoke rendering application named
@uref{http://askra.de/software/prooftree/, Prooftree}.


@node News for Version 4.1
@unnumberedsec News for Version 4.1
@cindex news

Proof General version 4.1 adds some compatibility fixes to
Proof General 4.0, specifically for Coq version 8.3
and Isabelle 2011.

It also contains a new implementation of multiple file handling
for Coq provided by Hendrik Tews.

@node News for Version 4.0
@unnumberedsec News for Version 4.0
@cindex news

Proof General version 4.0 is a major overhaul of Proof General.
The main changes are:
@itemize @bullet
@item support for GNU Emacs only, @b{you cannot use XEmacs any more};
@item a new @b{Unicode Tokens} mode, which now replaces X-Symbol,
      @pxref{Unicode symbols and special layout support};
@item to allow ``document centred'' working, annotating scripts with prover output
      and automatically sending commands to the prover, @pxref{Document centred working};
@item support for latest versions of provers (Isabelle2009-2 and Coq 8.2);
@item numerous smaller enhancements and efficiency improvements.
@end itemize

See the @file{CHANGES} file in the distribution for more complete
details of changes, and the appendix @ref{History of Proof General} for
old news.


@node Future
@unnumberedsec Future
@cindex Proof General Kit
@cindex Future

The aim of the Proof General project is to provide powerful environments
and tools for interactive proof.

Proof General has been Emacs based so far and uses heavy per-prover
customisation.  The @b{Proof General Kit} project proposes that proof
assistants use a @i{standard} XML-based protocol for interactive proof,
dubbed @b{PGIP}.  PGIP will enable middleware for interactive proof
tools and interface components.  Rather than configuring Proof General
for your proof assistant, you will need to configure your proof
assistant to understand PGIP.  There is a similarity however; the design
of PGIP was based heavily on the Emacs Proof General framework.

At the time of writing, the Proof General Kit software is in a prototype
stage and the PGIP protocol is still being refined.  We have a prototype
Proof General plugin for the Eclipse IDE and a prototype version of a
PGIP-enabled Isabelle.  There is also a middleware component for
co-ordinating proof written in Haskell, the @i{Proof General Broker}.
Further collaborations are sought for more developments, especially the
PGIP enabling of other provers.  For more details, see
@uref{http://proofgeneral.inf.ed.ac.uk/kit, the Proof General Kit
webpage}.  Help us to help you organize your proofs!



@node Credits
@unnumberedsec Credits
@cindex maintenance

The original developers of the basis of Proof General were:

@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 written by
Thomas Kleymann and Dilip Sequeira.  It is no longer maintained.
@c
@c It is presently maintained by David Aspinall and
@c Paul Callaghan. 
@c
Coq Proof General was written by Healfdene Goguen, with
later contributions from Patrick Loiseleur.
It is now maintained by Pierre Courtieu.
@c
Isabelle Proof General was written and is being maintained by David
Aspinall.  It has benefited greatly from tweaks and suggestions by
Markus Wenzel, who wrote the first support for Isar and added Proof
General support inside Isabelle.  David von Oheimb supplied the
original patches for X-Symbol support, which improved Proof General
significantly.  Christoph Wedler, the author of X-Symbol, provided
much useful support in adapting his package for PG.

The generic base for Proof General was developed by Kleymann, Sequeira,
Goguen and Aspinall. 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, with
words borrowed from user documentation of LEGO mode, prepared by Dilip
Sequeira.  Healfdene Goguen wrote some text for Coq Proof General.
Since Proof General 2.0, this manual has been maintained by David
Aspinall, with contributions from Pierre Courtieu, Markus Wenzel
and Hendrik Tews.

The Proof General project has benefited from (indirect) funding by EPSRC
(@i{Applications of a Type Theory Based Proof Assistant} in the late
1990s and @i{The Integration and Interaction of Multiple Mathematical
Reasoning Processes}, EP/E005713/1 (RA0084) in 2006-8), the EC (the
Co-ordination Action @i{Types} and previous related projects), and the
support of the LFCS.  Version 3.1 was prepared whilst David Aspinall was
visiting ETL, Japan, supported by the British Council.  

For Proof General 3.7, Graham Dutton helped with web pages and
infrastructure; since then the the computing support team at the School
of Informatics have given help.  For testing and feedback for older
versions of Proof General, thanks go to Rod Burstall, Martin Hofmann,
and James McKinna, and several on the longer list below.

For the Proof General 4.0 release, special thanks go to Stefan Monnier
for patches and suggestions, to Makarius for many bug reports and help
with Isabelle support and to Pierre Courtieu for providing new
features for Coq support.

Between Proof General 4.3 and 4.4 releases, the PG sources have been
migrated from CVS to to GitHub; special thanks go to Clement
Pit--Claudel for help in this migration.

Proof General 4.4's new icons were contributed by Yoshihiro Imai
(@uref{http://proofcafe.org/wiki/Generaltan}) under CC-BY-SA 3.0
(@uref{https://creativecommons.org/licenses/by-sa/3.0/})

@c FIXME: watch contributors here!
During the development of Proof General 3.x and 4.x releases, 
many people helped provide testing and other feedback, 
including the Proof General maintainers,
Paul Callaghan, Pierre Courtieu, and Markus Wenzel, 
Stefan Berghofer, Gerwin Klein, and other folk who
tested pre-releases or sent bug reports and patches, including 
Cuihtlauac Alvarado,
Esben Andreasen,
Lennart Beringer,
Pascal Brisset,
James Brotherston,
Martin Buechi,
Pierre Casteran,
Lucas Dixon,
Erik Martin-Dorel,
Matt Fairtlough, 
Ivan Filippenko, 
Georges Gonthier,
Robin Green,
Florian Haftmann,
Kim Hyung Ho,
Mark A. Hillebrand,
Greg O'Keefe,
Alex Krauss,
Peter Lammich,
Pierre Lescanne,
John Longley,
Erik Martin-Dorel,
Assia Mahboubi,
Adam Megacz,
Stefan Monnier,
Tobias Nipkow, 
Clement Pit--Claudel, 
Leonor Prensa Nieto, 
David von Oheimb,
Lawrence Paulson,
Paul Roziere,
Randy Pollack,
Robert R. Schneck,
Norbert Schirmer,
Sebastian Skalberg,
Mike Squire, 
Hendrik Tews,
Norbert Voelker,
Tjark Weber,
Mitsuharu Yamamoto.

Thanks to all of you (and apologies to anyone missed)!



@c =================================================================
@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.
@html
<img src="ProofGeneral-image.jpg" alt="[ Proof General logo ]" >
@end html

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

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 accidentally.  You can undo
steps as usual.

The aim of Proof General is to provide a powerful and configurable
interface for numerous interactive proof assistants.  We target Proof
General mainly at intermediate or expert users, so that the interface
should be useful for large proof developments.  

Please help us!

Send us comments, suggestions, or (the best) patches to improve support
for your chosen proof assistant.  Contact us at
@uref{https://github.com/ProofGeneral/PG/issues}.

If your chosen proof assistant isn't supported, read the accompanying
@i{Adapting Proof General} manual to find out how to configure PG for a
new prover.  

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




@node Installing Proof General
@section Installing Proof General

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

For much more information, @xref{Obtaining and Installing}.


@node Quick start guide
@section Quick start guide

Once Proof General is correctly installed, the corresponding Proof
General mode will be invoked automatically when you visit a proof
script file for your proof assistant, for example:

@multitable @columnfractions .35 .3 .35
@item       @b{Prover}    @tab @b{Extensions} @tab @b{Mode}
@item       Coq           @tab @file{.v}      @tab @code{coq-mode}
@item       Phox          @tab @file{.phx}    @tab @code{phox-mode}
@item       PG-Shell      @tab @file{.pgsh}   @tab @code{pgshell-mode}
@item       EasyCrypt     @tab @file{.ec}     @tab @code{easycrypt-mode}
@end multitable
(the exact list of Proof Assistants supported may vary according to the
version of Proof General and its local configuration).  You can also
invoke the mode command directly, e.g., type @kbd{M-x coq-mode}, to
turn a buffer into a Coq script buffer.

You'll find commands to process the proof script are available from the
toolbar, menus, and keyboard.  Type @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 start the proof assistant manually with the
menu command "Start proof assistant".

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



@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, proof-tree visualization,
toolbar and menus, syntax highlighting, real symbols,
functions menu, tags, and finally, adaptability.

Here is an outline of some of these features.   Look in the contents
page or index of this manual to find out about the others!

@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 and Editing}.

@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{Proof-tree visualization}@*
In cooperation with the external program Prooftree
(available from the @uref{http://askra.de/software/prooftree/,
Prooftree website}), Proof General can display proof trees
graphically and provide visual information about the proof status
of different branches in a proof. The proof-tree display provides
additional means for inspecting the proof tree and thus helps
against loosing track in proofs.

The graphical proof-tree visualization is currently only
supported for Coq. For more details, @pxref{Graphical Proof-Tree
Visualization}. 


@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 several
proof assistants, including these:

@c FLAG VERSIONS HERE
@itemize @bullet
@item 
@b{Coq Proof General} for Coq Version 8.2@*
@xref{Coq Proof General}, for more details.
@c @item
@c @b{PhoX Proof General} for PhoX 0.8X@*
@c @xref{PhoX Proof General}, for more details.
@item
@b{EasyCrypt Proof General} for EasyCrypt@*
@xref{EasyCrypt Proof General}, for mode details.
@item
@b{Shell Proof General} for shell scripts (not really a proof assistant!)@*
@xref{Shell 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,
see the accompanying manual @i{Adapting Proof General}.
@end itemize

The exact list of Proof Assistants supported may vary according to the
version of Proof General you have and its local configuration; only the
standard instances documented in this manual are listed above.

Note that there is some variation between the features supported by
different instances of Proof General.  The main variation is proof by
pointing, which has been supported only in LEGO so far.  For advanced
features like this, some extensions to the output routines of the proof
assistant are required, typically.  If you like Proof General, @b{please
help us by asking the implementors of your favourite proof assistant to
support Proof General} as much as possible.

@node Prerequisites for this manual
@section Prerequisites for this manual
@cindex Meta
@cindex Alt
@cindex key sequences

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 with x, followed by b".
A key sequence like @kbd{M-z} means "meta with z".  (@key{Meta} may be
labelled @key{Alt} on your keyboard).

The manual also assumes you have a basic understanding of your proof
assistant and the language and files it uses for proof scripts.  But
even without this, Proof General is not useless: you can use the
interface to @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{Customization, ,emacs},
for documentation in Emacs.

To get the absolute most from Proof General, to improve it or to adapt
it for new provers, you'll need to know a little bit of Emacs lisp.
Emacs is self-documenting, so you can begin from @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

This manual covers the user-level view and customization of Proof
General.  The accompanying @i{Adapting Proof General} manual considers
adapting Proof General to new proof assistants, and documents some of
the internals of Proof General.

Three appendices of this manual contain some details about obtaining and
installing Proof General and some known bugs.  The contents of these
final chapters is also covered in the files @file{INSTALL} and
@file{BUGS} contained in the distribution.  Refer to those files
for the latest information.

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






@c =================================================================
@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 Isabelle::  
* Proof scripts::               
* Script buffers::              
* Summary of Proof General buffers::               
* Script editing commands::     
* Script processing commands::  
* Proof assistant commands::    
* Toolbar commands::            
* Interrupting during trace output::
@end menu

@c FIXME: Rewrite this to use Coq since Isabelle support was removed.
@node Walkthrough example in Isabelle
@section Walkthrough example in Isabelle

[@emph{Debian specific note}: The Debian Proof-General package
does not support Isabelle and the Isar example file is not
available in Debian. A small Coq example file is installed as
@file{/usr/share/doc/proofgeneral/examples/coq_example.v} by
package `proofgeneral'.]

Here's a short example in Isabelle to see how script management
is used.  The file you are asked to type below is included in the
distribution as @file{isar/Example.thy}.  If you're not using
Isabelle, substitute some lines from a simple proof for your proof
assistant, or consult the example file supplied with Proof General for
your prover, called something like @file{foo/example.foo} for a proof
assistant Foo.

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, start Emacs with Proof General loaded.  According to how you
have installed Proof General, this may be by typing
@code{proofgeneral} in a terminal, 
selecting it from a menu, or simply by starting
Emacs itself.
@item
Next, find a new file by @kbd{C-x C-f} and typing as the filename
@file{Walkthrough.thy}.  This should load Isabelle 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 or toolbar.

If you're not using Isabelle, 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
theory Walkthrough imports Main begin;
@end lisp
This first command begins the definition of a new theory inside
Isabelle, which extends the theory @code{Main}.  (We're assuming that
you have Isabelle/HOL available, which declares the @code{Main}
theory.  You should be able to see the list of installed logics in
Isabelle on the @code{Logics} menu).
@end itemize

Electric terminator sends commands to the proof assistant as you type
them. 
At the moment you type the semicolon, the @code{theory} command will
be sent to Isabelle behind the scenes.  First, there is a short delay
while Isabelle is launched; you may see a welcome message.  Then, you
may notice that the command briefly is given an orange/pink background
(or shown in inverse video if you don't have a colour display), before
you see a window containing text like this:
@lisp
theory Walkthrough 
@end lisp
which reflects the command just executed.
@c =
@c   @{ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
@c     Sum_Type, Relation, Record, Inductive, Transitive_Closure,
@c     Wellfounded_Recursion, Ring_and_Field, Nat, NatArith, Divides, Power,
@c     Finite_Set, Equiv, IntDef, Datatype_Universe, Datatype, Numeral, Bin,
@c     IntArith, Wellfounded_Relations, Recdef, IntDiv, NatBin, NatSimprocs,
@c     SetInterval, Presburger, Relation_Power, Parity, PreList, List, Map,
@c     Hilbert_Choice, Infinite_Set, Extraction, Refute, Main, #@}
@c (Which gives you some idea of the theories that go to build up @code{Main}!).

@c FIXME: explain window layouts a bit

In this case of this first command, it is hard to see the orange/pink
stage because the command is processed very quickly on modern machines.
But in general, processing commands can take an arbitrary amount of time
(or not terminate at all).  For this reason, Proof General maintains a
queue of commands which are sent one-by-one from the proof script.  As
Isabelle successfully processes commands in the queue, they will turn
from the orange/pink colour into blue.  

The blue regions indicate text that has been read by the prover and
should not be edited, to avoid confusion between what the prover has
processed and what you are looking at.  To enforce this (and avoid
potentially expensive reprocessing) the blue region can be made
read-only.  This is controlled by the menu item: 
@lisp
  Proof-General -> Quick Options -> Read Only
@end lisp
The first option `Strict Read Only' was formerly the default for Proof
General, and causes the blue region to be @i{locked}.  Because of this,
the term @dfn{locked region} term is used in Proof General documentation
to mean the blue portion of the text which has been processed, although
it is no longer locked by default.  The current default is `Undo on
Edit' which causes the prover to undo back to any user edits.  So if you
change a processed piece of text you will need to re-process it.  The
final option, `Freely Edit', allows you to freely edit the buffer
without causing the prover to reprocess it.  This can quickly lead to
confusion and a loss of synchronization between what you are reading and
what the prover has processed, so it is best used sparingly.

Electric terminator mode is popular, but not enabled by default because
of the principle of least surprise.  Moreover, in Isabelle, the
semicolon terminators are optional so proof scripts are usually written
without them to avoid clutter.  You'll notice that although you typed a
semi-colon it was not included in the buffer!  The electric terminator
tries to be smart about comments and strings but sometimes it may be
confused (e.g., adding a semi-colon inside an already written comment),
or you may need to type several terminator commands together.
In this case you can use the standard Emacs @b{quote next character},
typing @kbd{C-q ;} to quote the semi-colon.  Alternatively you can use
a prefix argument, as in @kbd{M-3 ;} to type three semi-colons.

Without using electric terminator, you can trigger processing the text
up to the current position of the point with the key @kbd{C-c C-RET}, or
just up to the next command with @kbd{C-c C-n}.  We show the rest of the
example in Isabelle with semi-colons, but these will not appear in the
final text.

Coq, on the other hand, requires a full-stop terminator at the end of
each line. If you want to enable electric terminator, use the menu item:
@code{Proof-General -> Quick Options -> Processing -> Electric Terminator}

If you want to keep electric terminator enabled all the time, you can
customize Proof General to do so, @xref{Customizing Proof General}.  For
the common options, customization is easy: just use the menu item
@code{Proof General -> Quick Options} to make your choices, and
@code{Proof-General -> Quick Options -> Save Options} to save your
choices.



@itemize @bullet
@item
Next type on a new line:
@lisp
theorem my_theorem: "A & B --> B & A";
@end lisp
@end itemize

The goal we have set ourselves to prove
should be displayed in the @i{goals buffer}.
@c FIXME explain again

@itemize @bullet
@item 
Now type:
@lisp
proof
  assume "A & C";
@end lisp
@end itemize
This will update the goals buffer.

But whoops!  That was the wrong command, we typed @code{C} instead
of @code{B}.

@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 Isabelle, and deletes the @code{assume} 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 left-arrow toolbar navigation button.

@itemize @bullet
@item
Instead, let's try:
@lisp
  assume "A & B";
@end lisp
Which is better.  

@item
From this assumption we can get @code{B} and @code{A} by the
trivial step @code{..} which splits the assumption using an elimination
step:
@lisp
  then obtain B and A ..;
@end lisp

@item
Finally, we establish the goal by the trivial step
@code{..} again, which triggers an introduction rule:
@lisp
  then show "B & A" ..;
@end lisp
@end itemize

After this proof step, the message from Isabelle indicates that the
proof has succeeded, so we can conclude the proof with the @code{qed}
command.

@itemize @bullet
@item
Finally, type:
@lisp
qed;
@end lisp
@end itemize

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

Moving the mouse pointer over the qed command now reveals that the
entire proof has been aggregated into a single segment (if you did this
before, you would see highlighting of each command separately).
@c This is no longer true!
@c This reflects the fact that Isabelle has thrown away the history of the
@c proof, so if we want to undo now, the whole proof must be retracted.

@itemize  @bullet
@item 
Suppose we decide to call the theorem something more sensible. Move the
cursor up into the locked region, somewhere between @samp{theorem} and
@samp{qed}, 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, or as near as possible above or below it, sending
undoing commands or proof commands as necessary.  In this case, the
locked region will always be moved back to the end of the @code{theory}
line, since that is the closest possible position to the cursor that
appears before it.  If you simply want to @i{retract} the whole file in
one go, you can use the key @kbd{C-c C-r} (which corresponds to the up
arrow on the toolbar), which will automatically move the cursor to
the top of the file.

@itemize @bullet
@item 
Now improve the goal name, for example:
@lisp
theorem and_commutes: "A & B --> B & A"
@end lisp
You can swiftly replay the rest of the buffer now
with @kbd{C-c C-b} (or the down arrow on the toolbar).
@item 
At the end of the buffer, you may insert the command
@lisp
end
@end lisp
to complete the theory.  
@end itemize

Notice that if you right-click on one of the highlighted regions in the
blue area you will see a context menu for the region.  This includes a
``show/hide'' option for @i{folding} a proof, as well as some editing
commands for copying the region or rearranging its order in the
processed text: ``move up/move down''. (These latter commands
occasionally help you reorder text without needing to reprove it,
although they risk breaking the proof!)

@c da: no longer true with Isabelle2007
@c Note that once a theory is completed in Isabelle, you cannot undo into
@c it, again because Isabelle discards the history of the theory's
@c creation.  Just like completed proofs, there is no option other than
@c undoing the whole theory.  To prevent you doing this inadvertently,
@c however (maybe undoing many proofs which are time-consuming to replay),
@c the @kbd{C-c C-u} or @kbd{C-c C-RET} commands will generate an error
@c message, typically:
@c @lisp
@c *** Cannot undo "end"
@c *** At command "cannot_undo".
@c @end lisp
@c If you really want to retract the theory for editing once more, you can
@c use the key @kbd{C-c C-r} (which corresponds to the up arrow on the
@c toolbar).

Finally, once you are happy with your theory, you should save the file
with @kbd{C-x C-s} before moving on to edit another file or exiting
Emacs.  If you forget to do this, Proof General or Emacs will surely
prompt you sooner or later!


@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} (e.g. @code{qed}) 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{Imenu and Speedbar}).

@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 at the bottom of
the screen.  This is coloured to indicate the status:
if it has a pink or blue background, the prover is processing the
text (busy when pink).  If it is in green, the buffer is
completely processed.

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.v, retract?}
or if you want to process the remainder of the active buffer, 
@code{Completely process buffer myproof.v 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.
@item The @dfn{trace buffer} is a special version of the response
 buffer.  It may be used to display unusual debugging output from the
 prover, for example, tracing proof tactics or rewriting procedures.
 This buffer is also displayed whenever Proof General puts a new message
 in it (although it may be quickly replaced with the response or goals
 buffer in two-buffer mode).
@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, for example, to prevent
auxiliary buffers being displayed at all (@pxref{Display
customization}).

The menu @code{Proof General -> Buffers} provides a convenient way to
display or switch to a Proof General buffer: the active scripting
buffer; the goal or response buffer; the tracing buffer; or the shell
buffer.  Another command on this menu, @code{Clear Responses}, clears
the response and tracing buffer.


@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 end of command at point.
@end deffn

@vindex proof-terminal-string
The variable @code{proof-terminal-string} is a prover-specific string
to terminate proof commands.  LEGO and Isabelle used 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 called interactively or @var{switch} is non-nil, switch to script buffer.
If called interactively, a mark is set at the current location with @samp{@code{push-mark}}
@end deffn

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

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

@c @c DOCSTRING MAGIC: proof-mouse-track-insert
@c @deffn Command proof-mouse-track-insert event
@c Copy highlighted command under mouse @var{event} to point.  Ignore comments.@*
@c If there is no command under the mouse, behaves like mouse-track-insert.
@c @end deffn

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

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.  LEGO and Isabelle used @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.

In normal development, one often jumps into the middle or to the
end of some file, because this is the point, where a lemma must
be added or a definition must be fixed. Before starting the real
work, one needs to assert the file up to that point, usually with
@kbd{C-c C-RET} (@code{proof-goto-point}). Even for medium sized
files, asserting a big portion can take several seconds. There
are different ways to speed this process up.
@itemize @bullet
@item
One can split the development into smaller files. This works
quite well with Coq, automatic background compilation,
@ref{Automatic Compilation in Detail}, and the fast compilation
options, @ref{Quick and inconsistent compilation}.
@item
One can configure @code{proof-omit-proofs-option} to @code{t} to
omit complete opaque proofs when larger chunks are asserted. A
proof is opaque, if its proof script or proof term cannot
influence the following code. In Coq, opaque proofs are finished
with @code{Qed}, non-opaque ones with @code{Defined}. When this
omit proofs feature is configured, complete opaque proofs are
silently replace with a suitable cheating command
(@code{Admitted} for Coq) before sending the proof to the proof
assistant. For files with big proofs this can bring down the
processing time to 10% with the obvious disadvantage that errors
in the omitted proofs go unnoticed. For checking the proofs
occasionally, a prefix argument for @code{proof-goto-point} and
@code{proof-process-buffer} causes these commands to disregard
the setting of @code{proof-omit-proofs-option}. Currently, the
omit proofs feature is only supported for Coq.
@item
An often used poor man's solution is to collect all new material
at the end of one file, regardless where the material really
belongs. When the final theorem has been proved, one cleans up
the mess and moves all stuff where it really belongs.
@end itemize

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 &optional raw
Assert or retract to the command at current position.@*
Calls @samp{@code{proof-assert-until-point}} or @samp{@code{proof-retract-until-point}} as
appropriate. With prefix argument @var{raw} the omit proofs feature
(@samp{@code{proof-omit-proofs-option}}) is temporaily disabled to check all
proofs in the asserted region.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-process-buffer
@deffn Command proof-process-buffer &optional raw
Process the current (or script) buffer, and maybe move point to the end.@*
With prefix argument @var{raw} the omit proofs feature (@samp{@code{proof-omit-proofs-option}})
is temporaily disabled to check all proofs in the asserted region.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-retract-buffer
@deffn Command proof-retract-buffer &optional called-interactively
Retract the current buffer, and maybe move point to the start.@*
Point is only moved according to @samp{@code{proof-follow-mode}}, if
@var{called-interactively} is non-nil, which is the case for all
interactive calls.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-electric-terminator-toggle
@deffn Command proof-electric-terminator-toggle &optional arg
Toggle @samp{@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.
@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.@*
If inside a comment, just process until 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

As experienced Emacs users will know, a @i{prefix argument} is a numeric
argument supplied by some key sequence typed before a command key
sequence.  You can supply a specific number by typing @key{Meta} with
the digits, or a ``universal'' prefix of @kbd{C-u}.  See
@inforef{Arguments, ,emacs} for more details.  Several Proof General
commands, like @code{proof-retract-until-point-interactive}, may accept
a @i{prefix argument} to adjust their behaviour somehow.


@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 and
Proof General, which do not involve the proof script.  Here are the
key-bindings and functions.

@table @kbd
@item C-c C-l
@code{proof-display-some-buffers}
@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-i
@code{proof-query-identifier}
@item C-c C-f
@code{proof-find-theorems}
@item C-c C-w
@code{pg-response-clear-displays}
@item C-c C-c
@code{proof-interrupt-process}
@item C-c C-v
@code{proof-minibuffer-cmd}
@item C-c C-s
@code{proof-shell-start}
@item C-c C-x
@code{proof-shell-exit}
@end table


@c TEXI DOCSTRING MAGIC: proof-display-some-buffers
@deffn Command proof-display-some-buffers 
Display the response, trace, goals, or shell buffer, rotating.@*
A fixed number of repetitions of this command switches back to
the same buffer.
Also move point to the end of the response buffer if it's selected.
If in three window or multiple frame mode, display two buffers.
The idea of this function is to change the window->buffer mapping
without adjusting window layout.
@end deffn

@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-query-identifier
@deffn Command proof-query-identifier string
Query the prover about the identifier @var{string}.@*
If called interactively, @var{string} defaults to the current word near point.
@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: pg-response-clear-displays
@deffn Command pg-response-clear-displays 
Clear Proof General response and tracing buffers.@*
You can use this command to clear the output from these buffers when
it becomes overly long.  Particularly useful when @samp{@code{proof-tidy-response}}
is set to nil, so responses are not cleared automatically.
@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 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.

Some provers may ignore (and lose) interrupt signals, or fail to indicate
that they have been acted upon yet stop in the middle of output.
In the first case, PG will terminate the queue of commands at the first
available point.  In the second case, you may need to press enter inside
the prover command buffer (e.g., with Isabelle@var{2009} press RET inside @strong{isabelle}).
@end deffn

@c TEXI DOCSTRING MAGIC: proof-minibuffer-cmd
@deffn Command proof-minibuffer-cmd cmd
Send @var{cmd} to proof assistant.  Interactively, read from minibuffer.@*
The command isn't added to the locked region.

If a prefix arg is given and there is a selected region, that is
pasted into the command.  This is handy for copying terms, etc from
the script.

If @samp{@code{proof-strict-state-preserving}} is set, and @samp{@code{proof-state-preserving-p}}
is configured, then the latter 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.

@var{warning}: this command risks spoiling synchronization if the test
@samp{@code{proof-state-preserving-p}} is not configured, if it is
only an approximate test, or if @samp{@code{proof-strict-state-preserving}}
is off (nil).
@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 starting, stopping, and restarting the
proof assistant process.  The first two have key bindings but restart
does not.  As with any Emacs command, you can invoke these with
@kbd{M-x} followed by the command name.


@c TEXI DOCSTRING MAGIC: proof-shell-start
@deffn Command proof-shell-start 
Initialise a shell-like buffer for a proof assistant.@*
Does nothing if proof assistant is already running.

Also generates goal and response buffers.

If @samp{@code{proof-prog-name-ask}} is set, query the user for the
process command.
@end deffn

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

This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function

@samp{@code{proof-shell-kill-function}} to do the hard work.  If optional
argument @var{dont-ask} is non-nil, the proof process is terminated
without confirmation.

The kill function uses @samp{<PA>-quit-timeout} as a timeout to wait
after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process.

This function should not be called if
@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of
@samp{@code{proof-shell-kill-function}} will give strange errors.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-shell-restart
@deffn Command proof-shell-restart 
Clear script buffers and send @samp{@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
@samp{@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 Coq).
@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 to
inspect the prover's state, 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


@node Interrupting during trace output
@section Interrupting during trace output

If your prover generates output which is recognized as tracing output in
Proof General, you may need to know about a special provision for
interrupting the prover process.
@c %
If the trace output is voluminous, perhaps looping, it may be difficult
to interrupt with the ordinary @kbd{C-c C-c}
(@code{proof-interrupt-process}) or the corresponding button/menu.  In
this case, you should try Emacs's @b{quit key}, @kbd{C-g}.  This will
cause a quit in any current editing commands, as usual, but during
tracing output it will also send an interrupt signal to the prover.
Hopefully this will stop the tracing output, and Emacs should catch up
after a short delay.

Here's an explanation of the reason for this special provision.  When
large volumes of output from the prover arrive quickly in Emacs, as
typically is the case during tracing (especially tracing looping
tactics!), Emacs may hog the CPU and spend all its time updating the
display with the trace output.  This is especially the case when
features like output fontification and token display are active.  If
this happens, ordinary user input in Emacs is not processed, and it
becomes difficult to do normal editing.  The root of the problem is that
Emacs runs in a single thread, and pending process output is dealt with
before pending user input.  Whether or not you see this problem depends
partly on the processing power of your machine (or CPU available to
Emacs when the prover is running).  One way to test is to start an Emacs
shell with @kbd{M-x shell} and type a command such as @code{yes} which
produces output indefinitely.  Now see if you can interrupt the process!
(Warning --- on slower machines especially, this can cause lockups, so
use a fresh Emacs.)




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

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

@menu
* Document centred working::
* Automatic processing::
* Visibility of completed proofs::
* Switching between proof scripts::  
* View of processed files ::    
* Retracting across files::     
* Asserting across files::      
* Automatic multiple file handling::
* Escaping script management::
* Editing features::
@end menu

@node Document centred working
@section Document centred working
@cindex annotation

Proof scripts can be annotated with the output produced by the prover
while they are checked.  By hovering the mouse on the completed
regions you can see any output that was produced when they were
checked.  Depending on the proof language (it works well with
declarative languages), this may enable a ``document centred'' way of
working, where you may not need to keep a separate window open for
displaying prover output.

This way of working is controlled by several settings.  To help
configure things appropriately for document-centred working, there are
two short-cut commands:
@lisp
Proof-General -> Quick Options -> Display -> Document Centred 
Proof-General -> Quick Options -> Display -> Default
@end lisp
which change settings appropriately between a document centred
mode and the original classic Proof General behaviour and appearance.  
The first command also engages automatic processing of the whole
buffer, explained in the following section further below.

The behaviour can be fine-tuned with the individual settings.
Starting with the classic settings, first, you may select
@lisp
Proof-General -> Quick Options -> Processing -> Full Annotations
@end lisp
to ensure that the details are recorded in the script.  This is not the
default because it can cause long sequences of commands to execute more
slowly as the output is collected from the prover eagerly when the
commands are executed, and printing can be be slow for large and complex
expressions.  It also increases the space requirements for Emacs
buffers.  However, when interactively developing smaller files, it is
very useful.

Next, you may @i{de}select 
@lisp
Proof-General -> Quick Options -> Display -> Auto Raise
@end lisp
which will prevent the prover output being eagerly displayed.  You can
still manually arrange your Emacs windows and frames to ensure the
output buffers are present if you want.  

You may like to @i{de}select
@lisp
Proof General -> Quick Options -> Display -> Colour Locked
@end lisp
to prevent highlighting of the locked region.  This text which
has been checked and that which has not is less obvious, but 
you can see the position of the next command to be processed
with the marker.

If you have no colouring on the locked region, it can be hard to see
where processing has got to.  Look for the ``overlay marker'', a triangle
in the left-hand fringe of the display, to see which line processing has
stopped at.   If it has stopped on a region with
an error, you might want to see that.  You can select
@lisp
Proof-General -> Quick Options -> Display -> Sticky Errors
@end lisp
to add a highlight for regions which did not successfully process
on the last attempt.  Whenever the region is edited, the
highlight is removed. 

Finally, you may want to ensure that
@lisp
Proof-General -> Quick Options -> Read Only -> Undo On Edit
@end lisp
is selected.  
Undo on edit is a setting for the @code{proof-strict-read-only} variable.
This allows you to freely edit the processed region, but first it
automatically retracts back to the point of the edit.  Comments can
be edited freely without retraction.

The configuration variables controlled by the above menu items can be
customized as Emacs variables.  The two settings which control
interaction with the prover are @code{proof-full-annotation} and
@code{proof-strict-read-only}.  Note that you can also record the
history of output from the prover @i{without} adding mouse hovers to the
script.  This is controlled by @code{proof-output-tooltips} which is
also on the Display menu in Quick Options.  @xref{Display
customization}, for more information about customizing display options.

@c TEXI DOCSTRING MAGIC: proof-full-annotation
@defopt proof-full-annotation 
Non-nil causes Proof General to record output for all proof commands.@*
Proof output is recorded as it occurs interactively; normally if
many steps are taken at once, this output is suppressed.  If this
setting is used to enable it, the proof script can be annotated
with full details.  See also @samp{@code{proof-output-tooltips}} to enable
automatic display of output on mouse hovers.

The default value is @code{nil}.
@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, except for the special value @code{'retract} which means
undo first.  If nil, Proof General is more relaxed (but may give
you a reprimand!).

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




@node Automatic processing
@section Automatic processing
@cindex Automatic processing
@cindex autosend
@vindex proof-autosend-enable


If you like making your hair stand on end, the electric
terminator mode is probably not enough.  Proof General has another
feature that will automatically send text to the prover, while
you aren't looking.

Enabling
@lisp
Proof-General -> Quick Options -> Processing -> Process Automatically
@end lisp

Causes Proof General to start processing text when Emacs is idle for a
while.  You can choose either to send just the next command beyond the
point, or the whole buffer.  See
@lisp
Proof-General -> Quick Options -> Processing -> Automatic Processing Mode
@end lisp
for the choices.

The text will be sent in a fast loop that processes more quickly than
@kbd{C-c C-b} (i.e., @code{proof-process-buffer}, the down toolbar
button), but ignores user input and doesn't update the display.  But the
feature tries to be non-intrusive to the user: if you start to type
something or use the mouse, the fast loop will be interrupted and revert
to a slower interactive loop with display updates.

In the check next command mode, the successfully checked region will
briefly flash up as green to indicate it is okay.

You can use @kbd{C-c C-.} (@code{proof-goto-end-of-locked}) to find out
where processing got to, as usual.  Text is only sent if the last
interactive command processed some text (i.e., wasn't an undo step
backwards into the buffer) and processing didn't stop with an error.  To
start automatic processing again after an error, simply hit @kbd{C-c
C-n} after editing the buffer.  To turn the automatic processing on or
off from the keyboard, you can use the key binding:

@table @kbd
@item C-c >
@code{proof-autosend-toggle}
@end table

@c TEXI DOCSTRING MAGIC: proof-autosend-toggle
@deffn Command proof-autosend-toggle &optional arg
Toggle @samp{@code{proof-autosend-enable}}. With @var{arg}, turn on iff ARG>0.@*
This function simply uses @code{customize-set-variable} to set the variable.
@end deffn


@node Visibility of completed proofs
@section Visibility of completed proofs
@cindex Visibility of proofs

Large developments may consist of large files with many proofs.  To help
see what has been proved without the detail of the proof itself, Proof
General can hide portions of the proof script.  Two different kinds of
thing can be hidden: comments and (what Proof General designates as) the
body of proofs.

You can toggle the visibility of a proof script portion by using the
context sensitive menu triggered by @b{clicking the right mouse button
on a completed proof}, or the key @kbd{C-c v}, which runs
@code{pg-toggle-visibility}.

You can also select the ``disappearing proofs'' mode from the menu,
@lisp
  Proof-General -> Quick Options -> Display -> Disappearing Proofs
@end lisp 
This automatically hides each the body of each proof portion
as it is completed by the proof assistant.
Two further menu commands in the main Proof-General menu,
@emph{Show all} and @emph{Hide all} apply to all the completed
portions in the buffer.

Notice that by design, this feature only applies to completed proofs,
@emph{after} they have been processed by the proof assistant.  When
files are first visited in Proof General, no information is stored about
proof boundaries.

The relevant elisp functions and settings are mentioned below.

@c TEXI DOCSTRING MAGIC: pg-toggle-visibility
@deffn Command pg-toggle-visibility 
Toggle visibility of region under point.
@end deffn

@c TEXI DOCSTRING MAGIC: pg-show-all-proofs
@deffn Command pg-show-all-proofs 
Display all completed proofs in the buffer.
@end deffn

@c TEXI DOCSTRING MAGIC: pg-hide-all-proofs
@deffn Command pg-hide-all-proofs 
Hide all completed proofs in the buffer.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-disappearing-proofs
@defopt proof-disappearing-proofs 
Non-nil causes Proof General to hide proofs as they are completed.

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


@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, Coq's proof script
files have to end with @file{.v}.} @file{HSound.v}. 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.v} and retract to where changes are required. Then, using
script management, you want to develop some more basic theory in
@file{sos.v}. 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.v} 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 generated 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.



@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, see @i{Handling multiple files} in
the @i{Adapting Proof General} manual.



@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 you can use to interact with the prover if necessary.  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 Editing features
@section Editing features
@cindex Input ring

To make editing proof scripts more productive, Proof General provides
some additional editing commands.

One facility is the @i{input ring} of previously processed commands.
This allows a convenient way of repeating an earlier command or a small
edit of it.  The feature is reminiscent of history mechanisms provided
in shell terminals (and the implementation is borrowed from the Emacs
Comint package).  The input ring only contains commands which have been
successfully processed (coloured blue).  Duplicated commands are only
entered once.  
@c this is disabled for now, it's not robust
@c When commands are undone, they are removed from the ring.
The size of the ring is set by the variable @code{pg-input-ring-size}.

@kindex M-p
@kindex M-n
@table @kbd
@item M-p
@code{pg-previous-matching-input-from-input}
@item M-n
@code{pg-next-matching-input-from-input}
@end table


@c TEXI DOCSTRING MAGIC: pg-previous-input
@deffn Command pg-previous-input arg
Cycle backwards through input history, saving input.@*
If called interactively, @var{arg} is given by the prefix argument.
@end deffn
@c TEXI DOCSTRING MAGIC: pg-next-input
@deffn Command pg-next-input arg
Cycle forwards through input history.@*
If called interactively, @var{arg} is given by the prefix argument.
@end deffn
@c TEXI DOCSTRING MAGIC: pg-previous-matching-input
@deffn Command pg-previous-matching-input regexp n
Search backwards through input history for match for @var{regexp}.@*
(Previous history elements are earlier commands.)
With prefix argument @var{n}, search for Nth previous match.
If @var{n} is negative, find the next or Nth next match.
@end deffn
@c TEXI DOCSTRING MAGIC: pg-next-matching-input
@deffn Command pg-next-matching-input regexp n
Search forwards through input history for match for @var{regexp}.@*
(Later history elements are more recent commands.)
With prefix argument @var{n}, search for Nth following match.
If @var{n} is negative, find the previous or Nth previous match.
@end deffn
@c TEXI DOCSTRING MAGIC: pg-previous-matching-input-from-input
@deffn Command pg-previous-matching-input-from-input n
Search backwards through input history for match for current input.@*
(Previous history elements are earlier commands.)
With prefix argument @var{n}, search for Nth previous match.
If @var{n} is negative, search forwards for the -Nth following match.
@end deffn
@c TEXI DOCSTRING MAGIC: pg-next-matching-input-from-input
@deffn Command pg-next-matching-input-from-input n
Search forwards through input history for match for current input.@*
(Following history elements are more recent commands.)
With prefix argument @var{n}, search for Nth following match.
If @var{n} is negative, search backwards for the -Nth previous match.
@end deffn


@c =================================================================
@c 
@c  CHAPTER:  Unicode Tokens
@c
@node Unicode symbols and special layout support
@chapter Unicode symbols and special layout support

@cindex symbols
@cindex X-Symbols
@cindex Greek letters
@cindex logical symbols
@cindex mathematical symbols
@cindex subscripts
@cindex superscripts
@cindex Maths Menu
@cindex Tokens Mode

Proof General inherits support for displaying Unicode (and any other)
fonts from the underlying Emacs program.  If you are lucky, your system
will be able to use or synthesise a font that provides a rich set of
mathematical symbols.  To store symbols directly in files you need to
use a particular coding, for example UTF-8.  Newer Emacs versions can
handle a multitude of different coding systems and will try to
automatically detect an appropriate one; consult the Emacs documentation
for more details.  Of course, the prover that you are using will need to
understand the same encodings and symbol meanings.

Alternatively, you can use the @b{Unicode Tokens} mode provided in Proof
General to display mathematical symbols in place of sequences of other
characters (usually plain ASCII).  This can provide better
compatibility, portability, and flexibility.  Even if you use real
Unicode characters as prover input, the Unicode Tokens mode can provide
some helpful facilities for input shorthands and giving special layout.

@menu
* Maths menu::
* Unicode Tokens mode::
* Configuring tokens symbols and shortcuts::
* Special layout::
* Moving between Unicode and tokens::
* Finding available tokens shortcuts and symbols::
* Selecting suitable fonts::
@end menu



@node Maths menu
@section Maths menu

The @b{Maths Menu} minor mode (adapted from a menu by Dave Love) simply
adds a menu @code{Maths} to the main menubar for inserting common
mathematical symbols.  You can enable or disable it via the menu
@example
  Proof-General -> Quick Options -> Minor Modes -> Unicode Maths Menu
@end example
(@code{proof-maths-menu-toggle}).  Whether or not the symbols display
well the menus depends on the font used to display the menus (which
depends on the Emacs version, toolkit and platform).  Ordinarily, the
symbols inserted into the text will be Unicode characters which will be
saved in the file using the encoding selected by standard Emacs
mechanisms.


@node Unicode Tokens mode
@section Unicode Tokens mode


The @b{Unicode Tokens} minor mode has been written specially for Proof
General (with thanks to Stefan Monnier for providing inspiration and a
starting point).  It supports the display of symbols when the underlying
text of the file and buffer actually contains something else, typically,
plain ASCII text.  It provides backward compatibility with the older
X-Symbol mode.

Unicode Tokens can be enabled or disabled using the menu:
@example
  Proof-General -> Quick Options -> Display -> Unicode Tokens
@end example
The mode to allows ASCII tokens (i.e., sequences of plain ASCII
characters) to be displayed as Unicode character compositions, perhaps
with additional text properties.  The additional text properties allow
the use of tokens to cause font changes (bold, italic), text size
changes, and sub-script/super-script.

For example, the ASCII sequences @code{/\} or @code{\<And>} could be
displayed as a conjunction symbol.
@comment %% fixme
The sequence @code{x __ y} might be written to display @code{y}
as subscript.  This allows a file to be stored in perfectly portable plain ASCII
encoding, but be displayed and edited with real symbols and
appealing layout.  Of course, the proof assistant needs to understand
the underlying tokens in each case.

Technically, the mechanism is based on Emacs Font Lock facility, using
the @code{composition} text property to display ASCII character sequence
tokens as something else.  This means that the underlying buffer text is
@i{not} altered.  This is a major advantage over the older X-Symbol (and
the experimental version of Unicode Tokens in PG 3.7.1), which had the
annoying risk of saving your buffer text in a corrupted format.  This
can never happen with the new mode.

When the Unicode Tokens mode is enabled, Maths Menu is automatically
modified to insert tokenised versions of the Unicode characters
(whenever a reverse mapping can be found).  This means that you can
still use the Maths Menu to conveniently input symbols.  You can easily
add custom key bindings for particular symbols you need to enter often
(@pxref{Adding your own keybindings} for examples).

The Unicode Tokens mode also allows short-cut sequences of ordinary
characters to quickly type tokens (similarly to the facility provided by
X-Symbol).  These, along with the token settings themselves, are
configured on a per-prover basis.

@node Configuring tokens symbols and shortcuts
@section Configuring tokens symbols and shortcuts

To edit the strings used to display tokens, or the collection of 
short-cuts, you can edit the 
file @code{@i{PA}-unicode-tokens.el}, or customize the main
variables it contains, for example @code{@i{PA}-token-name-alist} and 
@code{@i{PA}-shortcut-alist}. 

@c FIXME: Isabelle support was removed.
E.g., for Isabelle 
@example
  M-x customize-variable isar-token-name-alist RET
@end example
provides an interface to the tokens, and
@example
  M-x customize-variable isar-shortcut-alist
@end example
an interface to the shortcuts.

Where possible, it is better to use the more fine grained way is
available to do this, which edits the separate tables which are combine
to form the big list of tokens.  This is available via the menus, e.g.,
in Isabelle, use
@example
  Tokens -> Customize -> Extended Symbols
@end example
to customize the symbols used for the ``extended'' (non standard)
symbol list.


@node Special layout 
@section Special layout 

The Unicode Tokens mode supports both @i{symbol tokens} used to display
character sequences in different ways and @i{control tokens} used to
control the layout of the text in various ways, such as superscript,
subscript, large, small, bold, italic, etc.  (The size and position
layout is managed using Emacs's @code{display} text property)

As well as displaying token sequences as special symbols, symbol tokens
themselves can define layout options as well; for example you might
define a token @code{\<hugeOplus>} to display a large circled-plus
glyph.  If you try the customization mentioned in the section above you
will see the options available when defining symbols.

These options are fixed layout schemes which also make layout tokens
easy to configure for provers.  The layout possibilities include the
ones shown in the table below.  There are two ways of configuring
control tokens for layout: @i{character controls} and @i{region
controls}.  The character controls apply to the next ``character'',
although this is a prover-specific notion and might actually mean the
next word or identifier.  An example might be writing @code{BOLDCHAR x}
to make a bold @b{x}.  Similarly the region controls apply to a
delineated region of text, for example, writing @code{BEGINBOLD this is
bold ENDBOLD} could cause the enclosed text @b{this is bold} to be
displayed in a bold font.

The control tokens that have been configured populate the Tokens
menu, so, for example, you may be able to select a region
of text and then use the menu item:
@example
  Tokens -> Format Region -> Bold
@end example
to cause the bold region tokens to be inserted around the selected
text, which should cause the buffer presentation to show the text
in a bold format (hiding the tokens).

Here is the table of layout controls available.  What you actually
can use will depend on the configuration for the underlying prover.
@table @code
@item sub
lower the text (subscript)
@item sup
raise the text (superscript)
@item bold
make the text be in the bold weight of the current font
@item italic
make the text be in the italic variant of the current font
@item big
make the text be in a bigger size of the current font
@item small
make the text be in a smaller size of the current font
@item underline
underline the text
@item overline
overline the text
@item script
display the text in a ``script'' font
@item frakt
display the text in a ``fraktur'' font
@item serif
display the text in a serif font
@item sans
display the text in a sans serif font
@item keyword
display the text in the keyword face (@code{font-lock-keyword-face})
@item function 
display the text in the function name face (@code{font-lock-function-name-face})
@item type
display the text in the type name face (@code{font-lock-type-face})
@item preprocessor
display the text in the preprocessor face (@code{font-lock-preprocessor-face})
@item doc
display the text in the documentation face (@code{font-lock-doc-face})
@item builtin
display the text in the builtin face (@code{font-lock-builtin-face})
@end table

Notice that the fonts can be set conveniently by the menu commands
@example
        Tokens -> Set Fonts -> Script
@end example
etc.  @xref{Selecting suitable fonts}, for more.

The symbols used to select the various font-lock faces (see @code{M-x
list-faces-display} to show them) allow you to define custom colouring
of text for proof assistant input and output, exploiting rich underlying
syntax mechanisms of the prover.


@c note: see unicode-tokens-fontsymb-properties

@c TEXI DOCSTRING MAGIC: unicode-tokens-serif-font-face
@deffn Face unicode-tokens-serif-font-face 
Serif (roman) font face.
@end deffn
@c TEXI DOCSTRING MAGIC: unicode-tokens-sans-font-face
@deffn Face unicode-tokens-sans-font-face 
Sans serif font face.
@end deffn
@c TEXI DOCSTRING MAGIC: unicode-tokens-fraktur-font-face
@deffn Face unicode-tokens-fraktur-font-face 
Fraktur font face.
@end deffn
@c TEXI DOCSTRING MAGIC: unicode-tokens-script-font-face
@deffn Face unicode-tokens-script-font-face 
Script font face.
@end deffn


@node Moving between Unicode and tokens
@section Moving between Unicode and tokens

If you want to share text between applications (e.g., email some text
from an Isabelle theory file which heavily uses symbols), it is
useful to convert to and from Unicode with cut-and-paste operations.
The default buffer cut and paste functions will copy the underlying text,
which contains the tokens (ASCII format).  To copy and convert 
or paste then convert back, use these commands:
@example
  Tokens -> Copy as unicode
  Tokens -> Paste from unicode
@end example

Both of these are necessarily approximate.  The buffer presentation
may use additional controls (for super/subscript layout or bold fonts,
etc), which cannot be converted.  Pasting relies on being able to
identify a unique token mapped from a single Unicode character; the
token table may not include such an entry, or may be ambiguous.

@c TEXI DOCSTRING MAGIC: unicode-tokens-copy
@deffn Command unicode-tokens-copy beg end
Copy presentation of region between @var{beg} and @var{end}.@*
This is an approximation; it makes assumptions about the behaviour
of symbol compositions, and will lose layout information.
@end deffn

@c TEXI DOCSTRING MAGIC: unicode-tokens-paste
@deffn Command unicode-tokens-paste 
Paste text from clipboard, converting Unicode to tokens where possible.
@end deffn

If you are using a mixture of ``real'' Unicode and tokens like this
you may want to be careful to check the buffer contents: the command
@code{unicode-tokens-highlight-unicode} helps you to manage this.
It
is available on the Tokens menu as
@example
  Tokens -> Highlight Real Unicode Chars
@end example
Alternative ways to check are to toggle the display of tokens using
@example
  Tokens -> Reveal Symbol Tokens
@end example
(the similar entry for @code{Control Tokens} displays tokens being used
to control layout).  Or simply toggle the tokens mode, which will leave
the true Unicode tokens untouched.


@c TEXI DOCSTRING MAGIC: unicode-tokens-highlight-unicode
@defvar unicode-tokens-highlight-unicode 
Non-nil to highlight Unicode characters.
@end defvar


@node Finding available tokens shortcuts and symbols
@section Finding available tokens shortcuts and symbols

Two commands (both on the Tokens menu) allow you to see the tokens and
shortcuts available:
@example
        Tokens -> List Tokens
        Tokens -> List Shortcuts
@end example

Additionally, you can view the complete Unicode character set available
in the default Emacs font, with
@example
        Tokens -> List Unicode Characters
@end example
(this uses a list adapted from Norman Walsh's @code{unichars.el}).

Note that the Unicode Tokens modes displays symbols defined by
symbol tokens in a special font.


@c TEXI DOCSTRING MAGIC: unicode-tokens-list-tokens
@deffn Command unicode-tokens-list-tokens 
Show a buffer of all tokens.
@end deffn

@c TEXI DOCSTRING MAGIC: unicode-tokens-list-shortcuts
@deffn Command unicode-tokens-list-shortcuts 
Show a buffer of all the shortcuts available.
@end deffn

@c TEXI DOCSTRING MAGIC: unicode-tokens-list-unicode-chars
@deffn Command unicode-tokens-list-unicode-chars 
Insert each Unicode character into a buffer.@*
Lets you see which characters are available for literal display
in your Emacs font.
@end deffn
@node Selecting suitable fonts
@section Selecting suitable fonts

The precise set of symbol glyphs that are available to you will depend
in complicated ways on your operating system, Emacs version,
configuration options used when Emacs was compiled, installed font sets,
and (even) command line options used to start Emacs.  So it is hard to
give comprehensive and accurate advice in this manual.  In general,
things work @i{much} better with Emacs 23 than earlier versions.

To improve flexibility, Unicode Tokens mode allows you to select another
font to display symbols from the default font that is used to display
text in the buffer.    This is the font that is configured by the menu
@example
        Tokens -> Set Fonts -> Symbol
@end example
its customization name is @code{unicode-tokens-symbol-font-face}, but
notice that only the font family aspect of the face is used.  Similarly,
other fonts can be configured for controling different font families
(script, fraktur, etc).

For symbols, good results are possible by using a proportional font for
displaying symbols that has many symbol glyphs, for example the main font
StixGeneral font from the Stix Fonts project
(@uref{http://www.stixfonts.org/}).  At the time of writing you can
obtain a beta version of these fonts in TTF format from
@uref{http://olegueret.googlepages.com/stixfonts-ttf}.  On recent Linux
distributions and with an Emacs 23 build that uses Xft, simply copy
these @code{ttf} files into the @code{.fonts} directory inside your home
directory to make them available.

Another font I like is @b{DejaVu Sans Mono}.  It covers all of the
standard Isabelle symbols.  Some of the symbols are currently not
perfect; however this font is an open source effort so users can
contribute or suggest improvements.  See @uref{http://dejavu-fonts.org}.

If you are stuck with Emacs 22, you need to use the @i{fontset}
mechanism which configures sets of fonts to use for display.  The
default font sets may not include enough symbols (typical symptom:
symbols display as empty boxes).  To address this, the menu command 
@example
        Tokens -> Set Fonts -> Make Fontsets
@end example
constructs a number of fontsets at particular point sizes, based on
several widely available fonts.  See @code{pg-fontsets.el} for the code.
After running this command, you can select from additional fontsets from
the menus for changing fonts.


For further suggestions, please search (and contribute!) to the Proof
General wiki at @uref{http://proofgeneral.inf.ed.ac.uk/wiki}.


@c TEXI DOCSTRING MAGIC: unicode-tokens-symbol-font-face
@deffn Face unicode-tokens-symbol-font-face 
The default font used for symbols.  Only :family and :slant attributes are used.
@end deffn
@c TEXI DOCSTRING MAGIC: unicode-tokens-font-family-alternatives
@defvar unicode-tokens-font-family-alternatives 
Not documented.
@end defvar
@c =================================================================
@c 
@c  CHAPTER:  Support for other Packages
@c
@node Support for other Packages
@chapter Support for other Packages

Proof General makes some configuration for other Emacs packages which
provide various useful facilities that can make your editing
more effective.

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 include
@code{font-lock}, 
@code{imenu} and @code{speedbar},
@code{outline-mode},
@code{completion},
and @code{etags}.


@menu
* Syntax highlighting::         
* Imenu and Speedbar::
* Support for outline mode::    
* Support for completion::            
* Support for tags::            
@end menu

@node Syntax highlighting
@section Syntax highlighting
@vindex coq-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}.

To automatically switch on fontification in Emacs, you may need
to engage @code{M-x global-font-lock-mode}.  

By the way, the choice of colour, font, etc, for each kind of markup is
fully customizable in Proof General.  Each @emph{face} (Emacs
terminology) is controlled by its own customization setting.
You can display a list of all of them using the customize
menu: 
@lisp
Proof General -> Advanced -> Customize -> Faces -> Proof Faces.
@end lisp

@node Imenu and Speedbar
@section Imenu and Speedbar
@vindex proof-goal-with-hole-regexp
@vindex proof-goal-with-hole-result
@c FIXME: should be see alsos.
@cindex Speedbar
@cindex Imenu
@cindex index menu

The Emacs package @code{imenu} (Index Menu) provides a menu built from
the names of entities (e.g., theorems, definitions, etc) declared in a
buffer.  This allows easy navigation within the file.  Proof General
configures both packages automatically so that you can quickly jump to
particular proofs in a script buffer.

(Developers note: the automatic configuration is done with the settings
@code{proof-goal-with-hole-regexp} and
@code{proof-save-with-hole-regexp}.  Better configuration may be made
manually with several other settings, see the @i{Adapting Proof General}
manual for further details).

To use Imenu, select the option
@lisp
        Proof-General -> Quick Options -> Minor Modes -> Index Menu
@end lisp
This adds an "Index" menu to the main menu bar for proof script buffers.
You can also use @kbd{M-x imenu} for keyboard-driven completion of tags
built from names in the buffer.

Speedbar displays a file tree in a separate window on the display,
allowing quick navigation.  Middle/double-clicking or pressing @kbd{+}
on a file icon opens up to display tags (definitions, theorems, etc)
within the file.  Middle/double-clicking on a file or tag jumps to that
file or tag.

To use Speedbar, use 
@lisp
        Proof-General -> Quick Options -> Minor Modes -> Speedbar 
@end lisp
If you prefer the old fashioned way, `M-x speedbar' does
the same job.

For more information about Speedbar,
see @uref{http://cedet.sourceforge.net/speedbar.shtml}.


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

@c 3.5: this remark taken from BUGS
Please note that outline-mode may not work well in processed proof
script files, because of read-only restrictions of the protected region.
This is an inherent problem with outline because it works by modifying
the buffer.  If you want to use outline with processed scripts, you
can turn off the @code{Strict Read Only} option. 

See @inforef{Outline Mode, ,emacs} for more information about outline mode.

@node Support for completion
@section Support for completion
@cindex completion

You might find the @emph{completion} facility of Emacs useful when
you're using Proof General.  The key @kbd{C-RET} is defined to invoke
the @code{complete} command.  Pressing @kbd{C-RET} cycles through
completions displaying hints in the minibuffer.

Completions are filled in according to what has been recently typed,
from a database of symbols.  The database is automatically saved at
the end of a session.

Proof General has the additional facility for setting a completion table
for each supported proof assistant, which gets loaded into the
completion database automatically.  Ideally the completion table would
be set from the running process according to the identifiers available
are within the particular context of a script file.  But until this is
available, this table may be set to contain a number of standard
identifiers available for your proof assistant.

The setting @code{@emph{PA}-completion-table} holds the list of
identifiers for a proof assistant.  The function
@code{proof-add-completions} adds these into the completion
database.

@c TEXI DOCSTRING MAGIC: PA-completion-table
@defvar PA-completion-table 
List of identifiers to use for completion for this proof assistant.@*
Completion is activated with M-x complete.

If this table is empty or needs adjusting, please make changes using
@samp{@code{customize-variable}} and post suggestions at
https://github.com/ProofGeneral/PG/issues
@end defvar

The completion facility uses a library @file{completion.el} which
usually ships with Emacs, and supplies the @code{complete} function.

@c FIXME: edited from default.
@c NOT DOCSTRING MAGIC: complete
@deffn Command complete 
Fill out a completion of the word before point.  @*
Point is left at end.  Consecutive calls rotate through all possibilities.
Prefix args:
@table @kbd
@item C-u
leave point at the beginning of the completion, not the end.
@item a number
rotate through the possible completions by that amount
@item 0
same as -1 (insert previous completion)
@end table
See the comments at the top of @samp{completion.el} for more info.
@end deffn


@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 Coq) are
supplied with external programs (@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
tags 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 (or may be taken by the window manager), Proof
General doesn't do this automatically.

Apart from completion, there are several other operations on tags.  One
common one is replacing identifiers across all files using
@code{tags-query-replace}.  For more information on how to use tags,
@inforef{Tags, ,emacs}.

To use tags for completion at the same time as the completion mechanism
mentioned already, you can use the command @kbd{M-x add-completions-from-tags-table}.

@c TEXI DOCSTRING MAGIC: add-completions-from-tags-table
@deffn Command add-completions-from-tags-table 
Add completions from the current tags table.
@end deffn


@c =================================================================
@c
@c CHAPTER: Proof by Pointing
@c 
@node Subterm Activation and Proof by Pointing
@chapter Subterm Activation and 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 4.4, this support has existed only for LEGO and
proof-by-pointing functionality has been temporarily removed from the
interface.  If you would like to see subterm activation 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 some 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 mouse-1
@code{pg-goals-button-action}
@item C-mouse-3
@code{proof-undo-and-delete-last-successful-command}
@c @item mouse-3
@c @code{pg-goals-yank-subterm}
@item C-S-mouse-1
@code{pg-identifier-under-mouse-query}
@end table

Where @kbd{mouse-1} indicates the left mouse button, and @kbd{mouse-3}
indicates the right hand mouse button.  The functions available provide
a way to construct commands automatically (@code{pg-goals-button-action})
and to inspect identifiers (@code{pg-identifier-under-mouse-query}) as
the Info toolbar button does.

Proof-by-pointing is a cute idea.  It lets you automatically construct
parts of a proof by clicking.  You can ask 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 comment use the
control key with the right button to undo the step and delete it from
your script (@code{proof-undo-and-delete-last-successful-command}).

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.

The main function for proof-by-pointing is @code{pg-goals-button-action}.

@c TEXI FIXME DOCSTRING MAGIC: pg-goals-button-action
@deffn Command pg-goals-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.

@c The right-hand mouse button provides this convenient way to copy
@c subterms from the goals buffer, using the function
@c @code{pg-goals-yank-subterm}.

@c TEXI FIXME DOCSTRING MAGIC: pg-goals-yank-subterm
@c @deffn Command pg-goals-yank-subterm event
@c Copy the subterm indicated by the mouse-click @var{event}.@*
@c This function should be bound to a mouse button in the Proof General
@c goals buffer.

@c The @var{event} is used to find the smallest subterm around a point.  The
@c subterm is copied to the @samp{@code{kill-ring}}, and immediately yanked (copied)
@c into the current buffer at the current cursor position.

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

@c TEXI DOCSTRING MAGIC: pg-identifier-under-mouse-query
@deffn Command pg-identifier-under-mouse-query event
Query the prover about the identifier near mouse click @var{event}.
@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
@c CHAPTER
@c
@node Graphical Proof-Tree Visualization
@chapter Graphical Proof-Tree Visualization
@cindex proof-tree visualization

Since version 4.2, Proof General supports proof-tree
visualization on graphical desktops via the additional program
Prooftree. Currently, proof-tree visualization is only supported
for the Coq proof assistant. 

This version of Proof General requires Prooftree version 0.11.
Check the @uref{http://askra.de/software/prooftree/, Prooftree website},
to see if some later versions are also compatible. (Because of
the communication protocol, Proof General is always only
compatible with certain versions of Prooftree.)


For installation instructions and
more detailed information about Prooftree, please refer to the
@uref{http://askra.de/software/prooftree/, Prooftree website} and
the @uref{http://askra.de/software/prooftree/prooftree.man.html,
Prooftree man page}. For information about how to support
proof-tree visualization for a different proof assistant, see
Section @i{Configuring Proof-Tree Visualization} in the
@i{Adapting Proof General} manual.

@menu
* Starting and Stopping Proof-Tree Visualization::
* Features of Prooftree::
* Prooftree Customization::
@end menu


@node Starting and Stopping Proof-Tree Visualization
@section Starting and Stopping Proof-Tree Visualization

When proof-tree visualization is supported (currently only for
the Coq proof assistant), you can start the visualization via the
proof-tree button in the tool-bar, via the menu 
@lisp
   Proof-General -> Start/Stop Prooftree
@end lisp
or via the keyboard shortcut @kbd{C-c C-d}, all of which invoke
@code{proof-tree-external-display-toggle}.

If you are inside a proof, the graphical display is started
immediately for your current proof. Otherwise the display starts
as soon as you start the next proof. Starting the proof-tree
display in the middle of a proof involves an automatic
reexecution of your current proof script in the locked region,
which should be almost unnoticeable, except for the time it
takes.

The proof-tree display stops at the end of the proof or when you
invoke @code{proof-tree-external-display-toggle} by one of the
three indicated means again. Alternatively you can also close the
proof-tree window. 

Proof General launches only one instance of Prooftree,
which can manage an arbitrary amount of proof-tree windows. 

@node Features of Prooftree
@section Features of Prooftree

The proof-tree window provides visual information about the
status of the different branches in your proof (by coloring
completely proved branches in green, for example) and means for
inspecting previous proof states without the need to retract
parts of your proof script. Currently, Prooftree provides
the following features:

@itemize @bullet
@item Navigation in the proof tree and display of all previous
proof states and proof commands.
@item Display branches of the proof in different colors according to
their proof state, distinguishing branches with open, partially
or fully instantiated existential variables as well as branches
that have been finished by a cheating command such as
@code{admit}.
@item Display the status of existential variables and their
dependencies.
@item Mark proof commands that introduce or instantiate a
given existential variable.
@item Snapshots of proof trees for reference when you retract
your proof to try a different approach.
@item Trigger a retract (undo) operation with a selected sequent
as target.
@item Insert proof scripts from the proof tree in the current buffer.
@end itemize

For a more elaborated description please consult the help dialog
of Prooftree or the
@uref{http://askra.de/software/prooftree/prooftree.man.html,
Prooftree man page}.


@node Prooftree Customization
@section Prooftree Customization

The location of the Prooftree program and command line
arguments can be configured in the customization group
@code{proof-tree}. You can visit this customization group inside
a running instance of Proof General by typing @code{M-x
customize-group <RET> proof-tree <RET>}.

The graphical aspects of the proof-tree rendering, fonts and
colors can be changed inside Prooftree by invoking the
@code{Configuration} item of the main menu.

Prover specific parts such as the regular expressions for
recognizing subgoals, existential variables and navigation and
cheating commands are in the customization group
@code{proof-tree-internals}. Under normal circumstances there
should be no need to change one of these internal settings. 


@c =================================================================
@c
@c CHAPTER
@c
@node Customizing Proof General
@chapter Customizing Proof General
@cindex Customization


There are two ways of customizing 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.
The latter kind of customization we call instantiation, or
@emph{adapting}. See the @i{Adapting Proof General} manual for how to do
this.  Here we cover the user-level customization for Proof General.

There are two kinds of user-level settings in Proof General: 
@itemize @bullet
@item Settings that apply @emph{globally} to all proof assistants.
@item those that can be adjusted for each proof assistant @emph{individually}.
@end itemize
The first sort have names beginning with @code{proof-}.  The second sort
have names which begin with a symbol corresponding to the proof
assistant: for example, @code{isa-}, @code{coq-}, etc.  The symbol is
the root of the mode name.  @xref{Quick start guide}, for a table of the
supported modes.  To stand for an arbitrary proof assistant, we write
@code{@emph{PA}-} for these names.

In this chapter we only consider the generic settings: ones which apply
to all proof assistants (globally or individually).  The support for a
particular proof assistant may provide extra individual customization
settings not available in other proof assistants.  See the chapters
covering each assistant for details of those settings.


@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 common options which you can toggle directly from
the menu:
@lisp
   Proof-General -> Quick 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 the current settings for these options (only), use the Save
Options command in the submenu:
@lisp
   Proof-General -> Quick 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.  For this you need
to know a little bit about how to customize in Emacs.


@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 -> Advanced -> 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.  The command @kbd{M-x customize-save-customized} or Emacs menubar 
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.  Use the menu:
@lisp
   Options -> Customize Emacs -> 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{Customization, ,emacs}.



@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
@cindex auto raise

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 (@code{*goals*}) or the response
buffer (@code{*response*}).  Proof General raises and switches between
these last two automatically.  

Proof General allows several ways to customize this default display
model, by splitting the Emacs frames in different ways and maximising
the amount of information shown, or by using multiple frames.
The customization options are explained below; they are also available 
on the menu:
@lisp
  Proof-General -> Quick Options -> Display
@end lisp
and you can save your preferred default. 

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-three-window-enable} to
make Proof General keep both the goals and response buffer displayed.

If you prefer to switch windows and buffers manually when you want to
see the prover output, you can customize the user option
@code{proof-auto-raise-buffers} to prevent the automatic behaviour.
You can browse interaction output by hovering the mouse over the
command regions in the proof script.

@c TEXI DOCSTRING MAGIC: proof-auto-raise-buffers
@defopt proof-auto-raise-buffers 
If non-nil, automatically raise buffers to display latest output.@*
If this is not set, buffers and windows will not be managed by
Proof General.

The default value is @code{t}.
@end defopt
@c TEXI DOCSTRING MAGIC: proof-three-window-enable
@defopt proof-three-window-enable 
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.

The default value is @code{t}.
@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-three-window-mode}.

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-three-window-mode} is on.


Finally, there are two commands available which help to switch between
buffers or refresh the window layout.  These are on the menu:
@lisp
  Proof-General -> Buffers
@end lisp

@c TEXI DOCSTRING MAGIC: proof-display-some-buffers
@deffn Command proof-display-some-buffers 
Display the response, trace, goals, or shell buffer, rotating.@*
A fixed number of repetitions of this command switches back to
the same buffer.
Also move point to the end of the response buffer if it's selected.
If in three window or multiple frame mode, display two buffers.
The idea of this function is to change the window->buffer mapping
without adjusting window layout.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-layout-windows
@deffn Command proof-layout-windows 
Refresh the display of windows according to current display mode.

For multiple frame mode, this function obeys the setting of
@samp{@code{pg-response-eagerly-raise}}, which see.

For single frame mode:

- In two panes mode, this uses a canonical layout made by splitting
Emacs windows in equal proportions.  The splitting is vertical if
Emacs width is smaller than @samp{@code{split-width-threshold}} and
horizontal otherwise.  You can then adjust the proportions by
dragging the separating bars.

- In three pane mode, there are three display modes, depending
@lisp
  where the three useful buffers are displayed: scripting
  buffer, goals buffer and response buffer.

  Here are the three modes:

  - vertical: the 3 buffers are displayed in one column.
  - hybrid: 2 columns mode, left column displays scripting buffer
    and right column displays the 2 others.
  - horizontal: 3 columns mode, one for each buffer (script, goals,
    response).

  By default, the display mode is automatically chosen by
  considering the current Emacs frame width: if it is smaller
  than @samp{@code{split-width-threshold}} then vertical mode is chosen,
  otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}}
  then hybrid mode is chosen, finally if the frame is larger than
  1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen.

  You can change the value of @samp{@code{split-width-threshold}} at your
  will.

  If you want to force one of the layouts, you can set variable
  @samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or
  @code{'hybrid}.  The default value is @code{'smart} which sets the automatic
  behaviour described above.
@end lisp
@end deffn

@c TEXI DOCSTRING MAGIC: proof-shrink-windows-tofit
@defopt proof-shrink-windows-tofit 
If non-nil, automatically shrink output windows to fit contents.@*
In single-frame mode, this option will reduce the size of the
goals and response windows to fit their contents.

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

@c TEXI DOCSTRING MAGIC: proof-colour-locked
@defopt proof-colour-locked 
If non-nil, colour the locked region with @samp{@code{proof-locked-face}}.@*
If this is not set, buffers will have no special face set
on locked regions.

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

@c TEXI DOCSTRING MAGIC: proof-output-tooltips
@defopt proof-output-tooltips 
Non-nil causes Proof General to add tooltips for prover output.@*
Hovers will be added when this option is non-nil.  Prover outputs
can be displayed when the mouse hovers over the region that
produced it and output is available (see @samp{@code{proof-full-annotation}}).
If output is not available, the type of the output region is displayed.
Changes of this option will not be reflected in already-processed
regions of the script.

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



@node User options
@section User options
@c Index entries for each option 'concept'
@cindex User options
@cindex Strict read-only
@cindex Undo in read-only region
@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
@cindex Input ring
@c @cindex formatting proof script

Here is a list of the important user options for Proof General, apart from
the 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{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-next-command-insert-space
@defopt proof-next-command-insert-space 
If non-nil, PG will use heuristics to insert newlines or spaces in scripts.@*
In particular, if electric terminator is switched on, spaces or newlines will
be inserted as the user types commands to the prover.

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

@c TEXI DOCSTRING MAGIC: proof-toolbar-enable
@defopt proof-toolbar-enable 
If non-nil, display Proof General toolbar for script buffers.

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

@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: PA-script-indent
@defopt PA-script-indent 
If non-nil, enable indentation code for proof scripts.

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

@c TEXI DOCSTRING MAGIC: PA-one-command-per-line
@defopt PA-one-command-per-line 
If non-nil, format for newlines after each command in a script.

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

@c TEXI DOCSTRING MAGIC: proof-omit-proofs-option
@defvar proof-omit-proofs-option 
Set to t to omit complete opaque proofs for speed reasons.@*
When t, complete opaque proofs in the asserted region are not
sent to the proof assistant (and thus not checked). For files
with big proofs this can drastically reduce the processing time
for the asserted region at the cost of not checking the proofs.
For partial and non-opaque proofs in the asserted region all
proof commands are sent to the proof assistant.

Using a prefix argument for @samp{@code{proof-goto-point}} (M-x @code{proof-goto-point})
or @samp{@code{proof-process-buffer}} (M-x @code{proof-process-buffer}) temporarily
disables omitting proofs.
@end defvar

@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: PA-prog-args
@defvar PA-prog-args 
Arguments to be passed to @samp{@code{proof-prog-name}} to run the proof assistant.@*
If non-nil, will be treated as a list of arguments for @samp{@code{proof-prog-name}}.
Otherwise @samp{@code{proof-prog-name}} will be split on spaces to form arguments.

Remark: Arguments are interpreted strictly: each one must contain only one
word, with no space (unless it is the same word). For example if the
arguments are -x foo -y bar, then the list should be '("-x" "foo"
"-y" "bar"), notice that '("-x foo" "-y bar") is @strong{wrong}.
@end defvar

@c TEXI DOCSTRING MAGIC: PA-prog-env
@defvar PA-prog-env 
Modifications to @samp{@code{process-environment}} made before running @samp{@code{proof-prog-name}}.@*
Each element should be a string of the form ENVVARNAME=@var{value}.  They will be
added to the environment before launching the prover (but not pervasively).
For example for coq on Windows you might need something like:
(setq @code{coq-prog-env} '("HOME=C:\Program Files\Coq\"))
@end defvar

@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 @samp{@code{proof-prog-name}}.@*
This option is compatible with @samp{@code{proof-prog-name-ask}}.
No effect if @samp{@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-keep-response-history
@defopt proof-keep-response-history 
Whether to keep a browsable history of responses.@*
With this feature enabled, the buffers used for prover responses will have a
history that can be browsed without processing/undoing in the prover.
(Changes to this variable take effect after restarting the prover).

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

@c TEXI DOCSTRING MAGIC: pg-input-ring-size
@defopt pg-input-ring-size 
Size of history ring of previous successfully processed commands.

The default value is @code{32}.
@end defopt
@c TEXI DOCSTRING MAGIC: proof-general-debug
@defopt proof-general-debug 
Non-nil to run Proof General in debug mode.@*
This changes some behaviour (e.g. markup stripping) and displays
debugging messages in the response buffer.  To avoid erasing
messages shortly after they're printed, set @samp{@code{proof-tidy-response}} to nil.
This is only useful for PG developers.

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{'followdown}, @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{'followdown}, point if necessary to stay in writeable region
If @code{'ignore}, point is never moved after movement commands or on errors.

If you choose @code{'ignore}, you can find the end of the locked using
M-x @code{proof-goto-end-of-locked}

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.

For some proof assistants (such as Coq) fully processed buffers make
no sense.  Setting this option to @code{'process} has then the same effect
as leaving it unset (nil).  (This behaviour is controlled by
@samp{@code{proof-no-fully-processed-buffer}}.)

The default value is @code{nil}.
@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 coqtop}
to start Coq 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.  For proper
behaviour with interrupts, the program should also communicate
signals to the remote host.

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




@node Changing faces
@section Changing faces

The numerous 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!

@menu
* Script buffer faces::
* Goals and response faces::
@end menu

@node Script buffer faces
@subsection Script buffer faces

@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-script-sticky-error-face
@deffn Face proof-script-sticky-error-face 
Proof General face for marking an error in the proof script. 
@end deffn
@c TEXI DOCSTRING MAGIC: proof-script-highlight-error-face
@deffn Face proof-script-highlight-error-face 
Proof General face for highlighting an error in the proof script. 
@end deffn
@c TEXI DOCSTRING MAGIC: proof-mouse-highlight-face
@deffn Face proof-mouse-highlight-face 
General mouse highlighting face used in script buffer.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-highlight-dependent-face
@deffn Face proof-highlight-dependent-face 
Face for showing (backwards) dependent parts.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-highlight-dependency-face
@deffn Face proof-highlight-dependency-face 
Face for showing (forwards) dependencies.
@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


@node Goals and response faces
@subsection Goals and response faces

@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-boring-face
@deffn Face proof-boring-face 
Face for boring text in proof assistant output.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-active-area-face
@deffn Face proof-active-area-face 
Face for showing active areas (clickable regions), outside of subterm markup.
@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 @i{Adapting Proof General} for full details.  To browse
the settings, 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 Coq code from the value
of the customization setting @code{coq-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 configuration
settings editable in Customize, by shadowing the settings as 
prover specific ones using the @code{@emph{PA}-} mechanism).
@c Please contact us if this proves to be a problem for any variable.



@c =================================================================
@c
@c CHAPTER
@c
@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 a bit of 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
* Adding your own keybindings::
* Using file variables::
* Using abbreviations::
@end menu

@node Adding your own keybindings
@section Adding your own keybindings
@cindex keybindings

Proof General follows Emacs convention for file modes in using @key{C-c}
prefix key-bindings for its own functions, which is why some of the
default keyboard short-cuts are quite lengthy.

Some users may prefer to add additional key-bindings for shorter
sequences.  This can be done interactively with the command
@code{M-x local-set-key}, or for longevity, by adding 
code like this to your @file{.emacs} file:
@lisp

(eval-after-load "proof-script" '(progn
 (define-key proof-mode-map [(control n)] 
                            'proof-assert-next-command-interactive)
 (define-key proof-mode-map [(control b)] 
                            'proof-undo-last-successful-command)
 ))
@end lisp

This lisp fragment adds bindings for every buffer in proof script
mode (the Emacs keymap is called @code{proof-mode-map}).  To just
affect one prover, use a keymap name like @code{coq-mode-map} and
evaluate after the library @code{coq} has been loaded.

To find the names of the functions you may want to bind, look in this
manual, or query current bindings interactively with @kbd{C-h k}.  This
command (@code{describe-key}) works for menu operations as well; also
use it to discover the current key-bindings which you're losing by
declarations such as those above.  By default, @kbd{C-n} is
@code{next-line} and @kbd{C-b} is @code{backward-char-command}; neither
are really needed if you have working cursor keys.


If your keyboard has a @i{super} modifier (on my
PC keyboard it has a Windows symbol and is next to the control key), you
 can freely bind keys on that modifier globally (since none are used
by default).  Use lisp like this:
@lisp
(global-set-key [?\s-l] 'maths-menu-insert-lambda)
(global-set-key [?\s-l] 'maths-menu-insert-lambda)

(global-set-key [?\s-l] 'maths-menu-insert-lambda)
(global-set-key [?\s-L] 'maths-menu-insert-Lambda)
(global-set-key [?\s-D] 'maths-menu-insert-Delta)

(global-set-key [?\s-a] 'maths-menu-insert-for-all)
(global-set-key [?\s-e] 'maths-menu-insert-there-exists)
(global-set-key [?\s-t] 'maths-menu-insert-down-tack)
(global-set-key [?\s-b] 'maths-menu-insert-up-tack)

(global-set-key [?\s-\#] 'maths-menu-insert-music-sharp-sign)
(global-set-key [?\s-\.] 'maths-menu-insert-horizontal-ellipsis)

(global-set-key [?\s-3] 'proof-three-window-toggle)
@end lisp
This defines a bunch of short-cuts for inserting symbols taken
from the Maths Menu, @pxref{Unicode symbols and special layout support}
and a short-cut for enabling three window mode,
@pxref{Display customization}.


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

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

@b{Remark 1:} The examples in the following are for Coq but the
trick is applicable to other provers. 

@b{Remark 2:} For Coq specifically, there is a recommended other way of
configuring Coq command-line options: project files (@ref{Using the Coq
project file}). However file variables are useful to set a specific
@code{coqtop} executable, or for defining file-specific command-line
options. Actually, since project files are intended to be included in
the distribution of a library (and included in its repository), the file
variables can be used to set non versioned options like
@code{coq-prog-name}.

@b{Remark 3:} For obvious security reasons, when emacs reads file
variables, it asks for permission to the user before applying the
assignment. You should read carefully the content of the variable before
accepting. You can hit @code{!} to accept definitely the exact values at
hand.

Let us take a concrete example: suppose the makefile for @file{foo.v} is
located in directory @file{.../dir/}, you need the right compile command
in the @code{compile-command} emacs variable. Moreover suppose that you
want @code{coqtop} to be found in a non standard directory. To put these
values in file variables, here is what you should put at the end of
@file{foo.v}:

@lisp
(* 
*** Local Variables: ***
*** coq-prog-name: "../../coqsrc/bin/coqtop" ***
*** 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, and the correct @code{coqtop} will be called by
ProofGeneral. Note that the lines are commented in order to be ignored
by the proof assistant. It is possible to use this mechanism for all
variables, @inforef{File Variables, ,emacs}.

@emph{NOTE:} @code{coq-prog-name} should contain only the @code{coqtop}
executable, @emph{not the options}.

One can also specify file variables on a per directory basis,
@inforef{Directory Variables, ,emacs}. You can achieve almost the same
as above for all the files of a directory by storing

@lisp
((coq-mode . ((coq-prog-name . "/home/xxx/yyy/coqsrc/bin/coqtop")
              (compile-command . "make -C .. -k"))))
@end lisp

into the file @code{.dir-locals.el} in one of the parent directories.
The value in this file must be an alist that maps mode names to alists,
where these latter alists map variables to values. You can aso put
arbitrary code in this file @inforef{Directory Variables, ,emacs}.

@emph{Note:} if you add such content to the @code{.dir-locals.el} file
you should restart Emacs or revert your buffer.

@node Using abbreviations
@section Using abbreviations

A very useful package of Emacs supports automatic expansions of
abbreviations as you type, @inforef{Abbrevs, ,emacs}.

For example, the proof assistant Coq has many command strings that are
long, such as ``reflexivity,'' ``Inductive,'' ``Definition'' and
``Discriminate.''  Here is a part of the Coq Proof General
abbreviations:
@lisp
"abs" "absurd "
"ap" "apply "
"as" "assumption"
@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 automatic
expansion of abbreviations (which can be annoying), the @code{Abbrev}
minor mode, type @kbd{M-x abbrev-mode RET}. When you are not in Abbrev
mode you can expand an abbreviation by pressing @kbd{C-x '}
(@code{expand-abbrev}). See the Emacs manual for more details.


@c =================================================================
@c
@c  CHAPTER: Coq Proof General
@c
@node Coq Proof General
@chapter Coq Proof General

@macro coqrefman {sectionurl,txt}
@uref{https://coq.inria.fr/distrib/current/refman/\sectionurl\,\txt\}
@end macro

Coq Proof General is an instantiation of Proof General for the Coq proof
assistant.  It supports most of the generic features of Proof General.

@menu
* Coq-specific commands::
* Using the Coq project file::
* Proof using annotations::
* Multiple File Support::
* Omitting proofs for speed::
* Editing multiple proofs::
* User-loaded tactics::
* Indentation tweaking::
* Holes feature::
* Proof-Tree Visualization::
* Showing Proof Diffs::
* Opam-switch-mode support::
@end menu


@node Coq-specific commands
@section Coq-specific commands
@kindex C-c C-a C-i
@kindex C-c C-a C-a
@kindex C-c C-a C-b
@kindex C-c C-a C-s
@kindex C-c C-a C-)
@kindex C-c C-a C-p
@kindex C-c C-a C-c
@kindex C-c C-a C-o

Coq Proof General supplies the following key-bindings:
@table @kbd
@item C-c C-a C-i   
Inserts ``intros '' and also introduces the name of the hypothesis
proposed by coq on the current goal.

@item C-c C-a C-s
Show the goal (enter for the current goal, i <enter> for the ith goal).

Add the prefix C-u to see the answer with all pretty printing options
temporarily disable (Set Printing All).

@item C-c C-a C-c   
Prompts for ``Check '' query arguments, the default input name is built
from the identifier under the cursor.

Add the prefix C-u to see the answer with all pretty printing options
temporarily disable (Set Printing All).

@item C-c C-a C-p
The same for a ``Print '' query.
@item C-c C-a C-b
The same for a ``About '' query.
@item C-c C-a C-a
The same for a ``Search '' query (no C-u prefix).
@item C-c C-a C-o
The same for a Search ``SearchIsos'' (no C-u prefix).

@item C-c C-a C-)
Inserts ``End <section-name>.'' (this should work well with nested sections).
@end table



@node Using the Coq project file
@section Using the Coq project file

The Coq project file is the recommended way to configure the Coq
load path and the mapping of logical module names to physical
file path (-R,-Q,-I options). The project file is typically named
@code{_CoqProject} and must be located at the directory root of
your Coq project. Proof General searches for the Coq project file
starting at the current directory and walking the directory
structure upwards. The Coq project file contains the common
options (especially @code{-R}) and a list of the files of the
project, see the Coq reference manual, Section
@coqrefman{practical-tools/utilities.html#building-a-coq-project,
``Building a Coq project''}.


@c @uref{https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html#building-a-coq-project,
@c ``Building a Coq project''}.

The Coq project file should contain something like:

@verbatim
-R foo bar
-I foo2
-arg -foo3
file.v
bar/other_file.v
...
@end verbatim

Proof General only extracts the common options from the Coq
project file and uses them for @code{coqtop} background
processes as well as for @code{coqdep} and @code{coqc} when you use
the auto compilation feature, @ref{Automatic Compilation in
Detail}. For the example above, Proof General will start
@code{coqtop -emacs -foo3 -R foo bar -I foo2} (remark:
@code{-emacs} is always added to the options).

@emph{NOTE:} @code{-arg} must be followed by one and only one option
to pass to coqtop/coqc, use several @code{-arg} to issue several
options. One per line (limitation of Proof General).

For backward compatibility, one can also configure the load path
with the option @code{coq-load-path}, but this is not compatible
with @code{CoqIde} or @code{coq_makefile}.

@emph{NOTE:} the Coq project file cannot define which version of
@code{coqtop} is launched. You need either to launch emacs with the
right executable in the path or use @inforef{File Variables, ,emacs} or
@inforef{Directory Variables, ,emacs}. See @ref{Using file variables}
below.

@menu
* Changing the name of the coq project file::
* Disabling the coq project file mechanism::
@end menu

@node Changing the name of the coq project file
@subsection Changing the name of the coq project file

To change the name of the Coq project file, configure
@code{coq-project-filename} (select menu @code{Proof-General ->
Advanced -> Customize -> Coq} and scroll down to ``Coq Project
Filename''). Customizing @code{coq-project-filename} this way
will change the Coq project file name permanently and globally.

If you only want to change the name of the Coq project file for
one project you can set the option as local file variable,
@ref{Using file variables}. This can be done either directly in
every file or once for all files of a directory tree with a
@code{.dir-local.el} file, @inforef{Directory Variables, ,emacs}.
The file @code{.dir-local.el} should then contain

@lisp
((coq-mode . ((coq-project-filename . "myprojectfile"))))
@end lisp

Note that variables set in @code{.dir-local.el} are automatically
made buffer local (such that files in different directories can
have their independent setting of @code{coq-project-filename}).
If you make complex customizations using @code{eval} in
@code{.dir-local.el}, you might want to add appropriate calls to
@code{make-local-variable}.

Documentation of the user option @code{coq-project-filename}:

@c TEXI DOCSTRING MAGIC: coq-project-filename
@defvar coq-project-filename 
The name of coq project file.@*
The coq project file of a coq development (cf. Coq documentation on
"makefile generation") should contain the arguments given to
coq_makefile. In particular it contains the -I and -R
options (preferably one per line).  If @samp{coq-use-coqproject} is
t (default) the content of this file will be used by Proof General to
infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables that set
the coqtop invocation by Proof General.  This is now the recommended
way of configuring the coqtop invocation.  Local file variables may
still be used to override the coq project file's configuration.
.dir-locals.el files also work and override project file settings.
@end defvar


@node Disabling the coq project file mechanism
@subsection Disabling the coq project file mechanism

To disable the Coq project file feature in Proof General, set
@code{coq-use-project-file} to nil (select menu
@code{Proof-General -> Advanced -> Customize -> Coq} and scroll
down to ``Coq Use Project File'').

@c TEXI DOCSTRING MAGIC: coq-use-project-file
@defvar coq-use-project-file 
If t, when opening a Coq file read the dominating _CoqProject.@*
If t, when a Coq file is opened, Proof General will look for a
project file (see @samp{@code{coq-project-filename}}) somewhere in the
current directory or its parent directories.  If there is one,
its contents are read and used to determine the arguments that
must be given to coqtop.  In particular it sets the load
path (including the -R lib options) (see @samp{@code{coq-load-path}}).
@end defvar

You can also use the .dir-locals.el as above to configure this setting
on a per project basis.

@node Proof using annotations
@section Proof using annotations

In order to process files asynchronously and pre-compile files (.vos and
.vok files), it is advised (inside sections) to list the section
variables (and hypothesis) on which each lemma depends on. This must be
done at the beginning of a proof with this syntax:

@verbatim
Lemma foo: ... .
Proof using x y H1 H2.
@end verbatim

If the annotation is missing, then at Qed time (i.e. later in the
script) coq complains with a warning and a suggestion of a correct
annotation that should be added. ProofGeneral intercepts this suggestion
and stores relevant information. Then depending on user preference it
can either
@itemize @bullet
@item insert immediately the ``using...'' annotation after ``Proof'',
without replaying the proof.
@item highlight the place where the annotation should be inserted and
allow the user to perform the insertion later either via right click
menu on the proof or by @code{M-x coq-insert-suggested-dependency} (it
won't replay the proof)
@item ask the user each time which of the two solutions above he wants
@item ignore completely the suggestion. 
@end itemize

This can be configured either via Coq menu or by setting variable
@code{coq-accept-proof-using-suggestion} to one of the following values:
@code{'always}, @code{'highlight}, @code{'ask} or @code{'never}.

@node Multiple File Support
@section Multiple File Support

Since version 4.1 Coq Proof General has multiple file support. It
consists of the following points:

@table @asis
@item Restarting @code{coqtop} when changing the active scripting buffer
Different buffers may require different load path' or different
sets of @code{-I} options. Because Coq cannot undo changes in the
load path, Proof General is forced to restart @code{coqtop} when
the active scripting buffer changes.
@item Locking ancestors
Locking those buffers on which the current active scripting
buffer depends. This is controlled by the user option
@code{coq-lock-ancestors}, 
@ref{Customizing Coq Multiple File Support} and 
@ref{Locking Ancestors}.
@item (Re-)Compilation 
Before a @code{Require} command is processed it may be necessary
to save some buffers and compile some files. When automatic
(re-)compilation is enabled (it's off by default), one can freely
work in different buffers within one Proof General session.
Proof General will compile the
necessary files whenever a @code{Require} command is processed. 

The compilation feature does currently not support ML modules.
@end table

There are actually two implementations of the Recompilation
feature. 

@table @asis
@item Parallel asynchronous compilation (stable, default)
With parallel compilation, coqdep and coqc are launched in the
background and Proof General stays responsive during compilation.
Up to `coq-max-background-compilation-jobs' coqdep and coqc
processes may run in parallel. Compiled interfaces (@code{-vos}
for Coq 8.11 or newer) and quick compilation
(@code{-quick}/@code{-vio} for Coq 8.5 or newer) is
supported with various modes, @ref{Quick and inconsistent compilation}.
@item Synchronous single threaded compilation (obsolete)
With synchronous compilation, coqdep and coqc are called
synchronously for each Require command. Proof General is locked
until the compilation finishes. Neither quick nor vos compilation is
supported with synchronously compilation.
@end table

To enable the automatic compilation feature, you have to follow
these points:

@itemize @bullet
@item
Set the option @code{coq-compile-before-require} (menu @code{Coq
-> Auto Compilation -> Compile Before Require}) to enable
compilation before processing @code{Require} commands. By
default, this enables parallel asynchronous compilation.
@item 
Nonstandard load path elements @emph{must} be configured via a
Coq project file (this is the recommended option),
@ref{Using the Coq project file} or via
option @code{coq-load-path}. @code{-I} or @code{-R} options in
@code{coq-prog-name} or @code{coq-prog-args} must be deleted.
@item
Configure
@code{coq-max-background-compilation-jobs} if you want to limit
the number of parallel background jobs and set
@code{coq-compile-keep-going} (menu @code{Coq -> Auto Compilation
-> Keep going}) to let compilation continue after the first
error.
@end itemize

To abort parallel background compilation, use @code{C-c C-c}
(@code{proof-interrupt-process}), the tool bar interrupt icon,
the menu entry @code{Abort Background Compilation} (menu
@code{Coq -> Auto Compilation}) or kill the Coq toplevel via
@code{C-c C-x} (@code{proof-shell-exit}). To abort synchronous
single threaded compilation, simply hit @code{C-g}.


@menu
* Automatic Compilation in Detail::
* Locking Ancestors::
* Quick and inconsistent compilation::
* Customizing Coq Multiple File Support::
* Current Limitations::
@end menu


@node Automatic Compilation in Detail
@subsection Automatic Compilation in Detail

When @code{coq-compile-before-require} is enabled, Proof
General looks for @code{Require} commands in text that gets
asserted (i.e., in text that is moved from the editing region to
the queue region, @ref{Locked queue and editing regions}). If
Proof General finds a @code{Require} command, it checks the
dependencies and (re-)compiles files as necessary. The Require
command and the following text is only sent to Coq after the
compilation has finished.

@code{Declare ML Module} commands are currently not recognized
and dependencies on ML Modules reported by @code{coqdep} are
ignored.

Proof General uses @code{coqdep} to determine which libraries a
@code{Require} command will load and which files must be
up-to-date. Because Proof
General cannot know whether files are updated outside of Emacs,
it checks for every @code{Require} command the complete
dependency tree and recompiles files as necessary.

Output from the compilation is only shown in case
of errors. It then appears in the buffer
@code{*coq-compile-response*}.
One can use @code{C-x `} (bound to @code{next-error},
@inforef{Compilation Mode,,emacs}) to jump to error locations.
Sometimes the compilation commands do not produce error messages
with location information, then @code{C-x `} does only work in a
limited way.

Proof General supports both vos and quick/vio
compilation to speed up compilation of required modules at the
price of consistency. Because quick/vio compilation does not seem
to have a benefit with vos compilation present, the former is
only supported for Coq before 8.11. Both can be configured via
the settings @code{coq-compile-vos} and @code{coq-compile-quick}
and via menu entries in @code{Coq -> Auto Compilation},
@ref{Quick and inconsistent compilation}. 

Similar to @code{make -k}, background compilation can be
configured to continue as far as possible after the first error,
see option @code{coq-compile-keep-going} (menu @code{Coq -> Auto
Compilation -> Keep going}). The keep-going option applies
to errors from @code{coqdep} and @code{coqc}. However, when
starting @code{coqc} or
@code{coqdep} fails), the compilation is immediately aborted.

When a @code{Require} command causes a compilation of some files,
one may wish to save some buffers to disk beforehand. The option
@code{coq-compile-auto-save} controls how and which files are
saved. There are two orthogonal choices: One may wish to save all
or only the Coq source files, and, one may or may not want to
confirm the saving of each file. 

With `coq-compile-parallel-in-background' (menu @code{Coq ->
Settings -> Compile Parallel In Background}) you can choose
between two implementations of internal compilation.

@table @asis
@item Synchronous single threaded compilation
This is the old, now outdated version supported since Proof General
4.1. This method starts coqdep and coqc processes one after each
other in synchronous subprocesses. Your Emacs session will be
locked until compilation finishes. Use @code{C-g} to interrupt
compilation. This method supports compilation via an external
command (such as @code{make}), see option
@code{coq-compile-command} in @ref{Customizing Coq Multiple File
Support} below. Synchronous compilation does neither support
quick/vio nor vos compilation.

@item Parallel asynchronous compilation
This is the newer, recommended
and default version added in Proof General version 4.3. It
runs up to @code{coq-max-background-compilation-jobs} coqdep and
coqc jobs in parallel in asynchronous subprocesses (or uses all
your CPU cores if @code{coq-max-background-compilation-jobs}
equals @code{'all-cpus}). Your Emacs will stay responsive during
compilation. To abort the background compilation process, use
@code{C-c C-c} (@code{proof-interrupt-process}), the tool bar
interrupt icon, the menu entry @code{Abort Background
Compilation} (menu @code{Coq -> Auto Compilation}) or kill the
Coq toplevel via @code{C-c C-x} (@code{proof-shell-exit}).

For the usual case, you have at most
`coq-max-background-compilation-jobs' parallel processes
@emph{including} your Proof General process. The usual case
applies, when the Require commands are the first commands in the
file. If you have other commands between two Require commands or
before the first Require, then you may see Proof General and Coq
running in addition to `coq-max-background-compilation-jobs'
compilation jobs.

Parallel asynchronous compilation supports both vos and quick/vio
compilation, but exclusively, depending on the Coq version,
@ref{Quick and inconsistent compilation}. 
@end table


@node Locking Ancestors
@subsection Locking Ancestors


Locking ancestor files works as a side effect of dependency
checking. This means that ancestor locking does only work when
Proof General performs dependency checking and compilation
itself. If an external command is used, Proof General does not see
all dependencies and can therefore only lock direct ancestors.

In the default setting,
when you want to edit a locked ancestor, you are
forced to completely retract the current scripting buffer. 
You can simplify this by setting @code{proof-strict-read-only} to
@code{'retract} (menu @code{Proof-General -> Quick Options ->
Read Only -> Undo On Edit}). Then typing in some ancestor will
immediately retract your current scripting buffer and unlock that
ancestor.

You have two choices, if you don't like ancestor locking in its
default way.
You can either switch ancestor locking completely off via
menu @code{Coq -> Auto Compilation -> Lock Ancestors} or
@code{coq-lock-ancestors} (@ref{Customizing Coq Multiple
File Support}). Alternatively, you can generally permit editing in locked
sections with selecting 
@code{Proof-General} -> @code{Quick Options} -> @code{Read Only}
-> @code{Freely Edit} (which will set the option
@code{proof-strict-read-only} to @code{nil}).


[The right behaviour for Coq, namely to retract the current
scripting buffer only up to the appropriate @code{Require}
command, would be quite difficult to implement in the current
Proof General infrastructure. Further, it has only dubious
benefit, as Require commands are usually on the top of each
file.]


@node Quick and inconsistent compilation
@subsection Quick and inconsistent compilation

Coq now supports two different modes for speeding up compilation
at the price of consistency. Since Coq 8.11, @code{-vos} compiles
interfaces into @code{.vos} files and since Coq 8.5
@code{-quick}/@code{-vio} produces @code{.vio} files. Proof
General supports both modes with parallel asynchronous
compilation, but exclusively, depending on the detected Coq
version. For Coq 8.11 or newer only @code{-vos} can be used.
There are a number of different compilation options supported,
see below.

For Coq 8.11 or newer (decided by the automatic Coq version
detection of Proof General or by the setting
@code{coq-pinned-version}) required modules are either compiled
to @code{.vo} or @code{.vos} files, depending on the setting
@code{coq-compile-vos}, which can also be set on menu @code{Coq
-> Auto Compilation -> vos compilation}. There are four choices:

@table @asis
@item @code{vos-and-vok}
First compile using @code{-vos}, skipping proofs. When
compilation finished, run @code{coqc -vok} in a second stage to
check proofs on all files that require it. Some universe
constraints might be missed, rendering this method possibly
inconsistent.
@item @code{vos}
Only compile using @code{-vos}, skipping proofs. No @code{coqc
-vok} run to check proofs. Obviously inconsistent.
@item @code{ensure-vo}
Compile without @code{-vos} to @code{.vo} files, checking all
proofs and universe constraints. Only consistent choice.
@item unset (@code{nil})
Compile with @code{-vos} if @code{coq-compile-quick} (see below)
equals @code{quick-no-vio2vo}. Otherwise compile without
@code{-vos} to @code{.vo}. This value provides an upgrade path
for users that configured @code{coq-compile-quick} in the past.
@end table

For @code{vos-and-vok} the second @code{-vok} stage runs
asynchronously @code{coq-compile-second-stage-delay} seconds
after the last @code{Require} command has been processed. Errors
might pop up later and interrupt your normal interaction with
Coq. Because the second stage is not time critical, it runs on
@code{coq-max-background-second-stage-percentage} per cent of the
cores configured for the first stage. When
@code{coq-compile-keep-going} is configured and an error occurs,
the second @code{-vok} stage is run on those dependencies not
affected by the error.

For Coq version 8.5 until before 8.11, Proof General supports
quick or vio compilation with parallel asynchronous compilation.
There are 4 modes that can be
configured with @code{coq-compile-quick} or by selecting one of
the radio buttons in the @code{Coq -> Auto Compilation -> Quick
compilation} menu. For Coq before 8.11 @code{coq-compile-vos} is
ignored.

Value @code{no-quick} was provided for the transition, for those
that have not switched there development to
@code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick
recompilation without producing .vo files. Option
@code{quick-and-vio2vo} recompiles with @code{-quick}/@code{-vio} as
@code{quick-no-vio2vo} does, but schedules a second vio2vo stage
for missing @code{.vo} files. Finally, use
@code{ensure-vo} for only importing @code{.vo} files with
complete universe checks. 

Note that with all of @code{no-quick}, @code{quick-no-vio2vo} and
@code{quick-and-vio2vo} your development might be unsound because
proofs might have been skipped and
universe constraints are not fully present in @code{.vio} files.

There are a few peculiarities of quick compilation in Coq 8.5
and possibly also in other versions.

@itemize
@item
Quick compilation runs noticeably slower when section
variables are not declared via @code{Proof using}.
@item
Even when section variables are declared, quick compilation runs
slower on very small files, probably because of the
comparatively big size of the @code{.vio} files. You can speed up
quick compilation noticeably by running on a RAM disk.
@item
If both, the @code{.vo} and the @code{.vio} files are present,
Coq loads the more recent one, regardless of whether
@code{-quick}, and emits a warning when the @code{.vio} is more
recent than the @code{.vo}.
@item
Under some circumstances, files compiled when only the
@code{.vio} file of some library was present are not compatible
with (other) files compiled when also the @code{.vo} file of that
library was present, see Coq issue #5223 for details. As a rule
of thumb one should run vio2vo compilation only before or after
library loading.
@item
Apart from the previous point, Coq works fine when libraries are
present as a mixture of @code{.vio} and @code{.vo} files. While
@code{make} insists on building all prerequisites as either
@code{.vio} or @code{.vo} files, Proof General just checks
whether an up-to-date compiled library file is present.
@item
To ensure soundness, all library dependencies must be compiled as
@code{.vo} files and loaded into one Coq instance.
@end itemize

Detailed description of the 4 possible settings of
@code{coq-compile-quick}:

@table @code
@item no-quick
Compile outdated prerequisites without @code{-quick}, producing @code{.vo}
files, but don't compile prerequisites for which an up-to-date
@code{.vio} file exists. Delete or overwrite outdated @code{.vo} files.

@item quick-no-vio2vo
Compile outdated prerequisites with @code{-quick}, producing @code{.vio}
files, but don't compile prerequisites for which an up-to-date
@code{.vo} file exists. Delete or overwrite outdated @code{.vio} files.

@item quick-and-vio2vo
Same as @code{quick-no-vio2vo}, but start a second vio2vo stage for
missing @code{.vo} files. Everything described previously for the
second @code{-vok} stage applies here as well.

@emph{Warning}: This mode does only work when you process require
commands in batches. Slowly single-stepping through require's
might lead to inconsistency errors when loading some libraries,
see Coq issue #5223. To mitigate this risk, vio2vo compilation
only starts after a certain delay after the last require command
of the current queue region has been processed. This is
controlled by @code{coq-compile-second-stage-delay}, @ref{Customizing
Coq Multiple File Support}.

@item ensure-vo
Ensure that all library dependencies are present as @code{.vo}
files and delete outdated @code{.vio} files or @code{.vio} files
that are more recent than the corresponding @code{.vo} file. This
setting is the only one that ensures soundness.
@end table

The options @code{no-quick} and @code{ensure-vo} are compatible
with Coq 8.4 or older. When Proof General detects such an older
Coq version, it changes the quick compilation mode automatically.
For this to work, the option @code{coq-compile-quick} must only
be set via the customization system or via the menu.



@node Customizing Coq Multiple File Support
@subsection Customizing Coq Multiple File Support

The customization settings for multiple file support of Coq Proof
General are in a separate customization group, the
@code{coq-auto-compile} group. To view all options in this
group do @code{M-x customize-group coq-auto-compile} or select
menu entry @code{Proof-General -> Advanced -> Customize -> Coq ->
Coq Auto Compile -> Coq Auto Compile}. 


@c TEXI DOCSTRING MAGIC: coq-compile-before-require
@defvar coq-compile-before-require 
If non-nil, check dependencies of required modules and compile if necessary.@*
If non-nil ProofGeneral intercepts "Require" commands and checks if the
required library module and its dependencies are up-to-date.  If not, they
are compiled from the sources before the "Require" command is processed.

This option can be set/reset via menu
@samp{Coq -> Auto Compilation -> Compile Before Require}.
@end defvar


@c TEXI DOCSTRING MAGIC: coq-compile-auto-save
@defvar coq-compile-auto-save 
Buffers to save before checking dependencies for compilation.@*
There are two orthogonal choices: Firstly one can save all or only the coq
buffers, where coq buffers means all buffers in coq mode except the current
buffer.  Secondly, Emacs can ask about each such buffer or save all of them
unconditionally.

This makes four permitted values: @code{'ask-coq} to confirm saving all
modified Coq buffers, @code{'ask-all} to confirm saving all modified
buffers, @code{'save-coq} to save all modified Coq buffers without
confirmation and @code{'save-all} to save all modified buffers without
confirmation.

This option can be set via menu
@samp{Coq -> Auto Compilation -> Auto Save}.
@end defvar


The following options configure parallel compilation.

@c TEXI DOCSTRING MAGIC: coq-compile-parallel-in-background
@defvar coq-compile-parallel-in-background 
Choose the internal compilation method.@*
When Proof General compiles itself, you have the choice between
two implementations.  If this setting is nil, then Proof General
uses the old implementation and compiles everything sequentially
with synchronous job.  With this old method Proof General is
locked during compilation.  If this setting is t, then the new
method is used and compilation jobs are dispatched in parallel in
the background.  The maximal number of parallel compilation jobs
is set with @samp{@code{coq-max-background-compilation-jobs}}.

This option can be set/reset via menu
@samp{Coq -> Auto Compilation -> Compile Parallel In Background}.
@end defvar


The options @code{coq-compile-vos} and @code{coq-compile-quick}
are described in detail above, @ref{Quick and inconsistent
compilation}.


@c TEXI DOCSTRING MAGIC: coq-compile-keep-going
@defvar coq-compile-keep-going 
Continue compilation after the first error as far as possible.@*
Similar to @samp{`make -k}', with this option enabled, the background
compilation continues after the first error as far as possible.
With this option disabled, background compilation is
immediately stopped after the first error.

This option can be set/reset via menu
@samp{Coq -> Auto Compilation -> Keep going}.
@end defvar


@c TEXI DOCSTRING MAGIC: coq-max-background-compilation-jobs
@defvar coq-max-background-compilation-jobs 
Maximal number of parallel jobs, if parallel compilation is enabled.@*
Use the number of available CPU cores if this is set to
@code{'all-cpus}.  This variable is the user setting.  The value that is
really used is @samp{@code{coq--internal-max-jobs}}.  Use @samp{@code{coq-max-jobs-setter}}
or the customization system to change this variable.  Otherwise
your change will have no effect, because @samp{@code{coq--internal-max-jobs}}
is not adapted.
@end defvar


@c TEXI DOCSTRING MAGIC: coq-max-background-second-stage-percentage
@defvar coq-max-background-second-stage-percentage 
Percentage of @samp{@code{coq-max-background-compilation-jobs}} for the second stage.@*
This setting configures the maximal number of @samp{`-vok}' or vio2vo background
jobs running in a second stage as
percentage of @samp{@code{coq-max-background-compilation-jobs}}.

For backward compatibility, if this option is not customized, it
is initialized from the now deprecated option
@samp{@code{coq-max-background-vio2vo-percentage}}.
@end defvar


@c TEXI DOCSTRING MAGIC: coq-compile-second-stage-delay
@defvar coq-compile-second-stage-delay 
Delay in seconds before starting the second stage compilation.@*
The delay is applied to both @samp{`-vok}' and vio2vo second stages.
For Coq < 8.11 and vio2vo delay helps to avoid running into a
library inconsistency with @code{'quick-and-vio2vo}, see Coq issue
#@var{5223}.

For backward compatibility, if this option is not customized, it
is initialized from the now deprecated option
@samp{@code{coq-compile-vio2vo-delay}}.
@end defvar

Locking ancestors can be disabled with the following option.

@c TEXI DOCSTRING MAGIC: coq-lock-ancestors
@defvar coq-lock-ancestors 
If non-nil, lock ancestor module files.@*
If external compilation is used (via @samp{@code{coq-compile-command}}) then
only the direct ancestors are locked.  Otherwise all ancestors are
locked when the "Require" command is processed.

This option can be set via menu
@samp{Coq -> Auto Compilation -> Lock Ancestors}.
@end defvar


The sequential compilation setting supports an external
compilation command (which could be a parallel running
@code{make}). For this set
@code{coq-compile-parallel-in-background} to @code{nil} and
configure the compilation command in @code{coq-compile-command}.

@c TEXI DOCSTRING MAGIC: coq-compile-command
@defvar coq-compile-command 
External compilation command.  If empty ProofGeneral compiles itself.@*
If unset (the empty string) ProofGeneral computes the dependencies of
required modules with coqdep and compiles as necessary.  This internal
dependency checking does currently not handle ML modules.

If a non-empty string, the denoted command is called to do the
dependency checking and compilation.  Before executing this
command the following keys are substituted as follows:
@lisp
  %p  the (physical) directory containing the source of
      the required module
  %o  the Coq object file in the physical directory that will
      be loaded
  %s  the Coq source file in the physical directory whose
      object will be loaded
  %q  the qualified id of the "Require" command
  %r  the source file containing the "Require"
@end lisp
For instance, "make -C %p %o" expands to "make -C bar foo.vo"
when module "foo" from directory "bar" is required.

After the substitution the command can be changed in the
minibuffer if @samp{@code{coq-confirm-external-compilation}} is t.
@end defvar


@c TEXI DOCSTRING MAGIC: coq-confirm-external-compilation
@defvar coq-confirm-external-compilation 
If set let user change and confirm the compilation command.@*
Otherwise start the external compilation without confirmation.

This option can be set/reset via menu
@samp{Coq -> Auto Compilation -> Confirm External Compilation}.
@end defvar


The preferred way to configure the load path and the mapping of
logical library names to physical file path is the Coq project
file, @ref{Using the Coq project file}. Alternatively one can
configure these things with the following options.

@c TEXI DOCSTRING MAGIC: coq-load-path
@defvar coq-load-path 
Non-standard coq library load path.@*
This list specifies the LoadPath extension for coqdep, coqc and
coqtop.  Usually, the elements of this list are strings (for
"-I") or lists of two strings (for "-R" dir path and
"-Q" dir path).

The possible forms of elements of this list correspond to the 4
forms of include options (@samp{-I} @samp{-Q} and @samp{-R}).  An element can be
@lisp
  - A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a
    directory to be added to ocaml path (@samp{-I}).
  - A list of the form @samp{(}rec dir path)' (where dir and path are
    strings) specifying a directory to be recursively mapped to the
    logical path @samp{path} (@samp{-R dir path}).
  - A list of the form @samp{(}recnoimport dir path)' (where dir and
    path are strings) specifying a directory to be recursively
    mapped to the logical path @samp{path} (@samp{-Q dir path}), but not
    imported (modules accessible for import with qualified names
    only).  Note that -Q dir "" has a special, nonrecursive meaning.
  - A list of the form (8.4 only) @samp{(}nonrec dir path)', specifying a
    directory to be mapped to the logical path @code{'path'} ('-I dir -as path').
@end lisp
For convenience the symbol @samp{rec} can be omitted and entries of
the form @samp{(dir path)} are interpreted as @samp{(rec dir path)}.

A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4.

Under normal circumstances this list does not need to
contain the coq standard library or "." for the current
directory (see @samp{@code{coq-load-path-include-current}}).

@var{warning}: if you use coq <= 8.4, the meaning of these options is
not the same (-I is for coq path).
@end defvar


@c TEXI DOCSTRING MAGIC: coq-load-path-include-current
@defvar coq-load-path-include-current 
If t, let coqdep search the current directory too.@*
Should be t for normal users.  If t, pass -Q dir "" to coqdep when
processing files in directory "dir" in addition to any entries in
@samp{@code{coq-load-path}}.

This setting is only relevant with Coq < 8.5.
@end defvar

During library dependency checking Proof General does not dive
into the Coq standard library or into libraries that are
installed as user contributions. This stems from @code{coqdep},
which does not output dependencies to these directories.
The internal dependency check can also ignore additional
libraries.

@c TEXI DOCSTRING MAGIC: coq-compile-ignored-directories
@defvar coq-compile-ignored-directories 
Directories in which ProofGeneral should not compile modules.@*
List of regular expressions for directories in which ProofGeneral
should not compile modules.  If a library file name matches one
of the regular expressions in this list then ProofGeneral does
neither compile this file nor check its dependencies for
compilation.  It makes sense to include non-standard coq library
directories here if they are not changed and if they are so big
that dependency checking takes noticeable time.  The regular
expressions in here are always matched against the .vo file name,
regardless whether @samp{`-quick}' would be used to compile the file
or not.
@end defvar


@node Current Limitations
@subsection Current Limitations

@itemize
@item
No support for @code{Declare ML Module} commands and files
depending on an ML module.
@item
When a compiled library has the same time stamp as the source
file, it is considered outdated. Some old file systems (for
instance ext3) or Emacs before version 24.3 support only time
stamps with one second granularity. On such configurations Proof
General will perform some unnecessary compilations.
@end itemize


@node Omitting proofs for speed
@section Omitting proofs for speed

To speed up asserting larger chunks, Proof General can omit
complete opaque proofs by silently replacing the whole proof
script with @code{Admitted}, @ref{Script processing commands}.
This works when
@itemize
@item
proofs are not nested
@item
opaque and non-opaque proofs start with @code{Proof.} or
@code{Proof using}
@item
opaque proofs end with @code{Qed} or @code{Admitted}
@item
non-opaque proofs or definition end with @code{Defined}
@end itemize
Aborted proofs can be present if they start with a variant of
@code{Proof} and end with @code{Abort}. They are handled like
non-opaque proofs (i.e., not omitted).

To enable omitting proofs, configure
@code{proof-omit-proofs-option} or select @code{Proof-General ->
Quick Options -> Processing -> Omit Proofs}.

With a prefix argument, both @code{proof-goto-point} and
@code{proof-process-buffer} will temporarily disable the omit
proofs feature and send the full proof script to Coq.

If a nested proof is detected while searching for opaque proofs
to omit, a warning is displayed and the complete remainder of the
asserted region is sent unmodified to Coq. 

If the proof script relies on sections, it is highly recommended to use
a @code{Proof using} annotation for all lemmas contained in a Section,
otherwise @code{Coq} will compute a wrong type for these lemmas when
this omitting-proofs feature is enabled.

To automate this, we recall that ProofGeneral provides a dedicated
feature to generate these @code{Proof using} annotations (a defective
form being e.g. @code{Proof using Type} if no section hypothesis is
used), see the menu command @code{Coq > "Proof using" mode} and
@ref{Proof using annotations} for details.

@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 well backtracked. 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 it falls back to the previous
one.  This is supported to any nesting depth that Coq allows.

Warning! Using Coq commands for navigating inside the different proofs
(@code{Resume} and especially @code{Suspend}) are not supported,
backtracking will break synchronization.

@b{Special note:} The old feature that moved nested proofs outside the
current proof is disabled.

@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.  When the user
tries to retract across an extended tactic in a script, the algorithm
for calculating how far to undo has a default behavior that is not
always accurate in proof mode: do "@code{Undo}".

Coq Proof General does not currently support dynamic tactic extension in
Coq: this is desirable but requires assistance from the Coq core.
Instead we provide a way to add tactic and command names in the
@file{.emacs} file. Four Configurable variables allows to register
personal new tactics and commands into four categories:
@itemize @bullet

@item @emph{state changing commands}, 
which need "@code{Back}" to be backtracked;
@item @emph{state changing tactics},
which need "@code{Undo}" to be backtracked; 
@item @emph{state preserving commands},
which do not need to be backtracked; 
@item @emph{state preserving tactics},
which do not need to be backtracked; 
@end itemize

We give an example of existing commands that fit each category.

@itemize @bullet

@item @code{coq-user-state-preserving-commands}: example: "@code{Print}"

@item @code{coq-user-state-changing-commands}: example: "@code{Require}"

@item @code{coq-user-state-changing-tactics}: example: "@code{Intro}"
 
@item @code{coq-user-state-preserving-tactics}: example: "@code{Idtac}"
@end itemize

This variables are regexp string lists. See their documentations in
emacs (@code{C-h v coq-user...})  for details on how to set them in your
@file{.emacs} file.

Here is a simple example:
@lisp
(setq coq-user-state-changing-commands 
      '("MyHint" "MyRequire"))
(setq coq-user-state-preserving-commands 
      '("Show\\s-+Mydata"))
@end lisp

The regexp character sequence @code{\\s-+} means "one or more
whitespaces". See the Emacs documentation of @code{regexp-quote} for the
syntax and semantics.  WARNING: you need to restart Emacs to make the
changes to these variables effective.

In case of losing synchronization, the user can use @kbd{C-c C-z} to
move the locked region to the proper position,
(@code{proof-frob-locked-end}, @pxref{Escaping script management}) or
@kbd{C-c C-v} to re-issue an erroneously back-tracked tactic without
recording it in the script.

@node Indentation tweaking
@section Indentation tweaking

Indentation of Coq script is provided by Proof General, but it may
behave badly especially if you use syntax extensions. You can sometimes
fix this problem by telling PG that some token should be considered as
identical to other ones by the indentation mechanism. Use the two
variables @code{coq-smie-user-tokens} and
@code{coq-smie-monadic-tokens}. This variables contains associations
between user tokens and the existing pg tokens they should be equated
too.

@itemize @bullet
@item @code{coq-smie-user-tokens}

this is where users should put ther own tokens. For instance:

@lisp
(setq coq-smie-user-tokens '((\"xor\" . \"or\") (\"ifb\" . \"if\")))
@end lisp
to have token \"xor\" and \"ifb\" be considered as having
@item @code{coq-smie-monadic-tokens}

is specific to monadic operators: it contains usual monadic notations
by default (but you can redefine it if needed).

Specific tokens are defined for the two usual monadic forms: 

@verbatim
"let monadic" E "<- monadic" E "in monadic" E
E "<- monadic" E ";; monadic" E
@end verbatim

The default value of @code{coq-smie-monadic-tokens} gives the following
concrete syntax to these tokens:
@lisp
((";;" . ";; monadic")
 ("do" . "let monadic")
 ("<-" . "<- monadic")
 (";" . "in monadic"))
@end lisp

thus allowing for the following:

@verbatim
  do x <- foo;
  do y <- bar;
  ...
@end verbatim
and
@verbatim
  x <- foo;;
  y <- bar;;
  ...
@end verbatim
@end itemize

@emph{NOTE:} This feature is experimental.

@emph{NOTE:} the ``pg tokens'' are actually the ones PG generates internally by
exploring the file around the indentation point. Consequently this
refers to internals of PoofGeneral. Contact the Proof General team if you
need help.


@node Holes feature
@section Holes feature

@emph{Holes} are an experimental feature for complex expression editing
by filling in templates. It is inspired from other tools, like Pcoq
(@uref{http://www-sop.inria.fr/lemme/pcoq/index.html}).  The principle
is simple, holes are pieces of text that can be "filled" by various
means. The Coq command insertion menu system makes use of the holes
system.  Almost all holes operations are available in the Holes menu.

@b{Notes:} Holes make use of the Emacs abbreviation mechanism, it will
work without problem if you don't have an abbrev table defined for Coq
in your config files.  Use @code{C-h v abbrev-file-name} to see the name
of the abbreviation file. 

If you already have such a table it won't be automatically overwritten
(so that you keep your own abbreviations).  But you must read the abbrev
file given in the Proof General sources to be able to use the command
insertion menus.  You can do the following to merge your abbreviations
with ProofGeneral's abbreviations: @code{M-x read-abbrev-file}, then
select the file named @code{coq-abbrev.el} in the
@code{ProofGeneral/coq} directory. At Emacs exit you will be asked if
you want to save abbrevs; answer yes.


@node Proof-Tree Visualization
@section Proof-Tree Visualization

Starting with Proof General version 4.2 and Coq version 8.4, Coq
Proof General has full support for proof-tree visualization, 
@pxref{Graphical Proof-Tree Visualization}. To find out which
versions of Prooftree are compatible with this version of Proof
General, @pxref{Graphical Proof-Tree Visualization} or the 
@uref{http://askra.de/software/prooftree/, Prooftree website}.

For the visualization to work properly, proofs must be started
with @code{Proof}, which is encouraged practice anyway (see Coq Bug
#2776). Without @code{Proof} you lose the initial proof goal,
possibly having two or more initial goals in the display.

To support @code{Grab Existential Variables} Prooftree can
actually display several graphically independent proof trees in
several layers.

@node Showing Proof Diffs
@section Showing Proof Diffs

Coq 8.10 supports automatically highlighting the differences
between successive proof steps in Proof General.  The feature is described in the
Coq Documentation, section @coqrefman{proofs/writing-proofs/proof-mode.html#showing-differences-between-proof-steps, Showing differences between proof steps}.

The Coq proof diff does more than a basic "diff" operation.  For example:

@itemize @bullet
@item diffs are computed on a per-token basis (as determined by the Coq lexer) rather
  than on a per-character basis, probably a better match for how people understand
  the output.  (For example, a token-based diff between "abc" and "axc" will
  highlight all of "abc" and "axc" as a difference, while a character-based diff
  would indicate that "a" and "c" are in common and that only the "b"/"x" is a
  difference.)
@item diffs ignore the order of hypotheses
@item tactics that only change the proof view are handled specially, for
  example "swap" after a "split" will show the diffs between before "split"
  and after "swap", which is more useful
@item some error messages have been instrumented to show diffs where it is helpful
@end itemize

To enable or disable diffs, set @code{coq-diffs} (select menu @code{Coq -> Diffs})
to "on", "off" or "removed".  "on" highlights added tokens with the background
color from @code{diff-refine-added}.  "removed" highlights removed tokens
with the background color from @code{diff-refine-removed}.  With the "removed" setting,
lines that have both added and removed text may be shown twice, as "before" and
"after" lines.
To preserve the settings for the next time you start Proof General,
select @code{Coq -> Settings -> Save Settings}.

The colors used to highlight diffs are configurable in the
@code{Proof-General -> Advanced -> Customize -> Proof Faces} menu.
The 4 @code{Coq Diffs ...} faces control the highlights.  Lines that
have added or removed tokens are shown with the entire line highlighted with
a @code{Coq Diffs ... Bg} face.  The added or removed tokens themselves are highlighted
with non-@code{Bg} faces.

@node Opam-switch-mode support
@section Opam-switch-mode support

Coq can be installed using @code{opam} (the OCaml package manager),
which makes it easy to manage several different switches, having each
a different version of Coq.

Instead of running a command like @code{opam switch ...} in a terminal
and restarting emacs to benefit from a different switch, one can:

@itemize @bullet
@item
@b{Install} the
@uref{https://github.com/ProofGeneral/opam-switch-mode,
opam-switch-mode} and use the dedicated mode bar menu @code{OPSW} it
provides.
@item
@b{Configure} Proof General using the customization option
@code{coq-kill-coq-on-opam-switch}, so that the Coq background process
is killed when changing the opam switch through
@code{opam-switch-mode}.
@end itemize

@c TEXI DOCSTRING MAGIC: coq-kill-coq-on-opam-switch
@defvar coq-kill-coq-on-opam-switch 
If t kill coq when the opam switch changes (requires @samp{opam-switch-mode}).@*
When @samp{opam-switch-mode} is loaded and the user changes the opam switch
through @samp{opam-switch-mode} then this option controls whether the coq
background process (the proof shell) is killed such that the next
assert command starts a new proof shell, probably using a
different coq version from a different opam switch.

See https://github.com/ProofGeneral/opam-switch-mode for @samp{opam-switch-mode}
@end defvar

@c =================================================================
@c
@c  CHAPTER: EasyCrypt Proof General
@c
@node EasyCrypt Proof General
@chapter EasyCrypt Proof General
@cindex EasyCrypt Proof General

@menu
* EasyCrypt specific commands::
* EasyCrypt weak-check mode::
* EasyCrypt customizations::
@end menu

EasyCrypt Proof General is an instantiation of Proof General for the
EasyCrypt proof assistant.

@node EasyCrypt specific commands
@section EasyCrypt specific commands

@kindex C-c C-a C-p
@kindex C-c C-a C-c

EasyCrypt Proof General supplies the following key-bindings:
@table @kbd
@item C-c C-a C-p
Prompts for ``print'' query arguments.

@item C-c C-a C-c
The same for a ``check'' query.
@end table

@node EasyCrypt weak-check mode
@section EasyCrypt weak-check mode

The EasyCrypt menu contains a @code{Weak-check mode} toggle menu, which
allows you to enable or disable the EasyCrypt Weak-Check mode. When
enabled, all @code{smt} calls are ignored and assumed to succeed.

@node EasyCrypt customizations
@section EasyCrypt customizations

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

@c TEXI DOCSTRING MAGIC: easycrypt-prog-name
@defopt easycrypt-prog-name 
Name of program to run EasyCrypt.

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

@c TEXI DOCSTRING MAGIC: easycrypt-load-path
@defvar easycrypt-load-path 
Non-standard EasyCrypt library load path.@*
This list specifies the include path for EasyCrypt.  The elements of
this list are strings.
@end defvar

@c TEXI DOCSTRING MAGIC: easycrypt-web-page
@defvar easycrypt-web-page 
URL of web page for EasyCrypt.
@end defvar


@c =================================================================
@c
@c  CHAPTER: Shell Proof General
@c
@node Shell Proof General
@chapter Shell Proof General
@cindex Shell Proof General

This instance of Proof General is not really for proof assistants at
all, but simply provided as a handy way to use a degenerate form of
script management with other tools.  

Suppose you have a software tool of some kind with a command line
interface, and you want to demonstrate several example uses of it,
perhaps at a conference.  But the command lines for your tool may be
quite complicated, so you do not want to type them in live.  Instead,
you just want to cut and paste from a pre-recorded list.  But watching
somebody cut and paste commands into a window is almost as tedious as
watching them type those commands!

Shell Proof General comes to the rescue.  Simply record your commands in
a file with the extension @code{.pgsh}, and load up Proof General.  Now
use the toolbar to send each line of the file to your tool, and have the
output displayed clearly in another window.  Much easier and more
pleasant for your audience to watch!

If you wish, you may adjust the value of @code{proof-prog-name} in
@file{pgshell.el} to launch your program rather than the shell
interpreter.  

We welcome feedback and suggestions concerning this subsidiary provision
in Proof General.  Please recommend it to your colleagues (e.g., the
model checking crew).


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

Proof General has its own
@uref{https://proofgeneral.github.io,home page} hosted at
GitHub.  Visit this page for the latest news!

@menu
* Obtaining Proof General::     
* Installing Proof General from sources::  
* 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{https://github.com/ProofGeneral/PG}.
@end example

The distribution is available in the master branch of the repository.
Tagged versions of the sources may be redistributed by third party
packagers in other forms.

The sources includes the generic elisp code, and code for Coq, EasyCrypt,
and other provers.  Also included are installation
instructions (reproduced in brief below) and this documentation.

@node Installing Proof General from sources
@section Installing Proof General from sources

Remove old versions of Proof General, then download and install the new
release from GitHub:
@example
$ git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
$ cd ~/.emacs.d/lisp/PG
$ make
@end example

Then add the following to your @file{.emacs}:
@lisp
;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")
@end lisp

If Proof General complains about a version mismatch, make sure that the
shell's @code{emacs} is indeed your usual Emacs. If not, run the Makefile
again with an explicit path to Emacs. On macOS in particular you'll
probably need something like
@example
make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
@end example

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

The @code{load} 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 -> Advanced -> 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

If you do not want to use customize, simply add a line like this:
@lisp
  (setq coq-prog-name "/usr/bin/coqtop")
@end lisp
to your @file{.emacs} file.
For more advice on how to customize the @code{coq-prog-name} variable,
@pxref{Using file variables}, Remark 2.


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

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.  It may be necessary to do this if you use
a different version of Emacs.


@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 @i{Proof General site configuration} in
@i{Adapting Proof General} for more details).  Make sure that
the @file{generic/} and assistant-specific elisp files are kept in
subdirectories (@file{coq/}, @file{phox/}, @file{easycrypt/}, ...) 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{.ec} file will not load EasyCrypt
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 
@c @code{sml-mode} for @file{.ML} files, or
Verilog mode for @file{.v} files clashes with Coq mode.  

See @i{Proof General site configuration} in @i{Adapting Proof General},
for more details of how to adjust the @code{proof-assistants} setting.

Instead of altering @code{proof-assistants}, a simple way to disable
support for some prover is to delete the relevant directories from the
PG installation.  For example, to remove support for Coq, delete the
@file{coq} directory in the Proof General home directory.


@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: Reporting Bugs
@c
@c
@node Bugs and Enhancements
@appendix Bugs and Enhancements

For an up-to-date description of bugs and other issues, please consult
the bugs file included in the distribution:
@uref{http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest/BUGS,@file{BUGS}}.

If you discover a problem which isn't mentioned in @file{BUGS}, please
use the search facility on our Trac tracking system at
@uref{http://proofgeneral.inf.ed.ac.uk/trac}.  If you cannot find the
problem mentioned, please add a ticket, giving a careful description of
how to repeat your problem, and saying @b{exactly} which versions of all
Emacs and theorem prover you are using.

@sp 1

If you have some suggested enhancements to request or contribute, please
also use the tracking system at
@uref{http://proofgeneral.inf.ed.ac.uk/trac} for this.


@node References
@unnumbered References

A short overview of the Proof General system is described in the
note:
@itemize @bullet
@item @b{[Asp00]}
David Aspinall.
@i{Proof General: A Generic Tool for Proof Development}.
Tools and Algorithms for the Construction and 
Analysis of Systems, Proc TACAS 2000.  LNCS 1785.
@end itemize

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

@itemize @bullet
@item @b{[BT98]}
Yves Bertot and Laurent Théry. @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 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



@c
@c
@c APPENDIX: History
@c
@c
@node History of Proof General
@unnumbered History of Proof General
@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://homepages.inf.ed.ac.uk/da/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.  

Despite views of some detractors, we demonstrated that an interface
both friendly and powerful can be built on top of Emacs.  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 that went into Proof General 3.0.

@menu
* Old News for 3.0::
* Old News for 3.1::
* Old News for 3.2::
* Old News for 3.3::
* Old News for 3.4::
* Old News for 3.5::
* Old News for 3.6::
* Old News for 3.7::
@end menu


@node Old News for 3.0
@unnumberedsec Old News for 3.0

Proof General 3.0 (released November 1999) 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://x-symbol.sourceforge.net/,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 improvements in both Coq and LEGO instances
for this release were made by David Aspinall.  Markus Wenzel provided
support for his Isar language, a new proof language for Isabelle.  David
von Oheimb helped to develop the generic version of his X-Symbol
addition 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 Old News for 3.1
@unnumberedsec Old News for 3.1
@cindex news

Proof General 3.1 (released March 2000) is 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 GNU 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 much 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 Old News for 3.2
@unnumberedsec Old News for 3.2
@cindex news

Proof General 3.2 introduced several new features and some bug fixes.
One noticeable new feature is the addition of a prover-specific menu for
each of the supported provers.  This menu has a ``favourites'' feature
that you can use to easily define new functions.  Please contribute
other useful functions (or suggestions) for things you
would like to appear on these menus.

Because of the new menus and to make room for more commands, we have
made a new key map for prover specific functions.  These now all begin
with @kbd{C-c C-a}.  This has changed a few key bindings slightly.

Another new feature is the addition of prover-specific completion
tables, to encourage the use of Emacs's completion facility, using
@kbd{C-RET}.  @xref{Support for completion}, for full details.

A less obvious new feature is support for turning the proof assistant
output on and off internally, to improve efficiency when processing
large scripts.  This means that more of your CPU cycles can be spent on
proving theorems.

Adapting for new proof assistants continues to be made more flexible,
and easier in several places.  This has been motivated by adding
experimental support for some new systems.  One new system which had
good support added in a very short space of time is @b{PhoX} (see
@uref{http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html, the PhoX home
page} for more information).  PhoX joins the rank of officially
supported Proof General instances, thanks to its developer Christophe
Raffalli.

Breaking the manual into two pieces was overdue: now all details on
adapting Proof General, and notes on its internals, are in the
@i{Adapting Proof General} manual.  You should find a copy of that
second manual close to wherever you found this one; consult the
Proof General home page if in doubt.

The internal code of Proof General has been significantly overhauled for
this version, which should make it more robust and readable.  The
generic code has an improved file structure, and there is support for
automatic generation of autoload functions.  There is also a new
mechanism for defining prover-specific customization and instantiation
settings which fits better with the customize library.  These settings
are named in the form @code{@i{PA}-setting-name} in the documentation;
you replace @i{PA} by the symbol for the proof assistant you are
interested in.  @xref{Customizing Proof General}, for details.

Finally, important bug fixes include the robustification against
@code{write-file} (@kbd{C-x C-w}), @code{revert-buffer}, and friends.
These are rather devious functions to use during script management, but
Proof General now tries to do the right thing if you're deviant enough
to try them out!

Work on this release was undertaken by David Aspinall between
May-September 2000, and includes contributions from Markus Wenzel,
Pierre Courtieu, and Christophe Raffalli.  Markus added some Isar
documentation to this manual.


@node Old News for 3.3
@unnumberedsec Old News for 3.3

Proof General 3.3 includes a few feature additions, but mainly the focus
has been on compatibility improvements for new versions of provers (in
particular, Coq 7), and new versions of emacs (in particular, XEmacs
21.4).

One new feature is control over visibility of completed proofs,
@xref{Visibility of completed proofs}.  Another new feature is the
tracking of theorem dependencies inside Isabelle.  A context-sensitive
menu (right-button on proof scripts) provides facility for browsing the
ancestors and child theorems of a theorem, and highlighting them.  The
idea of this feature is that it can help you untangle and rearrange big
proof scripts, by seeing which parts are interdependent.  The implementation
is provisional and not documented yet in the body of this manual.  It only
works for the "classic" version of Isabelle99-2.


@node Old News for 3.4
@unnumberedsec Old News for 3.4

Proof General 3.4 adds improvements and also compatibility fixes for
new versions of Emacs, in particular, for GNU Emacs 21, which adds
the remaining pretty features that have only been available to XEmacs
users until now (the toolbar and X-Symbol support).

One major improvement has been to provide better support for
synchronization with Coq proof scripts; now Coq Proof General should
be able to retract and replay most Coq proof scripts reliably.  Credit
is due to Pierre Courtieu, who also updated the documentation in this
manual.

As of version 3.4, Proof General is distributed under the GNU General
Public License (GPL).  Compared with the previous more restrictive
license, this means the program can now be redistributed by third
parties, and used in any context without applying for a special
license.  Despite these legal changes, we would still appreciate if
you send us back any useful improvements you make to Proof General.

@node Old News for 3.5
@unnumberedsec Old News for 3.5


@node Old News for 3.6
@unnumberedsec Old News for 3.6

There was no 3.6 release of Proof General.

@node Old News for 3.7
@unnumberedsec Old News for 3.7

Proof General version 3.7.1 is an updated and enhanced version
of Proof General 3.7.  See  @file{CHANGES} for more details.

Proof General version 3.7 collects together a cumulative set of
improvements to Proof General 3.5.  There are compatibility fixes for
newer Emacs versions, and particularly for GNU Emacs: credit is due to
Stefan Monnier for an intense period of debugging and patching.  The
options menu has been simplified and extended, and the display
management is improved and repaired for Emacs API changes.  There are
some other usability improvements, some after feedback from use at TYPES
Summer Schools.  Many new features have been added to enhance Coq mode
(thanks to Pierre Courtieu) and several improvements made for Isabelle
(thanks to Makarius Wenzel, Stefan Berghofer and Tjark Weber).

Support has been added for the useful Emacs packages Speedbar
@c @uref{http://cedet.sourceforge.net/speedbar.shtml,Speedbar} 
and Index Menu, both usually distributed with Emacs.  A compatible
version of the Emacs package Math-Menu (for Unicode symbols) is bundled with Proof General.
An experimental Unicode Tokens package has been added which will replace
X-Symbol.

See the @file{CHANGES} file in the distribution for more complete
details of changes since version 3.5, and the appendix
@ref{History of Proof General} for old news.


@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