\input texinfo @c -*-texinfo-*- @c @c $Id$ @c @c %**start of header @setfilename ProofGeneral.info @settitle Proof General @setchapternewpage odd @paragraphindent 0 @iftex @afourpaper @end iftex @c %**end of header @c @c TODO, priority order @c . finish incomplete sections @c . polish mark-up @c . add more index entries @c . screenshots might be nice (one day) @c @c NB: try keep full node lines out of this file because Emacs makes a @c mess of updating them in general. Instead, rely on makeinfo @c and friends to do the equivalent job. For this to work, @c we write nodes in the form: @c @c @node node-name @c @c @c @set version 2.0 @set xemacsversion 20.4 @set fsfversion 20.2 @set last-update November 1998 @ifinfo @format START-INFO-DIR-ENTRY * ProofGeneral::Organize your proofs with Emacs! END-INFO-DIR-ENTRY @end format @end ifinfo @c @c MACROS @c @c define one here for a command with a keybinding? @c @c I like the idea, but it's maybe against the texinfo @c style to fix together a command and its keybinding. @c merge functions and variables into concept index. @syncodeindex fn cp @syncodeindex vr cp @finalout @titlepage @title Proof General @subtitle Organise your proofs with Emacs! @subtitle Proof General @value{version} @subtitle @value{last-update} @iftex @image{ProofGeneral} @end iftex @author D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira @page @vskip 0pt plus 1filll This manual and the program Proof General are Copyright @copyright{} 1998 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 XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion} or later versions. @end titlepage @page @ifinfo @node Top @top Proof General This file documents version @value{version} of @b{Proof General}, a generic Emacs interface for proof assistants. Proof General @value{version} has been tested with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion}. It is supplied ready customized for the proof assistants Coq, Lego, and Isabelle. @menu * Introducing Proof General:: * Basic Script Management:: * Advanced Script Management:: * Support for other Packages:: * Customizing Proof General:: * LEGO Proof General:: * Coq Proof General:: * Isabelle Proof General:: * Adapting Proof General to New Provers:: * Internals of Proof General:: * Credits and References:: * Obtaining and Installing Proof General:: * Known bugs and workarounds:: * Plans and ideas:: * Keystroke Index:: * Index:: @end menu @detailmenu --- The Detailed Node Listing --- Introducing Proof General --- The Detailed Node Listing --- Introducing Proof General * Quick start guide:: * Features of Proof General:: * Supported proof assistants:: Basic Script Management * Proof scripts:: * The buffer model:: * Regions in a proof script:: * Script editing commands:: * Script processing commands:: * Toolbar commands:: * Proof assistant commands:: * Walkthrough example in LEGO:: Proof scripts * Goals and saves:: Advanced Script Management * Switching between proof scripts:: * View of processed files :: * Retracting across files:: * Asserting across files:: * Working directly with the proof shell:: Support for other Packages * Support for function menus:: * Support for tags:: Customizing Proof General * Easy customization:: * Setting the user options:: * Tweaking configuration settings:: LEGO Proof General * LEGO specific commands:: * LEGO tags:: * LEGO customizations:: Coq Proof General * Coq specific commands:: * Coq customizations:: Isabelle Proof General * Isabelle specific commands:: * Isabelle customizations:: Adapting Proof General to New Provers * Skeleton example:: * Proof script settings:: * Proof shell settings:: Proof shell settings * Special annotations:: Internals of Proof General * Proof script mode:: * Proof shell mode:: * Handling multiple files:: Credits and References * Credits:: * References:: Obtaining and Installing Proof General * Obtaining Proof General:: * Installing Proof General from tarball:: * Installing Proof General from RPM package:: * Notes for syssies:: Known bugs and workarounds * Bugs at the generic level:: * Bugs specific to LEGO Proof General:: * Bugs specific to Coq Proof General:: * Bugs specific to Isabelle Proof General:: Bugs specific to LEGO Proof General * Retraction and @code{Discharge}:: * Retraction and proving:: Plans and ideas * Granularity of Atomic Command Sequences:: * Browser mode for script files and theories:: @end detailmenu @end ifinfo @node Introducing Proof General @chapter Introducing Proof General @cindex proof assistant @cindex Proof General @c would like the logo on the title page really but @c it doesn't seem to work there for html. @ifhtml [ Proof General logo ] @end ifhtml A @dfn{proof assistant} is a computerized helper for developing mathematical proofs. @dfn{Proof General} is a generic Emacs interface for proof assistants, developed at the LFCS in the University of Edinburgh. It works best under XEmacs, but can also be used with FSF GNU Emacs. You do not have to be an Emacs militant to use Proof General! @* The interface is designed to be very easy to use. You develop your proof script in-place rather than line-by-line and later reassembling the pieces. Proof General keeps track of which proof steps have been processed by the prover, and prevents you editing them accidently. You can undo steps as usual. Our aim is provide a powerful and configurable Emacs mode which helps user-interaction with interactive proof assistants. Please help us with this aim! Configure Proof General for your proof assistant, by adding features at the generic level wherever possible. See @ref{Adapting Proof General to New Provers} for more details, and send ideas, comments, patches, and code to @code{proofgen@@dcs.ed.ac.uk}. @menu * Quick start guide:: * Features of Proof General:: * Supported proof assistants:: @end menu @node Quick start guide @section Quick start guide Proof General may have been installed for you already. If so, when you visit a proof script file for your proof assistant, 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 keys for the current mode. The proof assistant is automatically started inside Emacs when you ask for some of the proof script to be processed. To follow an example use of Proof General on a LEGO proof, see @pxref{Walkthrough example in LEGO}. If Proof General has not already been installed, you should insert the line: @lisp (load "@var{ProofGeneral}/generic/proof-site.el") @end lisp into your @file{~/.emacs} file, where @var{ProofGeneral} is the top-level directory that was created when Proof General was unpacked. For more details on obtaining and installing Proof General, see @pxref{Obtaining and Installing Proof General}. @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? Here is an outline of its main features. @itemize @bullet @item @i{Simplified communication}@* The proof assistant's shell is normally hidden from the user. Communication takes place via two or 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 assistants. This means that the user only sees the output from the most recent proof step, rather than a screen full of output from the proof assistant. @c Optionally, the goals buffer and script buffer can be identified. For more details, see @pxref{The buffer model}. @item @i{Script management}@* Proof General colours proof script regions blue when they have already been processed by the prover, and colours regions red when the prover is currently processing them. The appearance of Emacs buffers always matches the proof assistant's state. For more details, see @pxref{Basic Script Management} and @pxref{Advanced Script Management}. @item @i{Script editing mode}@* Proof General provides useful facilities for editing proof scripts, including syntax hilighting and a menu to jump to particular goals, definitions, or declarations. Special editing functions send lines of proof script to the proof assistant, or undo previous proof steps. For more details, see @pxref{Script editing commands} and @pxref{Script processing commands}. @item @i{Toolbar and menus}@* A script buffer has a toolbar with navigation buttons for processing parts of the proof script. A menu provides further functions for operations in the proof assistant, as well as customization of Proof General. For more details, see @pxref{Toolbar commands}, @pxref{Proof assistant commands}, and @pxref{Customizing Proof General}. @c not yet @c @item @i{Proof by pointing} @end itemize @node Supported proof assistants @section Supported proof assistants Proof General comes ready-customised for these proof assistants: @itemize @bullet @item @b{LEGO Proof General} for LEGO Version 1.3.1@* @c written by Thomas Kleymann and Dilip Sequeira. @c All features of Proof General are supported. See @pxref{LEGO Proof General} for more details. @item @b{Coq Proof General} for Coq Version 6.2@* @c written by Healfdene Goguen. @c All of features of Proof General are supported except multiple files. See @pxref{Coq Proof General} for more details. @item @b{Isabelle Proof General} for Isabelle 98-1@* @c written by David Aspinall. All features of Proof General are supported, except for an external tags program. Isabelle Proof General handles theory files as well as ML (proof script files), and has an extensive theory file editing mode taken from @uref{http://www.dcs.ed.ac.uk/home/da/Isamode,Isamode}. See @pxref{Isabelle Proof General} for more details. @end itemize Proof General is designed to be generic, so you can adapt it to other proof assistants if you know a little bit of Emacs Lisp. @itemize @bullet @item @b{Your Proof General} for your favourite proof assistant@* See @pxref{Adapting Proof General to New Provers} for more details of how to do this. @end itemize @c @c CHAPTER: Basic Script Management @c @node Basic Script Management @chapter Basic Script Management @menu * Proof scripts:: * The buffer model:: * Regions in a proof script:: * Script editing commands:: * Script processing commands:: * Toolbar commands:: * Proof assistant commands:: * Walkthrough example in LEGO:: @end menu @node Proof scripts @section Proof scripts @cindex proof script A @dfn{proof script} is a sequence of commands to a proof assistant used to construct a proof. Proof General is designed to work with @i{interactive} proof assistants, where the mode of working is usually a dialogue between the user and the proof assistant. Primitive interfaces for proof assistants simply present a shell-like view of this dialogue: the user repeatedly types commands to the shell until the proof is completed. The system responds at each step, maybe with a new list of subgoals to be solved, or maybe with a failure report. Often we want to keep a record of the proof commands used to prove a theorem, in the form of a proof script kept in a file. Then we can @dfn{replay} the proof later on to reprove the theorem, without having to type in all the commands 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 organize interactive proofs by issuing commands directly from a proof script file, while it is written and edited. @c developing them in proof script files. @menu * Goals and saves:: @end menu @node Goals and saves @unnumberedsubsec Goals and saves @cindex goal @cindex save @cindex goal-save region A proof script contains a sequence of commands used to prove one or more theorems. Proof General assumes that for each proved theorem, a proof script contains a sequence of commands delimited by a pair of special commands, known as @code{goal} and @code{save}. So a proof script has a series of proofs which look something like this (of course, the exact syntax will depend on the proof assistant you use): @lisp goal @var{mythm} is @var{G} @dots{} save theorem @var{mythm} @end lisp Proof General recognizes the goal-save regions in proof scripts. The name @var{mythm} can appear in the menu for the proof script @pxref{Support for function menus} to help quickly find a proof, and once a goal-save region has been processed by the proof assistant, it is treated as atomic when undoing proof steps. @node The buffer model @section The buffer model @cindex script buffer @cindex goals buffer @cindex response buffer @c FIXME: fix this in the light of what gets implemented. Proof General runs your proof assistant in a shell buffer in Emacs. This @dfn{proof shell buffer} is usually hidden from view, @pxref{Working directly with the proof shell} for further details. When Proof General sees an error in the shell buffer, it will highlight the error and display the buffer automatically. Communication with the proof shell takes place via two or three intermediate buffers. The @dfn{script buffer} holds input destined for the proof shell, in the form of a @i{proof script}. Normally this is a buffer visiting a file, which can be later loaded directly by the prover to replay the proof. The @dfn{goals buffer} displays the current list of subgoals to be solved for a proof in progress. This is normally displayed at the same time as the script buffer. The @dfn{response buffer} displays other output from the proof assistant, for example warning or informative messages. @c Optionally, the goals buffer and script buffer can be identified @c @pxref{Identify goals and response}. The disadvantage of this is that @c the goals display can be replaced by other messages, so you must ask for @c it to be refreshed. The advantage is that it is simpler to deal with @c fewer Emacs buffers. @node Regions in a proof script @section Regions in a proof script @node Script editing commands @section Script editing commands @kindex C-c C-e @node Script processing commands @section Script processing commands @kindex C-c C-n @kindex C-c C-p @kindex C-c RET @kindex C-c u @kindex C-c C-u @deffn Command proof-assert-next-command @end deffn @deffn Command proof-undo-last-successful-command @end deffn @deffn Command proof-try-command @end deffn @deffn Command proof-retract-until-point @end deffn @deffn Command proof-process-buffer @end deffn @c FIXME: requires formatting Why is C-c C-b useful? Could just use the file to read it one go (will we have a command to do this other than via the process?). BUT it's nice because it stops exactly where a proof fails, so you can continue development from there. @node Toolbar commands @section Toolbar commands @node Proof assistant commands @section Proof assistant commands @kindex C-c C-p @kindex C-c c @kindex C-c h @deffn Command proof-prf List proof state. @end deffn @deffn Command proof-ctxt List context. @end deffn @deffn Command proof-help Print help message giving syntax. @end deffn @deffn Command proof-execute-minibuffer-cmd Prompt for a command in the minibuffer and send it to proof assistant. @end deffn @deffn Command proof-interrupt-process Interrupt the proof assistant. WARNING! This may confuse Proof General. @end deffn @c Please explain C-c C-v here. @c Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working @c directly with the proof shell} @node Walkthrough example in LEGO @section Walkthrough example in LEGO @c @c CHAPTER: Advanced Script Management @c @node Advanced Script Management @chapter Advanced Script Management @cindex Multiple Files What we really mean by @emph{advanced} is that Proof General supports large proof developments. These are typically spread across various files which depend on each other in some way. Proof General knows enough about the dependencies to allow script management across multiple files. @menu * Switching between proof scripts:: * View of processed files :: * Retracting across files:: * Asserting across files:: * Working directly with the proof shell:: @end menu @node Switching between proof scripts @section Switching between proof scripts @cindex Switching between proof scripts Basic modularity in large proof developments can be achieved by splitting proof scripts across various files. Let's assume that you are in the middle of a proof development. You are working on a soundness proof of Hoare Logic in a file called@footnote{The suffix may depend of the specific proof assistant you are using e.g, LEGO's proof script files have to end with @file{.l}.} @file{HSound.l}. It depends on a number of other files which develop underlying concepts e.g. syntax and semantics of expressions, assertions, imperative programs. You notice that the current lemma is too difficult to prove because you have forgotten to prove some more basic properties about determinism of the programming language. Or perhaps a previous definition is too cumbersome or even wrong. At this stage, you would like to visit the appropriate file, say @file{sos.l} and retract to where changes are required. For further details on how to accomplish this, we refer to @ref{Retracting across files}. Then, using script management, you want to develop some more basic theory in @file{sos.l}. Once this task has been completed (possibly involving retraction across even earlier files) and the new development has been asserted, you want to swich back to @file{HSound.l} and replay to the point you got stuck previously. Some hours (or days) later you have completed the soundness proof and are ready to tackle new challenges. Perhaps, you want to prove a property that builds on soundness or you want to prove an orthogonal property such as completeness. Proof General lets you do all of this while maintaining the consistency between proof script buffers and the state of the proof assistant. However, you cannot have more than one buffer where only a fraction of the proof script contains a locked region. Before you can employ script management in another proof script buffer, you must either fully assert or retract the current script buffer. @node View of processed files @section View of processed files Proof General is aware of all files that the proof assistant has processed or is currently processing. In fact, it relies on the proof assistant explicitly telling the Proof General whenever it processes a new file which corresponds@footnote{For example, LEGO generates additional compiled (optimised) proof script files for efficiency.} to a file containing a proof script. For further technical details, @pxref{Handling multiple files}. If the current proof script buffer depends on background material from other files, proof assistants typically process these files automatically. If you visit such a file, the whole file is locked as having been processed in a single step. From the user's point of view, you can only retract but not assert in this buffer. Furthermore, retraction is only possible to the @emph{beginning} of the buffer. To be more precise, buffers are locked as soon the Proof Assistant notifies the Proof General of processing a file different from the current proof script. Thus, if you visit the file while the Proof Assitant is still processing the file, it is already completely locked. If the Proof Assistant is not happy with the contents and complains with an error message, the buffer will still be marked as having been completely processed. Sorry. You need to visit the troublesome file, retract (which will always retract to the beginning of the file) and debug the problem e.g., by asserting all of the buffer under the supervision of the Proof General, @pxref{Script processing commands}. In case you wondered, inconsistencies may arise when you have unsaved changes in a proof script buffer and the Proof Assistant suddenly decides to automatically process the corresponding file. The good news is that Proof General detects this problem and flashes up a warning in the response buffer. You might then want to visit the modified buffer, save it and retract to the beginning. Then you are back on track. @node Retracting across files @section Retracting across files @cindex Retraction Make sure that the current script buffer has either been completely asserted or retracted. Then you can retract proof scripts in a different file. Simply visit a file that has been processed earlier and retract in it, using the retraction commands from @ref{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 Working directly with the proof shell @section Working directly with the proof shell @cindex Shell Occasionally you may want to review the dialogue of the entire session with the proof assistant, or check that it hasn't done something unexpected. Experienced users may also want to directly communicate with the Proof Assistant rather than sending commands via the minibuffer, @pxref{Proof assistant commands}. Although the proof shell is usually hidden from view, it is run in a buffer which provides the usual full editing and history facilities of Emacs shells (see the package @file{comint.el} distributed with your version of Emacs). You can switch to it using the menu: @lisp Proof-General -> Switch to buffers -> Proof 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. Proof General watches the output from the proof assistant to guess when a file is loaded or when a proof step is taken or undone, but it may not be guaranteed when the restricted interface is by-passed. What happens depends on how complete the communication is between Proof General and the prover (which depends on the particular instantion of Proof General). To resynchronise, you have two options. If you are lucky, it might suffice to @table @kbd @item C-c C-z move the end of the locked region backwards to the end of the segment containing the point. @end table Otherwise, you will need to restart script management altogether, @pxref{Toolbar commands}. @node Support for other Packages @chapter Support for other Packages @menu * Support for function menus:: * Support for tags:: @end menu @node Support for function menus @section Support for function menus @vindex proof-goal-with-hole-regexp @cindex fume-func fume-func is a handy package which makes a menu from the function declarations in a buffer. Proof General configures fume-func so that you can quickly jump to particular proofs in a script buffer. This is done with the configuration variable @code{proof-goal-with-hole-regexp}, @pxref{Proof script mode} for further details. If you want to use fume-func, you may need to enable it for yourself. It is distributed with XEmacs but by not enabled by default. To enable it you should find the file func-menu.el and follow the instructions there. At the time of writing, the current version of XEmacs is 20.4, supplied with function menu version 2.45, which suggests the following code for your @file{.emacs} file: @lisp (require 'func-menu) (define-key global-map 'f8 'function-menu) (add-hook 'find-file-hooks 'fume-add-menubar-entry) (define-key global-map "\C-cl" 'fume-list-functions) (define-key global-map "\C-cg" 'fume-prompt-function-goto) (define-key global-map '(shift button3) 'mouse-function-menu) (define-key global-map '(meta button1) 'fume-mouse-function-goto) @end lisp If you have another version of Emacs, you should check the fume-func.el file supplied with it. @node Support for tags @section Support for tags @cindex tags @c FIXME: instructions for setting up etags are needed @node Customizing Proof General @chapter Customizing Proof General @cindex Customization There are two kinds of customization for Proof General: it can be customized for a user's preferences using a particular proof assistant, or it can be customized by an Emacs expert to add a new proof assistant. Here we cover the user-level customization for Proof General. We only consider settings for Proof General itself. The support for a particular proof assistant can provide extra customization settings. See the chapters covering each assistant for details. @menu * Easy customization:: * Setting the user options:: * Changing faces:: * Tweaking configuration settings:: @end menu @node Easy customization @section Easy customization @cindex Using Customize @cindex Emacs customization library Proof General uses the Emacs customization library extensively to provide a friendly interface. You can access a menu of the customization settings for Proof General via the menu: @lisp Options -> Customize -> Emacs -> External -> Proof General @end lisp in XEmacs. In FSF Emacs, use the menu: @c FIXME @lisp Help -> Customize -> Specific group @end lisp and type @kbd{proof-general RET}. The complete set of customization settings will only be availabe after Proof General has been fully loaded. Proof General is fully loaded when you visit a script file for the first time. When visiting a script file, there is a more direct route to the settings: @lisp Proof-General -> Customize @end lisp Using the customize facility is straightforward. You can select the setting to customize via the menus, or with @code{M-x customize-variable}. When you have selected a setting, you are shown a buffer with its current value, and facility to edit it. Once you have edited it, you can use the special buttons @var{set}, @var{save} and @var{done}. You must use one of @var{set} or @var{save} to get any effect. The @var{save} button stores the setting in your @file{.emacs} file. For more help, see @inforef{Easy Customization, ,xemacs}. @node Setting the user options @section Setting the user options @c Index entries for each option 'concept' @cindex User options @cindex Strict read-only @cindex Query program name @cindex Dedicated windows @cindex Remote host @cindex Toolbar follow mode @cindex Toolbar disabling @cindex Proof script indentation @cindex Indentation @cindex Remote shell @cindex Running proof assistant remotely @c @cindex formatting proof script Here are the user options for Proof General. These can be set via the customization system, 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. Notice that in the customize menus, the variable names may be abbreviated by omitting the "@code{proof}-" prefix. 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 here. @defopt proof-prog-name-ask If non-@code{nil}, query user which program to run for the inferior process. The default value is @code{nil}. @end defopt @defopt proof-rsh-command A string to use as a prefix to allow a proof assistant to be run on a remote host. For example, @lisp ssh bigjobs @end lisp Would cause Proof General to issue the command @code{ssh bigjobs isabelle} to start Isabelle remotely on our large compute server called @code{bigjobs}. The protocol used should be configured so that no user interaction (passwords, or whatever) is required to get going. The default value is the empty string @code{""}. @end defopt @defopt proof-toolbar-wanted Whether to use toolbar in proof mode. Default is @code{t}. @end defopt @defopt proof-auto-delete-windows If non-nil, automatically remove windows when they are cleaned. For example, at the end of a proof the goals buffer window will be cleared; if this flag is set it will automatically be removed. If you use several frames to display the Proof General buffers, you may want to set this variable to 'nil' to avoid frames being deleted automatically. The default value is @code{t}. @end defopt @defopt proof-toolbar-follow-mode Choice of how point moves with toolbar commands. One of the symbols: @code{locked}, @code{follow}, @code{ignore}. If @code{locked}, point sticks to the end of the locked region with toolbar commands. @* If @code{follow}, point moves just when needed to display the locked region end. @* If @code{ignore}, point is never moved after toolbar movement commands. The default is @end defopt @defopt proof-window-dedicated Whether response and goals buffers have dedicated windows. If non-@code{nil}, windows displaying responses from the prover will not be switchable to display other windows. This helps manage your display, but can sometimes be inconvenient, especially for experienced Emacs users. @end defopt @c FIXME needs to mention that without dedicated windows, buffers may be @c hidden. Refer to the XEmacs manual on customising buffer display. @defopt proof-strict-read-only Whether Proof General is strict about the read-only region in buffers. If non-nil, an error is given when an attempt is made to edit the read-only region. If nil, Proof General is more relaxed (but may give you a reprimand!) @end defopt @defopt proof-script-indent If non-@code{nil}, enable indentation code for proof scripts. Currently the indentation code can be rather slow for large scripts, and is critical on the setting of regular expressions for particular provers. Enable it if it works for you. The default is @code{nil}. @end defopt @defopt proof-one-command-per-line If non-@code{nil}, format for newlines after each proof command in a script. This option is not fully-functional at the moment. The default is @code{nil}. @end defopt @node Changing faces @section Changing faces The fonts and colours that Proof General uses are configurable. @defopt proof-queue-face Face for commands in proof script waiting to be processed. @end defopt @defopt proof-locked-face Face for locked region of proof script (processed commands). @end defopt @defopt proof-declaration-name-face Face for declaration names in proof scripts. Exactly what uses this face depends on the proof assistant. @end defopt @defopt proof-tacticals-name-face Face for names of tacticals in proof scripts. Exactly what uses this face depends on the proof assistant. @end defopt @defopt proof-error-face Face for error messages from proof assistant. @end defopt @defopt proof-warning-face Face for warning messages. Could come either from proof assistant or Proof General itself. @end defopt @c Maybe this detail of explanation belongs in the internals, @c with just a hint here. The slightly bizarre name of the next face comes from the idea that while large amounts of output are being sent from the prover, some messages should be displayed to the user while the bulk of the output is hidden. The messages which are displayed may have a special annotation to help Proof General recognize them, and this is an "eager" annotation in the sense that it should be processed as soon as it is observed by Proof General. @defopt proof-eager-annotation-face Face for messages from proof assistant. @end defopt @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: @defvar proof-assistant-home-page Web address for information on proof assistant. @end defvar Most of the others are more complicated. More details of the settings are given in @xref{Adapting Proof General to New Provers}. To browse them, you can look through the customization groups @code{prover-config}, @code{proof-script} and @code{proof-shell}. The group @code{proof-script} contains the configuration variables for scripting, and the group @code{proof-shell} contains those for interacting with the proof assistant. Unfortunately, although you can use the customization mechanism to set and save these variables, saving them may have no effect because the default settings are often hard-wired into the proof assistant code. Ones we expect may need changing appear as proof assistant specific configurations. For example, @code{proof-assistant-home-page} is set in the LEGO code from the value of the customization setting @code{lego-www-home-page}. At present there is no easy way to save changes to other configuration variables across sessions, other than by editing the source code. Please contact us if this proves to be a problem for any variable. @c @c CHAPTER: LEGO Proof General @c @node LEGO Proof General @chapter LEGO Proof General @cindex LEGO Proof General LEGO proof script mode is a mode derived from proof script mode for editing LEGO scripts. An important convention is that proof script buffers @emph{must} start with a module declaration. If the proof script buffer's file name is @file{fermat.l}, then it must commence with a declaration of the form @lisp Module fermat; @end lisp If, in the development of the module @samp{fermat}, you require material from other module e.g., @samp{lib_nat} and @samp{galois}, you need to specify this dependency as part of the module declaration: @lisp Module fermat Import lib_nat galois; @end lisp No need to worry too much about effeciency. When you retract back to a module declaration to add a new import item, LEGO does not actually retract the previously imported modules. Therefore, reasserting the extended module declaration really only processes the newly imported modules. Using the LEGO Proof General, you never ever need to use administrative LEGO commands such as @samp{Forget}, @samp{ForgetMark}, @samp{KillRef}, @samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again @footnote{And please, don't even think of including those in your LEGO proof script!}. You can concentrate on your actual proof developments. Script management in the Proof General will invoke the appropriate commands for you. Proving with LEGO has never been easier. @menu * LEGO specific commands:: * LEGO tags:: * LEGO customizations:: @end menu @node LEGO specific commands @section LEGO specific commands In addition to the commands provided by the generic Proof General, see the previous sections, the LEGO Proof General provides a few extensions. In proof scripts, there are some abbreviations for common commands: @table @kbd @item C-c i intros @item C-c I Intros @item C-c R Refine @end table @node LEGO tags @section LEGO tags The LEGO Proof General provides the program @file{legotags} to generate tags for LEGO proof scripts. Invoking @samp{legotags *.l} produces a file @file{TAGS} for all LEGO modules in the current directory. The LEGO library itself is shipped out with all its modules already being tagged. See @ref{Support for tags} for further details. @node LEGO customizations @section LEGO customizations We refer to chapter @ref{Customizing Proof General} for an introduction to the customisation mechanism. In addition to customizations at the generic level, for LEGO you can also customize: @defopt lego-tags The directory of the TAGS table for the LEGO library. The default is @code{"/usr/lib/lego/lib_Type/"}. @end defopt @defopt lego-help-menu-list List of menu items, as defined in @code{easy-menu-define} for LEGO specific help. @end defopt @c We don't worry about the following for now. These are too obscure. @c lego-indent @c lego-test-all-name @c We also don't document any of the internal variables which have been @c set to configure the generic Proof General and which the user should @c not tamper with In Xemacs 20.4, LEGO script buffer are coloured (fontified as they say) by default. To automatically switch on fontification in FSF Emacs 20.2, you need to set @vindex lego-mode-hooks @cindex font-lock colour @lisp (add-hook 'lego-mode-hooks 'turn-on-font-lock) @end lisp in your @file{~/.emacs} file. @node Coq Proof General @chapter Coq Proof General @menu * Coq specific commands:: * Coq customizations:: @end menu @node Coq specific commands @section Coq specific commands @node Coq customizations @section Coq customizations @c @c CHAPTER: Isabelle Proof General @c @node Isabelle Proof General @chapter Isabelle Proof General @cindex Isabelle Proof General Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, @uref{http://www.dcs.ed.ac.uk/home/da/Isamode}. Detailed documentation for the theory file mode is included with @code{Isamode}, there are some notes on the special functions available and customization setttings below. @menu * Theory files:: * Isabelle specific commands:: * Isabelle customizations:: @end menu @node Theory files @section Theory files @cindex Theory files (in Isabelle) @cindex ML files (in Isabelle) Isabelle Proof General attempts to lock theory files as well as ML files when they are loaded. Theory files are always completely locked or completely unlocked, because they are processed atomically. Proof General attempts to load the theory file for a @file{.ML} file automatically before you start scripting. This is tricky because Isabelle's theory loader assumes that @file{.ML} files are always read together with theory files. At the moment Proof General uses an altered version of @code{use_thy} which doesn't load the top-level ML file in this case. @c FIXME: should say something about this: @c This can cause confusion in the theory loader later, @c especially with @code{update()}. To be safe, try to use just the Proof @c General interface, and report any repeatable problems to @c @code{isabelle@dcs.ed.ac.uk}. Compared to Isamode's theory editing mode, some of the functions and key bindings for interacting with Isabelle have been removed, and two new functions are available. The key @kbd{C-c C-b} (@code{isa-process-thy-file}) will cause Isabelle to read the theory file being edited. This causes the file and all its children (both theory and ML files) to be read. Any top-level ML file associated with this theory file is also read. The key @kbd{C-c C-u} (@code{isa-retract-thy-file}) will retract (unlock) the theory file being edited. This unlocks the file and all its children (theory and ML files); no changes occur in Isabelle itself. @node Isabelle specific commands @section Isabelle specific commands @unnumberedsubsec Switching to theory files @cindex Switching to theory files @kindex C-c C-o In Isabelle proofscript mode, @kbd{C-c C-o} (@code{thy-find-other-file}) finds and switches to the associated theory file, that is, the file with the same base name but extension @file{.thy} swapped for @file{.ML}. The same function (and keybinding) switches back to an ML file from the theory file. @deffn Command thy-find-other-file Find and switch to the associated ML file (when editing a theory file) or theory file (when editing an ML file). Usually the current window is split and the new file shown in the other window. With an optional argument (@kbd{C-u} prefix), the other file replaces the one in the current window. @end deffn @node Isabelle customizations @section Isabelle customizations Here are some of the user options specific to Isabelle. You can set these with the customization mechanism as usual. @defopt isabelle-web-page A string containing a URL for a web page for Isabelle. @end defopt @c @unnumberedsubsec Theory file editing customization @defopt thy-use-sml-mode If non-nil, attempt to use sml-mode in ML section of theory files. This option is left-over from Isamode. Really, it would be more useful if the script editing mode of Proof General itself could be based on sml-mode, but at the moment there is no way to do this. @end defopt @defopt thy-indent-level Indentation level for Isabelle theory files. An integer. @end defopt @defopt thy-sections A list containing names of theory file sections and their templates. Each item in the list is a pair of a section name and a template. A template is either a string to insert or a function. Useful functions are: @code{thy-insert-header}, @code{thy-insert-class}, @code{thy-insert-default-sort}, @code{thy-insert-const}, @code{thy-insert-rule}. The nil template does nothing. You can add extra sections to theory files by extending this variable. @end defopt @defopt thy-template Template for theory files. Contains a default selection of sections in a traditional order. You can use the following format characters: @code{%t} -- replaced by theory name @code{%p} -- replaced by names of parents, separated by @code{+}'s @end defopt @node Adapting Proof General to New Provers @chapter Adapting Proof General to New Provers Proof General has about 60 configuration variables which are set on a per-prover basis to configure the various features. However, many of these variables occcur in pairs (typically regular expressions matching the start and end of some text), and you can begin by setting just a few variables to get the basic features working. @menu * Skeleton example:: * Proof script settings:: * Proof shell settings:: @end menu @node Skeleton example @section Skeleton example Each proof assistant supported has its own subdirectory under @var{proof-home-directory}, used to store a root elisp file and any other files needed to adapt the proof assistant for Proof General. Here we show how a minimal configuration of Proof General works for Isabelle, without any special changes to Isabelle. @itemize @bullet @item Make a directory called 'myassistant' under the Proof General home directory, to put the specific customization and associated files in. @item Add a file myassistant.el to the new directory. @item Edit proof-site.el to add a new entry to the @var{proof-assistants-table} variable. The new entry should look like this: (myassistant "My New Assistant" "\\.myasst$") The first item is used to form the name of the internal variables for the new mode as well as the directory and file where it loads from. The second is a string, naming the proof assistant. The third item is a regular expression to match names of proof script files for this assistant. See the documentation of @var{proof-assistants-table} for more details. @item Define the new modes in myassistant.el, by looking at the files for the currently supported assistants for example. Basically you need to define some modes using @code{define-derived-mode} and set the configuration variables. You could begin by setting a minimum number of the variables, then adjust the settings via the customize menus, under Proof-General -> Internals. @end itemize @node Proof script settings @section Proof script settings @node Proof shell settings @section Proof shell settings @menu * Special annotations:: @end menu @node Special annotations @unnumberedsubsec Special annotations @node Internals of Proof General @chapter Internals of Proof General @menu * Proof script mode:: * Proof shell mode:: * Handling multiple files:: @end menu @node Proof script mode @section Proof script mode @node Proof shell mode @section Proof shell mode @node Handling multiple files @section Handling multiple files @cindex Multiple files Large proof developments are typically spread across multiple files. Many provers support such developments by keeping track of dependencies and automatically processing scripts. Proof General supports this mechanism. The user's point of view is explored further in @ref{Advanced Script Management}. Here, we describe the more technical nitty gritty. This is what you need to know when you customise another proof assistant to work with Proof General. The key idea is that we leave it to the specific proof assistant to worry about managing multiple files. But whenever the proof assistant processes or retracts a file it must clearly say so. @vindex proof-shell-eager-annotation-start @vindex proof-shell-eager-annotation-end Proof General considers @var{output} delimited by the the two regualar expressions @code{proof-shell-eager-annotation-start} and @code{proof-shell-eager-annotation-end} as being important. It displays the @var{output} in the Response buffer and analyses their contents further. Among possibly other important messages characterised by these regular expressions, the prover must tell the interface whenver it processes a file and retracts across file boundaries. @vtable @code @item proof-included-files-list records the file history. Whenever a new file is being processed, Proof General adds it to the front of the list. When the prover retracts across file boundaries, this list is resynchronised. It contains files in canonical truename format. @inforef{Truenames,,lispref}. You should not set this variable directly. The generic Proof General will modify @code{proof-included-files-list} itself. Instead, for a specific proof assistant you need to customise @code{proof-shell-process-file}. @code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list}. @item proof-shell-process-file is either nil or a tuple of the form (@var{regexp}, @var{function}). If @var{regexp} matches a substring of @var{str}, then the function @var{function} is invoked with input @var{str}. It must return a script file name (with complete path) the system is currently processing. In practice, @var{function} is likely to inspect the match data. @inforef{Match Data,,lispref}. Care has to be taken in case the prover only reports on compiled versions of files it is processing. In this case, @var{function} needs to reconstruct the corresponding script file name. The new (true) file name is then automatically added to the front of @code{proof-included-files-list} by the generic code. @item proof-shell-retract-files-regexp is a regular expression. It indicates that the prover has retracted across file boundaries. At this stage, Proof General's view of the processed files is out of date and needs to be updated with the help of the function @code{proof-shell-compute-new-files-list}. @end vtable @ftable @code @item proof-shell-compute-new-files-list Takes as argument the current output of the prover. It needs to return an up to date list of all processed files. Its output is then automatically stored in @code{proof-included-files-list} by the generic Proof General. In practice, this function is likely to inspect the previous (global) variable @code{proof-included-files-list} and the match data @inforef{Match Data,,lispref} triggered by @code{proof-shell-retract-files-regexp}. @end ftable @c @c @c CHAPTER: Obtaining and Installing Proof General @c @c @node Credits and References @chapter Credits and References @menu * Credits:: * References:: @end menu @node Credits @unnumberedsec Credits LEGO Proof General was written by Thomas Kleymann and Dilip Sequeira. Coq Proof General was written by Healfdene Goguen. Isabelle Proof General was written by David Aspinall. The generic base for Proof General was developed by all four of us. Thomas Kleymann provided the impetus to develop a generic Emacs interface, following ideas used in Projet CROAP, and with the help of Yves Bertot. David Aspinall provided the Proof General name and images. An early version of this manual was prepared by Dilip Sequeira. The present version was written by David Aspinall and Thomas Kleymann. During the development of Proof General, the following people helped by providing feedback, testing, or code: Pascal Brisset, Rod Burstall, Paul Callaghan, Martin Hofmann, James McKinna, and Markus Wenzel. Thanks to all of you! @node References @unnumberedsec References Script management as used in Proof General is described in the paper: @itemize @bullet @item Yves Bertot and Laurent Th@'ery. @i{A generic approach to building user interfaces for theorem provers}. To appear in Journal of Symbolic Computation. @end itemize Proof General has the beginnings of support for proof by pointing, as described in the document: @itemize @bullet @item 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: Obtaining and Installing Proof General @c @c @node Obtaining and Installing Proof General @appendix Obtaining and Installing Proof General Proof General has its own @uref{http://www.dcs.ed.ac.uk/home/proofgen,home page} hosted at Edinburgh. Visit this page for the latest news! @menu * Obtaining Proof General:: * Installing Proof General from tarball:: * Installing Proof General from RPM package:: * Notes for syssies:: @end menu @node Obtaining Proof General @section Obtaining Proof General You can obtain Proof General from the URL @example @uref{http://www.dcs.ed.ac.uk/home/proofgen/download.html}. @end example The distribution is available in three forms @itemize @bullet @item A source tarball, @* @uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz} @item A Linux RPM package (for any architecture), @* @uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm} @item A developer's tarball, @* @uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz} @end itemize Both the tarball and the RPM package include the generic elisp code, code for LEGO, Coq, and Isabelle, installation instructions (reproduced below) and this documentation. @c was Installing Proof General from @file{.tar.gz} @node Installing Proof General from tarball @section Installing Proof General from tarball Copy the distribution to some directory @var{mydir}. Unpack it there. For example: @example # cd @var{mydir} # gunzip ProofGeneral-@var{version}.tar.gz # tar -xpf ProofGeneral-@var{version}.tar @end example If you downloaded the version called @var{latest}, you'll find it unpacks to a numeric version number. Proof General will now be in some subdirectory of @var{mydir}. The name of the subdirectory will depend on the version number of Proof General. For example, it might be @file{ProofGeneral-2.0}. It's convenient to link it to a fixed name: @example # ln -sf ProofGeneral-2.0 ProofGeneral @end example Now put this line in your @file{.emacs} file: @lisp (load-file "@var{mydir}/ProofGeneral/generic/proof-site.el") @end lisp This command will load @file{proof-site} which sets the Emacs load path for Proof General and add auto-loads and modes for the assistants below: @multitable @columnfractions .3 .3 .4 @item @b{Prover} @tab @b{Extensions} @tab @b{Modes} @item Coq @tab @file{.v} @tab @code{coq-mode} @item LEGO @tab @file{.l} @tab @code{lego-mode} @item Isabelle @tab @file{.thy},@file{.ML} @tab @code{isa-mode} @end multitable When you load a file with one of these extensions, the corresponding Proof General mode will be entered. You can also invoke the mode command directly. The default names for proof assistant binaries may work on your system. If not, you will need to set the appropriate variables. The easiest way to do this (and most other customization of Proof General) is via the Customize mechanism, see the menu item: @example Proof-General -> Customize -> @var{Name of Assistant} -> Prog Name @end example The Proof-General menu is available from script buffers after Proof General is loaded. To load it manually, type @lisp M-x load-library RET proof RET @end lisp Notice that the customization mechanism is only available in Emacs 20.x and XEmacs. If you cannot use customize, simply add a line like this: @lisp (setq isabelle-prog-name "/usr/bin/isabelle FOL") @end lisp to your @file{.emacs} file. @node Installing Proof General from RPM package @section Installing Proof General from RPM package To install an RPM package you need to be root. Then type @example # rpm -Uvh ProofGeneral-latest.noarch.rpm @end example Now add the line: @lisp (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") @end lisp to your @file{.emacs} or the site-wide initialisation file @file{site-start.el}. @node 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 at the same time). You can compile Proof General by typing @code{make} in the directory where you installed it. @unnumberedsubsec Site-wide installation If you are installing Proof General site-wide, you can put the components in the standard directories of the filesystem if you prefer, providing the variables in @file{proof-site.el} are adjusted accordingly. Make sure that the @file{generic} and assistant-specific elisp files are kept in subdirectories (@file{coq}, @file{isa}, @file{lego}) of @code{proof-home-directory} so that the autoload directory calculations are correct. To prevent every user needing to edit their own @file{.emacs} files, you can put the @code{load-file} command to load @file{proof-site.el} into @file{site-start.el} or similar. Consult the Emacs documention for more details if you don't know where to find this file. @unnumberedsubsec Removing support for unwanted provers You cannot run more than one instance of Proof General at a time: so if you're using Coq, visiting an @file{.ML} file will not load Isabelle Proof General, and the buffer remains in fundamental mode. If there are some assistants supported that you never want to use, you can remove them from the variable @code{proof-assistants} in @file{proof-site.el} to solve this problem. Via the Customize mechanism, see the menu: @example Options -> Customize -> Emacs -> External -> Proof General @end example or, after loading Proof General, in a proof script buffer @example Proof-General -> Customize @end example @c @c @c APPENDIX: Known bugs and workarounds @c @c @node Known bugs and workarounds @appendix Known bugs and workarounds We only mention a few important problems here. The list is not a description of all bugs and may be out of date. @* Please consult the file @uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}} in the distribution for more detailed and up-to-date information. @* If you discover a problem which isn't mentioned in @file{BUGS}, please let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. @menu * Bugs at the generic level:: * Bugs specific to LEGO Proof General:: * Bugs specific to Coq Proof General:: * Bugs specific to Isabelle Proof General:: @end menu @node Bugs at the generic level @section Bugs at the generic level @unnumberedsubsec Undo in XEmacs When @code{proof-strict-read-only} is non-nil, ordinary undo in script buffer can edit the "uneditable region" in XEmacs. This doesn't happen in FSFmacs. Test case: Insert some nonsense text after the locked region. Kill the line. Process to the next command. Press @kbd{C-x u}, nonsense text appears in locked region. @strong{Workaround:} be careful with undo. @unnumberedsubsec Font locking and read-only in FSF Emacs When @code{proof-strict-read-only} is set and font lock is switched on, spurious "Region read only" errors are given which break font lock. @strong{Workaround:} turn off @code{proof-strict-read-only}, font lock, or for the best of all possible worlds, switch to XEmacs. @unnumberedsubsec Pressing keyboard quit @kbd{C-g} Using @kbd{C-g} can leave script management in a mess. The code is not properly protected from Emacs interrupts. @strong{Workaround:} Don't type @kbd{C-g} while script management is processing. If you do, use @code{proof-restart-scripting} to restart the system. @unnumberedsubsec One prover at a time You can't use more than one proof assistant at a time in the same Emacs session. Attempting to load Proof General for a second prover will fail, leaving a buffer in fundamental mode instead of the Proof General mode for proof scripts. @strong{Workaround:} stick to one prover per Emacs session, make sure that the proof-assistants variables only enables Proof General for the provers you need. @node Bugs specific to LEGO Proof General @section Bugs specific to LEGO Proof General @menu * Retraction and Discharge:: * Retraction and proving:: @end menu @node Retraction and Discharge @subsection Retraction and Discharge After a @code{Discharge}, retraction ought to only be possible back to the first declaration/definition which is discharged. However, LEGO Proof General does not know that @code{Discharge} has such a non-local effect. See @ref{Granularity of atomic command sequences} for a proposal on how to fix this bug. @strong{Workaround:} retract back to the first declaration/definition which is discharged. @node Retraction and proving @subsection Retraction and proving @cindex Retraction Getting retracting right is tricky when working on proofs. @unnumberedsubsec Definitions in a proof state A thorny issues are local definitions in a proof state. LEGO cannot undo them explicitly. @strong{Workaround:} retract back to a command before a definition. @unnumberedsubsec Normalisation in proofs Normalisation commands such as @samp{Dnf}, @samp{Hnf} @samp{Normal} cannot be undone in a proof state by the Proof General. @strong{Workaround:} retract back to the start of the proof. @unnumberedsubsec Not saving proofs. After LEGO has issued a @samp{*** QED ***} you may undo steps in the proof as long as you don't issue a @samp{Save} command or start a new proof. The LEGO Proof General assumes that all proofs are terminated with a proper @samp{Save} command. @strong{Workaround:} Always issue a @samp{Save} command after completing a proof. If you forget one, you should retract to a point before the offending proof development. @node Bugs specific to Coq Proof General @section Bugs specific to Coq Proof General @unnumberedsubsec Hard-wired tactics The collection of tactics which Proof General is aware of is hard-wired. Thus, user-defined tactics cannot be retracted. @strong{Workaround:} You may need to retract to the start of the proof. @unnumberedsubsec Sections The Coq Proof General does not know about Coq's section mechansim. @node Bugs specific to Isabelle Proof General @section Bugs specific to Isabelle Proof General @unnumberedsubsec Scripting lanugage limitations Since Isabelle uses ML as a top-level language for writing proof-scripts, Proof General may have difficulty understanding scripts which stray too far away from the standard functions, tactics, and tacticals. You will usually notice when a function, or whatever, doesn't get highlighted as you might expect. This probably has no detrimental impact on the interface unless you use your own variants of the @code{goal} or @code{qed} forms. @strong{Workaround:} Restrict yourself to standard proof script functions, or customize some of the variables from @file{isa.el} and @file{isa-syntax.el} appropriately. @node Plans and ideas @appendix Plans and ideas This section contains some tentative plans and ideas for improving Proof General. Please send us contributions to this wish list, or better still, offers to implement something from it! @menu * Granularity of atomic command sequences:: * Browser mode for script files and theories:: @end menu @node Granularity of atomic command sequences @section Granularity of atomic command sequences @c @cindex Granularity of Atomic Sequences @c @cindex Retraction @c @cindex Goal @c @cindex ACS (Atomic Command Sequence) This is a proposal by Thomas Kleymann for generalising the way Proof General handles sequences of proof commands @pxref{Goals and saves}, particularly to make retraction more flexible. The *Locked* region of a script buffer contains the initial segment of the proof script which has been processed successfully. It consists of atomic sequences of commands (ACS). Retraction is supported to the beginning of every ACS. By default, every command is an ACS. But the granularity of atomicity can be adjusted for different proof assistants. This is essential when arbitrary retraction is not supported. Usually, after a theorem has been proved, one may only retract to the start of the goal. One needs to mark the proof of the theorem as an ACS. @vtable @code @item proof-atomic-sequents-list is a list of instructions for setting up ACSs. Each instruction is a list of the form @code{(@var{end} @var{start} &optional @var{forget-command})}. @var{end} is a regular expression to recognise the last command in an ACS. @var{start} is a function. Its input is the last command of an ACS. Its output is a regular expression to recognise the first command of the ACS. It is evaluated once and the output is successively matched against previously processed commands until a match occurs (or the beginning of the current buffer is reached). The region determined by (@var{start},@var{end}) is locked as an ACS. Optionally, the ACS is annotated with the actual command to retract the ACS. This is computed by applying @var{forget-command} to the first and last command of the ACS. @end vtable @node Browser mode for script files and theories @section Browser mode for script files and theories This is a proposal by David Aspinall for a browser window. A browser window should provide support for browsing script files and theories. We should be able to inspect data in varying levels of detail, perhaps using outlining mechanisms. For theories, it would be nice to query the running proof assistant. This may require support from the assistant in the form of output which has been specially marked-up with an SGML like syntax, for example. A browser would be useful to: @itemize @bullet @item Provide impoverished proof assistants with a browser @item Extend the uniform interface of Proof General to theory browsing @item Interact closely with proof script-writing @end itemize The last point is the most important. We should be able to integrate a search mechanism for proofs of similar theorems, theorems containing particular constants, etc. @node Keystroke Index @unnumbered Keystroke Index @printindex ky @node Index @unnumbered Index @printindex cp @page @contents @bye