diff options
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 3930 |
1 files changed, 3930 insertions, 0 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi new file mode 100644 index 00000000..a2c3b256 --- /dev/null +++ b/doc/PG-adapting.texi @@ -0,0 +1,3930 @@ + +\def\fontdefs{\psfamily{bsf}{r}{c}{b}{b}{ri}{ri}{ro}{bo}\def\mainmagstep{1200}} +\input texinfo +@c TODO: setting for configuring proof hidden regions. +@c +@c +@c $Id$ +@c +@c NB: the first line of this file uses a non-standard TeXinfo +@c hack to print in Serifa fonts. It has no effect if you don't have +@c my hacked version of TeXinfo - da. +@c +@c +@setfilename PG-adapting.info +@settitle Adapting Proof General +@setchapternewpage odd +@paragraphindent 0 +@c A flag for whether to include the front image in the +@c DVI file. You can download the front image from +@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz +@c then put it into this directory and 'make dvi' (pdf,ps) +@c will set the flag below automatically. +@clear haveeps +@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://zermelo.dcs.ed.ac.uk/~isamode +@set URLpghome http://www.proofgeneral.org +@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz +@c +@c + +@c +@c IMPORTANT NOTE ABOUT THIS TEXINFO FILE: +@c I've tried keep full node lines *out* of this file because Emacs makes a +@c mess of updating them and they are a nuisance to do by hand. +@c Instead, rely on makeinfo and friends to do the equivalent job. +@c For this to work, we must follow each node +@c immediately with a section command, i.e.: +@c +@c @node node-name +@c <section-command> +@c +@c And each section with lower levels must have a menu command in +@c it. Menu updating with Emacs is a bit better than node updating, +@c but tends to delete the first section of the file in XEmacs! +@c (it's better in GNU Emacs at the time of writing). +@c +@c +@c reminder about references: +@c @xref{node} blah start of sentence: See [ref] +@c blah (@pxref{node}) blah bla (see [ref]), best at end of sentence +@c @ref{node} without "see". Careful for info. + + +@set version 3.5pre +@set xemacsversion 21.4 +@set fsfversion 21.2 +@set last-update September 2002 +@set rcsid $Id$ + +@ifinfo +@format +START-INFO-DIR-ENTRY +* Adapting Proof General: (PG-adapting). Adapt Proof General to new provers +END-INFO-DIR-ENTRY +@end format +@end ifinfo + +@c +@c MACROS +@c +@c define one here for a command with a key-binding? +@c +@c I like the idea, but it's maybe against the TeXinfo +@c style to fix together a command and its key-binding. +@c +@c merge functions and variables into concept index. +@c @syncodeindex fn cp +@c @syncodeindex vr cp + +@c merge functions into variables index +@c @syncodeindex fn vr + +@finalout +@titlepage +@title Adapting Proof General +@subtitle Proof General --- Organize your proofs! +@sp 1 +@subtitle Adapting Proof General @value{version} to new provers +@subtitle @value{last-update} +@subtitle @b{www.proofgeneral.org} + +@c nested ifs fail here completely, WHY? +@iftex +@ifset haveeps +@c @vskip 1cm +@c The .eps file takes 8.4M! A pity texi can't seem +@c to deal with gzipped files? (goes down to 1.7M). +@c But this still seems too much to put into the +@c PG distribution just for an image on the manual page, +@c so we take it out for now. +@c Ideally would like some way of generating eps from +@c the .jpg file. +@c image{ProofGeneralPortrait} +@end ifset +@end iftex +@author David Aspinall with T. Kleymann +@page +@vskip 0pt plus 1filll +This manual and the program Proof General are +Copyright @copyright{} 2000-2002 by members +of the 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 GNU Emacs @value{fsfversion} or +later versions. Proof General is distributed under the terms of the GNU +General Public License (GPL); please check the accompanying file +@file{COPYING} for more details. + +@sp 1 + +Visit Proof General on the web at @code{http://www.proofgeneral.org} + +Version control: @code{@value{rcsid}} +@end titlepage + +@page + + +@ifinfo +@node Top +@top Proof General + +This file documents configuration mechanisms for 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 GNU Emacs @value{fsfversion}. It is +supplied ready customized for the proof assistants Coq, Lego, +Isabelle, and HOL. + +This manual contains information for customizing to new proof +assistants; see the user manual for details about how to use +Proof General. + +@menu +* Introduction:: +* Beginning with a new prover:: +* Menus and toolbar and user-level commands:: +* Proof script settings:: +* Proof shell settings:: +* Goals buffer settings:: +* Splash screen settings:: +* Global constants:: +* Handling multiple files:: +* Configuring Font Lock:: +* Configuring X-Symbol:: +* Writing more lisp code:: +* Internals of Proof General:: +* Plans and ideas:: +* Demonstration Instantiations:: +* Function Index:: +* Variable Index:: +* Concept Index:: +@end menu +@end ifinfo + +@node Introduction +@unnumbered Introduction + +Welcome to Proof General! + +Proof General a generic Emacs-based interface for proof assistants. + +This manual contains information for adapting Proof General to new proof +assistants, and some sketches of the internal implementation. It is not +intended for most ordinary users of the system. +For full details about how to use Proof General, and information on its +availability and installation, please see the main Proof General manual +which should accompany this one. + +We positively encourage the support of new systems. Proof General has +grown more flexible and useful as it has been adapted to more proof +assistants. + +Typically, adding support for a new prover improves support for others, +both because the code becomes more robust, and because new ideas are +brought into the generic setting. Notice that the Proof General +framework has been built as a "product line architecture": generality +has been introduced step-by-step in a demand-driven way, rather than at +the outset as a grand design. Despite this strategy, the interface has +a surprisingly clean structure. The approach means that we fully expect +hiccups when adding support for new assistants, so the generic core may +need extension or modification. To support this we have an open +development method: if you require changes in the generic support, +please contact us (or make adjustments yourself and send them to us). + +Proof General has a home page at +@uref{http://www.proofgeneral.org}. Visit this page +for the latest version of the manuals, other documentation, system +downloads, etc. + + +@menu +* Future:: +* Credits:: +@end menu + +@node Future +@unnumberedsec Future +@cindex Proof General Kit +@cindex Future + +The aim of the Proof General project is to provide a powerful and +configurable interfaces which help user-interaction with interactive +proof assistants. + +The strategy Proof General uses is to targets power users rather than +novices; other interfaces have often neglected this class of users. But +we do include general user interface niceties, such as toolbar and +menus, which make use easier for all. + +Proof General has been Emacs based so far, but plans are afoot to +liberate it from the points and parentheses of Emacs Lisp. The +successor project Proof General Kit proposes that proof assistants use a +@i{standard} XML-based protocol for interactive proof, dubbed @b{PGIP}. + +PGIP enables 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. This means that effort on +customizing Emacs Proof General to a new proof assistant is worthwhile +even in the light of PGIP: it will help you to understand Proof +General's model of interaction, and moreover, we hope to use the Emacs +customizations to provide experimental filters which allow supported +provers to communicate using PGIP. + +At the time of writing, these ideas are in early stages. For latest +details, or to become involved, see +@uref{http://www.proofgeneral.org/kit, the Proof General Kit +webpage}. + + +@node Credits +@unnumberedsec Credits + +David Aspinall put together and wrote most of this manual. Thomas +Kleymann wrote some of the text in Chapter 8. Much of the content is +generated automatically from Emacs docstrings, some of which have been +written by other Proof General developers. + + + +@node Beginning with a new prover +@chapter Beginning with a new prover + +Proof General has about 100 configuration variables which are set on a +per-prover basis to configure the various features. It may sound like a +lot but don't worry! Many of the variables occur in pairs (typically +regular expressions matching the start and end of some text), and you +can begin by setting just a fraction of the variables to get the basic +features of script management working. The bare minimum for a working +prototype is about 25 simple settings. + +For more advanced features you may need (or want) to write some Emacs +Lisp. If you're adding new functionality please consider making it +generic for different proof assistants, if appropriate. When writing +your modes, please follow the Emacs Lisp conventions @inforef{Style +Tips, ,lispref}. + +The configuration variables are declared in the file +@file{generic/proof-config.el}. The details in the central part of this +manual are based on the contents of that file, beginning in @ref{Menus and toolbar +and user-level commands}, and continuing until @ref{Global constants}. +Other chapters cover the details of configuring for multiple files and +for supporting the other Emacs packages mentioned in the user manual +(@i{Support for other Packages}). If you write additional Elisp code +interfacing to Proof General, you can find out about some useful functions +by reading @ref{Writing more lisp code}. The last chapter of this +manual describes some of the internals of Proof General, in case you are +interested, maybe because you need to extend the generic core to do +something new. + +In the rest of this chapter we describe the general mechanisms for +instantiating Proof General. We assume some knowledge of the content +of the main Proof General manual. + +@menu +* Overview of adding a new prover:: +* Demonstration instance and easy configuration:: +* Major modes used by Proof General:: +@end menu + + +@node Overview of adding a new prover +@section Overview of adding a new prover + +Each proof assistant supported has its own subdirectory under +@code{proof-home-directory}, used to store a root elisp file and any +other files needed to adapt the proof assistant for Proof General. + +@c Here we show how a minimal configuration of Proof General works for +@c Isabelle, without any special changes to Isabelle. + +Here is how to go about adding support for a new prover. + +@enumerate +@item Make a directory called @file{myassistant/} under the Proof General home +directory @code{proof-home-directory}, to put the specific customization +and associated files in. +@item Add a file @file{myassistant.el} to the new directory. +@item Edit @file{proof-site.el} to add a new entry to the + @code{proof-assistants-table} variable. The new entry should look +like this: +@lisp + (myassistant "My Proof Assistant" "\\.myasst$") +@end lisp +The first item is used to form the name of the internal variables for +the new mode as well as the directory and file where it loads from. The +second is a string, naming the proof assistant. The third item is a +regular expression to match names of proof script files for this +assistant. See the documentation of @code{proof-assistant-table} for +more details. +@item Define the new Proof General modes in @file{myassistant.el}, + by setting configuration variables to customize the + behaviour of the generic modes. +@end enumerate + +@c You could begin by setting a minimum number of the variables, then +@c adjust the settings via the customize menus, under Proof-General -> +@c Internals. + +@c TEXI DOCSTRING MAGIC: proof-assistant-table +@defopt proof-assistant-table +Proof General's table of supported proof assistants.@* +Extend this table to add a new proof assistant. +Each entry is a list of the form +@lisp + (@var{symbol} @var{name} @var{automode-regexp}) +@end lisp +The @var{name} is a string, naming the proof assistant. +The @var{symbol} is used to form the name of the mode for the +assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp} +are visited. @var{symbol} is also used to form the name of the +directory and elisp file for the mode, which will be +@lisp + @var{proof-home-directory}/@var{symbol}/@var{symbol}.el +@end lisp +where @samp{PROOF-HOME-DIRECTORY} is the value of the +variable @code{proof-home-directory}. + +The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (isar "Isabelle/Isar" "\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (phox "PhoX" "\\.phx$") (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (twelf "Twelf" "\\.elf$") (plastic "Plastic" "\\.lf$") (lclam "Lambda-CLAM" "\\.lcm$"))}. +@end defopt + + +The final step of the description above is where the work lies. There +are two basic methods. You can write some Emacs lisp functions and +define the modes using the macro @code{define-derived-mode}. Or you can +use the new easy configuration mechanism of Proof General 3.0 described +in the next section, which calls @code{define-derived-mode} for you. +You still need to know which configuration variables should be set, and +how to set them. + +The documentation below (and inside Emacs) should help with that, but +the best way to begin might be to use an existing Proof General instance +as an example. + + +@node Demonstration instance and easy configuration +@section Demonstration instance and easy configuration + +Proof General is supplied with a demonstration instance for Isabelle +which configures the basic features. This is a whittled down version of +Isabelle Proof General, which you can use as a template to get support +for a new assistant going. Check the directory @file{demoisa} for the +two files @file{demoisa.el} and @file{demoisa-easy.el}. + +The file @file{demoisa.el} follows the scheme described in @ref{Major +modes used by Proof General}. It uses the Emacs Lisp macro +@code{define-derived-mode} to define the four modes for a Proof General +instance, by inheriting from the generic code. Settings which configure +Proof General are made by functions called from within each mode, as +appropriate. + +The file @file{demoisa-easy.el} uses a new simplified mechanism to +achieve (virtually) the same result. It uses the macro +@code{proof-easy-config} defined in @file{proof-easy-configl.el} to make +all of the settings for the Proof General instance in one go, defining +the derived modes automatically using a regular naming scheme. No lisp +code is used in this file except the call to this macro. The minor +difference in the end result is that all the variables are set at once, +rather than inside each mode. But since the configuration variables are +all global variables anyway, this makes no real difference. + +The macro @code{proof-easy-config} is called like this: +@lisp + (proof-easy-config @var{myprover} "@var{MyProver}" + @var{config_1} @var{val_1} + ... + @var{config_n} @var{val_n}) +@end lisp +The main body of the macro call is like the body of a @code{setq}. It +contains pairs of variables and value settings. The first argument to +the macro is a symbol defining the mode root, the second argument is a +string defining the mode name. These should be the same as the first +part of the entry in @code{proof-assistant-table} for your prover. +@xref{Overview of adding a new prover}. After the call to +@code{proof-easy-config}, the new modes @code{@var{myprover}-mode}, +@code{@var{myprover}-shell-mode}, @code{@var{myprover}-response-mode}, +and @code{@var{myprover}-goals-mode} will be defined. The configuration +variables in the body will be set immediately. + + +This mechanism is in fact recommended for new instantiations of +Proof General since it follows a regular pattern, and we can more +easily adapt it in the future to new versions of Proof General. + +Even Emacs Lisp experts should prefer the simplified mechanism. If you +want to set some buffer-local variables in your Proof General modes, or +invoke supporting lisp code, this can easily be done by adding functions +to the appropriate mode hooks after the @code{proof-easy-config} call. +For example, to add extra settings for the shell mode for +@code{demoisa}, we could do this: +@lisp + (defun demoisa-shell-extra-config () + @var{extra configuration ...} + ) + (add-hook 'demoisa-shell-mode-hook 'demoisa-shell-extra-config) +@end lisp +The function to do extra configuration @code{demoisa-shell-extra-config} +is then called as the final step when @code{demoisa-shell-mode} is +entered (be wary, this will be after the generic +@code{proof-shell-config-done} is called, so it will be too late to set +normal configuration variables which may be examined by +@code{proof-shell-config-done}). + + +@node Major modes used by Proof General +@section Major modes used by Proof General + +There are four major modes used by Proof General, one for each type of +buffer it handles. The buffer types are: script, shell, response and +goals. Each of these has a generic mode, respectively: +@code{proof-mode}, @code{proof-shell-mode}, @code{proof-response-mode}, +and @code{proof-goals-mode}. + +The pattern for defining the major mode for an instance of Proof General +is to use @code{define-derived-mode} to define a specific mode to inherit from +each generic one, like this: +@lisp +(define-derived-mode myass-shell-mode proof-shell-mode + "MyAss shell" nil + (myass-shell-config) + (proof-shell-config-done)) +@end lisp +Where @code{myass-shell-config} is a function which sets the +configuration variables for the shell (@pxref{Proof shell settings}). + +It's important that each of your modes invokes one of the functions + @code{proof-config-done}, + @code{proof-shell-config-done}, + @code{proof-response-config-done}, or + @code{proof-goals-config-done} +once it has set its configuration variables. These functions +finalize the configuration of the mode. + +For each mode, there is a configuration variable which names it so that +Proof General can set buffers to the proper mode, or find buffers in +that mode. These are documented below, and set like this: +@lisp + (setq proof-mode-for-script 'myass-mode) +@end lisp +where @code{myass-mode} is your major mode for scripts, derived from +@code{proof-mode}. You must set these variables before the proof shell +is started; one way to do this is inside a function which is called from +the hook @code{pre-shell-start-hook}. See the file @file{demoisa.el} +for details of how to do this. + +For future instantiations, it is recommended to follow the standard +scheme: @code{@var{PA}-mode}, @code{@var{PA}-shell-mode}, etc. + +@c TEXI DOCSTRING MAGIC: proof-mode-for-script +@defvar proof-mode-for-script +Mode for proof script buffers.@* +This is used by Proof General to find out which buffers +contain proof scripts. +The regular name for this is <PA>-mode. If you use any of the +convenience macros Proof General provides for defining commands +etc, then you should stick to this name. +Suggestion: this can be set in the script mode configuration. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-shell +@defvar proof-mode-for-shell +Mode for proof shell buffers.@* +Usually customised for specific prover. +Suggestion: this can be set a function called by @samp{@code{proof-pre-shell-start-hook}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-response +@defvar proof-mode-for-response +Mode for proof response buffer (and trace buffer, if used).@* +Usually customised for specific prover. +Suggestion: this can be set a function called by @samp{@code{proof-pre-shell-start-hook}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-goals +@defvar proof-mode-for-goals +Mode for proof state display buffers.@* +Usually customised for specific prover. +Suggestion: this can be set a function called by @samp{@code{proof-pre-shell-start-hook}}. +@end defvar + +@node Menus and toolbar and user-level commands +@chapter Menus, toolbar, and user-level commands + +The variables described in this chapter configure the menus, toolbar, +and user-level commands. They should be set in the script mode +before @code{proof-config-done} is called. (Toolbar configuration must +be made before @file{proof-toolbar.el} is loaded, which usually is +triggered automatically by an attempt to display the toolbar). + +@menu +* Settings for generic user-level commands:: +* Menu configuration:: +* Toolbar configuration:: +@end menu + +@node Settings for generic user-level commands +@section Settings for generic user-level commands + +@c TEXI DOCSTRING MAGIC: proof-assistant-home-page +@defvar proof-assistant-home-page +Web address for information on proof assistant.@* +Used for Proof General's help menu. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-context-command +@defvar proof-context-command +Command to display the context in proof assistant. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-info-command +@defvar proof-info-command +Command to ask for help or information in the proof assistant.@* +String or fn. If a string, the command to use. +If a function, it should return the command string to insert. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-showproof-command +@defvar proof-showproof-command +Command to display proof state in proof assistant. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-goal-command +@defvar proof-goal-command +Command to set a goal in the proof assistant. String or fn.@* +If a string, the format character @samp{%s} will be replaced by the +goal string. +If a function, it should return the command string to insert. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-save-command +@defvar proof-save-command +Command to save a proved theorem in the proof assistant. String or fn.@* +If a string, the format character @samp{%s} will be replaced by the +theorem name. +If a function, it should return the command string to insert. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-find-theorems-command +@defvar proof-find-theorems-command +Command to search for a theorem containing a given term. String or fn.@* +If a string, the format character @samp{%s} will be replaced by the term. +If a function, it should return the command string to insert. +@end defvar + + + +@node Menu configuration +@section Menu configuration + +As well as the generic Proof General menu, each proof assistant is +provided with a specific menu which can have prover-specific commands. +Proof General puts some default things on this menu, including the +commands to start/stop the prover, and the user-extensible "Favourites" +menu. + +@c TEXI DOCSTRING MAGIC: PA-menu-entries +@defvar PA-menu-entries +Extra entries for proof assistant specific menu. @* +A list of menu items [@var{name} @var{callback} @var{enabler} ...]. See the documentation +of @samp{@code{easy-menu-define}} for more details. +@end defvar + +@c TEXI DOCSTRING MAGIC: PA-help-menu-entries +@defvar PA-help-menu-entries +Extra entries for help submenu for proof assistant specific help menu.@* +A list of menu items [@var{name} @var{callback} @var{enabler} ...]. See the documentation +of @samp{@code{easy-menu-define}} for more details. +@end defvar + + +@node Toolbar configuration +@section Toolbar configuration + +Unlike the menus, Proof General has only one toolbar. For the "generic" +aspect of Proof General to work well, we shouldn't change (the meaning +of) the existing toolbar buttons too far. This would discourage people +from experimenting with different proof assistants when they don't +really know them, which is one of the advantages that Proof General +brings. + +But in case it is hard to map some of the generic buttons +onto functions in particular provers, and to allow extra +buttons, there is a mechanism for adjustment. + +I used The Gimp to create the buttons for Proof General. The +development distribution includes a button blank and some notes in +@file{etc/notes.txt} about making new buttons. + + +@c TEXI DOCSTRING MAGIC: proof-toolbar-entries-default +@defvar proof-toolbar-entries-default +Example value for proof-toolbar-entries. Also used to define scripting menu.@* +This gives a bare toolbar that works for any prover, providing the +appropriate configuration variables are set. +To add/remove prover specific buttons, adjust the @samp{<PA>-toolbar-entries} +variable, and follow the pattern in @samp{@code{proof-toolbar}.el} for +defining functions, images. +@end defvar + +@c TEXI DOCSTRING MAGIC: PA-toolbar-entries +@defvar PA-toolbar-entries +List of entries for Proof General toolbar and Scripting menu.@* +Format of each entry is (@var{token} @var{menuname} @var{tooltip} @var{dynamic-enabler-p} @var{enable}). + +For each @var{token}, we expect an icon with base filename @var{token}, +a function proof-toolbar-<TOKEN>, and (optionally) a dynamic enabler +proof-toolbar-<TOKEN>-enable-p. + +If @var{enablep} is absent, item is enabled; if @var{enablep} is present, item +is only added to menubar and toolbar if @var{enablep} is non-null. + +If @var{menuname} is nil, item will not appear on the scripting menu. + +If @var{tooltip} is nil, item will not appear on the toolbar. + +The default value is @samp{@code{proof-toolbar-entries-default}} which contains +the standard Proof General buttons. +@end defvar + +Here's an example of how to remove a button, from @file{af2.el}: +@lisp +(setq af2-toolbar-entries + (remassoc 'state af2-toolbar-entries)) +@end lisp + + + +@c defgroup proof-script +@node Proof script settings +@chapter Proof script settings + +The variables described in this chapter should be set in the script mode +before @code{proof-config-done} is called. These variables configure +recognition of commands in the proof script, and also control some of +the behaviour of script management. + + +@menu +* Recognizing commands and comments:: +* Recognizing proofs:: +* Recognizing other elements:: +* Configuring undo behaviour:: +* Nested proofs:: +* Safe (state-preserving) commands:: +* Activate scripting hook:: +* Automatic multiple files:: +* Completions:: +@end menu + + +@node Recognizing commands and comments +@section Recognizing commands and comments + +The first four settings configure the generic parsing strategy for +commands in the proof script. Usually only one of these three needs to +be set. If the generic parsing functions are not flexible for your +needs, you can supply a value for @code{proof-script-parse-function}. + +Note that for the generic functions to work properly, it is +@strong{essential} that you set the syntax table for your mode properly, +so that comments and strings are recognized. See the Emacs +documentation to discover how to do this (particularly for the function +@code{modify-syntax-entry}). + +@xref{Proof script mode}, for more details of the parsing +functions. + +@c TEXI DOCSTRING MAGIC: proof-terminal-char +@defvar proof-terminal-char +Character which terminates every command sent to proof assistant. nil if none. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-sexp-commands +@defvar proof-script-sexp-commands +Non-nil if proof script has a LISP-like syntax, and commands are @code{top-level} sexps.@* +You should set this variable in script mode configuration. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-command-start-regexp +@defvar proof-script-command-start-regexp +Regular expression which matches start of commands in proof script.@* +You should set this variable in script mode configuration. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-command-end-regexp +@defvar proof-script-command-end-regexp +Regular expression which matches end of commands in proof script.@* +You should set this variable in script mode configuration. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + + +The next four settings configure the comment syntax. Notice that to get +reliable behaviour of the parsing functions, you may need to modify the +syntax table for your prover's mode. Read the Elisp manual for details +about that. + +@c TEXI DOCSTRING MAGIC: proof-script-comment-start +@defvar proof-script-comment-start +String which starts a comment in the proof assistant command language.@* +The script buffer's @code{comment-start} is set to this string plus a space. +Moreover, comments are usually ignored during script management, and not +sent to the proof process. + +You should set this variable for reliable working of Proof General, +as well as @samp{@code{proof-script-comment-end}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-script-comment-start-regexp + +@defvar proof-script-comment-start-regexp +Regexp which matches a comment start in the proof command language. + +The default value for this is set as (@code{regexp-quote} @code{proof-script-comment-start}) +but you can set this variable to something else more precise if necessary. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-script-comment-end +@defvar proof-script-comment-end +String which ends a comment in the proof assistant command language.@* +The script buffer's @code{comment-end} is set to a space plus this string. +See also @samp{@code{proof-script-comment-start}}. + +You should set this variable for reliable working of Proof General, +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-comment-end-regexp +@defvar proof-script-comment-end-regexp +Regexp which matches a comment end in the proof command language. + +The default value for this is set as (@code{regexp-quote} @code{proof-script-comment-end}) +but you can set this variable to something else more precise if necessary. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-case-fold-search +@defvar proof-case-fold-search +Value for @code{case-fold-search} when recognizing portions of proof scripts.@* +Also used for completion, via @samp{@code{proof-script-complete}}. +The default value is @samp{nil}. If your prover has a case @strong{insensitive} +input syntax, @code{proof-case-fold-search} should be set to @samp{t} instead. +NB: This setting is not used for matching output from the prover. +@end defvar + + +@node Recognizing proofs +@section Recognizing proofs + +Up to three settings each may be supplied for recognizing goal-like and +save-like commands. The @code{-with-hole-} settings are used to make a +record of the name of the theorem proved, and also to build a default +value for the rather complicated setting +@code{proof-script-next-entity-regexps}, which activates the @i{function +menu} feature. + +The @code{-p} subsidiary predicates were added to allow more +discriminating behaviour for particular proof assistants. (This is a +typical example of where the core framework needs some additional +generalization, to simplify matters, and allow for a smooth handling of +nested proofs; the present state is only part of the way there). + + +@c TEXI DOCSTRING MAGIC: proof-goal-command-regexp +@defvar proof-goal-command-regexp +Matches a goal command in the proof script. @* +This is used (1) to make the default value for @samp{@code{proof-goal-command-p}}, +used as an important part of script management to find the start +of an atomic undo block, and (2) to construct the default +for @samp{@code{proof-script-next-entity-regexps}} used for function menus. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp +@defvar proof-goal-with-hole-regexp +Regexp which matches a command used to issue and name a goal.@* +The name of the theorem is build from the variable +@code{proof-goal-with-hole-result} using the same convention as +@code{query-replace-regexp}. +Used for setting names of goal..save regions and for default +@code{function-menu} configuration in @code{proof-script-find-next-entity}. + +It's safe to leave this setting as nil. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-goal-command-p +@defvar proof-goal-command-p +A function to test: is this really a goal command? + +This is added as a more refined addition to @code{proof-goal-command-regexp}, +to solve the problem that Coq and some other provers can have goals which +look like definitions, etc. (In the future we may generalize +@code{proof-goal-command-regexp} instead). +@end defvar + + +@c TEXI DOCSTRING MAGIC: proof-save-command-regexp +@defvar proof-save-command-regexp +Matches a save command. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp +@defvar proof-save-with-hole-regexp +Regexp which matches a command to save a named theorem.@* +The name of the theorem is build from the variable +@code{proof-save-with-hole-result} using the same convention as +@code{query-replace-regexp}. +Used for setting names of goal..save and proof regions and for +default @code{function-menu} configuration in @code{proof-script-find-next-entity}. + +It's safe to leave this setting as nil. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-completed-proof-behaviour +@defvar proof-completed-proof-behaviour +Indicates how Proof General treats commands beyond the end of a proof.@* +Normally goal...save regions are "closed", i.e. made atomic for undo. +But once a proof has been completed, there may be a delay before +the "save" command appears --- or it may not appear at all. Unless +nested proofs are supported, this can spoil the undo-behaviour in +script management since once a new goal arrives the old undo history +may be lost in the prover. So we allow Proof General to close +off the goal..[save] region in more flexible ways. +The possibilities are: +@lisp + nil - nothing special; close only when a save arrives + @code{'closeany} - close as soon as the next command arrives, save or not + @code{'closegoal} - close when the next "goal" command arrives + @code{'extend} - keep extending the closed region until a save or goal. +@end lisp +If your proof assistant allows nested goals, it will be wrong to close +off the portion of proof so far, so this variable should be set to nil. + +NB: @code{'extend} behaviour is not currently compatible with appearance of +save commands, so don't use that if your prover has save commands. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-really-save-command-p +@defvar proof-really-save-command-p +Is this really a save command? + +This is a more refined addition to @code{proof-save-command-regexp}. +It should be a function taking a span and command as argument, +and can be used to track nested proofs. (See what is done in +isar/ for example). In the future, this setting should be +removed when the generic core is extended to handle nested +proofs smoothly. +@end defvar + + +@node Recognizing other elements +@section Recognizing other elements + +To configure the @i{function menu} feature, there are a couple of +settings. These can be used to recognize named proofs, and other +elements in the proof script as well. + +@c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps +@defvar proof-script-next-entity-regexps +Regular expressions to help find definitions and proofs in a script.@* +This is the list of the form +@lisp + (@var{anyentity-regexp} + @var{discriminator-regexp} ... @var{discriminator-regexp}) +@end lisp +The idea is that @var{anyentity-regexp} matches any named entity in the +proof script, on a line where the name appears. This is assumed to be +the start or the end of the entity. The discriminators then test +which kind of entity has been found, to get its name. A +@var{discriminator-regexp} has one of the forms +@lisp + (@var{regexp} @var{matchnos}) + (@var{regexp} @var{matchnos} @code{'backward} @var{backregexp}) + (@var{regexp} @var{matchnos} @code{'forward} @var{forwardregexp}) +@end lisp +If @var{regexp} matches the string captured by @var{anyentity-regexp}, then +@var{matchnos} are the match numbers for the substrings which name the entity +(these may be either a single number or a list of numbers). + +If @code{'backward} @var{backregexp} is present, then the start of the entity +is found by searching backwards for @var{backregexp}. + +Conversely, if @code{'forward} @var{forwardregexp} is found, then the end of +the entity is found by searching forwards for @var{forwardregexp}. + +Otherwise, the start and end of the entity will be the region matched +by @var{anyentity-regexp}. + +This mechanism allows fairly complex parsing of the buffer, in +particular, it allows for goal..save regions which are named +only at the end. However, it does not parse strings, +comments, or parentheses. + +This variable may not need to be set: a default value which should +work for goal..saves is calculated from @code{proof-goal-with-hole-regexp}, +@code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-find-next-entity-fn +@defvar proof-script-find-next-entity-fn +Name of function to find next interesting entity in a script buffer.@* +This is used to configure @code{func-menu}. The default value is +@code{proof-script-find-next-entity}, which searches for the next entity +based on fume-function-name-regexp which by default is set from +@code{proof-script-next-entity-regexps}. + +The function should move point forward in a buffer, and return a cons +cell of the name and the beginning of the entity's region. + +Note that @code{proof-script-next-entity-regexps} is set to a default value +from @code{proof-goal-with-hole-regexp} and @code{proof-save-with-hole-regexp} in +the function @code{proof-config-done}, so you may not need to worry about any +of this. See whether function menu does something sensible by +default. +@end defvar + +@node Configuring undo behaviour +@section Configuring undo behaviour + +The settings here are used to configure the way "undo" commands are +calculated. + +@c TEXI DOCSTRING MAGIC: proof-non-undoables-regexp +@defvar proof-non-undoables-regexp +Regular expression matching commands which are @strong{not} undoable.@* +These are commands which should not appear in proof scripts, +for example, undo commands themselves (if the proof assistant +cannot "redo" an "undo"). +Used in default functions @samp{@code{proof-generic-state-preserving-p}} +and @samp{@code{proof-generic-count-undos}}. If you don't use those, +may be left as nil. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-undo-n-times-cmd +@defvar proof-undo-n-times-cmd +Command to undo n steps of the currently open goal.@* +String or function. +If this is set to a string, @samp{%s} will be replaced by the number of +undo steps to issue. +If this is set to a function, it should return the appropriate +command when called with an integer (the number of undo steps). + +This setting is used for the default @samp{@code{proof-generic-count-undos}}. +If you set @samp{@code{proof-count-undos-fn}} to some other function, there is no +need to set this variable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-ignore-for-undo-count +@defvar proof-ignore-for-undo-count +Matcher for script commands to be ignored in undo count.@* +May be left as nil, in which case it will be set to +@samp{@code{proof-non-undoables-regexp}}. +Used in default function @samp{@code{proof-generic-count-undos}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-count-undos-fn +@defvar proof-count-undos-fn +Function to calculate a command to issue undos to reach a target span.@* +The function takes a span as an argument, and should return a string +which is the command to undo to the target span. The target is +guaranteed to be within the current (open) proof. +This is an important function for script management. +The default setting @samp{@code{proof-generic-count-undos}} is based on the +settings @samp{@code{proof-non-undoables-regexp}} and +@samp{@code{proof-non-undoables-regexp}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-generic-count-undos +@defun proof-generic-count-undos span +Count number of undos in a span, return command needed to undo that far.@* +Command is set using @samp{@code{proof-undo-n-times-cmd}}. + +A default value for @samp{@code{proof-count-undos-fn}}. + +For this function to work properly, you must configure +@samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}. +@end defun + + + + + + +@c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn +@defvar proof-find-and-forget-fn +Function that returns a command to forget back to before its argument span.@* +This setting is used to for retraction (undoing) in proof scripts. + +It should undo the effect of all settings between its target span +up to (@code{proof-locked-end}). This may involve forgetting a number +of definitions, declarations, or whatever. + +The special string @code{proof-no-command} means there is nothing to do. + +This is an important function for script management. +Study one of the existing instantiations for examples of how to write it, +or leave it set to the default function @samp{@code{proof-generic-find-and-forget}} +(which see). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-generic-find-and-forget +@defun proof-generic-find-and-forget span +Calculate a forget/undo command to forget back to @var{span}.@* +This is a long-range forget: we know that there is no +open goal at the moment, so forgetting involves unbinding +declarations, etc, rather than undoing proof steps. + +This generic implementation assumes it is enough to find the +nearest following span with a @samp{name} property, and retract +that using @samp{@code{proof-forget-id-command}} with the given name. + +If this behaviour is not correct, you must customize the function +with something different. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-forget-id-command + + +@defvar proof-forget-id-command +Command to forget back to a given named span.@* +A string; @samp{%s} will be replaced by the name of the span. + +This is only used in the implementation of @samp{@code{proof-generic-find-and-forget}}, +you only need to set if you use that function (by not customizing +@samp{@code{proof-find-and-forget-fn}}. +@end defvar +@c TEXI DOCSTRING MAGIC: pg-topterm-goalhyp-fn +@defvar pg-topterm-goalhyp-fn +Function which returns cons cell if point is at a goal/hypothesis.@* +This is used to parse the proofstate output to mark it up for +proof-by-pointing. It should return a cons or nil. First element of +the cons is a symbol, @code{'goal'} or @code{'hyp'}. The second element is a +string: the goal or hypothesis itself. + +If you leave this variable unset, no proof-by-pointing markup +will be attempted. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-kill-goal-command +@defvar proof-kill-goal-command +Command to kill the currently open goal. + +If this is set to nil, PG will expect @code{proof-find-and-forget-fn} +to do all the work of retracting to an arbitrary point in a file. +Otherwise, the generic split-phase mechanism will be used: +@lisp + 1. If inside an unclosed proof, use proof-count-undos. + 2. If retracting to before an unclosed proof, use + @code{proof-kill-goal-command}, followed by @code{proof-find-and-forget-fn} + if necessary. +@end lisp +@end defvar + + + +@node Nested proofs +@section Nested proofs + +Proof General allows configuration for provers which have particular +notions of nested proofs. The right thing may happen automatically, +or you may need to adjust some of the following settings. + +First, you should alter the next setting if the prover retains history +for nested proofs. + +@c TEXI DOCSTRING MAGIC: proof-nested-goals-history-p +@defvar proof-nested-goals-history-p +Whether the prover supports recovery of history for nested proofs.@* +If it does (non-nil), Proof General will retain history inside +nested proofs. +If it does not, Proof General will amalgamate nested proofs into single +steps within the outer proof. +@end defvar +Second, it may happen (i.e. it does for Coq) that the prover has a +history mechanism which necessitates keeping track of the number of +nested "undoable" commands, even if the history of the proof itself is +lost. + +@c TEXI DOCSTRING MAGIC: proof-nested-undo-regexp +@defvar proof-nested-undo-regexp +Regexp for commands that must be counted in nested goal-save regions. + +Used for provers which allow nested atomic goal-saves, but with some +nested history that must be undone specially. + +At the moment, the behaviour is that a goal-save span has a @code{'nestedundos} +property which is set to the number of commands within it which match +this regexp. The idea is that the prover-specific code can create a +customized undo command to retract the goal-save region, based on the +@code{'nestedundos} setting. Coq uses this to forget declarations, since +declarations in Coq reside in a separate context with its own (flat) +history. +@end defvar + + +@node Safe (state-preserving) commands +@section Safe (state-preserving) commands + +A proof command is "safe" if it can be issued away from the proof +script. For this to work it should be state-preserving in the proof +assistant (with respect to an on-going proof). + +@c TEXI DOCSTRING MAGIC: proof-state-preserving-p +@defvar proof-state-preserving-p +A predicate, non-nil if its argument (a command) preserves the proof state.@* +This is a safety-test used by @code{proof-minibuffer-cmd} to filter out scripting +commands which should be entered directly into the script itself. + +The default setting for this function, @samp{@code{proof-generic-state-preserving-p}} +tests by negating the match on @samp{@code{proof-non-undoables-regexp}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-generic-state-preserving-p +@defun proof-generic-state-preserving-p cmd +Is @var{cmd} state preserving? Match on @code{proof-non-undoables-regexp}. +@end defun + + +@node Activate scripting hook +@section Activate scripting hook + + +@c TEXI DOCSTRING MAGIC: proof-activate-scripting-hook +@defvar proof-activate-scripting-hook +Hook run when a buffer is switched into scripting mode.@* +The current buffer will be the newly active scripting buffer. + +This hook may be useful for synchronizing with the proof +assistant, for example, to switch to a new theory +(in case that isn't already done by commands in the proof +script). + +When functions in this hook are called, the variable +@samp{activated-interactively} will be non-nil if +@code{proof-activate-scripting} was called interactively +(rather than as a side-effect of some other action). +If a hook function sends commands to the proof process, +it should wait for them to complete (so the queue is cleared +for scripting commands), unless activated-interactively is set. +@end defvar + + +@node Automatic multiple files +@section Automatic multiple files + +@xref{Handling multiple files}, for more details about this +setting. + +@c TEXI DOCSTRING MAGIC: proof-auto-multiple-files +@defvar proof-auto-multiple-files +Whether to use automatic multiple file management.@* +If non-nil, Proof General will automatically retract a script file +whenever another one is retracted which it depends on. It assumes +a simple linear dependency between files in the order which +they were processed. + +If your proof assistant has no management of file dependencies, or one +which depends on a simple linear context, you may be able to use this +setting to good effect. If the proof assistant has more complex +file dependencies then you should configure it to communicate with +Proof General about the dependencies rather than using this setting. +@end defvar + + +@node Completions +@section Completions + +Proof General allows provers to create a @i{completion table} to help +writing keywords and identifiers in proof scripts. This is documented +in the main @i{Proof General} user manual but summarized here for (a +different kind of) completion. + +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. Completion is usually a hand-wavy thing, so we don't +make any attempt to maintain a precise completion table or anything. + +The completion table maintained by @file{complete.el} is initialized +from @code{PA-completion-table} when @file{proof-script.el} is loaded. +This is done with the function @code{proof-add-completions} which +you may want to call at other times. + + +@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 C-return. + +If this table is empty or needs adjusting, please make changes using +@samp{@code{customize-variable}} and send suggestions to support@@proofgeneral.org +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-add-completions +@deffn Command proof-add-completions +Add completions from <PA>-completion-table to completion database.@* +Uses @samp{@code{add-completion}} with a negative number of uses and ancient +last use time, to discourage saving these into the users database. +@end deffn + + + + + + +@node Proof shell settings +@chapter Proof shell settings + +The variables in this chapter concern the proof shell mode, and are the +largest group. They are split into several subgroups. The first +subgroup are commands invoked at various points. The second subgroup of +variables are concerned with matching the output from the proof +assistant. The final subgroup contains various hooks which you can set +to add lisp customization to Proof General in various points (some of +them are also used internally for behaviour you may wish to adjust). + +Variables for configuring the proof shell are put into the customize +group @code{proof-shell}. + +These should be set in the shell mode configuration, before +@code{proof-shell-config-done} is called. + +To understand the way the proof assistant runs inside Emacs, you may +want to refer to the @code{comint.el} (Command interpreter) package +distributed with Emacs. This package controls several shell-like modes +available in Emacs, including the @code{proof-shell-mode} and +all specific shell modes derived from it. + +@menu +* Proof shell commands:: +* Script input to the shell:: +* Settings for matching various output from proof process:: +* Settings for matching urgent messages from proof process:: +* Hooks and other settings:: +@end menu + +@node Proof shell commands +@section Commands + +Settings in this section configure Proof General with commands +to send to the prover to activate certain actions. + +@c TEXI DOCSTRING MAGIC: proof-prog-name +@defvar proof-prog-name +System command to run the proof assistant in the proof shell.@* +Suggestion: this can be set in @code{proof-pre-shell-start-hook} from +a variable which is in the proof assistant's customization +group. This allows different proof assistants to coexist +(albeit in separate Emacs sessions). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-auto-terminate-commands + +@defvar proof-shell-auto-terminate-commands +Non-nil if Proof General should try to add terminator to every command.@* +If non-nil, whenever a command is sent to the prover using +@samp{@code{proof-shell-invisible-command}}, Proof General will check to see if it +ends with @code{proof-terminal-char}, and add it if not. +If @code{proof-terminal-char} is nil, this has no effect. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd +@defvar proof-shell-pre-sync-init-cmd +The command for configuring the proof process to gain synchronization.@* +This command is sent before Proof General's synchronization +mechanism is engaged, to allow customization inside the process +to help gain syncrhonization (e.g. engaging special markup). + +It is better to configure the proof assistant for this purpose +via command line options if possible, in which case this variable +does not need to be set. + +See also @samp{@code{proof-shell-init-cmd}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-init-cmd +@defvar proof-shell-init-cmd +The command for initially configuring the proof process.@* +This command is sent to the process as soon as synchronization is gained +(when an annotated prompt is first recognized). It can be used to configure +the proof assistant in some way, or print a welcome message +(since output before the first prompt is discarded). + +See also @samp{@code{proof-shell-pre-sync-init-cmd}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd +@defvar proof-shell-restart-cmd +A command for re-initialising the proof process. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd +@defvar proof-shell-quit-cmd +A command to quit the proof process. If nil, send EOF instead. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-quit-timeout +@defvar proof-shell-quit-timeout +The number of seconds to wait after sending @code{proof-shell-quit-cmd}.@* +After this timeout, the proof shell will be killed off more rudely. +If your proof assistant takes a long time to clean up (for +example writing persistent databases out or the like), you may +need to bump up this value. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd +@defvar proof-shell-cd-cmd +Command to the proof assistant to change the working directory.@* +The format character @samp{%s} is replaced with the directory, and +the escape sequences in @samp{@code{proof-shell-filename-escapes}} are +applied to the filename. + +This setting is used to define the function @code{proof-cd} which +changes to the value of (@code{default-directory}) for script buffers. +For files, the value of (@code{default-directory}) is simply the +directory the file resides in. + +NB: By default, @code{proof-cd} is called from @code{proof-activate-scripting-hook}, +so that the prover switches to the directory of a proof +script every time scripting begins. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-start-silent-cmd +@defvar proof-shell-start-silent-cmd +Command to turn prover goals output off when sending many script commands.@* +If non-nil, Proof General will automatically issue this command +to help speed up processing of long proof scripts. +See also @code{proof-shell-stop-silent-cmd}. +NB: terminator not added to command. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-stop-silent-cmd +@defvar proof-shell-stop-silent-cmd +Command to turn prover output on. @* +If non-nil, Proof General will automatically issue this command +to help speed up processing of long proof scripts. +See also @code{proof-shell-start-silent-cmd}. +NB: Terminator not added to command. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-silent-threshold +@defvar proof-shell-silent-threshold +Number of waiting commands in the proof queue needed to trigger silent mode.@* +Default is 2, but you can raise this in case switching silent mode +on or off is particularly expensive (or make it ridiculously large +to disable silent mode altogether). +@end defvar +@xref{Handling multiple files}, +for more details about the final two settings in this group, + + +@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-processed-cmd +@defvar proof-shell-inform-file-processed-cmd +Command to the proof assistant to tell it that a file has been processed.@* +The format character @samp{%s} is replaced by a complete filename for a +script file which has been fully processed interactively with +Proof General. See @samp{@code{proof-format-filename}} for other possibilities +to process the filename. + +This setting used to interface with the proof assistant's internal +management of multiple files, so the proof assistant is kept aware of +which files have been processed. Specifically, when scripting +is deactivated in a completed buffer, it is added to Proof General's +list of processed files, and the prover is told about it by +issuing this command. + +If this is set to nil, no command is issued. + +See also: @code{proof-shell-inform-file-retracted-cmd}, +@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd +@defvar proof-shell-inform-file-retracted-cmd +Command to the proof assistant to tell it that a file has been retracted.@* +The format character @samp{%s} is replaced by a complete filename for a +script file which Proof General wants the prover to consider as not +completely processed. See @samp{@code{proof-format-filename}} for other +possibilities to process the filename. + +This is used to interface with the proof assistant's internal +management of multiple files, so the proof assistant is kept aware of +which files have been processed. Specifically, when scripting +is activated, the file is removed from Proof General's list of +processed files, and the prover is told about it by issuing this +command. The action may cause the prover in turn to suggest to +Proof General that files depending on this one are +also unlocked. + +If this is set to nil, no command is issued. + +See also: @code{proof-shell-inform-file-processed-cmd}, +@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}. +@end defvar + + +@node Script input to the shell +@section Script input to the shell + +Generally, commands from the proof script are sent verbatim to the proof +process running in the proof shell. For historical reasons, carriage +returns are stripped by default. You can set +@code{proof-shell-strip-crs-from-input} to adjust that. For more +sophisticated pre-processing of the sent string, you may like to set +@code{proof-shell-insert-hook}. + +@c TEXI DOCSTRING MAGIC: proof-shell-strip-crs-from-input +@defvar proof-shell-strip-crs-from-input +If non-nil, replace carriage returns in every input with spaces.@* +This is enabled by default: it is appropriate for some systems +because several CR's can result in several prompts, which may mess +up the display (or even worse, the synchronization). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-insert-hook +@defvar proof-shell-insert-hook +Hooks run by @code{proof-shell-insert} before inserting a command.@* +Can be used to configure the proof assistant to the interface in +various ways -- for example, to observe or alter the commands sent to +the prover, or to sneak in extra commands to configure the prover. + +This hook is called inside a @code{save-excursion} with the @code{proof-shell-buffer} +current, just before inserting and sending the text in the +variable @samp{string}. The hook can massage @samp{string} or insert additional +text directly into the @code{proof-shell-buffer}. +Before sending @samp{string}, it will be stripped of carriage returns. + +Additionally, the hook can examine the variable @samp{action}. It will be +a symbol, set to the callback command which is executed in the proof +shell filter once @samp{string} has been processed. The @samp{action} variable +suggests what class of command is about to be inserted: +@lisp + @code{'proof-done-invisible} A non-scripting command + @code{'proof-done-advancing} A "forward" scripting command + @code{'proof-done-retracting} A "backward" scripting command +@end lisp +Caveats: You should be very careful about setting this hook. Proof +General relies on a careful synchronization with the process between +inputs and outputs. It expects to see a prompt for each input it +sends from the queue. If you add extra input here and it causes more +prompts than expected, things will break! Extending the variable +@samp{string} may be safer than inserting text directly, since it is +stripped of carriage returns before being sent. + +Example uses: +@var{lego} uses this hook for setting the pretty printer width if +the window width has changed; +Plastic uses it to remove literate-style markup from @samp{string}. +The x-symbol support uses this hook to convert special characters +into tokens for the proof assistant. +@end defvar + + + + + + +@node Settings for matching various output from proof process +@section Settings for matching various output from proof process + +These settings control the way Proof General reacts to process output. +The single most important setting is +@code{proof-shell-annotated-prompt-regexp}, which @b{must} be set as +part of the prover configuraton. This is used to configure the +communication with the prover process. + + +@c TEXI DOCSTRING MAGIC: proof-shell-wakeup-char +@defvar proof-shell-wakeup-char +A special character which terminates an annotated prompt.@* +Set to nil if proof assistant does not support annotated prompts. +@end defvar +@c TEXI DOCSTRING MAGIC: pg-subterm-first-special-char +@defvar pg-subterm-first-special-char +First special character.@* +Codes above this character can have special meaning to Proof General, +and are stripped from the prover's output strings. +Leave unset if no special characters are being used. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-prompt-pattern +@defvar proof-shell-prompt-pattern +Proof shell's value for comint-prompt-pattern, which see.@* +This pattern is just for interaction in comint (shell buffer). +You don't really need to set it. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp +@defvar proof-shell-annotated-prompt-regexp +Regexp matching a (possibly annotated) prompt pattern. + +@var{this} IS THE @var{most} @var{important} @var{setting} TO @var{configure}!! + +Output is grabbed between pairs of lines matching this regexp, +and the appearance of this regexp is used by Proof General to +recognize when the prover has finished processing a command. + +To help speed up matching you may be able to annotate the +proof assistant prompt with a special character not appearing +in ordinary output. The special character should appear in +this regexp, and should be the value of @code{proof-shell-wakeup-char}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-abort-goal-regexp +@defvar proof-shell-abort-goal-regexp +Regexp matching output from an aborted proof. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-error-regexp +@defvar proof-shell-error-regexp +Regexp matching an error report from the proof assistant. + +We assume that an error message corresponds to a failure in the last +proof command executed. So don't match mere warning messages with +this regexp. Moreover, an error message should not be matched as an +eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it +will be lost. + +Error messages are considered to begin from @code{proof-shell-error-regexp} +and continue until the next prompt. The variable +@samp{@code{proof-shell-truncate-before-error}} controls whether text before the +error message is displayed. + +The engine matches interrupts before errors, see @code{proof-shell-interrupt-regexp}. + +It is safe to leave this variable unset (as nil). +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp +@defvar proof-shell-interrupt-regexp +Regexp matching output indicating the assistant was interrupted.@* +We assume that an interrupt message corresponds to a failure in the last +proof command executed. So don't match mere warning messages with +this regexp. Moreover, an interrupt message should not be matched as an +eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it +will be lost. + +The engine matches interrupts before errors, see @code{proof-shell-error-regexp}. + +It is safe to leave this variable unset (as nil). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-truncate-before-error +@defvar proof-shell-truncate-before-error +Non-nil means truncate output that appears before error messages.@* +If nil, the whole output that the prover generated before the last +error message will be shown. + +NB: the default setting for this is @samp{t} to be compatible with +behaviour in Proof General before version 3.4. The more obvious +setting for new instances is probably @samp{nil}. + +Interrupt messages are treated in the same way. +See @samp{@code{proof-shell-error-regexp}} and @samp{@code{proof-shell-interrupt-regexp}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp +@defvar proof-shell-proof-completed-regexp +Regexp matching output indicating a finished proof. + +When output which matches this regexp is seen, we clear the goals +buffer in case this is not also marked up as a @samp{goals} type of +message. + +We also enable the QED function (save a proof) and we may automatically +close off the proof region if another goal appears before a save +command, depending on whether the prover supports nested proofs or not. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp +@defvar proof-shell-start-goals-regexp +Regexp matching the start of the proof state output.@* +This is an important setting. Output between @samp{@code{proof-shell-start-goals-regexp}} +and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer +and possibly analysed further for proof-by-pointing markup. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp +@defvar proof-shell-end-goals-regexp +Regexp matching the end of the proof state output, or nil.@* +If nil, just use the rest of the output following @code{proof-shell-start-goals-regexp}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp +@defvar proof-shell-assumption-regexp +A regular expression matching the name of assumptions. + +At the moment, this setting is not used in the generic Proof General. + +In the future it will be used for a generic implementation for @samp{@code{pg-topterm-goalhyp-fn}}, +used to help parse the goals buffer to annotate it for proof by pointing. +@end defvar + + + +@node Settings for matching urgent messages from proof process +@section Settings for matching urgent messages from proof process + +Among the various dialogue messages that the proof assistant outputs +during proof, Proof General can consider certain messages to be +"urgent". When processing many lines of a proof, Proof General will +normally supress the output, waiting until the final message appears +before displaying anything to the user. Urgent messages escape this: +typically they include messages that the prover wants the user to +notice, for example, perhaps, file loading messages, or timing +statistics. + +So that Proof General notices, these urgent messages should be marked-up +with "eager" annotations. + +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start +@defvar proof-shell-eager-annotation-start +Eager annotation field start. A regular expression or nil.@* +An eager annotation indicates to Proof General that some following output +should be displayed (or processed) immediately and not accumulated for +parsing later. + +It is nice to recognize (starts of) warnings or file-reading messages +with this regexp. You must also recognize any special messages +from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}}, +@samp{@code{proof-shell-retract-files-regexp}}, etc.) + +See also @samp{@code{proof-shell-eager-annotation-start-length}}, +@samp{@code{proof-shell-eager-annotation-end}}. + +Set to nil to disable this feature. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start-length + +@defvar proof-shell-eager-annotation-start-length +Maximum length of an eager annotation start. @* +Must be set to the maximum length of the text that may match +@samp{@code{proof-shell-eager-annotation-start}} (at least 1). +If this value is too low, eager annotations may be lost! + +This value is used internally by Proof General to optimize the process +filter to avoid unnecessary searching. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end +@defvar proof-shell-eager-annotation-end +Eager annotation field end. A regular expression or nil.@* +An eager annotation indicates to Emacs that some following output +should be displayed or processed immediately. + +See also @samp{@code{proof-shell-eager-annotation-start}}. + +It is nice to recognize (ends of) warnings or file-reading messages +with this regexp. You must also recognize (ends of) any special messages +from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}}, +@samp{@code{proof-shell-retract-files-regexp}}, etc.) + +The default value is "\n" to match up to the end of the line. +@end defvar + + +The default action for urgent messages is to display them in the +response buffer, highlighted. But we also allow for some control +messages, issued from the proof assistant to Proof General and not +intended for the user to see. These are recognized in the same way as +urgent messages (marked with eager annotations), so they will +be acted on as soon as they are issued by the prover. + + +@c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp +@defvar proof-shell-clear-response-regexp +Regexp matching output telling Proof General to clear the response buffer.@* +This feature is useful to give the prover more control over what output +is shown to the user. Set to nil to disable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-clear-goals-regexp +@defvar proof-shell-clear-goals-regexp +Regexp matching output telling Proof General to clear the goals buffer.@* +This feature is useful to give the prover more control over what output +is shown to the user. Set to nil to disable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-set-elisp-variable-regexp +@defvar proof-shell-set-elisp-variable-regexp +Regexp matching output telling Proof General to set some variable.@* +This allows the proof assistant to configure Proof General directly +and dynamically. + +If the regexp matches output from the proof assistant, there should be +two match strings: (@code{match-string} 1) should be the name of the elisp +variable to be set, and (@code{match-string} 2) should be the value of the +variable (which will be evaluated as a lisp expression). + +A good markup for the second string is to delimit with #'s, since +these are not valid syntax for elisp evaluation. + +Elisp errors will be trapped when evaluating; set +@code{proof-show-debug-messages} to be informed when this happens. + +Example uses are to adjust PG's internal copies of proof assistant's +settings, or to make automatic dynamic syntax adjustments in Emacs to +match changes in theory, etc. + +If you pick a dummy variable name (e.g. @samp{proof-dummy-setting}) you +can just evaluation arbitrary elisp expressions for their side +effects, to adjust menu entries, or even launch auxiliary programs. +But use with care -- there is no protection against catastrophic elisp! + +This setting could also be used to move some configuration settings +from PG to the prover, but this is not really supported (most settings +must be made before this mechanism will work). In future, the PG +standard protocol, @var{pgip}, will use this mechanism for making all +settings. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-theorem-dependency-list-regexp +@defvar proof-shell-theorem-dependency-list-regexp +Regexp matching output telling Proof General about dependencies.@* +This is to allow navigation and display of dependency information. +The output from the prover should be a message with the form +@lisp + @var{dependencies} OF X Y Z ARE A B C +@end lisp +with X Y Z, A B C separated by whitespace or somehow else (see +@samp{@code{proof-shell-theorem-dependency-list-split}}. This variable should +be set to a regexp to match the overall message (which should +be an urgent message), with two sub-matches for X Y Z and A B C. + +This is an experimental feature, currently work-in-progress. +@end defvar + +Two important control messages are recognized by +@code{proof-shell-process-file} and +@code{proof-shell-retract-files-regexp}, used for synchronizing Proof +General with a file loading mechanism built into the proof assistant. +@xref{Handling multiple files}, for more details about how to use the +final three settings described here. + +@vindex proof-included-files-list +@c TEXI DOCSTRING MAGIC: proof-shell-process-file +@defvar proof-shell-process-file +A pair (@var{regexp} . @var{function}) to match a processed file name. + +If @var{regexp} matches output, then the function @var{function} is invoked on the +output string chunk. It must return the name of a script file (with +complete path) that the system has successfully processed. In +practice, @var{function} is likely to inspect the match data. If it returns +the empty string, the file name of the scripting buffer is used +instead. If it returns nil, no action is taken. + +Care has to be taken in case the prover only reports on compiled +versions of files it is processing. In this case, @var{function} needs to +reconstruct the corresponding script file name. The new (true) file +name is added to the front of @samp{@code{proof-included-files-list}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp +@defvar proof-shell-retract-files-regexp +Matches a message that the prover has retracted a file. + +At this stage, Proof General's view of the processed files is out of +date and needs to be updated with the help of the function +@samp{@code{proof-shell-compute-new-files-list}}. +@end defvar +@vindex proof-included-files-list + +@c TEXI DOCSTRING MAGIC: proof-shell-compute-new-files-list +@defvar proof-shell-compute-new-files-list +Function to update @samp{proof-included-files list}. + +It needs to return an up to date list of all processed files. Its +output is stored in @samp{@code{proof-included-files-list}}. Its input is the +string of which @samp{@code{proof-shell-retract-files-regexp}} matched a +substring. In practice, this function is likely to inspect the +previous (global) variable @samp{@code{proof-included-files-list}} and the match +data triggered by @samp{@code{proof-shell-retract-files-regexp}}. +@end defvar + + + +@node Hooks and other settings +@section Hooks and other settings + +@c TEXI DOCSTRING MAGIC: proof-shell-filename-escapes +@defvar proof-shell-filename-escapes +A list of escapes that are applied to %s for filenames.@* +A list of cons cells, car of which is string to be replaced +by the cdr. +For example, when directories are sent to Isabelle, HOL, and Coq, +they appear inside ML strings and the backslash character and +quote characters must be escaped. The setting +@lisp + '(("@var{\\\\}" . "@var{\\\\}") + ("\"" . "\\\"")) +@end lisp +achieves this. This does not apply to @var{lego}, which does not +need backslash escapes and does not allow filenames with +quote characters. + +This setting is used inside the function @samp{@code{proof-format-filename}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type +@defvar proof-shell-process-connection-type +The value of @code{process-connection-type} for the proof shell.@* +Set non-nil for ptys, nil for pipes. +The default (and preferred) option is to use pty communication. +However there is a long-standing backslash/long line problem with +Solaris which gives a mess of ^G characters when some input is sent +which has a in the 256th position. +So we select pipes by default if it seems like we're on Solaris. +We do not force pipes everywhere because this risks loss of data. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-pre-shell-start-hook +@defvar proof-pre-shell-start-hook +Hooks run before proof shell is started.@* +Suggestion: set this to a function which configures just these proof +shell variables: +@lisp + @code{proof-prog-name} + @code{proof-mode-for-shell} + @code{proof-mode-for-response} + @code{proof-mode-for-goals} + @code{proof-shell-trace-output-regexp} +@end lisp +This is the bare minimum needed to get a shell buffer and +its friends configured in the function @code{proof-shell-start}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook +@defvar proof-shell-handle-error-or-interrupt-hook +Run after an error or interrupt has been reported in the response buffer.@* +Hook functions may inspect @samp{@code{proof-shell-error-or-interrupt-seen}} to +determine whether the cause was an error or interrupt. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook +@defvar proof-shell-pre-interrupt-hook +Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@* +This hook is added to allow customization for Poly/ML and other +systems where the system queries the user before returning to +the top level. For Poly/ML it can be used to send the string "f", +for example. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-output-system-specific +@defvar proof-shell-process-output-system-specific +Set this variable to handle system specific output.@* +Errors, start of proofs, abortions of proofs and completions of +proofs are recognised in the function @samp{@code{proof-shell-process-output}}. +All other output from the proof engine is simply reported to the +user in the @var{response} buffer. + +To catch further special cases, set this variable to a pair of +functions '(condf . actf). Both are given (cmd string) as arguments. +@samp{cmd} is a string containing the currently processed command. +@samp{string} is the response from the proof system. To change the +behaviour of @samp{@code{proof-shell-process-output}}, (condf cmd string) must +return a non-nil value. Then (actf cmd string) is invoked. + +See the documentation of @samp{@code{proof-shell-process-output}} for the required +output format. +@end defvar + + + + + +@node Goals buffer settings +@chapter Goals buffer settings + +The goals buffer settings allow configuration of Proof General for proof +by pointing or similar features. +See the Proof General @uref{http://www.proofgeneral.org/doc, documentation web page} +for a link to the technical report ECS-LFCS-97-368 which hints +at how to use these settings. + +@c At the moment these settings are disabled. + +@c TEXI DOCSTRING MAGIC: pg-goals-change-goal +@defvar pg-goals-change-goal +Command to change to the goal @samp{%s} +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-goal-command +@defvar pbp-goal-command +Command sent when @samp{@code{pg-goals-button-action}} is requested on a goal. +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-hyp-command +@defvar pbp-hyp-command +Command sent when @samp{@code{pg-goals-button-action}} is requested on an assumption. +@end defvar +@c TEXI DOCSTRING MAGIC: pg-goals-error-regexp +@defvar pg-goals-error-regexp +Regexp indicating that the proof process has identified an error. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-result-start +@defvar proof-shell-result-start +Regexp matching start of an output from the prover after pbp commands.@* +In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-result-end +@defvar proof-shell-result-end +Regexp matching end of output from the prover after pbp commands.@* +In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: pg-subterm-start-char +@defvar pg-subterm-start-char +Opening special character for subterm markup.@* +Subsequent special characters with values @strong{below} +@code{pg-subterm-first-special-char} are assumed to be subterm position +indicators. Annotations should be finished with @code{pg-subterm-sep-char}; +the end of the concrete syntax is indicated by @code{pg-subterm-end-char}. + +If @samp{@code{pg-subterm-start-char}} is nil, subterm markup is disabled. + +See doc of @samp{@code{pg-goals-analyse-structure}} for more details of +subterm and proof-by-pointing markup mechanisms.. +@end defvar +@c TEXI DOCSTRING MAGIC: pg-subterm-sep-char +@defvar pg-subterm-sep-char +Finishing special for a subterm markup.@* +See doc of @samp{@code{pg-subterm-start-char}}. +@end defvar +@c TEXI DOCSTRING MAGIC: pg-topterm-char +@defvar pg-topterm-char +Annotation character that indicates the beginning of a "top" element.@* +A "top" element may be a sub-goal to be proved or a named hypothesis, +for example. It is currently assumed (following @var{lego}/Coq conventions) +to span a whole line. + +The function @samp{@code{pg-topterm-goalhyp-fn}} examines text following this +special character, to determine what kind of top element it is. + +This setting is also used to see if proof-by-pointing features +are configured. If it is unset, some of the code +for parsing the prover output is disabled. +@end defvar +@c TEXI DOCSTRING MAGIC: pg-subterm-end-char +@defvar pg-subterm-end-char +Closing special character for subterm markup.@* +See @samp{@code{pg-subterm-start-char}}. +@end defvar + + +@node Splash screen settings +@chapter Splash screen settings + +The splash screen can be configured, in a rather limited way. + +@c TEXI DOCSTRING MAGIC: proof-splash-time +@defvar proof-splash-time +Minimum number of seconds to display splash screen for.@* +The splash screen may be displayed for a couple of seconds longer than +this, depending on how long it takes the machine to initialise +Proof General. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-splash-contents +@defvar proof-splash-contents +Evaluated to configure splash screen displayed when entering Proof General.@* +A list of the screen contents. If an element is a string or an image +specifier, it is displayed centred on the window on its own line. +If it is nil, a new line is inserted. +@end defvar + + + + + + +@node Global constants +@chapter Global constants + +The settings here are internal constants used by Proof General. +You don't need to configure these for your proof assistant +unless you want to modify or extend the defaults. + +@c TEXI DOCSTRING MAGIC: proof-general-name +@defvar proof-general-name +Proof General name used internally and in menu titles. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-general-home-page +@defopt proof-general-home-page +Web address for Proof General + +The default value is @code{"http://www.proofgeneral.org"}. +@end defopt +@c TEXI DOCSTRING MAGIC: proof-universal-keys +@defvar proof-universal-keys +List of key-bindings made for the script, goals and response buffer. @* +Elements of the list are tuples @samp{(k . f)} +where @samp{k} is a @code{key-binding} (vector) and @samp{f} the designated function. +@end defvar + + + +@node Handling multiple files +@chapter 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 considered in the user manual. +Here, we describe the more technical nitty gritty. This is what you +need to know when you customise another proof assistant to work with +Proof General. + +Documentation for the configuration settings mentioned here appears in +the previous sections, this section is intended to help explain the use +of those settings. + +Proof General maintains a list @code{proof-included-files-list} of files +which it thinks have been processed by the proof assistant. When a file +which is on this list is visited in Emacs, it will be coloured entirely +blue to indicate that it has been processed. No editing of the file +will be allowed (unless @code{proof-strict-read-only} allows it). + + +@c TEXI DOCSTRING MAGIC: proof-included-files-list +@defvar proof-included-files-list +List of files currently included in proof process.@* +This list contains files in canonical truename format +(see @samp{@code{file-truename}}). + +Whenever a new file is being processed, it gets added to this list +via the @code{proof-shell-process-file} configuration settings. +When the prover retracts a file, this list is resynchronised via the +@code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list} +configuration settings. + +Only files which have been @strong{fully} processed should be included here. +Proof General itself will automatically add the filenames of a script +buffer which has been completely read when scripting is deactivated. +It will automatically remove the filename of a script buffer which +is completely unread when scripting is deactivated. + +NB: Currently there is no generic provision for removing files which +are only partly read-in due to an error, so ideally the proof assistant +should only output a processed message when a file has been successfully +read. +@end defvar + +The way that @code{proof-included-files-list} is maintained is the key +to multiple file management. (But you should not set this variable +directly, it is managed via the configuration settings). + +@vindex proof-shell-process-file +@vindex proof-shell-retract-files-regexp +@vindex proof-shell-compute-new-files-list + +There is a range of strategies for managing multiple files. Ideally, +file dependencies should be managed by the proof assistant. Proof +General will use the prover's low-level commands to process a whole file +and its requirements non-interactively, without going through script +management. So that the user knows which files have been processed, the +proof assistant should issue messages which Proof General can recognize +(``file @code{foo} has been processed'') --- see +@code{proof-shell-process-file}. When the user wants to edit a file +which has been processed, the file must be retracted (unlocked). The +proof assistant should provide a command corresponding to this action, +which undoes a given file and all its dependencies. As each file is +undone, a message should be issued which Proof General can recognize +(``file @code{foo} has been undone'') -- see +@code{proof-shell-retract-files-regexp}. (The function +@code{proof-shell-compute-new-files-list} should be set to calculate the +new value for @code{proof-included-files-list} after a retract message +has been seen). + + +@c The key idea is that we leave it to the specific proof assistant to +@c worry about managing multiple files, as far as possible. Whenever the +@c proof assistant processes or retracts a file it must clearly say so, so +@c that Proof General can register this. + +As well as this communication from the assistant to Proof General about +processed or retracted files, Proof General can communicate the other +way: it will tell the proof assistant when it has processed or retracted +a file via script management. This is because during script management, +the proof assistant may not be aware that it is actually dealing with a +file of proof commands (rather than just terminal input). + +Proof General will provide this information in two special instances. +First, when scripting is turned off in a file that has been completely +processed, Proof General will tell the proof assistant using +@code{proof-shell-inform-file-processed-cmd}. Second, when scripting is +turned on in a file which is completely processed, Proof General will +tell the proof assistant to reconsider: the file should not be +considered completely processed yet. This uses the setting +@code{proof-shell-inform-file-retracted-cmd}. This second case might +lead to a series of messages from the prover telling Proof General to +unlock files which depend on the present one, again via +@code{proof-shell-retract-files-regexp}. + +What we have described so far is the ideal case, but it may require some +support from the proof assistant to set up (for example, if file-level +undo is not normally supported, or the messages during file processing +are not suitable). Moreover, some proof assistants may not have file +handling with dependencies, or may have a particularly simple case of a +linear context: each file depends on all the ones processed before it. +Proof General allows you a shortcut to get automatic management of +multiple files in these cases by setting the flag +@code{proof-auto-multiple-files}. This setting is probably an +approximation to the right thing for any proof assistant. More files +than necessary will be retracted if the prover has a tree-like file +dependency rather than a linear one. + +@vindex proof-shell-eager-annotation-start +@vindex proof-shell-eager-annotation-end +Finally, we should mention how Proof General recognizes file processing +messages from the proof assistant. Proof General considers @var{output} +delimited by the the two regular expressions +@code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end} as being important. It displays +the @var{output} in the Response buffer and analyses the contents +further. Among other important messages characterised by these regular +expressions (warnings, errors, or information), the prover can tell the +interface whenever it processes or retracts a file. + + +To summarize, the settings for multiple file management that may be +customized are as follows. To recognize file-processing, +@code{proof-shell-process-file}. To recognize messages about file +undoing, @code{proof-shell-retract-files-regexp} and +@code{proof-shell-compute-new-files-list}. @xref{Settings for matching +urgent messages from proof process}. To tell the prover about files +handled with script management, use + @code{proof-shell-inform-file-processed-cmd} and + @code{proof-shell-inform-file-retracted-cmd}. @xref{Proof shell + commands}. Finally, set the flag @code{proof-auto-multiple-files} +for a automatic approximation to multiple file handling. +@xref{Proof script settings}. + + +@node Configuring Font Lock +@chapter Configuring Font Lock +@cindex font lock + +Support for Font Lock in Proof General is described in the user manual +(see the @i{Syntax highlighting} section). To configure Font Lock for a +new proof assistant, you need to set the variable +@code{font-lock-keywords} in each of the mode functions you want +highlighting for. Proof General will automatically install these +settings, and use font lock minor mode (for syntax highlighting as you +type) in script buffers. + +@c nope: too big. TEXI DOCSTRING MAGIC: font-lock-keywords +To understand its format, check the documentation of +@code{font-lock-keywords} inside Emacs. + +Proof General provides a special function, @code{proof-zap-commas}, for +tweaking the font lock behaviour of provers which have declarations of +the form @code{x,y,z:Ty}. This function removes highlighting on the +commas, and can be added as the last element of +@code{font-lock-keywords}. Further manipulation of font lock behaviour +can be achieved via two hook functions which are run before and after +fontifying the output buffers. + +@c TEXI DOCSTRING MAGIC: proof-zap-commas +@defun proof-zap-commas limit +Remove the face of all @samp{,} from point to @var{limit}.@* +Meant to be used from @samp{@code{font-lock-keywords}}. +@end defun + +@c TEXI DOCSTRING MAGIC: pg-before-fontify-output-hook +@defvar pg-before-fontify-output-hook +This hook is called before fontifying a region in an output buffer.@* +A function on this hook can alter the region of the buffer within +the current restriction, and must return the final value of (@code{point-max}). +[This hook is presently only used by @code{phox-sym-lock}]. +@end defvar + +@c TEXI DOCSTRING MAGIC: pg-after-fontify-output-hook +@defvar pg-after-fontify-output-hook +This hook is called before fonfitying a region in an output buffer.@* +[This hook is presently only used by Isabelle]. +@end defvar +@node Configuring X-Symbol +@chapter Configuring X-Symbol +@cindex X-Symbol + +The X-Symbol package is described in the Proof General user manual. To +configure X-Symbol for Proof General, you must understand a little bit +of how X-Symbol works: read the documentation that is supplied with it. + +The basic task is to set up a @i{token language} for your proof +assistant. If your assistant is stored in the subdirectory +@var{myprover}, the token language will be called @var{myprover} and be +defined in a file @file{x-symbol-@var{myprover}.el} which is +automatically loaded by X-Symbol. The name of the token language mode +will be @code{@var{myprover}sym}. + +Proof General will check that the file @file{x-symbol-@var{myprover}.el} +exists and set up X-Symbol to load it. The token language file must +define a number of standard settings, and X-Symbol will give warnings if +any of them are missing. + +Apart from the token language file, there are several settings for +X-Symbol which you can set in the usual configuration file +@file{@var{myprover}.el}. These settings are optional. + +@c There's also proof-xsym-font-lock-keywords, but I don't +@c really know what this setting is good for. + +@c TEXI DOCSTRING MAGIC: proof-xsym-activate-command +@defvar proof-xsym-activate-command +Command to activate token input/output for X-Symbol.@* +If non-nil, this command is sent to the proof assistant when +X-Symbol support is activated. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-xsym-deactivate-command +@defvar proof-xsym-deactivate-command +Command to deactivate token input/output for X-Symbol.@* +If non-nil, this command is sent to the proof assistant when +X-Symbol support is deactivated. +@end defvar + +We expect tokens to be used uniformly, so that along with each script +mode buffer, the response buffer and goals buffer also invoke X-Symbol +to display special characters in the same token language. This happens +automatically. If you want additional modes to use X-Symbol with the +token language for your proof assistant, you can set +@code{proof-xsym-extra-modes}. + +@c TEXI DOCSTRING MAGIC: proof-xsym-extra-modes +@defvar proof-xsym-extra-modes +List of additional mode names to use X-Symbol with Proof General tokens.@* +These modes will have X-Symbol enabled for the proof assistant token language, +in addition to the four modes for Proof General (script, shell, response, pbp). + +Set this variable if you want additional modes to also display +tokens (for example, editing documentation or source code files). +@end defvar + + + +@node Writing more lisp code +@chapter Writing more lisp code + +You may want to add some extra features to your instance of Proof +General which are not supported in the generic core. To do this, you +can use the settings described above, plus a small number of fundamental +functions in Proof General which you can consider as exported in the +generic interface. Be careful using more functions than are mentioned +here because the internals of Proof General may change between versions. + +@menu +* Default values for generic settings:: +* Adding prover-specific configurations:: +* Useful variables:: +* Useful functions and macros:: +@end menu + +@node Default values for generic settings +@section Default values for generic settings + +Several generic settings are defined using @code{defpgcustom} in +@file{proof-config.el}. This introduces settings of the form +@code{<PA>-name} for each proof assistant @var{PA}. + +To set the default value for these settings in prover-specific cases, +you should use the special @code{defpgdefault} macro: + +@c TEXI DOCSTRING MAGIC: defpgdefault +@deffn Macro defpgdefault +Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@* +This should be used in prover-specific code to alter the default values +for prover specific settings. + +Usage: (defpgdefault SYM @var{value}) +@end deffn + +In your prover-specific code you can simply use the setting +@code{<PA>-sym} directly, i.e., write @code{myprover-home-page}. + +In the generic code, you can use a macro, writing @code{(proof-ass +home-page)} to refer to the @code{<PA>-home-page} setting for the +currently running instance of Proof General. + +@xref{Configuration variable mechanisms}, for more details on this +mechanism. + + +@node Adding prover-specific configurations +@section Adding prover-specific configurations + +Apart from the generic settings, your prover instance will probably need +some specific customizable settings. + +Defining new prover-specific settings using customize is pretty easy. +You should do it at least for your prover-specific user options. + +The code in @file{proof-site.el} provides each prover with two +customization groups automatically (based on the name of the assistant): +@code{<PA>} for user options for prover @var{PA} +and +@code{<PA>-config} for configuration of prover @var{PA}. +Typically @code{<PA>-config} holds settings which are +constants but which may be nice to tweak. + +The first group appears in the menu +@lisp + ProofGeneral -> Customize -> <PA> +@end lisp +The second group appears in the menu: +@lisp + ProofGeneral -> Internals -> <PA> config +@end lisp + +A typical use of @code{defcustom} looks like this: +@lisp +(defcustom myprover-search-page + "http://findtheorem.myprover.org" + "URL of search web page for myprover." + :type 'string + :group 'myprover-config) +@end lisp +This introduces a new customizable setting, which you might use to make +a menu entry, for example. The default value is the string +@code{"http://findtheorem.myprover.org"}. + + + + + + +@node Useful variables +@section Useful variables + +In @file{proof-compat}, two architecture flags are defined. These can +be used to write conditional pieces of code for different Emacs and +operating systems. + + +@c TEXI DOCSTRING MAGIC: proof-running-on-XEmacs + +@defvar proof-running-on-XEmacs +Non-nil if Proof General is running on XEmacs. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-running-on-win32 + + + + +@defvar proof-running-on-win32 +Non-nil if Proof General is running on a win32 system. +@end defvar +@node Useful functions and macros +@section Useful functions and macros + +The recommended functions you may invoke are these: + +@itemize @bullet +@item Any of the interactive commands (i.e. anything you + can invoke with @kbd{M-x}, including all key-bindings) +@item Any of the internal functions and macros mentioned below +@end itemize + +To insert text into the current (usually script) buffer, the function +@code{proof-insert} is useful. There's also a handy macro +@code{proof-defshortcut} for defining shortcut functions using it. + + +@c TEXI DOCSTRING MAGIC: proof-insert +@defun proof-insert text +Insert @var{text} into the current buffer.@* +@var{text} may include these special characters: +@lisp + %p - place the point here after input +@end lisp +Any other %-prefixed character inserts itself. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-defshortcut +@deffn Macro proof-defshortcut +Define shortcut function FN to insert @var{string}, optional keydef KEY.@* +This is intended for defining proof assistant specific functions. +@var{string} is inserted using @samp{@code{proof-insert}}, which see. +KEY is added onto @code{proof-assistant} map. +@end deffn +The function @code{proof-shell-invisible-command} is a useful utility +for sending a single command to the process. You should use this to +implement user-level or internal functions rather than attempting to +directly manipulate the proof action list, or insert into the shell +buffer. + +@c TEXI DOCSTRING MAGIC: proof-shell-invisible-command +@defun proof-shell-invisible-command cmd &optional wait +Send @var{cmd} to the proof process. @* +Automatically add @code{proof-terminal-char} if necessary, examining +proof-shell-no-auto-terminate-commands. +By default, let the command be processed asynchronously. +But if optional @var{wait} command is non-nil, wait for processing to finish +before and after sending the command. +If @var{wait} is an integer, wait for that many seconds afterwards. +@end defun + +There are several handy macros to help you define functions +which invoke @code{proof-shell-invisible-command}. + +@c TEXI DOCSTRING MAGIC: proof-definvisible +@deffn Macro proof-definvisible +Define function FN to send @var{string} to proof assistant, optional keydef KEY.@* +This is intended for defining proof assistant specific functions. +@var{string} is sent using @code{proof-shell-invisible-command}, which see. +KEY is added onto @code{proof-assistant} map. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-define-assistant-command +@deffn Macro proof-define-assistant-command +Define command FN to send string @var{body} to proof assistant, based on @var{cmdvar}.@* +@var{body} defaults to @var{cmdvar}, a variable. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-define-assistant-command-witharg +@deffn Macro proof-define-assistant-command-witharg +Define command FN to prompt for string @var{cmdvar} to proof assistant.@* +@var{cmdvar} is a function or string. Automatically has history. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-format-filename + + + + + + +@defun proof-format-filename string filename +Format @var{string} by replacing quoted chars by escaped version of @var{filename}. + +%e uses the canonicalized expanded version of filename (including +directory, using @code{default-directory} -- see @samp{@code{expand-file-name}}). + +%r uses the unadjusted (possibly relative) version of @var{filename}. + +%m ('module') uses the basename of the file, without directory +or extension. + +%s means the same as %e. + +Using %e can avoid problems with dumb proof assistants who don't +understand ~, for example. + +For all these cases, the escapes in @samp{@code{proof-shell-filename-escapes}} +are processed. + +If @var{string} is in fact a function, instead invoke it on @var{filename} and +return the resulting (string) value. +@end defun +@node Internals of Proof General +@chapter Internals of Proof General + +This chapter sketches some of the internal functions and variables of +Proof General, to help developers who wish to understand or modify the +code. + +Most of the documentation below is generated automatically from the +comments in the code. Because Emacs lisp is interpreted and +self-documenting, the best way to find your way around the source is +inside Emacs once Proof General is loaded. Read the source files, and +use functions such as @kbd{C-h v} and @kbd{C-h f}. + +The code is split into files. The following sections document the +important files, kept in the @file{generic/} subdirectory. + +@menu +* Spans:: +* Configuration variable mechanisms:: +* Proof General site configuration:: +* Global variables:: +* Proof script mode:: +* Proof shell mode:: +* Debugging:: +@end menu + + + +@node Spans +@section Spans +@cindex spans +@cindex extents +@cindex overlays + +@dfn{Spans} are an abstraction of XEmacs @dfn{extents} used to help +bridge the gulf between GNU Emacs and XEmacs. In GNU Emacs, spans are +implemented using @dfn{overlays}. + +See the files @file{span-extent.el} and @file{span-overlay.el} for the +implementation of the common interface in each case. + +@node Proof General site configuration +@section Proof General site configuration +@cindex installation directories +@cindex site configuration + +The file @file{proof-site.el} contains the initial configuration for +Proof General for the site (or user) and the choice of provers. + +The first part of the configuration is to set +@code{proof-home-directory} to the directory that @file{proof-site.el} +is located in, or to the variable of the environment variable +@code{PROOFGENERAL_HOME} if that is set. + +@c TEXI DOCSTRING MAGIC: proof-home-directory +@defvar proof-home-directory +Directory where Proof General is installed. Ends with slash.@* +Default value taken from environment variable @samp{PROOFGENERAL_HOME} if set, +otherwise based on where the file @samp{proof-site.el} was loaded from. +You can use customize to set this variable. +@end defvar + +@c They're no longer options. +@c The default value for @code{proof-home-directory} mentioned above is the +@c one for the author's system, it won't be the same for you! + +Further directory variables allow the files of Proof General to be split +up and installed across a system if need be, rather than under the +@code{proof-home-directory} root. + +@c TEXI DOCSTRING MAGIC: proof-images-directory +@defvar proof-images-directory +Where Proof General image files are installed. Ends with slash. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-info-directory +@defvar proof-info-directory +Where Proof General Info files are installed. Ends with slash. +@end defvar + + + +@cindex mode stub +After defining these settings, we define a @dfn{mode stub} for each +proof assistant enabled. The mode stub will autoload Proof General for +the right proof assistant when a file is visited with the corresponding +extension. The proof assistants enabled are the ones listed +in the @code{proof-assistants} setting. + +@c TEXI DOCSTRING MAGIC: proof-assistants +@defopt proof-assistants +Choice of proof assistants to use with Proof General.@* +A list of symbols chosen from: @code{'demoisa} @code{'isa} @code{'isar} @code{'lego} @code{'coq} @code{'phox} @code{'hol98} @code{'acl2} @code{'twelf} @code{'plastic} @code{'lclam}. +If nil, the default will be ALL proof assistants. + +Each proof assistant defines its own instance of Proof General, +providing session control, script management, etc. Proof General +will be started automatically for the assistants chosen here. +To avoid accidently invoking a proof assistant you don't have, +only select the proof assistants you (or your site) may need. + +You can select which proof assistants you want by setting this +variable before @samp{proof-site.el} is loaded, or by setting +the environment variable @samp{PROOFGENERAL_ASSISTANTS} to the +symbols you want, for example "lego isa". Or you can +edit the file @samp{proof-site.el} itself. + +Note: to change proof assistant, you must start a new Emacs session. + +The default value is @code{nil}. +@end defopt + +The file @file{proof-site.el} also defines a version variable. + +@c TEXI DOCSTRING MAGIC: proof-general-version +@defvar proof-general-version +Version string identifying Proof General release. +@end defvar + + + +@node Configuration variable mechanisms +@section Configuration variable mechanisms +@cindex conventions +@cindex user options +@cindex configuration +@cindex settings + +The file @file{proof-config.el} defines the configuration variables for +Proof General, including instantiation parameters and user options. See +previous chapters for details of its contents. Here we mention some +conventions for declaring user options. + +Global user options and instantiation parameters are declared using +@code{defcustom} as usual. User options should have `@code{*}' as the +first character of their docstrings (standard Emacs convention) and live +in the customize group @code{proof-user-options}. See +@file{proof-config.el} for the groups for instantiation parameters. + +User options which are generic (having separate instances for each +prover) and instantiation parameters (by definition generic) can be +declared using the special macro @code{defpgcustom}. It is used in the +same way as @code{defcustom}, except that the symbol declared will +automatically be prefixed by the current proof assistant symbol. + +@c TEXI DOCSTRING MAGIC: defpgcustom +@deffn Macro defpgcustom +Define a new customization variable <PA>@var{-sym} for the current proof assistant.@* +The function proof-assistant-<SYM> is also defined, which can be used in the +generic portion of Proof General to set and retrieve the value for the current p.a. +Arguments as for @samp{defcustom}, which see. + +Usage: (defpgcustom SYM &rest @var{args}). +@end deffn + +In specific instances of Proof General, the macro @code{defpgdefault} +can be used to give a default value for a generic setting. + +@c TEXI DOCSTRING MAGIC: defpgdefault +@deffn Macro defpgdefault +Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@* +This should be used in prover-specific code to alter the default values +for prover specific settings. + +Usage: (defpgdefault SYM @var{value}) +@end deffn + +All new instantiation variables are best declared using the +@code{defpgcustom} mechanism (old code may be converted gradually). +Customizations which are liable to be different for different instances +of Proof General are also best declared in this way. An example is the +use of X Symbol, controlled by @code{@emph{PA}-x-symbol-enable}, since +it works poorly or not at all with some provers. + +To access the generic settings, the following four functions and +macros are useful. + +@c TEXI DOCSTRING MAGIC: proof-ass +@deffn Macro proof-ass +Return the value for SYM for the current prover. +@end deffn +@c TEXI DOCSTRING MAGIC: proof-ass-sym +@deffn Macro proof-ass-sym +Return the symbol for SYM for the current prover. SYM not evaluated. +@end deffn +@c TEXI DOCSTRING MAGIC: proof-ass-symv +@defun proof-ass-symv sym +Return the symbol for @var{sym} for the current prover. @var{sym} is evaluated. +@end defun + +If changing a user option setting amounts to more than just setting a +variable (it may have some dynamic effect), we can set the +@code{custom-set} property for the variable to the function +@code{proof-set-value} which does an ordinary @code{set-default} to set +the variable, and then calls a function with the same name as the +variable, to do whatever is necessary according to the new value for the +variable. + +There are several settings which can be switched on or off by the user, +which use this @code{proof-set-value} mechanism. They are controlled by +boolean variables with names like @code{proof-@var{foo}-enable}, and +appear at the start of the customize group @code{proof-user-options}. +They should be edited by the user through the customization mechanism, +and set in the code using @code{customize-set-variable}. + +In @code{proof-utils.el} there is a handy macro, +@code{proof-deftoggle}, which constructs an interactive function +for toggling boolean customize settings. We can use this to make an +interactive function @code{proof-@var{foo}-toggle} to put on a menu or +bind to a key, for example. + +This general scheme is followed as far as possible, to give uniform +behaviour and appearance for boolean user options, as well as +interfacing properly with the @code{customize} mechanism. + +@c TEXI DOCSTRING MAGIC: proof-set-value +@defun proof-set-value sym value +Set a customize variable using @code{set-default} and a function.@* +We first call @samp{@code{set-default}} to set @var{sym} to @var{value}. +Then if there is a function @var{sym} (i.e. with the same name as the +variable @var{sym}), it is called to take some dynamic action for the new +setting. + +If there is no function @var{sym}, we try stripping +@code{proof-assistant-symbol} and adding "proof-" instead to get +a function name. This extends @code{proof-set-value} to work with +generic individual settings. + +The dynamic action call only happens when values @strong{change}: as an +approximation we test whether proof-config is fully-loaded yet. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-deftoggle +@deffn Macro proof-deftoggle +Define a function VAR-toggle for toggling a boolean customize setting VAR.@* +The toggle function uses @code{customize-set-variable} to change the variable. +@var{othername} gives an alternative name than the default <VAR>-toggle. +The name of the defined function is returned. +@end deffn +@node Global variables +@section Global variables + +Global variables are defined in @file{proof.el}. The same file defines +a few utility functions and some triggers to load in the other files. + +@c TEXI DOCSTRING MAGIC: proof-script-buffer +@defvar proof-script-buffer +The currently active scripting buffer or nil if none. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-buffer +@defvar proof-shell-buffer +Process buffer where the proof assistant is run. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-response-buffer +@defvar proof-response-buffer +The response buffer. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-goals-buffer +@defvar proof-goals-buffer +The goals buffer. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-buffer-type +@defvar proof-buffer-type +Symbol for the type of this buffer: @code{'script}, @code{'shell}, @code{'goals}, or @code{'response}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-included-files-list +@defvar proof-included-files-list +List of files currently included in proof process.@* +This list contains files in canonical truename format +(see @samp{@code{file-truename}}). + +Whenever a new file is being processed, it gets added to this list +via the @code{proof-shell-process-file} configuration settings. +When the prover retracts a file, this list is resynchronised via the +@code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list} +configuration settings. + +Only files which have been @strong{fully} processed should be included here. +Proof General itself will automatically add the filenames of a script +buffer which has been completely read when scripting is deactivated. +It will automatically remove the filename of a script buffer which +is completely unread when scripting is deactivated. + +NB: Currently there is no generic provision for removing files which +are only partly read-in due to an error, so ideally the proof assistant +should only output a processed message when a file has been successfully +read. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed +@defvar proof-shell-proof-completed +Flag indicating that a completed proof has just been observed.@* +If non-nil, the value counts the commands from the last command +of the proof (starting from 1). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-error-or-interrupt-seen +@defvar proof-shell-error-or-interrupt-seen +Flag indicating that an error or interrupt has just occurred.@* +Set to @code{'error} or @code{'interrupt} if one was observed from the proof +assistant during the last group of commands. +@end defvar + + +@node Proof script mode +@section Proof script mode + +The file @file{proof-script.el} contains the main code for proof script +mode, as well as definitions of menus, key-bindings, and user-level +functions. + +Proof scripts have two important variables for the locked and queue +regions. These variables are local to each script buffer (although we +only really need one queue span in total rather than one per buffer). + +@c TEXI DOCSTRING MAGIC: proof-locked-span +@defvar proof-locked-span +The locked span of the buffer.@* +Each script buffer has its own locked span, which may be detached +from the buffer. +Proof General allows buffers in other modes also to be locked; +these also have a non-nil value for this variable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-queue-span +@defvar proof-queue-span +The queue span of the buffer. May be detached if inactive or empty.@* +Each script buffer has its own queue span, although only the active +scripting buffer may have an active queue span. +@end defvar + +Various utility functions manipulate and examine the spans. An +important one is @code{proof-init-segmentation}. + +@c TEXI DOCSTRING MAGIC: proof-init-segmentation +@defun proof-init-segmentation +Initialise the queue and locked spans in a proof script buffer.@* +Allocate spans if need be. The spans are detached from the +buffer, so the regions are made empty by this function. +Also clear list of script portions. +@end defun + +For locking files loaded by a proof assistant, we use the next function. + +@c TEXI DOCSTRING MAGIC: proof-complete-buffer-atomic +@defun proof-complete-buffer-atomic buffer +Make sure @var{buffer} is marked as completely processed, completing with a single step. + +If buffer already contains a locked region, only the remainder of the +buffer is closed off atomically. + +This works for buffers which are not in proof scripting mode too, +to allow other files loaded by proof assistants to be marked read-only. +@end defun + +Atomic locking is instigated by the next function, which uses the +variables @code{proof-included-files-list} documented earlier +(@pxref{Handling multiple files} and @pxref{Global variables}). + +@c TEXI DOCSTRING MAGIC: proof-register-possibly-new-processed-file +@defun proof-register-possibly-new-processed-file file &optional informprover noquestions +Register a possibly new @var{file} as having been processed by the prover. + +If @var{informprover} is non-nil, the proof assistant will be told about this, +to co-ordinate with its internal file-management. (Otherwise we assume +that it is a message from the proof assistant which triggers this call). +In this case, the user will be queried to save some buffers, unless +@var{noquestions} is non-nil. + +No action is taken if the file is already registered. + +A warning message is issued if the register request came from the +proof assistant and Emacs has a modified buffer visiting the file. +@end defun + +An important pair of functions activate and deactivate scripting for the +current buffer. A change in the state of active scripting can trigger +various actions, such as starting up the proof assistant, or altering +@code{proof-included-files-list}. + +@c TEXI DOCSTRING MAGIC: proof-activate-scripting +@deffn Command proof-activate-scripting &optional nosaves queuemode +Ready prover and activate scripting for the current script buffer. + +The current buffer is prepared for scripting. No changes are +necessary if it is already in Scripting minor mode. Otherwise, it +will become the new active scripting buffer, provided scripting +can be switched off in the previous active scripting buffer +with @samp{@code{proof-deactivate-scripting}}. + +Activating a new script buffer may be a good time to ask if the +user wants to save some buffers; this is done if the user +option @samp{@code{proof-query-file-save-when-activating-scripting}} is set +and provided the optional argument @var{nosaves} is non-nil. + +The optional argument @var{queuemode} relaxes the test for a +busy proof shell to allow one which has mode @var{queuemode}. +In all other cases, a proof shell busy error is given. + +Finally, the hooks @samp{@code{proof-activate-scripting-hook}} are run. +This can be a useful place to configure the proof assistant for +scripting in a particular file, for example, loading the +correct theory, or whatever. If the hooks issue commands +to the proof assistant (via @samp{@code{proof-shell-invisible-command}}) +which result in an error, the activation is considered to +have failed and an error is given. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-deactivate-scripting +@deffn Command proof-deactivate-scripting &optional forcedaction +Deactivate scripting for the active scripting buffer. + +Set @code{proof-script-buffer} to nil and turn off the modeline indicator. +No action if there is no active scripting buffer. + +We make sure that the active scripting buffer either has no locked +region or a full locked region (everything in it has been processed). +If this is not already the case, we question the user whether to +retract or assert, or automatically take the action indicated in the +user option @samp{@code{proof-auto-action-when-deactivating-scripting}.} + +If the scripting buffer is (or has become) fully processed, and it is +associated with a file, it is registered on +@samp{@code{proof-included-files-list}}. Conversely, if it is (or has become) +empty, we make sure that it is @strong{not} registered. This is to be +certain that the included files list behaves as we might expect with +respect to the active scripting buffer, in an attempt to harmonize +mixed scripting and file reading in the prover. + +This function either succeeds, fails because the user refused to +process or retract a partly finished buffer, or gives an error message +because retraction or processing failed. If this function succeeds, +then @code{proof-script-buffer} is nil afterwards. + +The optional argument @var{forcedaction} overrides the user option +@samp{@code{proof-auto-action-when-deactivating-scripting}} and prevents +questioning the user. It is used to make a value for +the @code{kill-buffer-hook} for scripting buffers, so that when +a scripting buffer is killed it is always retracted. +@end deffn + +The function @code{proof-segment-up-to} is the main one used for parsing +the proof script buffer. There are several variants of this function +available corresponding to different parsing strategies; the appropriate +one is aliased to @code{proof-segment-up-to} according to which +configuration variables have been set. If only +@code{proof-script-command-end-regexp} or @code{proof-terminal-char} are set, +then the default is @code{proof-segment-up-to-cmdend}. If +@code{proof-script-command-start-regexp} is set, the choice is +@code{proof-segment-up-to-cmdstart}. + +@c TEXI DOCSTRING MAGIC: proof-segment-up-to-cmdend +@defun proof-segment-up-to-cmdend pos &optional next-command-end +Parse the script buffer from end of locked to @var{pos}.@* +Return a list of (type, string, int) tuples. + +Each tuple denotes the command and the position of its terminator, +type is one of @code{'comment}, or @code{'cmd}. @code{'unclosed-comment} may be consed onto +the start if the segment finishes with an unclosed comment. + +If optional @var{next-command-end} is non-nil, we include the command +which continues past @var{pos}, if any. + +This version is used when @samp{@code{proof-script-command-end-regexp}} is set. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-segment-up-to-cmdstart +@defun proof-segment-up-to-cmdstart pos &optional next-command-end +Parse the script buffer from end of locked to @var{pos}.@* +Return a list of (type, string, int) tuples. + +Each tuple denotes the command and the position of its terminator, +type is one of @code{'comment}, or @code{'cmd}. + +If optional @var{next-command-end} is non-nil, we include the command +which continues past @var{pos}, if any. (NOT @var{implemented} IN @var{this} @var{version}). + +This version is used when @samp{@code{proof-script-command-start-regexp}} is set. +@end defun + + +The function @code{proof-semis-to-vanillas} is used to convert +a parsed region of the script into a series of commands to +be sent to the proof assistant. + +@c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas +@defun proof-semis-to-vanillas semis &optional callback-fn +Convert a sequence of terminator positions to a set of vanilla extents.@* +Proof terminator positions @var{semis} has the form returned by +the function proof-segment-up-to. +Set the callback to @var{callback-fn} or @code{'proof-done-advancing} by default. +@end defun + +The function @code{proof-assert-until-point} is the main one used to +process commands in the script buffer. It's actually used to implement +the assert-until-point, electric terminator keypress, and +find-next-terminator behaviours. In different cases we want different +things, but usually the information (i.e. are we inside a comment) isn't +available until we've actually run @code{proof-segment-up-to (point)}, +hence all the different options when we've done so. + +@c TEXI DOCSTRING MAGIC: proof-assert-until-point +@defun proof-assert-until-point &optional unclosed-comment-fun ignore-proof-process-p +Process the region from the end of the locked-region until point.@* +Default action if inside a comment is just process as far as the start of +the comment. + +If you want something different, put it inside +@var{unclosed-comment-fun}. If @var{ignore-proof-process-p} is set, no commands +will be added to the queue and the buffer will not be activated for +scripting. +@end defun + +@code{proof-assert-next-command} is a variant of this function. + +@c TEXI DOCSTRING MAGIC: proof-assert-next-command +@deffn Command proof-assert-next-command &optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command +Process until the end of the next unprocessed command after point.@* +If inside a comment, just process until the start of the comment. + +If you want something different, put it inside @var{unclosed-comment-fun}. +If @var{ignore-proof-process-p} is set, no commands will be added to the queue. +Afterwards, move forward to near the next command afterwards, unless +@var{dont-move-forward} is non-nil. If @var{for-new-command} is non-nil, +a space or newline will be inserted automatically. +@end deffn + +The main command for retracting parts of a script is +@code{proof-retract-until-point}. + +@c TEXI DOCSTRING MAGIC: proof-retract-until-point +@defun proof-retract-until-point &optional delete-region +Set up the proof process for retracting until point.@* +In particular, set a flag for the filter process to call +@samp{@code{proof-done-retracting}} after the proof process has successfully +reset its state. +If @var{delete-region} is non-nil, delete the region in the proof script +corresponding to the proof command sequence. +If invoked outside a locked region, undo the last successfully processed +command. +@end defun + +To clean up when scripting is stopped, a script buffer is killed, or the +proof assistant exits, we use the functions +@code{proof-restart-buffers} and +@code{proof-script-remove-all-spans-and-deactivate}. + +@c TEXI DOCSTRING MAGIC: proof-restart-buffers +@defun proof-restart-buffers buffers +Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@* +No effect on a buffer which is nil or killed. If one of the buffers +is the current scripting buffer, then @code{proof-script-buffer} +will deactivated. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-script-remove-all-spans-and-deactivate +@defun proof-script-remove-all-spans-and-deactivate +Remove all spans from scripting buffers via @code{proof-restart-buffers}. +@end defun + + +@c +@c SECTION: Proof Shell Mode +@c +@node Proof shell mode +@section Proof shell mode +@cindex proof shell mode +@cindex comint-mode + +The proof shell mode code is in the file @file{proof-shell.el}. Proof +shell mode is defined to inherit from @code{comint-mode} using +@code{define-derived-mode} near the end of the file. The bulk of the +code in the file is concerned with sending code to and from the shell, +and processing output for the associated buffers (goals and response). + +Good process handling is a tricky issue. Proof General attempts to +manage the process strictly, by maintaining a queue of commands to send +to the process. Once a command has been processed, another one is +popped off the queue and sent. + +There are several important internal variables which control +interaction with the process. + +@c TEXI DOCSTRING MAGIC: proof-shell-busy +@defvar proof-shell-busy +A lock indicating that the proof shell is processing.@* +When this is non-nil, @code{proof-shell-ready-prover} will give +an error. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-marker +@defvar proof-marker +Marker in proof shell buffer pointing to previous command input. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-action-list +@defvar proof-action-list +A list of@* +@lisp + (@var{span} @var{command} @var{action}) +@end lisp +triples, which is a queue of things to do. +See the functions @samp{@code{proof-start-queue}} and @samp{proof-exec-loop}. +@end defvar + +@c TEXI DOCSTRING MAGIC: pg-subterm-anns-use-stack +@defvar pg-subterm-anns-use-stack +Choice of syntax tree encoding for terms. + +If nil, prover is expected to make no optimisations. +If non-nil, the pretty printer of the prover only reports local changes. +For @var{lego} 1.3.1 use @samp{nil}, for Coq 6.2, use @samp{t}. +@end defvar + + +The function @code{proof-shell-start} is used to initialise a shell +buffer and the associated buffers. + +@c TEXI DOCSTRING MAGIC: proof-shell-start +@deffn Command proof-shell-start +Initialise a shell-like buffer for a proof assistant. + +Also generates goal and response buffers. +Does nothing if proof assistant is already running. +@end deffn + +The function @code{proof-shell-kill-function} performs the converse +function of shutting things down; it is used as a hook function for +@code{kill-buffer-hook}. Then no harm occurs if the user kills the +shell directly, or if it is done more cautiously via +@code{proof-shell-exit}. The function @code{proof-shell-restart} allows +a less drastic way of restarting scripting, other than killing and +restarting the process. + +@c TEXI DOCSTRING MAGIC: proof-shell-kill-function +@defun proof-shell-kill-function +Function run when a proof-shell buffer is killed.@* +Attempt to shut down the proof process nicely and +clear up all the locked regions and state variables. +Value for @code{kill-buffer-hook} in shell buffer. +Also called by @code{proof-shell-bail-out} if the process is +exited by hand (or exits by itself). +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-exit +@deffn Command proof-shell-exit +Query the user and exit the proof process. + +This simply kills the @code{proof-shell-buffer} relying on the hook function +@code{proof-shell-kill-function} to do the hard work. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-shell-bail-out +@defun proof-shell-bail-out process event +Value for the process sentinel for the proof assistant process.@* +If the proof assistant dies, run @code{proof-shell-kill-function} to +cleanup and remove the associated buffers. The shell buffer is +left around so the user may discover what killed the process. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-restart +@deffn Command proof-shell-restart +Clear script buffers and send @code{proof-shell-restart-cmd}.@* +All locked regions are cleared and the active scripting buffer +deactivated. + +If the proof shell is busy, an interrupt is sent with +@code{proof-interrupt-process} and we wait until the process is ready. + +The restart command should re-synchronize Proof General with the proof +assistant, without actually exiting and restarting the proof assistant +process. + +It is up to the proof assistant how much context is cleared: for +example, theories already loaded may be "cached" in some way, +so that loading them the next time round only performs a re-linking +operation, not full re-processing. (One way of caching is via +object files, used by Lego and Coq). +@end deffn + +@c +@c INPUT +@c +@subsection Input to the shell + +Input to the proof shell via the queue region is managed by the +functions @code{proof-start-queue} and @code{proof-shell-exec-loop}. + +@c TEXI DOCSTRING MAGIC: proof-start-queue +@defun proof-start-queue start end alist +Begin processing a queue of commands in @var{alist}.@* +If @var{start} is non-nil, @var{start} and @var{end} are buffer positions in the +active scripting buffer for the queue region. + +This function calls @samp{@code{proof-append-alist}}. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-append-alist + +@defun proof-append-alist alist &optional queuemode +Chop off the vacuous prefix of the command queue @var{alist} and queue it.@* +For each @samp{@code{proof-no-command}} item at the head of the list, invoke its +callback and remove it from the list. + +Append the result onto @samp{@code{proof-action-list}}, and if the proof +shell isn't already busy, grab the lock with @var{queuemode} and +start processing the queue. + +If the proof shell is busy when this function is called, +then @var{queuemode} must match the mode of the queue currently +being processed. +@end defun +@vindex proof-action-list +@c TEXI DOCSTRING MAGIC: proof-shell-exec-loop +@defun proof-shell-exec-loop +Process the @code{proof-action-list}. + +@samp{@code{proof-action-list}} contains a list of (@var{span} @var{command} @var{action}) triples. + +If this function is called with a non-empty @code{proof-action-list}, the +head of the list is the previously executed command which succeeded. +We execute (@var{action} @var{span}) on the first item, then (@var{action} @var{span}) on any +following items which have @code{proof-no-command} as their cmd components. +If a there is a next command after that, send it to the process. If +the action list becomes empty, unlock the process and remove the queue +region. + +The return value is non-nil if the action list is now empty. +@end defun + +Input is actually inserted into the shell buffer and sent to the process +by the low-level function @code{proof-shell-insert}. + +@c TEXI DOCSTRING MAGIC: proof-shell-insert +@defun proof-shell-insert string action +Insert @var{string} at the end of the proof shell, call @code{comint-send-input}. + +First call @code{proof-shell-insert-hook}. The argument @var{action} may be +examined by the hook to determine how to process the @var{string} variable. + +Then strip @var{string} of carriage returns before inserting it and updating +@code{proof-marker} to point to the end of the newly inserted text. + +Do not use this function directly, or output will be lost. It is only +used in @code{proof-append-alist} when we start processing a queue, and in +@code{proof-shell-exec-loop}, to process the next item. +@end defun + + +When Proof General is processing a queue of commands, the lock +is managed using a couple of utility functions. You should +not need to use these directly. + + +@c TEXI DOCSTRING MAGIC: proof-grab-lock + +@defun proof-grab-lock &optional queuemode +Grab the proof shell lock, starting the proof assistant if need be.@* +Runs @code{proof-state-change-hook} to notify state change. +Clears the @code{proof-shell-error-or-interrupt-seen} flag. +If @var{queuemode} is supplied, set the lock to that value. +@end defun +@c TEXI DOCSTRING MAGIC: proof-release-lock + + + + + + + +@defun proof-release-lock &optional err-or-int +Release the proof shell lock, with error or interrupt flag @var{err-or-int}.@* +Clear @code{proof-shell-busy}, and set @code{proof-shell-error-or-interrupt-seen} +to err-or-int. +@end defun + + +@c +@c OUTPUT +@c +@subsection Output from the shell + +Two main functions deal with output, @code{proof-shell-process-output} +and @code{proof-shell-process-urgent-message}. In effect we consider +the output to be two streams intermingled: the "urgent" messages which +have "eager" annotations, as well as the ordinary ruminations from the +prover. + +The idea is to conceal as much irrelevant information from the user as +possible; only the remaining output between prompts and after the last +urgent message will be a candidate for the goal or response buffer. The +internal variable @code{proof-shell-urgent-message-marker} tracks the +last urgent message seen. + +When output is grabbed from the prover process, the first action +is to strip spurious carriage return characters from the end of +lines, if @code{proof-shell-strip-crs-from-output} requires it. +Then the output is stored into +@code{proof-shell-last-output}, and its type is stored in +@code{proof-shell-last-output-kind}. Output which is deferred or +possibly discarded until the queue is empty is copied into +@code{proof-shell-delayed-output}, with type +@code{proof-shell-delayed-output-kind}. A record of the last prompt +seen from the prover process is also kept, in +@code{proof-shell-last-prompt}. + + +@c TEXI DOCSTRING MAGIC: proof-shell-strip-crs-from-output + + +@defvar proof-shell-strip-crs-from-output +If non-nil, remove carriage returns (^M) at the end of lines from output.@* +This is enabled for cygwin32 systems by default. You should turn it off +if you don't need it (slight speed penalty). +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-last-prompt +@defvar proof-shell-last-prompt +A record of the last prompt seen from the proof system.@* +This is the string matched by @code{proof-shell-annotated-prompt-regexp}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-last-output +@defvar proof-shell-last-output +A record of the last string seen from the proof system. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-last-output-kind +@defvar proof-shell-last-output-kind +A symbol denoting the type of the last output string from the proof system.@* +Specifically: +@lisp + @code{'interrupt} An interrupt message + @code{'error} An error message + @code{'abort} A proof abort message + @code{'loopback} A command sent from the PA to be inserted into the script + @code{'response} A response message + @code{'goals} A goals (proof state) display + @code{'systemspecific} Something specific to a particular system, + -- see @samp{@code{proof-shell-process-output-system-specific}} +@end lisp +The output corresponding to this will be in @code{proof-shell-last-output}. + +See also @samp{@code{proof-shell-proof-completed}} for further information about +the proof process output, when ends of proofs are spotted. + +This variable can be used for instance specific functions which want +to examine @code{proof-shell-last-output}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output +@defvar proof-shell-delayed-output +A copy of @code{proof-shell-last-output} held back for processing at end of queue. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-kind +@defvar proof-shell-delayed-output-kind +A copy of proof-shell-last-output-lind held back for processing at end of queue. +@end defvar +@vindex proof-action-list + +@c TEXI DOCSTRING MAGIC: proof-shell-process-output +@defun proof-shell-process-output cmd string +Process shell output (resulting from @var{cmd}) by matching on @var{string}.@* +@var{cmd} is the first part of the @code{proof-action-list} that lead to this +output. The result of this function is a pair (@var{symbol} @var{newstring}). + +Here is where we recognizes interrupts, abortions of proofs, errors, +completions of proofs, and proof step hints (proof by pointing results). +They are checked for in this order, using +@lisp + @code{proof-shell-interrupt-regexp} + @code{proof-shell-error-regexp} + @code{proof-shell-abort-goal-regexp} + @code{proof-shell-proof-completed-regexp} + @code{proof-shell-result-start} +@end lisp +All other output from the proof engine will be reported to the user in +the response buffer by setting @code{proof-shell-delayed-output} to a cons +cell of ('insert . @var{text}) where @var{text} is the text string to be inserted. + +Order of testing is: interrupt, abort, error, completion. + +To extend this function, set @code{proof-shell-process-output-system-specific}. + +The "aborted" case is intended for killing off an open proof during +retraction. Typically it matches the message caused by a +@code{proof-kill-goal-command}. It simply inserts the word "Aborted" into +the response buffer. So it is expected to be the result of a +retraction, rather than the indication that one should be made. + +This function sets @samp{@code{proof-shell-last-output}} and @samp{@code{proof-shell-last-output-kind}}, +which see. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker +@defvar proof-shell-urgent-message-marker +Marker in proof shell buffer pointing to end of last urgent message. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message +@defun proof-shell-process-urgent-message message +Analyse urgent @var{message} for various cases.@* +Cases are: included file, retracted file, cleared response buffer, +variable setting or dependency list. +If none of these apply, display @var{message}. + +@var{message} should be a string annotated with +@code{proof-shell-eager-annotation-start}, @code{proof-shell-eager-annotation-end}. +@end defun + +The main processing point which triggers other actions is +@code{proof-shell-filter}. + +@c TEXI DOCSTRING MAGIC: proof-shell-filter +@defun proof-shell-filter str +Filter for the proof assistant shell-process.@* +A function for @code{comint-output-filter-functions}. + +Deal with output and issue new input from the queue. + +Handle urgent messages first. As many as possible are processed, +using the function @samp{@code{proof-shell-process-urgent-messages}}. + +Otherwise wait until an annotated prompt appears in the input. +If @code{proof-shell-wakeup-char} is set, wait until we see that in the +output chunk @var{str}. This optimizes the filter a little bit. + +If a prompt is seen, run @code{proof-shell-process-output} on the output +between the new prompt and the last input (position of @code{proof-marker}) +or the last urgent message (position of +@code{proof-shell-urgent-message-marker}), whichever is later. +For example, in this case: +@lisp + PROMPT> @var{input} + @var{output-1} + @var{urgent-message} + @var{output-2} + PROMPT> +@end lisp +@code{proof-marker} is set after @var{input} by @code{proof-shell-insert} and +@code{proof-shell-urgent-message-marker} is set after @var{urgent-message}. +Only @var{output-2} will be processed. For this reason, error +messages and interrupt messages should @strong{not} be considered +urgent messages. + +Output is processed using the function +@samp{@code{proof-shell-filter-process-output}}. + +The first time that a prompt is seen, @code{proof-marker} is +initialised to the end of the prompt. This should +correspond with initializing the process. The +ordinary output before the first prompt is ignored (urgent messages, +however, are always processed; hence their name). +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-filter-process-output +@defun proof-shell-filter-process-output string +Subroutine of @code{proof-shell-filter} to process output @var{string}. + +Appropriate action is taken depending on the what +@code{proof-shell-process-output} returns: maybe handle an interrupt, an +error, or deal with ordinary output which is a candidate for the goal +or response buffer. Ordinary output is only displayed when the proof +action list becomes empty, to avoid a confusing rapidly changing +output. + +After processing the current output, the last step undertaken +by the filter is to send the next command from the queue. +@end defun + + + + + + +@c +@c SECTION: Debugging +@c +@node Debugging +@section Debugging +@cindex debugging + +@c FIXME: better to have general hints on Elisp earlier, plus some +@c links to helpful docs. + +To debug Proof General, it may be helpful to set the +configuration variable @code{proof-show-debug-messages}. + +@c TEXI DOCSTRING MAGIC: proof-show-debug-messages +@defopt proof-show-debug-messages +Whether to display debugging messages in the response buffer.@* +If non-nil, debugging messages are displayed in the response giving +information about what Proof General is doing. +To avoid erasing the messages shortly after they're printed, +you should set @samp{@code{proof-tidy-response}} to nil. + +The default value is @code{nil}. +@end defopt + +For more information about debugging Emacs lisp, consult the Emacs Lisp +Reference Manual. I recommend using the source-level debugger +@code{edebug}. + + + + + + + + + + + + + + +@c +@c +@c APPENDIX: Plans and ideas +@c +@c +@node Plans and ideas +@appendix Plans and ideas + +This appendix contains some tentative plans and ideas for improving +Proof General. + +This appendix is no longer extended: instead we keep a list of Proof +General projects on the web, and forthcoming plans and ideas in the +@file{TODO} and @file{todo} files included in the ordinary and +developers PG distributions, respectively. Once the items mentioned +below are implemented, they will be removed from here. + +Please send us contributions to our wish lists, or better still, an +offer to implement something from them! + +@menu +* Proof by pointing and similar features:: +* Granularity of atomic command sequences:: +* Browser mode for script files and theories:: +@end menu + +@node Proof by pointing and similar features +@section Proof by pointing and similar features +@cindex proof by pointing + +This is a note by David Aspinall about proof by pointing and similar +features. + +Proof General already supports proof by pointing, and experimental +support is provided in LEGO. We would like to extend this support to +other proof assistants. Unfortunately, proof by pointing requires +rather heavy support from the proof assistant. There are two aspects to +the support: +@itemize @bullet +@item term structure mark-up +@item proof by pointing command generation +@end itemize +Term structure mark-up is useful in itself: it allows the user to +explore the structure of a term using the mouse (the smallest +subexpression that the mouse is over is highlighted), and easily copy +subterms from the output to a proof script. + +Command generation for proof by pointing is usually specific to a +particular logic in use, if we hope to generate a good proof command +unambiguously for any particular click. However, Proof General could +easily be generalised to offer the user a context-sensitive choice of +next commands to apply, which may be more useful in practice, and a +worthy addition to Proof General. + +Implementors of new proof assistants should be encouraged to consider +supporting term-structure mark up from the start. Command generation +should be something that the logic-implementor can specify in some way. + +Of the supported provers, we can certainly hope for proof-by-pointing +support from Coq, since the CtCoq proof-by-pointing code has been moved +into the Coq kernel lately. I hope the Coq community can encourage +somebody to do this. + + +@node Granularity of atomic command sequences +@section Granularity of atomic command sequences +@c @cindex Granularity of Atomic Sequences +@c @cindex Retraction +@c @cindex Goal +@cindex ACS (Atomic Command Sequence) + +This is a proposal by Thomas Kleymann for generalising the way Proof +General handles sequences of proof commands (see @i{Goal-save +sequences} in the user manual), particularly to make retraction more flexible. + +The blue region of a script buffer contains the initial segment of +the proof script which has been processed successfully. It consists of +atomic sequences of commands (ACS). Retraction is supported to the +beginning of every ACS. By default, every command is an ACS. But the +granularity of atomicity should be able to be adjusted. + +This is essential when arbitrary retraction is not supported. Usually, +after a theorem has been proved, one may only retract to the start of +the goal. One needs to mark the proof of the theorem as an ACS. At +present, support for goal-save sequences (see @i{Goal-save sequences} in +the user manual), has been hard wired. No other ACS are currently +supported. We propose the following to overcome this deficiency: + +@vtable @code +@item proof-atomic-sequents-list +is a list of instructions for setting up ACSs. Each instruction is a +list of the form @code{(@var{end} @var{start} &optional +@var{forget-command})}. @var{end} is a regular expression to recognise +the last command in an ACS. @var{start} is a function. Its input is the +last command of an ACS. Its output is a regular expression to recognise +the first command of the ACS. It is evaluated once and, starting with the +command matched by @var{end}, the output is +successively matched against previously processed commands until a match +occurs (or the beginning of the current buffer is reached). The region +determined by (@var{start},@var{end}) is locked as an ACS. Optionally, +the ACS is annotated with the actual command to retract the ACS. This is +computed by applying @var{forget-command} to the first and last command +of the ACS. + +For convenience one might also want to allow @var{start} to be the +symbol @samp{t} as a convenient short-hand for @code{'(lambda (str) +".")} which always matches. +@end vtable + +@node Browser mode for script files and theories +@section Browser mode for script files and theories + +This is a proposal by David Aspinall for a browser window. + +A browser window should provide support for browsing script files and +theories. We should be able to inspect data in varying levels of +detail, perhaps using outlining mechanisms. For theories, it would be +nice to query the running proof assistant. This may require support +from the assistant in the form of output which has been specially +marked-up with an SGML like syntax, for example. + +A browser would be useful to: +@itemize @bullet +@item Provide impoverished proof assistants with a browser +@item Extend the uniform interface of Proof General to theory browsing +@item Interact closely with proof script writing +@end itemize +The last point is the most important. We should be able to integrate a +search mechanism for proofs of similar theorems, theorems containing +particular constants, etc. + + + + +@c +@c +@c APPENDIX: Demonstration instantiation for Isabelle +@c +@c +@node Demonstration Instantiations +@appendix Demonstration Instantiations + +This appendix contains the code for the two demonstration +instantiations of Proof General, for Isabelle. + +These instantiations make an almost-bare minimum of settings to get +things working. To add embellishments, you should refer to +the instantiations for other systems distributed with +Proof General. + +@menu +* demoisa-easy.el:: +* demoisa.el:: +@end menu + +@node demoisa-easy.el +@section demoisa-easy.el + +@lisp +@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM +@c @includeverbatim ../demoisa/demoisa-easy.el +;; demoisa-easy.el Example Proof General instance for Isabelle +;; +;; Copyright (C) 1999 LFCS Edinburgh. +;; +;; Author: David Aspinall <David.Aspinall@@ed.ac.uk> +;; +;; $Id$ +;; +;; This is an alternative version of demoisa.el which uses the +;; proof-easy-config macro to do the work of declaring derived modes, +;; etc. +;; +;; See demoisa.el and the Proof General manual for more documentation. +;; +;; To test this file you must rename it demoisa.el. +;; + +(require 'proof-easy-config) ; easy configure mechanism + +(proof-easy-config + 'demoisa "Isabelle Demo" + proof-prog-name "isabelle" + proof-terminal-char ?\; + proof-script-comment-start "(*" + proof-script-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-non-undoables-regexp "undo\\|back" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-showproof-command "pr()" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-auto-multiple-files t + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-prompt-pattern "[ML-=#>]+>? " + proof-shell-interrupt-regexp "Interrupt" + proof-shell-start-goals-regexp "Level [0-9]" + proof-shell-end-goals-regexp "val it" + proof-shell-quit-cmd "quit();" + proof-assistant-home-page + "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" + proof-shell-annotated-prompt-regexp + "^\\(val it = () : unit\n\\)?ML>? " + proof-shell-error-regexp + "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-init-cmd + "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" + proof-shell-proof-completed-regexp "^No subgoals!" + proof-shell-eager-annotation-start + "^\\[opening \\|^###\\|^Reading") + +(provide 'demoisa) +@end lisp + +@node demoisa.el +@section demoisa.el + +@lisp +@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM +@c @includeverbatim ../demoisa/demoisa-easy.el +;; demoisa.el Example Proof General instance for Isabelle +;; +;; Copyright (C) 1999 LFCS Edinburgh. +;; +;; Author: David Aspinall <David.Aspinall@@ed.ac.uk> +;; +;; $Id$ +;; +;; ================================================================= +;; +;; See README in this directory for an introduction. +;; +;; Basic configuration is controlled by one line in `proof-site.el'. +;; It has this line in proof-assistant-table: +;; +;; (demoisa "Isabelle Demo" "\\.ML$") +;; +;; From this it loads this file "demoisa/demoisa.el" whenever +;; a .ML file is visited, and sets the mode to `demoisa-mode' +;; (defined below). +;; +;; I've called this instance "Isabelle Demo Proof General" just to +;; avoid confusion with the real "Isabelle Proof General" in case the +;; demo gets loaded by accident. +;; +;; To make the line above take precedence over the real Isabelle mode +;; later in the table, set PROOFGENERAL_ASSISTANTS=demoisa in the +;; shell before starting Emacs (or customize proof-assistants). +;; + + +(require 'proof) ; load generic parts + + +;; ======== User settings for Isabelle ======== +;; +;; Defining variables using customize is pretty easy. +;; You should do it at least for your prover-specific user options. +;; +;; proof-site provides us with two customization groups +;; automatically: (based on the name of the assistant) +;; +;; 'isabelledemo - User options for Isabelle Demo Proof General +;; 'isabelledemo-config - Configuration of Isabelle Proof General +;; (constants, but may be nice to tweak) +;; +;; The first group appears in the menu +;; ProofGeneral -> Customize -> Isabelledemo +;; The second group appears in the menu: +;; ProofGeneral -> Internals -> Isabelledemo config +;; + +(defcustom isabelledemo-prog-name "isabelle" + "*Name of program to run Isabelle." + :type 'file + :group 'isabelledemo) + +(defcustom isabelledemo-web-page + "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html" + "URL of web page for Isabelle." + :type 'string + :group 'isabelledemo-config) + + +;; +;; ======== Configuration of generic modes ======== +;; + +(defun demoisa-config () + "Configure Proof General scripting for Isabelle." + (setq + proof-terminal-char ?\; ; ends every command + proof-script-comment-start "(*" + proof-script-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-non-undoables-regexp "undo\\|back" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-showproof-command "pr()" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-assistant-home-page isabelledemo-web-page + proof-auto-multiple-files t)) + + +(defun demoisa-shell-config () + "Configure Proof General shell for Isabelle." + (setq + proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? " + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-prompt-pattern "[ML-=#>]+>? " + proof-shell-interrupt-regexp "Interrupt" + proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-start-goals-regexp "Level [0-9]" + proof-shell-end-goals-regexp "val it" + proof-shell-proof-completed-regexp "^No subgoals!" + proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" + proof-shell-init-cmd ; define a utility function, in a lib somewhere? + "fun pg_repeat f 0 = () + | pg_repeat f n = (f(); pg_repeat f (n-1));" + proof-shell-quit-cmd "quit();")) + + + +;; +;; ======== Defining the derived modes ======== +;; + +;; The name of the script mode is always <proofsym>-script, +;; but the others can be whatever you like. +;; +;; The derived modes set the variables, then call the +;; <mode>-config-done function to complete configuration. + +(define-derived-mode demoisa-mode proof-mode + "Isabelle Demo script" nil + (demoisa-config) + (proof-config-done)) + +(define-derived-mode demoisa-shell-mode proof-shell-mode + "Isabelle Demo shell" nil + (demoisa-shell-config) + (proof-shell-config-done)) + +(define-derived-mode demoisa-response-mode proof-response-mode + "Isabelle Demo response" nil + (proof-response-config-done)) + +(define-derived-mode demoisa-goals-mode proof-goals-mode + "Isabelle Demo goals" nil + (proof-goals-config-done)) + +;; The response buffer and goals buffer modes defined above are +;; trivial. In fact, we don't need to define them at all -- they +;; would simply default to "proof-response-mode" and "pg-goals-mode". + +;; A more sophisticated instantiation might set font-lock-keywords to +;; add highlighting, or some of the proof by pointing markup +;; configuration for the goals buffer. + +;; The final piece of magic here is a hook which configures settings +;; to get the proof shell running. Proof General needs to know the +;; name of the program to run, and the modes for the shell, response, +;; and goals buffers. + +(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start) + +(defun demoisa-pre-shell-start () + (setq proof-prog-name isabelledemo-prog-name) + (setq proof-mode-for-shell 'demoisa-shell-mode) + (setq proof-mode-for-response 'demoisa-response-mode) + (setq proof-mode-for-goals 'demoisa-goals-mode)) + +(provide 'demoisa) +@end lisp + + + + +@node Function Index +@unnumbered Function and Command Index +@printindex fn + +@node Variable Index +@unnumbered Variable and User Option Index +@printindex vr + +@c Nothing in this one! +@c @node Keystroke Index +@c @unnumbered Keystroke Index +@c @printindex ky + +@node Concept Index +@unnumbered Concept Index +@printindex cp + +@page +@contents +@bye + + |