diff options
| -rw-r--r-- | doc/Makefile | 9 | ||||
| -rw-r--r-- | doc/NewDoc.texi | 3768 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 3966 |
3 files changed, 3533 insertions, 4210 deletions
diff --git a/doc/Makefile b/doc/Makefile index fa3020fa..7401acfe 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -67,20 +67,21 @@ info: $(DOCNAME).info clean: rm -f $(DOCNAME).?? $(DOCNAME).fns $(DOCNAME).vrs $(DOCNAME).cps rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc $(DOCNAME).cp0 + rm -f $(DOCNAME).kys rm -f *~ ## ## distclean: Remove documentation targets ## distclean: clean - rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME).pdf $(DOCNAME)*.html + rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME)*.ps $(DOCNAME).pdf $(DOCNAME)*.html ## -## magic: update magic comments in NewDoc.texi from docstrings in code. +## texi: update magic comments in texi from docstrings in code. ## (developer use only!) ## -magic: - $(EMACS) -l docstring-magic.el NewDoc.texi -f texi-docstring-magic -f save-buffer +$(DOCNAME).texi: ../*/*.el + $(EMACS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi deleted file mode 100644 index 1a8ca3c4..00000000 --- a/doc/NewDoc.texi +++ /dev/null @@ -1,3768 +0,0 @@ -\input texinfo @c -*-texinfo-*- -@c -@c $Id$ -@c -@c %**start of header -@setfilename ProofGeneral.info -@settitle Proof General -@setchapternewpage odd -@paragraphindent 0 -@iftex -@afourpaper -@end iftex -@c %**end of header - -@c -@c TODO, priority order -@c . finish incomplete sections -@c . polish mark-up -@c . add more index entries -@c . screenshots might be nice (one day) -@c - -@c NOTE ON THIS TEXINFO FILE: -@c I've tried keep full node lines *out* of this file because Emacs makes a -@c mess of updating them. Instead, rely on makeinfo and friends to do -@c the equivalent job. For this to work, we must follow each node -@c immediately with a section command, i.e.: -@c -@c @node node-name -@c <section-command> -@c -@c And each section with lower levels must have a menu command in -@c it. Menu updating with Emacs is a bit better than node updating, -@c but tends to delete the first section of the file in XEmacs! -@c (it's better in FSF Emacs at the time of writing). -@c - - -@set version 2.0 -@set xemacsversion 20.4 -@set fsfversion 20.2 -@set last-update November 1998 -@set rcsid $Id$ - -@ifinfo -@format -START-INFO-DIR-ENTRY * ProofGeneral::Organize your proofs with Emacs! -END-INFO-DIR-ENTRY -@end format -@end ifinfo - -@c -@c MACROS -@c -@c define one here for a command with a keybinding? -@c -@c I like the idea, but it's maybe against the texinfo -@c style to fix together a command and its keybinding. - - -@c merge functions and variables into concept index. -@c @syncodeindex fn cp -@c @syncodeindex vr cp - -@c merge functions into variables index -@c @syncodeindex fn vr - -@finalout -@titlepage -@title Proof General -@subtitle Organise your proofs with Emacs! -@subtitle Proof General @value{version} -@subtitle @value{last-update} -@iftex -@image{ProofGeneral} -@end iftex -@author D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira -@page -@vskip 0pt plus 1filll -This manual and the program Proof General are -Copyright @copyright{} 1998 Proof General team, LFCS Edinburgh. - - -@c -@c COPYING NOTICE -@c -@ignore -Permission is granted to process this file through TeX and print the -results, provided the printed document carries copying permission notice -identical to this one except for the removal of this paragraph (this -paragraph not being relevant to the printed manual). -@end ignore - -@sp 2 -Permission is granted to make and distribute verbatim copies of this -manual provided the copyright notice and this permission notice are -preserved on all copies. -@sp 2 - -This manual documents Proof General, Version @value{version}, for use -with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion} -or later versions. - -Version control stamp: @code{@value{rcsid}} -@end titlepage - -@page - - -@ifinfo -@node Top -@top Proof General - -This file documents version @value{version} of @b{Proof General}, a -generic Emacs interface for proof assistants. - -Proof General @value{version} has been tested with XEmacs -@value{xemacsversion} and FSF GNU Emacs @value{fsfversion}. It is -supplied ready customized for the proof assistants Coq, Lego, and -Isabelle. - -@menu -* Introducing Proof General:: -* Basic Script Management:: -* Advanced Script Management:: -* Support for other Packages:: -* Customizing Proof General:: -* LEGO Proof General:: -* Coq Proof General:: -* Isabelle Proof General:: -* Adapting Proof General to New Provers:: -* Internals of Proof General:: -* Credits and References:: -* Obtaining and Installing Proof General:: -* Known bugs and workarounds:: -* Plans and ideas:: -* Function Index:: -* Variable Index:: -* Keystroke Index:: -* Index:: -@end menu - -@detailmenu --- The Detailed Node Listing --- - -Introducing Proof General - -* Quick start guide:: -* Features of Proof General:: -* Supported proof assistants:: -* Prerequisites for this manual:: - -Basic Script Management - -* Proof scripts:: -* Script buffers:: -* Summary of Proof General buffers:: -* Script editing commands:: -* Script processing commands:: -* Toolbar commands:: -* Proof assistant commands:: -* Walkthrough example in LEGO:: - -Script buffers - -* Locked queue and editing regions:: -* Goal-save sequences:: -* Active scripting buffer:: - -Advanced Script Management - -* Switching between proof scripts:: -* View of processed files :: -* Retracting across files:: -* Asserting across files:: -* Working directly with the proof shell:: - -Support for other Packages - -* Support for function menus:: -* Support for outline mode:: -* Support for tags:: - -Customizing Proof General - -* Easy customization:: -* Display customization:: -* User options:: -* Changing faces:: -* Tweaking configuration settings:: - -LEGO Proof General - -* LEGO specific commands:: -* LEGO tags:: -* LEGO customizations:: - -Coq Proof General - -* Coq specific commands:: -* Coq customizations:: - -Isabelle Proof General - -* Theory files:: -* Isabelle specific commands:: -* Isabelle customizations:: - -Adapting Proof General to New Provers - -* Overview of adding a new prover:: -* Major modes used by Proof General:: -* Menus and user-level commands:: -* Proof script settings:: -* Proof shell settings:: -* Goals buffer configuration:: -* Global constants:: -* Handling multiple files:: - -Internals of Proof General - -* Spans:: -* Global variables:: -* Proof script mode:: -* Proof shell mode:: - -Credits and References - -* Credits:: -* References:: - -Obtaining and Installing Proof General - -* Obtaining Proof General:: -* Installing Proof General from tarball:: -* Installing Proof General from RPM package:: -* Notes for syssies:: - -Known bugs and workarounds - -* Bugs at the generic level:: -* Bugs specific to LEGO Proof General:: -* Bugs specific to Coq Proof General:: -* Bugs specific to Isabelle Proof General:: - -Bugs specific to LEGO Proof General - -* Retraction and Discharge:: -* Retraction and proving:: - -Plans and ideas - -* Granularity of atomic command sequences:: -* Browser mode for script files and theories:: -@end detailmenu -@end ifinfo - - - -@c -@c CHAPTER: Introduction -@c -@node Introducing Proof General -@chapter Introducing Proof General -@cindex proof assistant -@cindex Proof General - -@c would like the logo on the title page really but -@c it doesn't seem to work there for html. -@ifhtml -<IMG SRC="ProofGeneral.jpg" ALT="[ Proof General logo ]" > -@end ifhtml - -A @dfn{proof assistant} is a computerized helper for developing -mathematical proofs. - -@dfn{Proof General} is a generic Emacs interface for proof assistants, -developed at the LFCS in the University of Edinburgh. It works best -under XEmacs, but can also be used with FSF GNU Emacs. - -You do not have to be an Emacs militant to use Proof General! @* - -The interface is designed to be very easy to use. You develop your -proof script in-place rather than line-by-line and later reassembling -the pieces. Proof General keeps track of which proof steps have been -processed by the prover, and prevents you editing them accidently. You -can undo steps as usual. - -Our aim is provide a powerful and configurable Emacs mode which helps -user-interaction with interactive proof assistants. Please help us with -this aim! Configure Proof General for your proof assistant, by adding -features at the generic level wherever possible. See -@ref{Adapting Proof General to New Provers} -for more details, and send ideas, comments, patches, -and code to @code{proofgen@@dcs.ed.ac.uk}. - -@menu -* Quick start guide:: -* Features of Proof General:: -* Supported proof assistants:: -* Prerequisites for this manual:: -@end menu - - - - -@node Quick start guide -@section Quick start guide - -Proof General may have been installed for you already. If so, when you -visit a proof script file for your proof assistant, you'll find commands -to process the proof script are available from the toolbar, menus, and -keyboard. Type @kbd{C-h m} to get a list of keys for the current mode. - -The proof assistant is automatically started inside Emacs when you ask -for some of the proof script to be processed. To follow an example use -of Proof General on a LEGO proof, see @pxref{Walkthrough example in LEGO}. - -If Proof General has not already been installed, you should insert the -line: -@lisp - (load "@var{proof-general-home}/generic/proof-site.el") -@end lisp -into your @file{~/.emacs} file, where @var{proof-general-home} is the -top-level directory that was created when Proof General was unpacked. - -For more details on obtaining and installing Proof General, -see @pxref{Obtaining and Installing Proof General}. - - -@node Features of Proof General -@section Features of Proof General -@cindex Features -@cindex Why use Proof General? - -Why would you want to use Proof General? - -Here is an outline of its main features. - -@itemize @bullet -@item @i{Simplified communication}@* -The proof assistant's shell is normally hidden from the user. -Communication takes place via two or three buffers. The @dfn{script -buffer} holds input, the commands to construct a proof. The @dfn{goals -buffer} displays the current list of subgoals to be solved. The -@dfn{response buffer} displays other output from the proof assistants. -This means that the user only sees the output from the most recent proof -step, rather than a screen full of output from the proof assistant. -@c Optionally, the goals buffer and script buffer can be identified. - -For more details, see @xref{Basic Script Management}, -@xref{Script buffers} and @xref{Summary of Proof General buffers}. - -@item @i{Script management}@* -Proof General colours proof script regions blue when they have already -been processed by the prover, and colours regions red when the prover is -currently processing them. The appearance of Emacs buffers always -matches the proof assistant's state. Coloured parts of the buffer cannot -be edited. Proof General has functions for @emph{asserting} or -@emph{retracting} parts of a proof script, which alters the coloured -regions. - -For more details, see @xref{Basic Script Management}, -@xref{Script processing commands}. -and @pxref{Advanced Script Management}. -@item @i{Script editing mode}@* -Proof General provides useful facilities for editing proof scripts, -including syntax hilighting and a menu to jump to particular goals, -definitions, or declarations. -Special editing functions send lines of proof script to the proof -assistant, or undo previous proof steps. - -For more details, see @pxref{Script editing commands} -and @pxref{Script processing commands}. -@item @i{Toolbar and menus}@* -A script buffer has a toolbar with navigation buttons for processing -parts of the proof script. A menu provides further functions for -operations in the proof assistant, as well as customization of Proof -General. - -For more details, see @pxref{Toolbar commands}, @pxref{Proof assistant -commands}, and @pxref{Customizing Proof General}. - -@c not yet -@c @item @i{Proof by pointing} -@end itemize - - -@node Supported proof assistants -@section Supported proof assistants - -Proof General comes ready-customised for these proof assistants: - -@itemize @bullet -@item -@b{LEGO Proof General} for LEGO Version 1.3.1@* -@c written by Thomas Kleymann and Dilip Sequeira. -@c -All features of Proof General are supported. -See @pxref{LEGO Proof General} for more details. - -@item -@b{Coq Proof General} for Coq Version 6.2@* -@c written by Healfdene Goguen. -@c -All of features of Proof General are supported except multiple files. -See @pxref{Coq Proof General} for more details. - -@item -@b{Isabelle Proof General} for Isabelle 98-1@* -@c written by David Aspinall. -All features of Proof General are supported, except for an external tags -program. Isabelle Proof General handles theory files as well as ML -(proof script files), and has an extensive theory file editing mode -taken from @uref{http://www.dcs.ed.ac.uk/home/da/Isamode,Isamode}. -See @pxref{Isabelle Proof General} for more details. -@end itemize -Proof General is designed to be generic, so you can adapt it to other -proof assistants if you know a little bit of Emacs Lisp. -@itemize @bullet -@item -@b{Your Proof General} for your favourite proof assistant@* -See @pxref{Adapting Proof General to New Provers} -for more details of how to make Proof General work -with another proof assistant. -@end itemize - - -@node Prerequisites for this manual -@section Prerequisites for this manual - -This manual assumes that you understand a little about using Emacs, for -example, switching between buffers using @kbd{C-x b} and understanding -that key sequences like @kbd{C-x b} mean "control-X followed by b". - -The manual also assumes you have a basic understanding of your proof -assistant and the language and files it uses for proof scripts. But -even without this, Proof General is not useless: you can use the -interface to @emph{replay} proof scripts for any proof assistant without -knowing how to start it up or issue commands, etc. This is the beauty -of a common interface mechanism. - -To get more from Proof General and adapt it to your liking, it helps to -know a little bit about how Emacs lisp packages can be customized via -the Customization mechanism. It's really easy to use. See @xref{Easy -customization} and @inforef{Easy customization, ,(xemacs)} for details. - -To get the absolute most from Proof General, to improve it or to adapt -it for new provers, you'll need to know a little bit of Emacs lisp. -Emacs is self-documenting, so you can begin from @kbd{C-h} and find out -everything! Here are some useful commands: - -@table @asis -@item @kbd{C-h i} -@code{info} -@item @kbd{C-h m} -@code{describe-mode} -@item @kbd{C-h b} -@code{describe-bindings} -@item @kbd{C-h f} -@code{describe-function} -@item @kbd{C-h v} -@code{describe-variable} -@end table - -Most of this manual covers the user-level view and customization of -Proof General. Towards the end we consider adapting Proof General to -new proof assistants, and document some of the internals of Proof -General. The manual concludes with some credits and references. -See the table of contents for details. - - - - - - - -@c -@c CHAPTER: Basic Script Management -@c -@node Basic Script Management -@chapter Basic Script Management - -This chapter is an introduction to using the script management -facilities of Proof General. We begin with a quick walkthrough example, -then describe the concepts and functions in more detail. - -@menu -* Walkthrough example in LEGO:: -* Proof scripts:: -* Script buffers:: -* Summary of Proof General buffers:: -* Script editing commands:: -* Script processing commands:: -* Toolbar commands:: -* Proof assistant commands:: -@end menu - -@node Walkthrough example in LEGO -@section Walkthrough example in LEGO - -Here's a short example in LEGO to see how script management is used. -The file you are asked to type below is included in the distribution as -@file{lego/example.l}. If you're not using LEGO, substitute some lines -from a simple proof for your proof assistant, or consult the example -file provided with Proof General. - -First, find a new file by doing @kbd{C-x C-f} and typing as the filename -@file{walkthrough.l}. This should load LEGO Proof General and the -toolbar and Proof General menus will appear. This walkthrough is -keyboard based, although you could easily use the toolbar and menu -functions instead. - - - -Now turn on active terminator minor mode by typing @kbd{C-c ;} and -enter: -@lisp -Module Walkthrough Import lib_logic; -@end lisp -The command should be lit in pink (or inverse video if you don't have a -colour display). As LEGO imports each module, a line will appear in the -minibuffer showing the creation of context marks. Eventually the command -should turn blue, indicating that LEGO has successfully processed -it. Then type (on a separate line if you like): -@lisp -Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A); -@end lisp -The goal should be echoed in the goals buffer. -@lisp -Intros; -@end lisp -Whoops! @kbd{C-c C-u} to pretend that didn't happen. -@lisp -intros; andI; -@end lisp -A proof summary will appear in the goals buffer. -@c We could solve the goal by pointing now, but we'll stay with the keyboard. -@lisp -Refine H; intros; Immed; Refine H; intros; Immed; -@end lisp -finishes the Goal. -@lisp -Save bland_commutes; -@end lisp - -Moving the mouse pointer over the locked region now reveals that the -entire proof has been aggregated into a single segment. Suppose we -decide to call the goal something more sensible. Moving the cursor up -into the locked region, somewhere between `Goal' and `Save', we enter -@kbd{C-c u}. The segment is transferred back into the editing -region. Now we correct the goal name, move the cursor to the end of the -buffer, and type @kbd{C-c RET}. Proof mode queues the commands for -processing and executes them. - - - - -@node Proof scripts -@section Proof scripts -@cindex proof script -@cindex scripting - -A @dfn{proof script} is a sequence of commands which construct a proof -in a proof assistant. Proof General is designed to work with text-based -@i{interactive} proof assistants, where the mode of working is usually a -dialogue between the human and the proof assistant. - -Primitive interfaces for proof assistants simply present a shell-like -view of this dialogue: the human repeatedly types commands to the shell -until the proof is completed. The system responds at each step, perhaps -with a new list of subgoals to be solved, or perhaps with a failure -report. Proof General manages the dialogue to only show the human the -information which is relevant at each step. - -@c Many proof assistants can also process proof scripts held in files - -Often we want to keep a record of the proof commands used to prove a -theorem, to build up a library of proved results. An easy way to store -a proof is to keep a text file which contains a proof script; the proof -assitant usually provides facility to read a proof script from a file -instead of the terminal. Using the file, we can @dfn{replay} the proof -script to prove the theorem again. -@c Re-playing a proof script is a non-interactive procedure, -@c since it is supposed to succeed. - -Using only a primitive shell interface, it can be tedious to construct -proof scripts with cut-and-paste. Proof General helps out by issuing -commands directly from a proof script file, while it is being written -and edited. Proof General can also be used conveniently to replay a -proof step-by-step, to see the progress at each stage. -@c developing them in proof script files. - -@dfn{Scripting} is the process of building up a proof script file or -replaying a proof. When scripting, Proof General sends proof commands -to the proof assistant one at a time, and prevents you from editing -commands which have been successfully completed by the proof assistant. -Regions of the proof script are analysed based on syntax and the -behaviour of the proof assistant after each proof command. - - -@node Script buffers -@section Script buffers -@cindex script buffer -@cindex proof script mode - -A @dfn{script buffer} is a buffer displaying a proof script. Its Emacs -mode is particular to the proof assistant you are using (but it inherits -from @dfn{proof-script mode}). - - -A script buffer is divided into three regions: @emph{locked}, -@emph{queue} and @emph{editing}. The proof commands -in the script buffer can include a number of -@emph{Goal-save sequences}. - -@menu -* Locked queue and editing regions:: -* Goal-save sequences:: -* Active scripting buffer:: -@end menu - - -@node Locked queue and editing regions -@subsection Locked, queue, and editing regions -@cindex Locked region -@cindex Queue region -@cindex Editing region -@cindex blue text -@cindex pink text - - -A script buffer is divided into three regions: - -@itemize @bullet -@item The @emph{locked} region appears in blue (underlined on monochrome -displays) and contains commands which have been sent to the proof process -and verified. The commands in the locked region cannot be edited. - -@item The @emph{queue} region appears in pink (inverse video) and contains -commands waiting to be sent to the proof process. Like those in the -locked region, these commands can't be edited. - -@item The @emph{editing} region contains the commands the user is working -on, and can be edited as normal Emacs text. -@end itemize - -These three regions appear in the buffer in the order above; that is, -the locked region is always at the start of the buffer, and the editing -region always at the end. The queue region only exists if there is input -waiting to be sent to the proof process. - -Proof mode has two fundamental operations which transfer commands -between these regions: @emph{assertion} and @emph{retraction}. - -@cindex Assertion -@strong{Assertion} causes commands from the editing region to be -transferred to the queue region and sent one by one to the proof -process. If the command is accepted, it is transferred to the locked -region, but if an error occurs it is signalled to the user, and the -offending command is transferred back to the editing region together -with any remaining commands in the queue. - -Assertion corresponds to processing proof commands, and makes the locked -region grow. - -@cindex Retraction -@strong{Retraction} causes commands to be transferred from the locked -region to the editing region (again via the queue region) and the -appropriate 'undo' commands to be sent to the proof process. - -Retraction corresponds to undoing commands, and makes the locked region -shrink. @xref{Script processing commands} details the commands -available for doing assertion and retraction. - - -@node Goal-save sequences -@subsection Goal-save sequences -@cindex goal -@cindex save -@cindex goal-save sequences - -A proof script contains a sequence of commands used to prove one or more -theorems. - -As commands in a proof script are transferred to the locked region, they -are aggregated into segments which constitute the smallest units which -can be undone. Typically a segment consists of a declaration or -definition, or all the text from a @dfn{goal} command to the -corresponding @dfn{save} command, or the individual commands in the -proof of an unfinished goal. As the mouse moves over the the region, -the segment containing the pointer will be highlighted. - -Proof General therefore assumes that the proof script has a series of -proofs which look something like this: -@lisp - goal @var{mythm} is @var{G} - @dots{} - save theorem @var{mythm} -@end lisp -interspersed with comments, definitions, and the like. Of course, the -exact syntax and terminology will depend on the proof assistant you use. - -The name @var{mythm} can appear in the menu for the proof script to help -quickly find a proof (@pxref{Support for function menus}). - -@c Proof General recognizes the goal-save sequences in proof scripts. -@c once a goal-save region has been fully processed by the proof assistant, -@c it is treated as atomic when undoing proof steps. This reflects the -@c fact that most proof assistants discard the history of a proof once a it -@c is completed or once a new proof is begun. - - -@node Active scripting buffer -@subsection Active scripting buffer -@cindex active scripting buffer - -You can edit as many script buffers as you want simultaneously, but only -one buffer at a time can be used to process a proof script -incrementally: this is the @dfn{active scripting buffer}. - -The active scripting buffer has a special indicator: the word -@code{Scripting} appears in its mode line. - -Proof General will give an error message: @code{Cannot have more than -one active scripting buffer!} if you attempt to use the script -processing commands in a new script buffer when there is already an -active scripting buffer which is only partly completed. If you get this -error message, you must choose either to assert the remainder of the -active buffer, or to retract what has been proved so far, before you can -start scripting in another buffer. - -@xref{Switching between proof scripts} for more explanation of this. - -@c A completed script buffer is one which is completely blue: the locked -@c region covers the whole buffer, indicating that all the commands been -@c successfully processed by the prover. - - -@node Summary of Proof General buffers -@section Summary of Proof General buffers -@cindex shell buffer -@cindex goals buffer -@cindex response buffer -@cindex proof by pointing - -Proof General manages several kinds of buffers in Emacs. Here is a -summary of the different kinds of buffers you will use when developing -proofs. - -@itemize @bullet -@item The @dfn{proof shell buffer} is an Emacs shell buffer - used to run your proof assistant. Usually it is hidden from view - (but see @xref{Working directly with the proof shell}). - Communication with the proof shell takes place via two or three - intermediate buffers. -@item A @dfn{script buffer}, as we have explained, is a buffer for editing a - proof script. The @dfn{active scripting buffer} is the script buffer - which is currently being used to send commands to the proof shell. -@item The @dfn{goals buffer} displays the list of subgoals to be - solved for a proof in progress. During a proof it is usually - displayed together with the script buffer. -@c FIXME: change when pbp is added back! - The goals buffer has facility for @dfn{proof-by-pointing}, although - this is disabled in Proof General @value{version}. -@item The @dfn{response buffer} displays other output from the proof - assistant, for example error messages or informative messages. - The response buffer is displayed whenever Proof General puts - a new message in it. -@end itemize - -Normally Proof General will automatically reveal and hide the goals and -response buffers as necessary during scripting. However there are ways -to customize the way the buffers are displayed, @pxref{Display -customization}. - -The menu @code{Proof General -> Buffers} provides a convenient way to -display or switch to one of the four buffers: active scripting, goals, -response, or shell. - -@c When -@c Proof General sees an error in the shell buffer, it will highlight the -@c error and display the buffer automatically. - - -@c This facility was not added: -@c -@c Optionally, the goals buffer and script buffer can be identified -@c @pxref{Identify goals and response}. The disadvantage of this is that -@c the goals display can be replaced by other messages, so you must ask for -@c it to be refreshed. The advantage is that it is simpler to deal with -@c fewer Emacs buffers. - - - -@node Script editing commands -@section Script editing commands - -Proof General provides a few functions for editing proof scripts. -Specific proof assistant code may elaborate on these basics. - -@findex indent-for-tab-command -@vindex proof-script-indent -Indentation is controlled by the user option @code{proof-script-indent} -@pxref{User options}. When indentation is enabled, Proof General -will indent lines of proof script with the usual Emacs functions, -particularly @kbd{TAB}, @code{indent-for-tab-command}. - -@c FIXME: remove when indentation is fixed. -Unfortunately, indentation in Proof General @value{version} is -somewhat slow and buggy. Therefore with large proof scripts, -we recommend @code{proof-script-index} is turned off. - -Here are the commands for moving around in a proof script, -with their default key bindings: -@kindex C-c C-e -@kindex C-c C-a -@kindex C-c ' -@table @kbd -@item C-c C-e -@code{proof-find-next-terminator} -@item C-c C-a -@code{proof-goto-command-start}. -@item C-c ' -@code{proof-goto-end-of-locked-interactive} -@end table - -@c TEXI DOCSTRING MAGIC: proof-find-next-terminator -@deffn Command proof-find-next-terminator -Set point after next @samp{@code{proof-terminal-char}}. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-goto-command-start -@deffn Command proof-goto-command-start -Move point to start of current command. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-goto-end-of-locked-interactive -@deffn Command proof-goto-end-of-locked-interactive -Switch to @code{proof-script-buffer} and jump to the end of the locked region. -Must be an active scripting buffer. -@end deffn - - -@node Script processing commands -@section Script processing commands -@kindex C-c C-n -@kindex C-c RET -@kindex C-c u -@kindex C-c C-u - -Here are the commands for asserting and retracting portions of the proof -script, together with their default key bindings. Note that assertion -and retraction commands can only be issued when the queue is empty. You -will get an error message @code{Proof Process Busy!} if you try to -assert an retract when the queue is being processed.@footnote{In fact, -this is an unnecessary restriction imposed by the original design of -Proof General. There is nothing to stop future versions of Proof -General allowing the queue region to be extended or shrunk, whilst the -prover is processing it.} - -@table @kbd -@item C-c C-n -@code{proof-assert-next-command} -@item C-c C-u -@code{proof-undo-last-successful-command} -@item C-c RET -@code{proof-assert-until-point} -@item C-c u -@code{proof-retract-until-point} -@item C-c b -@code{proof-process-buffer} -@item C-c @var{terminator-character} -@code{proof-active-terminator-minor-mode} -@end table - -The last command, @code{proof-active-terminator-minor-mode}, is -triggered using the character which terminates proof commands for your -proof assistant's script language. For LEGO and Isabelle, use @kbd{C-c -;}, for Coq, use @kbd{C-c .}. This not really a script processing -command. Instead, it causes subsequent key presses of @kbd{;} or -@kbd{.} to automatically send the line you've typed to the proof -assistant. - -Rather than use any other way of reading a proof script, a good reason -to use @kbd{C-c C-b} (@code{proof-process-buffer}) is that with a faulty -proof script (e.g., a script you are adapting to prove a different -theorem), Proof General will stop exactly where the proof script fails, -showing you the error message and the last processed command. So you -can easily continue development from exactly the right place in the -script. - - - -@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 - -@c TEXI DOCSTRING MAGIC: proof-undo-last-successful-command -@deffn Command proof-undo-last-successful-command &optional no-delete -Undo last successful command at end of locked region. -Unless optional @var{no-delete} is set, the text is also deleted from -the proof script. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-assert-until-point -@deffn Command 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 deffn - -@c TEXI DOCSTRING MAGIC: proof-retract-until-point -@deffn Command 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 actually 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 deffn - -@c TEXI DOCSTRING MAGIC: proof-process-buffer -@deffn Command proof-process-buffer -Process the current buffer and set point at the end of the buffer. -@end deffn - - -@c TEXI DOCSTRING MAGIC: proof-active-terminator-minor-mode -@deffn Command proof-active-terminator-minor-mode &optional arg -Toggle Proof General's active terminator minor mode. -With arg, turn on the Active Terminator minor mode if and only if arg -is positive. - -If active terminator mode is enabled, a terminator will process the -current command. -@end deffn - - -@node Toolbar commands -@section Toolbar commands - -The toolbar provides a selection of functions for asserting -and retracting portions of the script, and inserting -"goal" and "save" type commands. - -These functions are available only from the toolbar, menu Proof General --> Scripting, or via @kbd{M-x}. There are no keybindings for them by -default. - - -@c TEXI DOCSTRING MAGIC: proof-toolbar-goal -@deffn Command proof-toolbar-goal -Insert a goal command into the script buffer, issue it to prover. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-toolbar-retract -@deffn Command proof-toolbar-retract -Retract entire buffer. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-toolbar-undo -@deffn Command proof-toolbar-undo -Undo last successful in locked region, without deleting it. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-toolbar-next -@deffn Command proof-toolbar-next -Assert next command in proof to proof process. -Move point if the end of the locked position is invisible. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-toolbar-use -@deffn Command proof-toolbar-use -Process the whole buffer -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-toolbar-restart -@deffn Command proof-toolbar-restart -Restart scripting via @code{proof-shell-restart}. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-toolbar-qed -@deffn Command proof-toolbar-qed -Insert a save theorem command into the script buffer, issue it. -@end deffn - - - -@node Proof assistant commands -@section Proof assistant commands -@kindex C-c C-p -@kindex C-c c -@kindex C-c h - -There are several commands for interacting with the proof assistant away -from a proof script. Here are the keybindings and functions. - -@table @kbd -@item C-c C-p -@code{proof-prf} -@item C-c c -@code{proof-ctxt} -@item C-c h -@code{proof-help} -@item C-c C-c -@code{proof-interrupt-process} -@item C-c t -@code{proof-try-command} -@item C-c C-v -@code{proof-execute-minibuffer-cmd} -@end table - -@c TEXI DOCSTRING MAGIC: proof-prf -@deffn Command proof-prf -List proof state. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-ctxt -@deffn Command proof-ctxt -List context. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-help -@deffn Command proof-help -Print help message giving syntax. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-interrupt-process -@deffn Command proof-interrupt-process -Interrupt the proof assistant. Warning! This may confuse Proof General. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-try-command -@deffn Command proof-try-command &optional unclosed-comment-fun -Process the command at point, but don't add it to the locked region. - -Supplied to let the user to test the types and values of -expressions. Checks via the function @code{proof-state-preserving-p} that the -command won't change the proof state, but this isn't guaranteed to be -foolproof and may cause Proof General to lose sync with the prover. - -Default action if inside a comment is just to go until the start of -the comment. If you want something different, put it inside -@var{unclosed-comment-fun}. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-execute-minibuffer-cmd -@deffn Command proof-execute-minibuffer-cmd -Prompt for a command in the minibuffer and send it to proof assistant. -The command isn't added to the locked region. - -Warning! No checking whatsoever is done on the command, so this is -even more dangerous than @code{proof-try-command}. -@end deffn - -As if the last few commands weren't dangerous enough, there's also a -command which explicitly adjusts the end of the locked region, to be -used in extreme circumstances only. @pxref{Working directly with the -proof shell}. - -@c Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working -@c directly with the proof shell} - -There are a few commands for stopping, starting, and restarting the -proof assistant process which have menu entries but no key bindings. -As with any Emacs command, you can invoke these with @kbd{M-x}. - -@c TEXI DOCSTRING MAGIC: proof-shell-start -@deffn Command proof-shell-start -Initialise a shell-like buffer for a proof assistant. - -Also generates goal and response buffers. -Does nothing if proof assistant is already running. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-shell-restart -@deffn Command proof-shell-restart -Clear script buffers and send @code{proof-shell-restart-cmd}. -All locked regions are cleared and the active scripting buffer -deactivated. The restart command should re-synchronize -Proof General with the proof assitant. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-shell-exit -@deffn Command proof-shell-exit -Query the user and exit the proof process. - -This simply kills the @code{proof-shell-buffer} relying on the hook function -@code{proof-shell-kill-function} to do the hard work. -@end deffn - - - - - - -@c -@c CHAPTER: Advanced Script Management -@c -@node Advanced Script Management -@chapter Advanced Script Management -@cindex Multiple Files - -What we really mean by @emph{advanced} is that Proof General supports -large proof developments. These are typically spread across various -files which depend on each other in some way. Proof General knows enough -about the dependencies to allow script management across multiple files. - - -@menu -* Switching between proof scripts:: -* View of processed files :: -* Retracting across files:: -* Asserting across files:: -* Working directly with the proof shell:: -@end menu - -@node Switching between proof scripts -@section Switching between proof scripts -@cindex Switching between proof scripts - -Basic modularity in large proof developments can be achieved by -splitting proof scripts across various files. Let's assume that you are -in the middle of a proof development. You are working on a soundness -proof of Hoare Logic in a file called@footnote{The suffix may depend of -the specific proof assistant you are using e.g, LEGO's proof script -files have to end with @file{.l}.} @file{HSound.l}. It -depends on a number of other files which develop underlying -concepts e.g. syntax and semantics of expressions, assertions, -imperative programs. You notice that the current lemma is too difficult -to prove because you have forgotten to prove some more basic properties -about determinism of the programming language. Or perhaps a previous -definition is too cumbersome or even wrong. - -At this stage, you would like to visit the appropriate file, say -@file{sos.l} and retract to where changes are required. For further -details on how to accomplish this, we refer to @ref{Retracting across -files}. Then, using script management, you want to develop some more -basic theory in @file{sos.l}. Once this task has been completed -(possibly involving retraction across even earlier files) and the new -development has been asserted, you want to swich back to @file{HSound.l} -and replay to the point you got stuck previously. - -Some hours (or days) later you have completed the soundness proof and -are ready to tackle new challenges. Perhaps, you want to prove a -property that builds on soundness or you want to prove an orthogonal -property such as completeness. - -Proof General lets you do all of this while maintaining the consistency -between proof script buffers and the state of the proof assistant. -However, you cannot have more than one buffer where only a fraction of -the proof script contains a locked region. Before you can employ script -management in another proof script buffer, you must either fully assert -or retract the current script buffer. - -@node View of processed files -@section View of processed files - -Proof General is aware of all files that the proof assistant has -processed or is currently processing. In fact, it relies on the proof -assistant explicitly telling Proof General whenever it processes a -new file which corresponds@footnote{For example, LEGO generates additional compiled -(optimised) proof script files for efficiency.} to a file containing a proof -script. For further technical -details, @pxref{Handling multiple files}. - -If the current proof script buffer depends on background material from -other files, proof assistants typically process these files -automatically. If you visit such a file, the whole file is locked as -having been processed in a single step. From the user's point of view, -you can only retract but not assert in this buffer. Furthermore, -retraction is only possible to the @emph{beginning} of the buffer. - -To be more precise, buffers are locked as soon the proof assistant -notifies Proof General of processing a file different from the -current proof script. Thus, if you visit the file while the proof -assitant is still processing the file, it is already completely locked. -If the proof assistant is not happy with the contents and -complains with an error message, the buffer will still be marked as -having been completely processed. Sorry. You need to visit the -troublesome file, retract (which will always retract to the beginning of -the file) and debug the problem e.g., by asserting all of the buffer -under the supervision of Proof General, @pxref{Script processing -commands}. - -In case you wondered, inconsistencies may arise when you have unsaved -changes in a proof script buffer and the proof assistant suddenly -decides to automatically process the corresponding file. The good news -is that Proof General detects this problem and flashes up a warning in -the response buffer. You might then want to visit the modified buffer, -save it and retract to the beginning. Then you are back on track. - -@node Retracting across files -@section Retracting across files -@cindex Retraction - -Make sure that the current script buffer has either been completely -asserted or retracted. Then you can retract proof scripts in a different -file. Simply visit a file that has been processed earlier and retract in -it, using the retraction commands from @ref{Script processing commands}. Apart from removing parts of the locked region in this -buffer, all files which depend on it will be retracted (and thus -unlocked) automatically. Proof General reminds you that now is a good -time to save any unmodified buffers. - -@node Asserting across files -@section Asserting across files -@cindex Assertion - -Make sure that the current script buffer has either been completely -asserted or retracted. Then you can assert proof scripts in a different -file. Simply visit a file that contains no locked region and assert some -command with the usual assertion commands, @pxref{Script processing -commands}. Proof General reminds you that now is a good time to save any -unmodified buffers. This is particularly useful as assertion may cause -the proof assistant to automatically process other files. - - -@node Working directly with the proof shell -@section Working directly with the proof shell -@cindex Shell - -Occasionally you may want to review the dialogue of the entire session -with the proof assistant, or check that it hasn't done something -unexpected. Experienced users may also want to directly communicate with -the proof assistant rather than sending commands via the minibuffer, -@pxref{Proof assistant commands}. - -Although the proof shell is usually hidden from view, it is run in a -buffer which provides the usual full editing and history facilities of -Emacs shells (see the package @file{comint.el} distributed with your -version of Emacs). You can switch to it using the menu: - -@lisp - Proof-General -> Switch to buffers -> Proof Shell -@end lisp - -@b{Warning:} you can probably cause confusion by typing in the shell -buffer! Proof General may lose track of the state of the proof -assistant. - -Proof General watches the output from the proof assistant to guess when -a file is loaded or when a proof step is taken or undone, but it may not -be guaranteed when the restricted interface is by-passed. What happens -depends on how complete the communication is between Proof General and -the prover (which depends on the particular instantion of Proof -General). - -To resynchronise, you have two options. If you are lucky, it might -suffice to - -@table @kbd -@item C-c C-z -move the end of the locked region backwards to the end of the segment -containing the point. -@end table - -Otherwise, you will need to restart script management altogether, -@pxref{Toolbar commands}. - - - - -@node Support for other Packages -@chapter Support for other Packages - -Proof General makes some configuration for other Emacs packages which -provide various useful facilities. Sometimes this configuration is at -the proof assistant specific level, but we suggest that it should be -made for all proof assistants, as a convention. - -The packages currently supported are @code{fume-func}, -@code{outline-mode} and @code{etags}. - -@menu -* Support for function menus:: -* Support for outline mode:: -* Support for tags:: -@end menu - -@node Support for function menus -@section Support for function menus -@vindex proof-goal-with-hole-regexp -@cindex fume-func - -The Emacs package @code{fume-func} is a provides the handy facility to -make a menu from the names of entities declared in a buffer. Proof -General configures @code{fume-func} so that you can quickly jump to -particular proofs in a script buffer. (This is done with the -configuration variables @code{proof-goal-with-hole-regexp} and -@code{proof-save-with-hole-regexp}.) -@c , @pxref{Proof script mode} for further details. - -If you want to use fume-func, you may need to enable it for yourself. -It is distributed with XEmacs but by not enabled by default. To enable -it you should find the file @file{func-menu.el} and follow the -instructions there. At the time of writing, the current version of -XEmacs is 20.4, supplied with function menu version 2.45, which suggests -the following code for your @file{.emacs} file: - -@lisp - (require 'func-menu) - (define-key global-map 'f8 'function-menu) - (add-hook 'find-file-hooks 'fume-add-menubar-entry t) - (define-key global-map "\C-cl" 'fume-list-functions) - (define-key global-map "\C-cg" 'fume-prompt-function-goto) - (define-key global-map '(shift button3) 'mouse-function-menu) - (define-key global-map '(meta button1) 'fume-mouse-function-goto) -@end lisp - -If you have another version of Emacs, you should check the -@file{fume-func.el} file supplied with it. - -@node Support for outline mode -@section Support for outline mode -@cindex outline mode - -Proof General configures Emacs variables (@code{outline-regexp} and -@code{outline-heading-end-regexp}) so that outline minor mode can be -used on proof script files. The headings taken for outlining are the -"goal" statements at the start of goal-save sequences, -@xref{Goal-save sequences}. - -Use @kbd{M-x outline-minor-mode} to turn on outline minor mode. -Functions for navigating, hiding, and revealing the proof script are -available in menus. - -See @inforef{Outline Mode, ,(xemacs)} for more information about -outline mode. - - - -@node Support for tags -@section Support for tags -@cindex tags - -A "tags table" is a description of how a multi-file program is broken up -into files. It lists the names of the component files and the names and -positions of the functions (or other named subunits) in each file. -Grouping the related files makes it possible to search or replace -through all the files with one command. Recording the function names -and positions makes possible the @kbd{M-.} command which finds the -definition of a function by looking up which of the files it is in. - -Some instantiations of Proof General (currently LEGO and Coq) are -supplied with external programs for making tags tables. Once a tag -table has been made for your proof developments, you can use the Emacs -tags mechanisms to find tags, and complete symbols from tags table. - -One useful key binding you might want to make is to set the usual -completion key @kbd{M-tab} to run @code{tag-complete-symbol} to use -completion from names in the tag table. To set this binding in Proof -General script buffers, put this code in your @file{.emacs} file: -@lisp -(add-hook 'proof-mode-hook - (lambda () (local-set-key '(meta tab) 'tag-complete-symbol))) -@end lisp -(Since this key binding interfers with a default binding that users may -already have customized, Proof General doesn't do this automatically). - -For more information on how to use tags, @inforef{Tags, ,(xemacs)}. - - - -@node Customizing Proof General -@chapter Customizing Proof General -@cindex Customization - - -There are two kinds of customization for Proof General: it can be -customized for a user's preferences using a particular proof assistant, -or it can be customized by an Emacs expert to add a new proof assistant. -Here we cover the user-level customization for Proof General. - -We only consider settings for Proof General itself. The support for a -particular proof assistant can provide extra customization settings. -See the chapters covering each assistant for details. - - -@menu -* Easy customization:: -* Display customization:: -* User options:: -* Changing faces:: -* Tweaking configuration settings:: -@end menu - -@node Easy customization -@section Easy customization -@cindex Using Customize -@cindex Emacs customization library - -Proof General uses the Emacs customization library extensively to -provide a friendly interface. - -You can access a menu of the customization settings for Proof General -via the menu: - -@lisp - Options -> Customize -> Emacs -> External -> Proof General -@end lisp -in XEmacs. - -In FSF Emacs, use the menu: -@c FIXME -@lisp - Help -> Customize -> Specific group -@end lisp -and type @kbd{proof-general RET}. - -The complete set of customization settings will only be availabe after -Proof General has been fully loaded. Proof General is fully loaded when -you visit a script file for the first time. - -When visiting a script file, there is a more direct route to the -settings: -@lisp - Proof-General -> Customize -@end lisp - -Using the customize facility is straightforward. You can select the -setting to customize via the menus, or with @code{M-x -customize-variable}. When you have selected a setting, you are shown a -buffer with its current value, and facility to edit it. Once you have -edited it, you can use the special buttons @var{set}, @var{save} and -@var{done}. You must use one of @var{set} or @var{save} to get any -effect. The @var{save} button stores the setting in your @file{.emacs} -file. - -Notice that in the customize menus, variable names mentioned later may -be abbreviated by omitting the "@code{proof}-" prefix. Also, some of -the option settings may have more descriptive names (for example, -@var{on} and @var{off}) than the low-level lisp values (non-@code{nil}, -@code{nil}) which are mentioned in this chapter. - -For more help, see @inforef{Easy Customization, ,xemacs}. - - - -@node Display customization -@section Display customization -@cindex display customization -@cindex multiple windows -@cindex buffer display customization -@cindex frames -@cindex multiple frames - -If you are working on a workstation with a window system, you can use -Emacs to manage several @i{frames} on the display, to keep the goals -buffer displayed in a fixed place on your screen and in a certain font, -for example. A convenient way to do this is via -@code{special-display-regexps}. - - -@c TEXI DOCSTRING MAGIC: proof-auto-delete-windows -@defopt proof-auto-delete-windows -If non-nil, automatically remove windows when they are cleaned. -For example, at the end of a proof the goals buffer window will -be cleared; if this flag is set it will automatically be removed. -If you want to fix the sizes of your windows you may want to set this -variable to @code{nil'} to avoid windows being deleted automatically. -If you use multiple frames, only the windows in the currently -selected frame will be automatically deleted. - -The default value is @code{nil}. -@end defopt - - - - -@node User options -@section User options -@c Index entries for each option 'concept' -@cindex User options -@cindex Strict read-only -@cindex Query program name -@cindex Dedicated windows -@cindex Remote host -@cindex Toolbar follow mode -@cindex Toolbar disabling -@cindex Proof script indentation -@cindex Indentation -@cindex Remote shell -@cindex Running proof assistant remotely -@c @cindex formatting proof script - -Here are the remaining user options for Proof General. These can be set -via the customization system, via the old-fashioned @code{M-x -edit-options} mechanism, or simply by adding @code{setq}'s to your -@file{.emacs} file. The first approach is strongly recommended. - - -@c TEXI DOCSTRING MAGIC: proof-prog-name-ask -@defopt proof-prog-name-ask -If non-nil, query user which program to run for the inferior process. - -The default value is @code{nil}. -@end defopt - - -@c TEXI DOCSTRING MAGIC: proof-rsh-command -@defopt proof-rsh-command -Shell command prefix to run a command on a remote host. -For example, -@lisp - ssh bigjobs -@end lisp -Would cause Proof General to issue the command @samp{ssh bigjobs isabelle} -to start Isabelle remotely on our large compute server called @samp{bigjobs}. - -The protocol used should be configured so that no user interaction -(passwords, or whatever) is required to get going. - -The default value is @code{""}. -@end defopt - -@c TEXI DOCSTRING MAGIC: proof-toolbar-wanted -@defopt proof-toolbar-wanted -Whether to use toolbar in proof mode. - -The default value is @code{t}. -@end defopt - - -@c TEXI DOCSTRING MAGIC: proof-toolbar-follow-mode -@defopt proof-toolbar-follow-mode -Choice of how point moves with toolbar commands. -One of the symbols: @code{locked}, @code{follow}, @code{ignore}. -If @code{locked}, point sticks to the end of the locked region with toolbar commands. -If @code{follow}, point moves just when needed to display the locked region end. -If @code{ignore}, point is never moved after toolbar movement commands. - -The default value is @code{locked}. -@end defopt - -@c TEXI DOCSTRING MAGIC: proof-window-dedicated -@defopt proof-window-dedicated -Whether response and goals buffers have dedicated windows. -If t, windows displaying responses from the prover will not -be switchable to display other windows. This may help manage -your display, but can sometimes be inconvenient, especially -for experienced Emacs users. -Moreover, this option may cause problems with multi-frame -use because of a bug. - -The default value is @code{nil}. -@end defopt - -@c FIXME needs to mention that without dedicated windows, buffers may be -@c hidden. Refer to the XEmacs manual on customising buffer display. - -@c TEXI DOCSTRING MAGIC: proof-strict-read-only -@defopt proof-strict-read-only -Whether Proof General is strict about the read-only region in buffers. -If non-nil, an error is given when an attempt is made to edit the -read-only region. If nil, Proof General is more relaxed (but may give -you a reprimand!) - -The default value is @code{15}. -@end defopt - - -@c TEXI DOCSTRING MAGIC: proof-script-indent -@defopt proof-script-indent -If non-nil, enable indentation code for proof scripts. -Currently the indentation code can be rather slow for large scripts, -and is critical on the setting of regular expressions for particular -provers. Enable it if it works for you. - -The default value is @code{nil}. -@end defopt - -@c TEXI DOCSTRING MAGIC: proof-one-command-per-line -@defopt proof-one-command-per-line -If non-nil, format for newlines after each proof command in a script. -This option is not fully-functional at the moment. - -The default value is @code{nil}. -@end defopt - - -@c TEXI DOCSTRING MAGIC: proof-splash-inhibit -@defopt proof-splash-inhibit -Non-nil prevents splash screen display when Proof General is loaded. - -The default value is @code{nil}. -@end defopt - - -@node Changing faces -@section Changing faces - -The fonts and colours that Proof General uses are configurable. If you -alter these through the customize menus, only the particular kind of -display in use (colour window system, monochrome window system, console, -@dots{}) will be affected. - -@c TEXI DOCSTRING MAGIC: proof-queue-face -@deffn Face proof-queue-face -Face for commands in proof script waiting to be processed. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-locked-face -@deffn Face proof-locked-face -Face for locked region of proof script (processed commands). -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-declaration-name-face -@deffn Face proof-declaration-name-face -Face for declaration names in proof scripts. -Exactly what uses this face depends on the proof assistant. -@end deffn - - -@c TEXI DOCSTRING MAGIC: proof-tacticals-name-face -@deffn Face proof-tacticals-name-face -Face for names of tacticals in proof scripts. -Exactly what uses this face depends on the proof assistant. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-error-face -@deffn Face proof-error-face -Face for error messages from proof assistant. -@end deffn - -@c TEXI DOCSTRING MAGIC: proof-warning-face -@deffn Face proof-warning-face -Face for warning messages. -Warning messages can come from proof assistant or from Proof General itself. -@end deffn - -@c Maybe this detail of explanation belongs in the internals, -@c with just a hint here. -The slightly bizarre name of the next face comes from the idea that -while large amounts of output are being sent from the prover, some -messages should be displayed to the user while the bulk of the output is -hidden. The messages which are displayed may have a special annotation -to help Proof General recognize them, and this is an "eager" annotation -in the sense that it should be processed as soon as it is observed -by Proof General. - -@c TEXI DOCSTRING MAGIC: proof-eager-annotation-face -@deffn Face proof-eager-annotation-face -Face for messages from proof assistant. -@end deffn - - - - -@node Tweaking configuration settings -@section Tweaking configuration settings - -This section is a note for advanced users. - -Configuration settings are the per-prover customizations of Proof -General. These are not intended to be adjusted by the user. But -occasionally you may like to test changes to these settings to improve -the way Proof General works. You may want to do this when a proof -assistant has a flexible proof script language in which one can define -new tactics or even operations, and you want Proof General to recognize -some of these which the default settings don't mention. So please feel -free to try adjusting the configuration settings and report to us if you -find better default values than the ones we have provided. - -The configuration settings appear in the customization group -@code{prover-config}, or via the menu -@lisp - Proof-General -> Internals -> Prover Config -@end lisp - -One basic example of a setting you may like to tweak is: - -@c TEXI DOCSTRING MAGIC: proof-assistant-home-page -@defvar proof-assistant-home-page -Web address for information on proof assistant -@end defvar - -Most of the others are more complicated. More details of the settings -are given in @xref{Adapting Proof General to New Provers}. To browse -them, you can look through the customization groups -@code{prover-config}, @code{proof-script} and @code{proof-shell}. The -group @code{proof-script} contains the configuration variables for -scripting, and the group @code{proof-shell} contains those for -interacting with the proof assistant. - -Unfortunately, although you can use the customization mechanism to set -and save these variables, saving them may have no effect because the -default settings are often hard-wired into the proof assistant code. -Ones we expect may need changing appear as proof assistant specific -configurations. For example, @code{proof-assistant-home-page} is set in -the LEGO code from the value of the customization setting -@code{lego-www-home-page}. At present there is no easy way to save -changes to other configuration variables across sessions, other than by -editing the source code. Please contact us if this proves to be a -problem for any variable. - - - - - -@c -@c CHAPTER: LEGO Proof General -@c -@node LEGO Proof General -@chapter LEGO Proof General -@cindex LEGO Proof General - -LEGO proof script mode is a mode derived from proof script mode for -editing LEGO scripts. An important convention is that proof script -buffers @emph{must} start with a module declaration. If the proof script -buffer's file name is @file{fermat.l}, then it must commence with a -declaration of the form - -@lisp -Module fermat; -@end lisp - -If, in the development of the module @samp{fermat}, you require material -from other module e.g., @samp{lib_nat} and @samp{galois}, you need to -specify this dependency as part of the module declaration: - -@lisp -Module fermat Import lib_nat galois; -@end lisp - -No need to worry too much about effeciency. When you retract back to a -module declaration to add a new import item, LEGO does not actually -retract the previously imported modules. Therefore, reasserting the -extended module declaration really only processes the newly imported -modules. - -Using the LEGO Proof General, you never ever need to use administrative -LEGO commands such as @samp{Forget}, @samp{ForgetMark}, @samp{KillRef}, -@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again -@footnote{And please, don't even think of including those in your LEGO -proof script!}. You can concentrate on your actual proof developments. -Script management in Proof General will invoke the appropriate commands -for you. Proving with LEGO has never been easier. - -@menu -* LEGO specific commands:: -* LEGO tags:: -* LEGO customizations:: -@end menu - - -@node LEGO specific commands -@section LEGO specific commands - -In addition to the commands provided by the generic Proof General, see -the previous sections, the LEGO Proof General provides a few extensions. -In proof scripts, there are some abbreviations for common commands: - -@table @kbd -@item C-c i -intros -@item C-c I -Intros -@item C-c R -Refine -@end table - -@node LEGO tags -@section LEGO tags - -The LEGO Proof General provides the program @file{legotags} to generate -tags for LEGO proof scripts. Invoking @samp{legotags *.l} produces a -file @file{TAGS} for all LEGO modules in the current directory. The LEGO -library itself is shipped out with all its modules already being tagged. -See @ref{Support for tags} for further details. - - -@node LEGO customizations -@section LEGO customizations - -We refer to chapter @ref{Customizing Proof General} for an introduction -to the customisation mechanism. In addition to customizations at the -generic level, for LEGO you can also customize: - -@c TEXI DOCSTRING MAGIC: lego-tags -@defopt lego-tags -The directory of the @var{tags} table for the @var{lego} library - -The default value is @code{"/usr/lib/lego/lib_Type/"}. -@end defopt - -@c TEXI DOCSTRING MAGIC: lego-help-menu-list -@defvar lego-help-menu-list -List of menu items, as defined in @samp{@code{easy-menu-define}} for @var{lego} -@lisp - specific help. -@end lisp -@end defvar - -@c We don't worry about the following for now. These are too obscure. -@c lego-indent -@c lego-test-all-name - -@c We also don't document any of the internal variables which have been -@c set to configure the generic Proof General and which the user should -@c not tamper with - -In Xemacs 20.4, LEGO script buffer are coloured (fontified as they say) -by default. To automatically switch on fontification in FSF Emacs 20.2, -you need to set -@vindex lego-mode-hooks -@cindex font-lock colour - -@lisp - (add-hook 'lego-mode-hooks 'turn-on-font-lock) -@end lisp - -in your @file{~/.emacs} file. - - - -@node Coq Proof General -@chapter Coq Proof General - -Sorry, there is no specific documentation written yet for Coq Proof -General. - -If any Coq user would like to contribute, please send a message to -@code{proofgen@@dcs.ed.ac.uk}. - -Type @kbd{C-h C-m} to get a list of Coq specific commands and -browse the customize menus to find out what customization -options there are for Coq. - -@menu -* Coq specific commands:: -* Coq customizations:: -@end menu - -@node Coq specific commands -@section Coq specific commands - -@node Coq customizations -@section Coq customizations - - -@c -@c CHAPTER: Isabelle Proof General -@c - -@node Isabelle Proof General -@chapter Isabelle Proof General -@cindex Isabelle Proof General - -Isabelle Proof General includes a mode for editing theory files taken -from David Aspinall's Isamode interface, -@uref{http://www.dcs.ed.ac.uk/home/da/Isamode}. Detailed documentation -for the theory file mode is included with @code{Isamode}, there are some -notes on the special functions available and customization setttings -below. - -@menu -* Theory files:: -* Isabelle specific commands:: -* Isabelle customizations:: -@end menu - - -@node Theory files -@section Theory files -@cindex Theory files (in Isabelle) -@cindex ML files (in Isabelle) - -Isabelle Proof General attempts to lock theory files as well as ML files -when they are loaded. Theory files are always completely locked or -completely unlocked, because they are processed atomically. - -Proof General attempts to load the theory file for a @file{.ML} file -automatically before you start scripting. This is tricky because -Isabelle's theory loader assumes that @file{.ML} files are always read -together with theory files. At the moment Proof General uses an altered -version of @code{use_thy} which doesn't load the top-level ML file in -this case. - -@c FIXME: should say something about this: -@c This can cause confusion in the theory loader later, -@c especially with @code{update()}. To be safe, try to use just the Proof -@c General interface, and report any repeatable problems to -@c @code{isabelle@dcs.ed.ac.uk}. - -Compared to Isamode's theory editing mode, some of the functions and key -bindings for interacting with Isabelle have been removed, and two new -functions are available. - -The key @kbd{C-c C-b} (@code{isa-process-thy-file}) will cause Isabelle -to read the theory file being edited. This causes the file and all its -children (both theory and ML files) to be read. Any top-level ML file -associated with this theory file is also read. - -The key @kbd{C-c C-u} (@code{isa-retract-thy-file}) will retract -(unlock) the theory file being edited. This unlocks the file and all -its children (theory and ML files); no changes occur in Isabelle itself. - - -@c TEXI DOCSTRING MAGIC: isa-process-thy-file -@deffn Command isa-process-thy-file file -Process the theory file @var{file}. If interactive, use @code{buffer-file-name}. -@end deffn - -@c TEXI DOCSTRING MAGIC: isa-retract-thy-file -@deffn Command isa-retract-thy-file file -Retract the theory file @var{file}. If interactive, use @code{buffer-file-name}. -@end deffn - - -@node Isabelle specific commands -@section Isabelle specific commands - - -@unnumberedsubsec Switching to theory files -@cindex Switching to theory files -@kindex C-c C-o - -In Isabelle proofscript mode, @kbd{C-c C-o} (@code{thy-find-other-file}) -finds and switches to the associated theory file, that is, the file with -the same base name but extension @file{.thy} swapped for @file{.ML}. - -The same function (and keybinding) switches back to an ML file from the -theory file. - - -@c TEXI DOCSTRING MAGIC: thy-find-other-file -@deffn Command thy-find-other-file &optional samewindow -Find associated .ML or .thy file. -Finds and switch to the associated ML file (when editing a theory file) -or theory file (when editing an ML file). -If @var{samewindow} is non-nil (interactively, with an optional argument) -the other file replaces the one in the current window. -@end deffn - - -@node Isabelle customizations -@section Isabelle customizations - -Here are some of the user options specific to Isabelle. You can set -these with the customization mechanism as usual. - -@c TEXI DOCSTRING MAGIC: isabelle-web-page -@defvar isabelle-web-page -URL of web page for Isabelle. -@end defvar - - -@c @unnumberedsubsec Theory file editing customization - -@c TEXI DOCSTRING MAGIC: thy-use-sml-mode -@defopt thy-use-sml-mode -If non-nil, invoke sml-mode inside "ML" section of theory files. -This option is left-over from Isamode. Really, it would be more -useful if the script editing mode of Proof General itself could be based -on sml-mode, but at the moment there is no way to do this. - -The default value is @code{nil}. -@end defopt - -@c TEXI DOCSTRING MAGIC: thy-indent-level -@defvar thy-indent-level -Indentation level for Isabelle theory files. An integer. -@end defvar - -@defopt thy-indent-level -Indentation level for Isabelle theory files. An integer. -@end defopt - -@c TEXI DOCSTRING MAGIC: thy-sections -@defvar thy-sections -Names of theory file sections and their templates. -Each item in the list is a pair of a section name and a template. -A template is either a string to insert or a function. Useful functions are: -@lisp - @code{thy-insert-header}, @code{thy-insert-class}, @code{thy-insert-default-sort}, - @code{thy-insert-const}, @code{thy-insert-rule}. -@end lisp -The nil template does nothing. -You can add extra sections to theory files by extending this variable. -@end defvar - -@c TEXI DOCSTRING MAGIC: thy-template -@defvar thy-template -Template for theory files. -Contains a default selection of sections in a traditional order. -You can use the following format characters: - -%t --- replaced by theory name. - -%p --- replaced by names of parents, separated by @samp{+} characters. -@end defvar - -@c ideal for above: -@c @defopt thy-template -@c Template for theory files. -@c Contains a default selection of sections in a traditional order. -@c You can use the following format characters: -@c @code{%t} -- replaced by theory name -@c @code{%p} -- replaced by names of parents, separated by @code{+}'s -@c @end defopt - - - - -@node Adapting Proof General to New Provers -@chapter Adapting Proof General to New Provers - -Proof General has about 60 configuration variables which are set on a -per-prover basis to configure the various features. However, many of -these variables occcur in pairs (typically regular expressions matching -the start and end of some text), and you can begin by setting just a few -variables to get the basic features working. - -The configuration variables are declared in the file -@file{generic/proof-config.el}. Documentation below is based on the -contents of that file. - -@menu -* Overview of adding a new prover:: -* Major modes used by Proof General:: -* Menus and user-level commands:: -* Proof script settings:: -* Proof shell settings:: -* Splash screen settings:: -* Goals buffer configuration:: -* Global constants:: -* Handling multiple files:: -@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. - -@itemize @bullet -@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 New 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 modes in @file{myassistant.el}, by looking at - the files for the currently supported assistants for example. - Basically you need to define some modes using @code{define-derived-mode} - and set the configuration variables. It's important that your modes - invoke the callbacks @code{proof-config-done} and - @code{proof-shell-config-done} once they've set the configuration - variables. -@end itemize - -You could begin by setting minimum number of the variables, then adjust -the settings via the customize menus, under Proof-General -> 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{@var{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{@var{proof-home-directory}} is the value of the -variable @code{proof-home-directory}. - -The default value is @code{((isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$"))}. -@end defopt - -@node Major modes used by Proof General -@section Major modes used by Proof General - -@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 in @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. -Usually customised for specific prover. -Suggestion: this can be set in @code{proof-pre-shell-start-hook}. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-mode-for-pbp -@defvar proof-mode-for-pbp -Mode for proof state display buffers. -Usually customised for specific prover. -Suggestion: this can be set in @code{proof-pre-shell-start-hook}. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-mode-for-script -@defvar proof-mode-for-script -Mode for proof script buffers. -This is used by Proof General to find out which buffers -contain proof scripts. -Suggestion: this can be set in the script mode configuration. -@end defvar - -@node Menus and user-level commands -@section Menus and user-level commands - -@c TEXI DOCSTRING MAGIC: proof-assistant-home-page -@defvar proof-assistant-home-page -Web address for information on proof assistant -@end defvar -@c TEXI DOCSTRING MAGIC: proof-ctxt-string -@defvar proof-ctxt-string -Command to display the context in proof assistant. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-help-string -@defvar proof-help-string -Command to ask for help in proof assistant. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-prf-string -@defvar proof-prf-string -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 %s will be replaced by the -goal string. If a function, should return a command string to -insert when called interactively. -@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 %s will be replaced by the -theorem name. If a function, should return a command string to -insert when called interactively. -@end defvar - -@c defgroup proof-script -@node Proof script settings -@section Proof script settings - -The following variables should be set before proof-config-done -is called. These configure the mode for the script buffer, -including highlighting, etc. - -@c TEXI DOCSTRING MAGIC: proof-terminal-char -@defvar proof-terminal-char -Character which terminates a proof command in a script buffer. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-comment-start -@defvar proof-comment-start -String which starts a comment in the proof assistant command language. -The script buffer's @code{comment-start} is set to this string plus a space. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-comment-end -@defvar proof-comment-end -String which starts a comment in the proof assistant command language. -The script buffer's @code{comment-end} is set to this string plus a space. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-save-command-regexp -@defvar proof-save-command-regexp -Matches a save command -@end defvar -@c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp -@defvar proof-save-with-hole-regexp -Regexp which matches a command to save a named theorem. -Match number 2 should be the name of the theorem saved. -Used for setting names of goal..save regions and for default -func-menu configuration in proof-script-find-next-goalsave. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-goal-command-regexp -@defvar proof-goal-command-regexp -Matches a goal command. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp -@defvar proof-goal-with-hole-regexp -Regexp which matches a command used to issue and name a goal. -Match number 2 should be the name of the goal issued. -Used for setting names of goal..save regions and for default -func-menu configuration in proof-script-find-next-goalsave. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps -@defvar proof-script-next-entity-regexps -Regular expressions to control finding definitions in script. -This is the list of the form -@lisp - (@var{anyentity-regexp} - @var{discriminator-regexp} ... @var{discriminator-regexp}) -@end lisp -The idea is that @var{anyentity-regexp} matches any named entity in the -proof script, on a line where the name appears. This is assumed to be -the start or the end of the entity. The discriminators then test -which kind of entity has been found, to get its name. A -@var{discriminator-regexp} has one of the forms -@lisp - (@var{regexp} @var{matchno}) - (@var{regexp} @var{matchno} @code{backward} @var{backregexp}) - (@var{regexp} @var{matchno} @code{forward} @var{forwardregexp}) -@end lisp -If @var{regexp} matches the string captured by @var{anyentity-regexp}, then -@var{matchno} is the match number for the substring which names the entity. - -If @code{backward} @var{backregexp} is present, then the start of the entity -is found by searching backwards for @var{backregexp}. - -Conversely, if @code{forward} @var{forwardregexp} is found, then the end of -the entity is found by searching forwards for @var{forwardregexp}. - -Otherwise, the start and end of the entity will be the region matched -by @var{anyentity-regexp}. - -This mechanism allows fairly complex parsing of the buffer, in -particular, it allows for goal..save regions which are named -only at the end. However, it does not parse strings, -comments, or parentheses. - -This variable may not need to be set: a default value which should -work for goal..saves is calculated from @code{proof-goal-with-hole-regexp}, -@code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}. -@end defvar -@c TEXI DOCSTRING MAGIC: nilproof-goal-command-p nil -@c TEXI DOCSTRING MAGIC: proof-lift-global -@defvar proof-lift-global -This function lifts local lemmas from inside goals out to top level. -This function takes the local goalsave span as an argument. Set this -to @samp{nil} of the proof assistant does not support nested goals. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-count-undos-fn -@defvar proof-count-undos-fn -Compute number of undos in a target segment -@end defvar -@c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn -@defvar proof-find-and-forget-fn -Function returning a command string to forget back to before its argument span. -The special string @code{proof-no-command} means there is nothing to do. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn -@defvar proof-goal-hyp-fn -Function which returns cons cell if point is at a goal/hypothesis. -First element of cell is a symbol, @code{goal'} or @code{hyp'}. The second -element is a string: the goal or hypothesis itself. This is used -when parsing the proofstate output -@end defvar -@c TEXI DOCSTRING MAGIC: proof-kill-goal-command -@defvar proof-kill-goal-command -Command to kill a goal. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-global-p -@defvar proof-global-p -Whether a command is a global declaration. Predicate on strings or nil. -This is used to handle nested goals allowed by some provers. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-state-preserving-p -@defvar proof-state-preserving-p -A predicate, non-nil if its argument preserves the proof state. -@end defvar -@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. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-stack-to-indent -@defvar proof-stack-to-indent -Prover-specific code for indentation. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-parse-indent -@defvar proof-parse-indent -Proof-assistant specific function for parsing. -Invoked in @samp{proof-parse-to-point}. Must be a -function taking two arguments, a character (the current character) -and a stack reflecting indentation, and must return a stack. The -stack is a list of the form (c . p) where @samp{c} is a character -representing the type of indentation and @samp{p} records the column for -indentation. The generic @samp{proof-parse-to-point} function supports -parentheses and commands. It represents these with the characters -@samp{?(}, @samp{?[} and @samp{@code{proof-terminal-char}}. -@end defvar - - - -@node Proof shell settings -@section Proof shell settings - -The variables in this section are the largest group. They concern the -proof shell mode. The first group of variables are hooks invoked at -various points. The second group of variables are concerned with -matching the output from the proof assistant. - -Variables here are put into the customize group @code{proof-shell}. - -These should be set in the shell mode configuration, again, -before @code{proof-shell-config-done} is called. - -@menu -* Proof shell commands:: -* Settings for matching output from proof process:: -* Hooks and function variables:: -@end menu - -@node Proof shell commands -@subsection Commands - -@c TEXI DOCSTRING MAGIC: proof-prog-name -@defvar proof-prog-name -System command to run program name in proof shell. -Suggestion: this can be set in @code{proof-pre-shell-start-hook} from -a variable which is in the proof assistant's customization -group. This allows different proof assistants to coexist -(albeit in separate Emacs sessions). -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-init-cmd -@defvar proof-shell-init-cmd -The command for initially configuring the proof process. -@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-cd -@defvar proof-shell-cd -Command to the proof assistant to change the working directory. -@end defvar - -@node Settings for matching output from proof process -@subsection Settings for matching output from proof process -@c TEXI DOCSTRING MAGIC: proof-shell-wakeup-char -@defvar proof-shell-wakeup-char -A special character which terminates an annotated prompt. -Set to nil if proof assistant does not support annotated prompts. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-first-special-char -@defvar proof-shell-first-special-char -First special character. -Codes above this character can have special meaning to Proof General, -and are stripped from the prover's output strings. -@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. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp -@defvar proof-shell-annotated-prompt-regexp -Regexp matching a (possibly annotated) prompt pattern. -Output is grabbed between pairs of lines matching this regexp. -To help matching you may be able to annotate the proof assistant -prompt with a special character not appearing in ordinary output. -The special character should appear in this regexp, 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. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp -@defvar proof-shell-interrupt-regexp -Regexp matching output indicating the assistant was interrupted. -Similar notes apply as for @code{proof-shell-error-regexp}, which see. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp -@defvar proof-shell-proof-completed-regexp -Regexp matching output indicating a finished proof. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp -@defvar proof-shell-clear-response-regexp -Regexp matching output telling Proof General to clear the response buffer. -This feature is useful to give the prover more control over what output -is shown to the user. Set to nil to disable. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp -@defvar proof-shell-start-goals-regexp -Regexp matching the start of the proof state output. -@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. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start -@defvar proof-shell-eager-annotation-start -Eager annotation field start. A regular expression or nil. -An eager annotation indicates to Emacs that some following output -should be displayed immediately and not accumulated for parsing. -Set to nil to disable this feature. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end -@defvar proof-shell-eager-annotation-end -Eager annotation field end. A regular expression or nil. -An eager annotation indicates to Emacs that some following output -should be displayed immediately and not accumulated for parsing. - -The default value is "\n" to match up to the end of the line. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp -@defvar proof-shell-assumption-regexp -A regular expression matching the name of assumptions. -@end defvar - - -@node Hooks and function variables -@subsection Hooks and function variables - -@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, setting the line width of output). -Any text inserted by these hooks will be sent to the proof process -before every command issued by Proof General. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-pre-shell-start-hook -@defvar proof-pre-shell-start-hook -Hooks run before proof shell is started. -Usually this is set to a function which configures the proof shell -variables. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-hook -@defvar proof-shell-handle-error-hook -Hooks run after an error has been reported in the response buffer. -@end defvar -@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 a script file name (with complete -path) the system is currently processing. 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 -A @var{regexp} to match that the prover has retracted across file boundaries. - -At this stage, Proof General's view of the processed files is out of -date and needs to be updated with the help of the function -@samp{@code{proof-shell-compute-new-files-list}}. -@end defvar -@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 -@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 Splash screen settings -@section Splash screen settings - -The splash screen can be configured, in a rather limited way. - -@c TEXI DOCSTRING MAGIC: proof-splash-time -@defvar proof-splash-time -Minimum number of seconds to display splash screen for. -The splash screen may be displayed for a couple of seconds longer than -this, depending on how long it takes the machine to initialise proof mode. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-splash-contents -@defvar proof-splash-contents -Evaluated to configure splash screen displayed when entering Proof General. -If an element is a string or an image specifier, it is displayed -centred on the window on its own line. If it is nil, a new line is -inserted. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-splash-extensions -@defvar proof-splash-extensions -Prover specific extensions of splash screen. -These are evaluated and appended to @code{proof-splash-contents}, which see. -@end defvar - - - - -@node Goals buffer configuration -@section Goals buffer configuration - -The goals buffer configuration will allow configuration of Proof General -for proof by pointing or similar features. At the moment these settings -are disabled. - -@c TEXI DOCSTRING MAGIC: pbp-change-goal -@defvar pbp-change-goal -Command to change to the goal %s -@end defvar -@c TEXI DOCSTRING MAGIC: pbp-goal-command -@defvar pbp-goal-command -Command informing the prover that @samp{@code{pbp-button-action}} has been -requested on a goal. -@end defvar -@c TEXI DOCSTRING MAGIC: pbp-hyp-command -@defvar pbp-hyp-command -Command informing the prover that @samp{@code{pbp-button-action}} has been -requested on an assumption. -@end defvar -@c TEXI DOCSTRING MAGIC: pbp-error-regexp -@defvar pbp-error-regexp -Regexp indicating that the proof process has identified an error. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-result-start -@defvar proof-shell-result-start -Regexp matching start of an output from the prover after pbp commands. -In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-result-end -@defvar proof-shell-result-end -Regexp matching end of output from the prover after pbp commands. -In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. -@end defvar - - - -@node Global constants -@section Global constants - -The settings here are internal constants used by Proof General. -You don't need to configure these for your proof assistant -unless you want to modify or extend the defaults. - -@c TEXI DOCSTRING MAGIC: proof-general-name -@defvar proof-general-name -Proof General name used internally and in menu titles. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-proof-general-home-page -@defopt proof-proof-general-home-page -Web address for Proof General - -The default value is @code{"http://www.dcs.ed.ac.uk/home/proofgen"}. -@end defopt -@c TEXI DOCSTRING MAGIC: proof-universal-keys -@defvar proof-universal-keys -List of keybindings which for the script and response buffer. -Elements of the list are tuples (k . f) -where @samp{k} is a keybinding (vector) and @samp{f} the designated function. -@end defvar - - - -@node Handling multiple files -@section Handling multiple files -@cindex Multiple files - -Large proof developments are typically spread across multiple files. -Many provers support such developments by keeping track of dependencies -and automatically processing scripts. Proof General supports this -mechanism. The user's point of view is -explored further in @ref{Advanced Script Management}. Here, we -describe the more technical nitty gritty. This is what you need to know -when you customise another proof assistant to work with Proof General. - -The key idea is that we leave it to the specific proof assistant to -worry about managing multiple files. But whenever the proof assistant -processes or retracts a file it must clearly say so. - -@vindex proof-shell-eager-annotation-start -@vindex proof-shell-eager-annotation-end - -Proof General considers @var{output} delimited by the the two regualar -expressions @code{proof-shell-eager-annotation-start} and -@code{proof-shell-eager-annotation-end} as being important. It displays -the @var{output} in the Response buffer and analyses their contents further. -Among possibly other important messages characterised by these regular -expressions, the prover must tell the interface whenver it processes a -file and retracts across file boundaries. - - -@vtable @code -@item proof-included-files-list -records the file history. Whenever a new file is being processed, Proof -General adds it to the -front of the list. When the prover retracts across file boundaries, this -list is resynchronised. It contains files in canonical truename format. -@inforef{Truenames,,lispref}. You should not set this variable directly. -The generic Proof General will modify @code{proof-included-files-list} -itself. Instead, for a specific proof assistant you need to customise -@code{proof-shell-process-file}. @code{proof-shell-retract-files-regexp} -and @code{proof-shell-compute-new-files-list}. - -@item proof-shell-process-file -is either nil or a tuple of the form (@var{regexp}, @var{function}). If -@var{regexp} matches a substring of @var{str}, then the function -@var{function} is invoked with input @var{str}. It must return a script -file name (with complete path) the system is currently processing. In -practice, @var{function} is likely to inspect the match -data. @inforef{Match Data,,lispref}. Care has to be taken in case the -prover only reports on compiled versions of files it is processing. In -this case, @var{function} needs to reconstruct the corresponding script -file name. The new (true) file name is then automatically added to the -front of @code{proof-included-files-list} by the generic code. - -@item proof-shell-retract-files-regexp -is a regular expression. It indicates that the prover has retracted -across file boundaries. At this stage, Proof General's view of the -processed files is out of date and needs to be updated with the help of -the function @code{proof-shell-compute-new-files-list}. -@end vtable - -@ftable @code -@item proof-shell-compute-new-files-list -Takes as argument the current output of the prover. It needs to return -an up to date list of all processed files. Its output is then -automatically stored in -@code{proof-included-files-list} by the generic Proof General. In practice, this function is likely -to inspect the previous (global) variable -@code{proof-included-files-list} and the match data -@inforef{Match Data,,lispref} triggered by @code{proof-shell-retract-files-regexp}. -@end ftable - - - - -@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:: -* Proof General site configuration:: -* Global variables:: -* Proof script mode:: -* Proof shell mode:: -@end menu - - - -@node Spans -@section Spans -@cindex spans -@cindex extents -@cindex overlays - -@dfn{Spans} are an abstraction of XEmacs @dfn{extents} used to help -bridge the gulf between FSF Emacs and XEmacs. In FSF 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 PROOFGENERAL_@var{home} if set, -otherwise based on where the file proof-site 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. -@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 assitants to use with Proof General. -A list of symbols chosen from: @code{isa} @code{lego} @code{coq}. -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. -@var{note}: to change proof assistant, you must start a new Emacs session. - -The default value is @code{(isa lego coq)}. -@end defopt - -The file @file{proof-site.el} also defines a version variable. - -@c TEXI DOCSTRING MAGIC: proof-version -@defvar proof-version -Version string identifying Proof General release. -@end defvar - - - - -@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-goals-buffer -@defvar proof-goals-buffer -The goals buffer (also known as the pbp buffer). -@end defvar - -@c TEXI DOCSTRING MAGIC: proof-buffer-type -@defvar proof-buffer-type -Symbol indicating the type of this buffer: @code{script}, @code{shell}, or @code{pbp}. -@end defvar - -@c TEXI DOCSTRING MAGIC: proof-included-files-list -@defvar proof-included-files-list -List of files currently included in proof process. -Whenever a new file is being processed, it gets added. -When the prover retracts across file boundaries, this list -is resynchronised. It contains files in canonical truename format -@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. -@end defvar - -The @file{proof.el} also loads @file{proof-config.el} which declares the -proof assistant configuration variables for Proof General, -@xref{Adapting Proof General to New Provers} for details. - - -@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, keybindings, and user-level -functions. - -Proof scripts have two important variables for the locked and queue -regions. These variables are local to each script buffer (although we -only really need one queue span in total rather than one per buffer). - -@c TEXI DOCSTRING MAGIC: proof-locked-span -@defvar proof-locked-span -The locked span of the buffer. -Each script buffer has its own locked span, which may be detached -from the buffer. -Proof General allows buffers in other modes also to be locked; -these also have a non-nil value for this variable. -@end defvar - -@c TEXI DOCSTRING MAGIC: proof-queue-span -@defvar proof-queue-span -The queue span of the buffer. May be detached if inactive or empty. -@end defvar - -Various utility functions manipulate and examine the spans. An -important one is @code{proof-init-segmentation}. - -@c TEXI DOCSTRING MAGIC: proof-init-segmentation -@defun proof-init-segmentation -Initialise the queue and locked spans in a proof script buffer. -No harm if the spans have already been allocated. -@end defun - -For locking files loaded by a proof assistant, we use the next function. - -@c TEXI DOCSTRING MAGIC: proof-mark-buffer-atomic -@defun proof-mark-buffer-atomic buffer -Mark @var{buffer} as having been processed in 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 -(@xref{Handling multiple files} and @xref{Global variables}). - -@c TEXI DOCSTRING MAGIC: proof-register-possibly-new-processed-file -@defun proof-register-possibly-new-processed-file file -Register a possibly new @var{file} as having been processed by the prover. -@end defun - -Another important function activates scripting for the current script -buffer. This may involve switching from one scripting buffer to -another. - -@c TEXI DOCSTRING MAGIC: proof-activate-scripting -@defun proof-activate-scripting -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 current scripting buffer provided the current -scripting buffer has either no locked region or everything in it has -been processed. - -If we're changing scripting buffer and the old one is associated with -a file, add it to @code{proof-included-files-list}. - -When a new script buffer has scripting minor mode turned on, -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. - -Finally, this may be a good time to ask if the user wants to save some -buffers. -@end defun - -The next function is the main one used for parsing the proof script -buffer. - -@c TEXI DOCSTRING MAGIC: proof-segment-up-to -@defun proof-segment-up-to pos &optional next-command-end -Create a list of (type,int,string) tuples from end of locked region to @var{pos}. -Each tuple denotes the command and the position of its terminator, -type is one of @code{comment}, or @code{cmd}. @code{unclosed-comment} may be consed onto -the start if the segment finishes with an unclosed comment. -If optional @var{next-command-end} is non-nil, we contine past @var{pos} until -the next command end. -@end defun - -The function @code{proof-semis-to-vanillas} is used to convert -a parsed region of the script into a series of commands to -be sent to the proof assistant. - -@c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas -@defun proof-semis-to-vanillas semis &optional callback-fn -Convert a sequence of terminator positions to a set of vanilla extents. -Proof terminator positions @var{semis} has the form returned by -the function @code{proof-segment-up-to}. -@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, active 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 -@deffn Command 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 deffn - -@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 -@deffn Command 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 actually 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 deffn - -To clean up when scripting is stopped 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). - -Clever process handling is a tricky issue. Proof General attempts to -manage the process strictly, by mainting 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 @code{proof-start-queue} and proof-exec-loop. -@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. -Value for @code{kill-buffer-hook} in shell buffer. -Attempt to shut down the proof process nicely and -clears up all the locked regions and state variables. -@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, kill the shell buffer, -ensuring that script buffers are cleaned up neatly. -@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. The restart command should re-synchronize -Proof General with the proof assitant. -@end deffn - -@c -@c INPUT -@c - -Input to the proof shell via the queue region is dealt with 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. -@end defun - -@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, 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 - -A useful utility function for sending a single command to the process is -@code{proof-shell-invisible-command}. This should be used to implement -user-level functions rather than attempting to manipulate the proof -action list directly. - -@c -@c OUTPUT -@c - -Two main functions deal with output, @code{proof-shell-process-output} -and @code{proof-shell-process-urgent-message}. In effect we consider -the output to be two streams intermingled: the "urgent" messages which -have "eager" annotations, as well as the ordinary ruminations from the -prover. - -The idea is to conceal as much irrelevant information from the user as -possible; only the remaining output between prompts and after the last -urgent message will be a candidate for the goal or response buffer. -The variable @code{proof-shell-urgent-message-marker} tracks -the last urgent message seen. - -@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. -This function deals with errors, start of proofs, abortions of -proofs and completions of proofs. All other output from the proof -engine is simply reported to the user in the response buffer -by setting @code{proof-shell-delayed-output} to a cons cell of -(@var{insert} . @var{text}) where @var{text} is the text to be inserted. - -To extend this function, set -@code{proof-shell-process-output-system-specific}. - -This function - it can return one of 4 things: @code{error}, @code{interrupt}, -@code{loopback}, or nil. @code{loopback} means this was output from pbp, and -should be inserted into the script buffer and sent back to the proof -assistant. -@end defun - -@c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker -@defvar proof-shell-urgent-message-marker -Marker in proof shell buffer pointing to end of last urgent message. -@end defvar - -@c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message -@defun proof-shell-process-urgent-message message -Analyse urgent @var{message} for various cases. -Included file, retracted file, cleared response buffer, or -if none of these apply, display. -@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}. - -Process 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, then -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 - @var{prompt} @var{input} - @var{output-1} - @var{urgent-message} - @var{output-2} - @var{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. - -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. -@end defun - - - - - - - - - - - - - - - - - - - -@c -@c -@c CHAPTER: Obtaining and Installing Proof General -@c -@c -@node Credits and References -@chapter Credits and References - -@menu -* Credits:: -* References:: -@end menu - -@node Credits -@unnumberedsec Credits - -LEGO Proof General was written by Thomas Kleymann and Dilip Sequeira. - -Coq Proof General was written by Healfdene Goguen. - -Isabelle Proof General was written by David Aspinall. - -The generic base for Proof General was developed by all four of us. - -Thomas Kleymann provided the impetus to develop a generic Emacs -interface, following ideas used in Projet CROAP, and with the help of -Yves Bertot. David Aspinall provided the Proof General name and images. - -An early version of this manual was prepared by Dilip Sequeira. The -present version was written by David Aspinall and Thomas Kleymann. - -During the development of Proof General, the following people helped -by providing feedback, testing, or code: -Pascal Brisset, -Rod Burstall, -Paul Callaghan, -Martin Hofmann, -James McKinna, -and Markus Wenzel. Thanks to all of you! - - -@node References -@unnumberedsec References - -Script management as used in Proof General is described in the paper: - -@itemize @bullet -@item -Yves Bertot and Laurent Th@'ery. @i{A generic approach to building -user interfaces for theorem provers}. To appear in Journal of -Symbolic Computation. -@end itemize - -Proof General has the beginnings of support for proof by pointing, -as described in the document: - -@itemize @bullet -@item -Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. @i{Implementing -Proof by Pointing without a -Structure Editor}. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de -l'INRIA Sophia Antipolis RR-3286 -@end itemize - - -@c -@c -@c APPENDIX: Obtaining and Installing Proof General -@c -@c -@node Obtaining and Installing Proof General -@appendix Obtaining and Installing Proof General - -Proof General has its own -@uref{http://www.dcs.ed.ac.uk/home/proofgen,home page} hosted at -Edinburgh. Visit this page for the latest news! - -@menu -* Obtaining Proof General:: -* Installing Proof General from tarball:: -* Installing Proof General from RPM package:: -* Notes for syssies:: -@end menu - - -@node Obtaining Proof General -@section Obtaining Proof General - -You can obtain Proof General from the URL -@example -@uref{http://www.dcs.ed.ac.uk/home/proofgen/download.html}. -@end example - -The distribution is available in three forms -@itemize @bullet -@item A source tarball, @* -@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz} -@item A Linux RPM package (for any architecture), @* -@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm} -@item A developer's tarball, @* -@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz} -@end itemize - -Both the tarball and the RPM package include the generic elisp code, -code for LEGO, Coq, and Isabelle, installation instructions (reproduced -below) and this documentation. - -@c was Installing Proof General from @file{.tar.gz} -@node Installing Proof General from tarball -@section Installing Proof General from tarball - -Copy the distribution to some directory @var{mydir}. -Unpack it there. For example: -@example -# cd @var{mydir} -# gunzip ProofGeneral-@var{version}.tar.gz -# tar -xpf ProofGeneral-@var{version}.tar -@end example -If you downloaded the version called @var{latest}, you'll find it -unpacks to a numeric version number. - -Proof General will now be in some subdirectory of @var{mydir}. The name -of the subdirectory will depend on the version number of Proof General. -For example, it might be @file{ProofGeneral-2.0}. It's convenient to -link it to a fixed name: -@example -# ln -sf ProofGeneral-2.0 ProofGeneral -@end example -Now put this line in your @file{.emacs} file: -@lisp - (load-file "@var{mydir}/ProofGeneral/generic/proof-site.el") -@end lisp - -This command will load @file{proof-site} which sets the Emacs load path -for Proof General and add auto-loads and modes for the assistants below: - -@multitable @columnfractions .3 .3 .4 -@item @b{Prover} @tab @b{Extensions} @tab @b{Modes} -@item Coq @tab @file{.v} @tab @code{coq-mode} -@item LEGO @tab @file{.l} @tab @code{lego-mode} -@item Isabelle @tab @file{.thy},@file{.ML} @tab @code{isa-mode} -@end multitable -When you load a file with one of these extensions, the corresponding -Proof General mode will be entered. You can also invoke the mode -command directly. - -The default names for proof assistant binaries may work on your system. -If not, you will need to set the appropriate variables. The easiest way -to do this (and most other customization of Proof General) is via the -Customize mechanism, see the menu item: -@example - Proof-General -> Customize -> @var{Name of Assistant} -> Prog Name -@end example -The Proof-General menu is available from script buffers after -Proof General is loaded. To load it manually, type -@lisp - M-x load-library RET proof RET -@end lisp - -Notice that the customization mechanism is only available in Emacs 20.x -and XEmacs. If you cannot use customize, simply add a line like this: -@lisp - (setq isabelle-prog-name "/usr/bin/isabelle FOL") -@end lisp -to your @file{.emacs} file. - - -@node Installing Proof General from RPM package -@section Installing Proof General from RPM package - -To install an RPM package you need to be root. Then type -@example -# rpm -Uvh ProofGeneral-latest.noarch.rpm -@end example - -Now add the line: -@lisp - (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") -@end lisp -to your @file{.emacs} or the site-wide initialisation file -@file{site-start.el}. - - -@node Notes for syssies -@section Notes for syssies - -Here are some more notes for installing Proof General in more complex -ways. Only attempt things in this section if you really understand what -you're doing. - -@unnumberedsubsec Byte compilation - -Compilation of the Emacs lisp files improves efficiency but can -sometimes cause compatibility problems (especially if you use more than -one version of Emacs at the same time). - -You can compile Proof General by typing @code{make} in the directory -where you installed it. - - -@unnumberedsubsec Site-wide installation - -If you are installing Proof General site-wide, you can put the -components in the standard directories of the filesystem if you prefer, -providing the variables in @file{proof-site.el} are adjusted -accordingly, @xref{Proof General site configuration}. Make sure that -the @file{generic} and assistant-specific elisp files are kept in -subdirectories (@file{coq}, @file{isa}, @file{lego}) of -@code{proof-home-directory} so that the autoload directory calculations -are correct. - -To prevent every user needing to edit their own @file{.emacs} files, you -can put the @code{load-file} command to load @file{proof-site.el} into -@file{site-start.el} or similar. Consult the Emacs documention for more -details if you don't know where to find this file. - -@unnumberedsubsec Removing support for unwanted provers - -You cannot run more than one instance of Proof General at a time: so if -you're using Coq, visiting an @file{.ML} file will not load Isabelle -Proof General, and the buffer remains in fundamental mode. If there are -some assistants supported that you never want to use, you can adjust the -variable @code{proof-assistants} in @file{proof-site.el} to solve this -problem, @xref{Proof General site configuration}. - -@c Via the Customize mechanism, see the menu: -@c @example -@c Options -> Customize -> Emacs -> External -> Proof General -@c @end example -@c or, after loading Proof General, in a proof script buffer -@c @example -@c Proof-General -> Customize -@c @end example - - - -@c -@c -@c APPENDIX: Known bugs and workarounds -@c -@c -@node Known bugs and workarounds -@appendix Known bugs and workarounds - -We only mention a few important problems here. The list is not a -description of all bugs and may be out of date. @* -Please consult the file -@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}} -in the distribution for more detailed and up-to-date information. @* -If you discover a problem which isn't mentioned in @file{BUGS}, please -let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. - -@menu -* Bugs at the generic level:: -* Bugs specific to LEGO Proof General:: -* Bugs specific to Coq Proof General:: -* Bugs specific to Isabelle Proof General:: -@end menu - -@node Bugs at the generic level -@section Bugs at the generic level - -@unnumberedsubsec Undo in XEmacs - -When @code{proof-strict-read-only} is non-nil, ordinary undo in script -buffer can edit the "uneditable region" in XEmacs. This doesn't happen -in FSFmacs. Test case: Insert some nonsense text after the locked -region. Kill the line. Process to the next command. Press @kbd{C-x u}, -nonsense text appears in locked region. - -@strong{Workaround:} be careful with undo. - -@unnumberedsubsec Font locking and read-only in FSF Emacs - -When @code{proof-strict-read-only} is set and font lock is switched on, -spurious "Region read only" errors are given which break font lock. - -@strong{Workaround:} turn off @code{proof-strict-read-only}, font lock, -or for the best of all possible worlds, switch to XEmacs. - - -@unnumberedsubsec Pressing keyboard quit @kbd{C-g} - -Using @kbd{C-g} can leave script management in a mess. The code is not -properly protected from Emacs interrupts. - -@strong{Workaround:} Don't type @kbd{C-g} while script management is -processing. If you do, use @code{proof-restart-scripting} to restart -the system. - -@unnumberedsubsec One prover at a time -You can't use more than one proof assistant at a time in the same Emacs -session. Attempting to load Proof General for a second prover will -fail, leaving a buffer in fundamental mode instead of the Proof General -mode for proof scripts. - -@strong{Workaround:} stick to one prover per Emacs session, make sure -that the proof-assistants variables only enables Proof General for the -provers you need. - - -@node Bugs specific to LEGO Proof General -@section Bugs specific to LEGO Proof General - -@menu -* Retraction and Discharge:: -* Retraction and proving:: -@end menu - -@node Retraction and Discharge -@subsection Retraction and Discharge - -After a @code{Discharge}, retraction ought to only be possible back to -the first declaration/definition which is discharged. However, LEGO -Proof General does not know that @code{Discharge} has such a non-local -effect. See @ref{Granularity of atomic command sequences} for a proposal -on how to fix this bug. - -@strong{Workaround:} retract back to the first declaration/definition -which is discharged. - -@node Retraction and proving -@subsection Retraction and proving -@cindex Retraction - -Getting retracting right is tricky when working on proofs. - -@unnumberedsubsec Definitions in a proof state -A thorny issues are local -definitions in a proof state. LEGO cannot undo them explicitly. - -@strong{Workaround:} retract back to a command before a definition. - -@unnumberedsubsec Normalisation in proofs -Normalisation commands such as @samp{Dnf}, @samp{Hnf} @samp{Normal} -cannot be undone in a proof state by Proof General. - -@strong{Workaround:} retract back to the start of the proof. - -@unnumberedsubsec Not saving proofs. -After LEGO has issued a @samp{*** -QED ***} you may undo steps in the proof as long as you don't issue a -@samp{Save} command or start a new proof. The LEGO Proof General assumes -that all proofs are terminated with a proper @samp{Save} command. - -@strong{Workaround:} Always issue a @samp{Save} command after completing -a proof. If you forget one, you should retract to a point before the -offending proof development. - -@node Bugs specific to Coq Proof General -@section Bugs specific to Coq Proof General - -@unnumberedsubsec Hard-wired tactics - -The collection of tactics which Proof General is aware of is hard-wired. -Thus, user-defined tactics cannot be retracted. - -@strong{Workaround:} You may need to retract to the start of the proof. - -@unnumberedsubsec Sections - -The Coq Proof General does not know about Coq's section mechansim. - -@node Bugs specific to Isabelle Proof General -@section Bugs specific to Isabelle Proof General - -@unnumberedsubsec Indentation - -Isabelle Proof General doesn't support Proof General's indentation -code to indent proof scripts. In any case, Proof General's -indentation code is somewhat broken. - -@strong{Workaround:} indent your script by hand. - -@unnumberedsubsec Scripting lanugage limitations - -Since Isabelle uses ML as a top-level language for writing -proof-scripts, Proof General may have difficulty understanding scripts -which stray too far away from the standard functions, tactics, and -tacticals. You will usually notice when a function, or whatever, -doesn't get highlighted as you might expect. This probably has no -detrimental impact on the interface unless you use your own variants -of the @code{goal} or @code{qed} forms. - -@strong{Workaround:} Restrict yourself to standard proof script -functions, or customize some of the variables from @file{isa.el} and -@file{isa-syntax.el} appropriately. - -@unnumberedsubsec Interaction with theory database - -Isabelle Proof General has a fragment written in ML which defines a -modified interface to the theory database. In particular, some internal -state records which files have been retracted by the interface, although -no changes are made inside Isabelle itself. This means that -re-asserting a retracted file does not need to re-load it if it has not -changed. (It is a shame that the standard theory loader provides no -such "retraction" mechanism for unlinking loaded theories). - -This means that Proof General can get confused if you use the theory -loader primitives directly in the proof shell, and the state inside -Emacs may not agree with Isabelle. You have been warned! - -@node Plans and ideas -@appendix Plans and ideas - -This section contains some tentative plans and ideas for improving Proof -General. Please send us contributions to this wish list, or better -still, offers to implement something from it! - -@menu -* 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. - -In fact, Proof General already contains code for proof by pointing, for -a reference @xref{Credits and References}. However, it is slightly LEGO -specific and not robust enough. - -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 might be specific to a -particular logic in use, if we hope to generate a proof command -unambiguously for any particular click. However, it 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. - -@node Granularity of atomic command sequences -@section Granularity of atomic command sequences -@c @cindex Granularity of Atomic Sequences -@c @cindex Retraction -@c @cindex Goal -@cindex ACS (Atomic Command Sequence) - -This is a proposal by Thomas Kleymann for generalising the way Proof -General handles sequences of proof commands @pxref{Goal-save sequences}, -particularly to make retraction more flexible. - -The locked region of a script buffer contains the initial segment of -the proof script which has been processed successfully. It consists of -atomic sequences of commands (ACS). Retraction is supported to the -beginning of every ACS. By default, every command is an ACS. But the -granularity of atomicity can be adjusted for different proof assistants. -This is essential when arbitrary retraction is not supported. Usually, -after a theorem has been proved, one may only retract to the start of -the goal. One needs to mark the proof of the theorem as an ACS. - -@vtable @code -@item proof-atomic-sequents-list -is a list of instructions for setting up ACSs. Each instruction is a -list of the form @code{(@var{end} @var{start} &optional -@var{forget-command})}. @var{end} is a regular expression to recognise -the last command in an ACS. @var{start} is a function. Its input is the -last command of an ACS. Its output is a regular expression to recognise -the first command of the ACS. It is evaluated once and the output is -successively matched against previously processed commands until a match -occurs (or the beginning of the current buffer is reached). The region -determined by (@var{start},@var{end}) is locked as an ACS. Optionally, -the ACS is annotated with the actual command to retract the ACS. This is -computed by applying @var{forget-command} to the first and last command -of the ACS. -@end vtable - -@node Browser mode for script files and theories -@section Browser mode for script files and theories - -This is a proposal by David Aspinall for a browser window. - -A browser window should provide support for browsing script files and -theories. We should be able to inspect data in varying levels of -detail, perhaps using outlining mechanisms. For theories, it would be -nice to query the running proof assistant. This may require support -from the assistant in the form of output which has been specially -marked-up with an SGML like syntax, for example. - -A browser would be useful to: -@itemize @bullet -@item Provide impoverished proof assistants with a browser -@item Extend the uniform interface of Proof General to theory browsing -@item Interact closely with proof script-writing -@end itemize -The last point is the most important. We should be able to integrate a -search mechanism for proofs of similar theorems, theorems containing -particular constants, etc. - - - - -@node Function Index -@unnumbered Function and Command Index -@printindex fn - -@node Variable Index -@unnumbered Variable and User Option Index -@printindex vr - -@node Keystroke Index -@unnumbered Keystroke Index -@printindex ky - -@node Index -@unnumbered Index -@printindex cp - -@page -@contents -@bye - - diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 68b74660..4e7f74e7 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4,109 +4,643 @@ @c @c %**start of header @setfilename ProofGeneral.info -@settitle Proof General Version 2.0 +@settitle Proof General +@setchapternewpage odd @paragraphindent 0 +@iftex +@afourpaper +@end iftex @c %**end of header +@c +@c TODO, priority order +@c . finish incomplete sections +@c . polish mark-up +@c . add more index entries +@c . screenshots might be nice (one day) +@c + +@c NOTE ON THIS TEXINFO FILE: +@c I've tried keep full node lines *out* of this file because Emacs makes a +@c mess of updating them. Instead, rely on makeinfo and friends to do +@c the equivalent job. For this to work, we must follow each node +@c immediately with a section command, i.e.: +@c +@c @node node-name +@c <section-command> +@c +@c And each section with lower levels must have a menu command in +@c it. Menu updating with Emacs is a bit better than node updating, +@c but tends to delete the first section of the file in XEmacs! +@c (it's better in FSF Emacs at the time of writing). +@c + + +@set version 2.0 +@set xemacsversion 20.4 +@set fsfversion 20.2 +@set last-update November 1998 +@set rcsid $Id$ + @ifinfo @format -START-INFO-DIR-ENTRY -* ProofGeneral::Organize your proofs with Emacs! +START-INFO-DIR-ENTRY * ProofGeneral::Organize your proofs with Emacs! END-INFO-DIR-ENTRY @end format @end ifinfo -@setchapternewpage odd +@c +@c MACROS +@c +@c define one here for a command with a keybinding? +@c +@c I like the idea, but it's maybe against the texinfo +@c style to fix together a command and its keybinding. + + +@c merge functions and variables into concept index. +@c @syncodeindex fn cp +@c @syncodeindex vr cp +@c merge functions into variables index +@c @syncodeindex fn vr + +@finalout @titlepage -@sp 10 -@comment The title is printed in a large font. -@center @titlefont{Proof General Version 2.0} +@title Proof General +@subtitle Organise your proofs with Emacs! +@subtitle Proof General @value{version} +@subtitle @value{last-update} +@iftex +@image{ProofGeneral} +@end iftex +@author D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira +@page +@vskip 0pt plus 1filll +This manual and the program Proof General are +Copyright @copyright{} 1998 Proof General team, LFCS Edinburgh. + + +@c +@c COPYING NOTICE +@c +@ignore +Permission is granted to process this file through TeX and print the +results, provided the printed document carries copying permission notice +identical to this one except for the removal of this paragraph (this +paragraph not being relevant to the printed manual). +@end ignore + @sp 2 -@center Organise your proofs with Emacs! +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 -@center D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira -@sp 1 -@center LFCS Edinburgh +This manual documents Proof General, Version @value{version}, for use +with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion} +or later versions. -@c The following two commands start the copyright page. -@page -@vskip 0pt plus 1filll -Copyright @copyright{} 1997, 1998 Proof General team, LFCS Edinburgh +Version control stamp: @code{@value{rcsid}} @end titlepage +@page + + +@ifinfo +@node Top +@top Proof General + +This file documents version @value{version} of @b{Proof General}, a +generic Emacs interface for proof assistants. + +Proof General @value{version} has been tested with XEmacs +@value{xemacsversion} and FSF GNU Emacs @value{fsfversion}. It is +supplied ready customized for the proof assistants Coq, Lego, and +Isabelle. + +@menu +* Introducing Proof General:: +* Basic Script Management:: +* Advanced Script Management:: +* Support for other Packages:: +* Customizing Proof General:: +* LEGO Proof General:: +* Coq Proof General:: +* Isabelle Proof General:: +* Adapting Proof General to New Provers:: +* Internals of Proof General:: +* Credits and References:: +* Obtaining and Installing Proof General:: +* Known bugs and workarounds:: +* Plans and ideas:: +* Function Index:: +* Variable Index:: +* Keystroke Index:: +* Index:: +@end menu + +@detailmenu --- The Detailed Node Listing --- + +Introducing Proof General + +* Quick start guide:: +* Features of Proof General:: +* Supported proof assistants:: +* Prerequisites for this manual:: + +Basic Script Management + +* Proof scripts:: +* Script buffers:: +* Summary of Proof General buffers:: +* Script editing commands:: +* Script processing commands:: +* Toolbar commands:: +* Proof assistant commands:: +* Walkthrough example in LEGO:: + +Script buffers + +* Locked queue and editing regions:: +* Goal-save sequences:: +* Active scripting buffer:: + +Advanced Script Management + +* Switching between proof scripts:: +* View of processed files :: +* Retracting across files:: +* Asserting across files:: +* Working directly with the proof shell:: + +Support for other Packages + +* Support for function menus:: +* Support for outline mode:: +* Support for tags:: + +Customizing Proof General + +* Easy customization:: +* Display customization:: +* User options:: +* Changing faces:: +* Tweaking configuration settings:: + +LEGO Proof General + +* LEGO specific commands:: +* LEGO tags:: +* LEGO customizations:: + +Coq Proof General + +* Coq specific commands:: +* Coq customizations:: + +Isabelle Proof General + +* Theory files:: +* Isabelle specific commands:: +* Isabelle customizations:: + +Adapting Proof General to New Provers + +* Overview of adding a new prover:: +* Major modes used by Proof General:: +* Menus and user-level commands:: +* Proof script settings:: +* Proof shell settings:: +* Goals buffer configuration:: +* Global constants:: +* Handling multiple files:: + +Internals of Proof General + +* Spans:: +* Global variables:: +* Proof script mode:: +* Proof shell mode:: + +Credits and References + +* Credits:: +* References:: + +Obtaining and Installing Proof General + +* Obtaining Proof General:: +* Installing Proof General from tarball:: +* Installing Proof General from RPM package:: +* Notes for syssies:: + +Known bugs and workarounds + +* Bugs at the generic level:: +* Bugs specific to LEGO Proof General:: +* Bugs specific to Coq Proof General:: +* Bugs specific to Isabelle Proof General:: + +Bugs specific to LEGO Proof General + +* Retraction and Discharge:: +* Retraction and proving:: + +Plans and ideas + +* Granularity of atomic command sequences:: +* Browser mode for script files and theories:: +@end detailmenu +@end ifinfo + + + +@c +@c CHAPTER: Introduction +@c +@node Introducing Proof General +@chapter Introducing Proof General +@cindex proof assistant +@cindex Proof General + +@c would like the logo on the title page really but +@c it doesn't seem to work there for html. +@ifhtml +<IMG SRC="ProofGeneral.jpg" ALT="[ Proof General logo ]" > +@end ifhtml + +A @dfn{proof assistant} is a computerized helper for developing +mathematical proofs. + +@dfn{Proof General} is a generic Emacs interface for proof assistants, +developed at the LFCS in the University of Edinburgh. It works best +under XEmacs, but can also be used with FSF GNU Emacs. + +You do not have to be an Emacs militant to use Proof General! @* + +The interface is designed to be very easy to use. You develop your +proof script in-place rather than line-by-line and later reassembling +the pieces. Proof General keeps track of which proof steps have been +processed by the prover, and prevents you editing them accidently. You +can undo steps as usual. + +Our aim is provide a powerful and configurable Emacs mode which helps +user-interaction with interactive proof assistants. Please help us with +this aim! Configure Proof General for your proof assistant, by adding +features at the generic level wherever possible. See +@ref{Adapting Proof General to New Provers} +for more details, and send ideas, comments, patches, +and code to @code{proofgen@@dcs.ed.ac.uk}. + +@menu +* Quick start guide:: +* Features of Proof General:: +* Supported proof assistants:: +* Prerequisites for this manual:: +@end menu + + -@node Top, Introduction, (dir), (dir) -@comment node-name, next, previous, up -@b{Proof General} is a generic Emacs interface for proof assistants. It -works ideally under XEmacs, but can also be used with Emacs 19. -It is supplied ready-customised for these proof assistants: +@node Quick start guide +@section Quick start guide + +Proof General may have been installed for you already. If so, when you +visit a proof script file for your proof assistant, you'll find commands +to process the proof script are available from the toolbar, menus, and +keyboard. Type @kbd{C-h m} to get a list of keys for the current mode. + +The proof assistant is automatically started inside Emacs when you ask +for some of the proof script to be processed. To follow an example use +of Proof General on a LEGO proof, see @pxref{Walkthrough example in LEGO}. + +If Proof General has not already been installed, you should insert the +line: +@lisp + (load "@var{proof-general-home}/generic/proof-site.el") +@end lisp +into your @file{~/.emacs} file, where @var{proof-general-home} is the +top-level directory that was created when Proof General was unpacked. + +For more details on obtaining and installing Proof General, +see @pxref{Obtaining and Installing Proof General}. + + +@node Features of Proof General +@section Features of Proof General +@cindex Features +@cindex Why use Proof General? + +Why would you want to use Proof General? + +Here is an outline of its main features. + +@itemize @bullet +@item @i{Simplified communication}@* +The proof assistant's shell is normally hidden from the user. +Communication takes place via two or three buffers. The @dfn{script +buffer} holds input, the commands to construct a proof. The @dfn{goals +buffer} displays the current list of subgoals to be solved. The +@dfn{response buffer} displays other output from the proof assistants. +This means that the user only sees the output from the most recent proof +step, rather than a screen full of output from the proof assistant. +@c Optionally, the goals buffer and script buffer can be identified. + +For more details, see @xref{Basic Script Management}, +@xref{Script buffers} and @xref{Summary of Proof General buffers}. + +@item @i{Script management}@* +Proof General colours proof script regions blue when they have already +been processed by the prover, and colours regions red when the prover is +currently processing them. The appearance of Emacs buffers always +matches the proof assistant's state. Coloured parts of the buffer cannot +be edited. Proof General has functions for @emph{asserting} or +@emph{retracting} parts of a proof script, which alters the coloured +regions. + +For more details, see @xref{Basic Script Management}, +@xref{Script processing commands}. +and @pxref{Advanced Script Management}. +@item @i{Script editing mode}@* +Proof General provides useful facilities for editing proof scripts, +including syntax hilighting and a menu to jump to particular goals, +definitions, or declarations. +Special editing functions send lines of proof script to the proof +assistant, or undo previous proof steps. + +For more details, see @pxref{Script editing commands} +and @pxref{Script processing commands}. +@item @i{Toolbar and menus}@* +A script buffer has a toolbar with navigation buttons for processing +parts of the proof script. A menu provides further functions for +operations in the proof assistant, as well as customization of Proof +General. + +For more details, see @pxref{Toolbar commands}, @pxref{Proof assistant +commands}, and @pxref{Customizing Proof General}. + +@c not yet +@c @item @i{Proof by pointing} +@end itemize + + +@node Supported proof assistants +@section Supported proof assistants + +Proof General comes ready-customised for these proof assistants: @itemize @bullet @item @b{LEGO Proof General} for LEGO Version 1.3.1@* -by Thomas Kleymann and Dilip Sequeira +@c written by Thomas Kleymann and Dilip Sequeira. +@c +All features of Proof General are supported. +See @pxref{LEGO Proof General} for more details. + @item @b{Coq Proof General} for Coq Version 6.2@* -by Healfdene Goguen +@c written by Healfdene Goguen. +@c +All of features of Proof General are supported except multiple files. +See @pxref{Coq Proof General} for more details. + @item @b{Isabelle Proof General} for Isabelle 98-1@* -by David Aspinall +@c written by David Aspinall. +All features of Proof General are supported, except for an external tags +program. Isabelle Proof General handles theory files as well as ML +(proof script files), and has an extensive theory file editing mode +taken from @uref{http://www.dcs.ed.ac.uk/home/da/Isamode,Isamode}. +See @pxref{Isabelle Proof General} for more details. +@end itemize +Proof General is designed to be generic, so you can adapt it to other +proof assistants if you know a little bit of Emacs Lisp. +@itemize @bullet +@item +@b{Your Proof General} for your favourite proof assistant@* +See @pxref{Adapting Proof General to New Provers} +for more details of how to make Proof General work +with another proof assistant. @end itemize -Proof General itself was written by the above with help from Yves Bertot -and using ideas from Projet CROAP. -Proof General is suitable for use by pacifists and Emacs lovers alike. +@node Prerequisites for this manual +@section Prerequisites for this manual + +This manual assumes that you understand a little about using Emacs, for +example, switching between buffers using @kbd{C-x b} and understanding +that key sequences like @kbd{C-x b} mean "control-X followed by b". + +The manual also assumes you have a basic understanding of your proof +assistant and the language and files it uses for proof scripts. But +even without this, Proof General is not useless: you can use the +interface to @emph{replay} proof scripts for any proof assistant without +knowing how to start it up or issue commands, etc. This is the beauty +of a common interface mechanism. + +To get more from Proof General and adapt it to your liking, it helps to +know a little bit about how Emacs lisp packages can be customized via +the Customization mechanism. It's really easy to use. See @xref{Easy +customization} and @inforef{Easy customization, ,(xemacs)} for details. + +To get the absolute most from Proof General, to improve it or to adapt +it for new provers, you'll need to know a little bit of Emacs lisp. +Emacs is self-documenting, so you can begin from @kbd{C-h} and find out +everything! Here are some useful commands: + +@table @asis +@item @kbd{C-h i} +@code{info} +@item @kbd{C-h m} +@code{describe-mode} +@item @kbd{C-h b} +@code{describe-bindings} +@item @kbd{C-h f} +@code{describe-function} +@item @kbd{C-h v} +@code{describe-variable} +@end table + +Most of this manual covers the user-level view and customization of +Proof General. Towards the end we consider adapting Proof General to +new proof assistants, and document some of the internals of Proof +General. The manual concludes with some credits and references. +See the table of contents for details. + -The code is designed to be generic, so you can adapt Proof General to -other proof assistants if you know a little bit of Emacs Lisp. Our aim -is provide a powerful and configurable Emacs mode which helps -user-interaction with interactive proof assistants. -Please help us with this aim! Configure Proof General for your proof -assistant, by adding features at the generic level wherever possible. -Send ideas, comments, patches, code to @email{proofgen@@dcs.ed.ac.uk}. -Please feel free to download Proof General to customize it for another -system, and tell us how you get on. + + + + +@c +@c CHAPTER: Basic Script Management +@c +@node Basic Script Management +@chapter Basic Script Management + +This chapter is an introduction to using the script management +facilities of Proof General. We begin with a quick walkthrough example, +then describe the concepts and functions in more detail. @menu -* Introduction:: -* Commands:: -* Multiple Files:: -* An Active Terminator:: -* Proof by Pointing:: -* Walkthrough:: -* LEGO mode:: -* Coq mode:: -* Known Problems:: -* Internals:: -* Variable Index:: -* Function Index:: -* Concept Index:: +* Walkthrough example in LEGO:: +* Proof scripts:: +* Script buffers:: +* Summary of Proof General buffers:: +* Script editing commands:: +* Script processing commands:: +* Toolbar commands:: +* Proof assistant commands:: @end menu +@node Walkthrough example in LEGO +@section Walkthrough example in LEGO + +Here's a short example in LEGO to see how script management is used. +The file you are asked to type below is included in the distribution as +@file{lego/example.l}. If you're not using LEGO, substitute some lines +from a simple proof for your proof assistant, or consult the example +file provided with Proof General. -@node Introduction, Commands, Top, Top -@comment node-name, next, previous, up -@unnumberedsec Introduction +First, find a new file by doing @kbd{C-x C-f} and typing as the filename +@file{walkthrough.l}. This should load LEGO Proof General and the +toolbar and Proof General menus will appear. This walkthrough is +keyboard based, although you could easily use the toolbar and menu +functions instead. -A @strong{Script Buffer} is the primary buffer for developing proof -scripts. Its major mode is @emph{proof mode}. A script buffer is divided -into three regions: + + +Now turn on active terminator minor mode by typing @kbd{C-c ;} and +enter: +@lisp +Module Walkthrough Import lib_logic; +@end lisp +The command should be lit in pink (or inverse video if you don't have a +colour display). As LEGO imports each module, a line will appear in the +minibuffer showing the creation of context marks. Eventually the command +should turn blue, indicating that LEGO has successfully processed +it. Then type (on a separate line if you like): +@lisp +Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A); +@end lisp +The goal should be echoed in the goals buffer. +@lisp +Intros; +@end lisp +Whoops! @kbd{C-c C-u} to pretend that didn't happen. +@lisp +intros; andI; +@end lisp +A proof summary will appear in the goals buffer. +@c We could solve the goal by pointing now, but we'll stay with the keyboard. +@lisp +Refine H; intros; Immed; Refine H; intros; Immed; +@end lisp +finishes the Goal. +@lisp +Save bland_commutes; +@end lisp + +Moving the mouse pointer over the locked region now reveals that the +entire proof has been aggregated into a single segment. Suppose we +decide to call the goal something more sensible. Moving the cursor up +into the locked region, somewhere between `Goal' and `Save', we enter +@kbd{C-c u}. The segment is transferred back into the editing +region. Now we correct the goal name, move the cursor to the end of the +buffer, and type @kbd{C-c RET}. Proof mode queues the commands for +processing and executes them. + + + + +@node Proof scripts +@section Proof scripts +@cindex proof script +@cindex scripting + +A @dfn{proof script} is a sequence of commands which construct a proof +in a proof assistant. Proof General is designed to work with text-based +@i{interactive} proof assistants, where the mode of working is usually a +dialogue between the human and the proof assistant. + +Primitive interfaces for proof assistants simply present a shell-like +view of this dialogue: the human repeatedly types commands to the shell +until the proof is completed. The system responds at each step, perhaps +with a new list of subgoals to be solved, or perhaps with a failure +report. Proof General manages the dialogue to only show the human the +information which is relevant at each step. + +@c Many proof assistants can also process proof scripts held in files + +Often we want to keep a record of the proof commands used to prove a +theorem, to build up a library of proved results. An easy way to store +a proof is to keep a text file which contains a proof script; the proof +assitant usually provides facility to read a proof script from a file +instead of the terminal. Using the file, we can @dfn{replay} the proof +script to prove the theorem again. +@c Re-playing a proof script is a non-interactive procedure, +@c since it is supposed to succeed. + +Using only a primitive shell interface, it can be tedious to construct +proof scripts with cut-and-paste. Proof General helps out by issuing +commands directly from a proof script file, while it is being written +and edited. Proof General can also be used conveniently to replay a +proof step-by-step, to see the progress at each stage. +@c developing them in proof script files. + +@dfn{Scripting} is the process of building up a proof script file or +replaying a proof. When scripting, Proof General sends proof commands +to the proof assistant one at a time, and prevents you from editing +commands which have been successfully completed by the proof assistant. +Regions of the proof script are analysed based on syntax and the +behaviour of the proof assistant after each proof command. + + +@node Script buffers +@section Script buffers +@cindex script buffer +@cindex proof script mode + +A @dfn{script buffer} is a buffer displaying a proof script. Its Emacs +mode is particular to the proof assistant you are using (but it inherits +from @dfn{proof-script mode}). + + +A script buffer is divided into three regions: @emph{locked}, +@emph{queue} and @emph{editing}. The proof commands +in the script buffer can include a number of +@emph{Goal-save sequences}. + +@menu +* Locked queue and editing regions:: +* Goal-save sequences:: +* Active scripting buffer:: +@end menu + + +@node Locked queue and editing regions +@subsection Locked, queue, and editing regions +@cindex Locked region +@cindex Queue region +@cindex Editing region +@cindex blue text +@cindex pink text + + +A script buffer is divided into three regions: @itemize @bullet -@item The @emph{Locked} region appears in blue (underlined on monochrome +@item The @emph{locked} region appears in blue (underlined on monochrome displays) and contains commands which have been sent to the proof process and verified. The commands in the locked region cannot be edited. -@item The @emph{Queue} region appears in pink (inverse video) and contains +@item The @emph{queue} region appears in pink (inverse video) and contains commands waiting to be sent to the proof process. Like those in the locked region, these commands can't be edited. -@item The @emph{Editing} region contains the commands the user is working +@item The @emph{editing} region contains the commands the user is working on, and can be edited as normal Emacs text. @end itemize @@ -115,22 +649,8 @@ the locked region is always at the start of the buffer, and the editing region always at the end. The queue region only exists if there is input waiting to be sent to the proof process. -Proof mode has two operations which transfer commands between these -regions: assertion and retraction. These cause commands to be sent to -the proof process. The @emph{Process Buffer} records the complete -communication between the prover and the Script Buffers. Error messages -and other important messages are highlighted in the Process Buffer. The -current proof obligations (if any) are always visible in the @emph{Goals -Buffer}. - -Proof General is generous. It is not a perfect interface and users may -occasionaly want to freely interact with the prover without being -watched over by the Proof General. Users may interact @emph{directly} -with the prover by entering text in the Process Buffer instead of -invoking commands in a Script Buffer. Proof mode supports a variety of -means to interact with the prover. Try these first! - - +Proof mode has two fundamental operations which transfer commands +between these regions: @emph{assertion} and @emph{retraction}. @cindex Assertion @strong{Assertion} causes commands from the editing region to be @@ -138,287 +658,1107 @@ transferred to the queue region and sent one by one to the proof process. If the command is accepted, it is transferred to the locked region, but if an error occurs it is signalled to the user, and the offending command is transferred back to the editing region together -with any remaining commands in the queue. +with any remaining commands in the queue. + +Assertion corresponds to processing proof commands, and makes the locked +region grow. @cindex Retraction -@strong{Retraction} causes -commands to be transferred from the locked region to the editing region -(again via the queue region) and the appropriate 'undo' commands to be -sent to the proof process. - -As commands are transferred to the locked region, they are aggregated -into segments which constitute the smallest units which can be -undone. Typically a segment consists of a declaration or definition, or -all the text from a `goal' command to the corresponding `save' command, -or the individual commands in the proof of an unfinished goal. As the -mouse moves over the the region, the segment containing the pointer will -be highlighted. - -Commands in the editing region can be freely edited while -commands in the queue are transferred to the proof process. However, -assertion and retraction commands can only be issued when the queue is -empty. - -@node Commands, Multiple Files, Introduction, Top -@unnumberedsec Proof Mode Commands +@strong{Retraction} causes commands to be transferred from the locked +region to the editing region (again via the queue region) and the +appropriate 'undo' commands to be sent to the proof process. + +Retraction corresponds to undoing commands, and makes the locked region +shrink. @xref{Script processing commands} details the commands +available for doing assertion and retraction. + + +@node Goal-save sequences +@subsection Goal-save sequences +@cindex goal +@cindex save +@cindex goal-save sequences + +A proof script contains a sequence of commands used to prove one or more +theorems. + +As commands in a proof script are transferred to the locked region, they +are aggregated into segments which constitute the smallest units which +can be undone. Typically a segment consists of a declaration or +definition, or all the text from a @dfn{goal} command to the +corresponding @dfn{save} command, or the individual commands in the +proof of an unfinished goal. As the mouse moves over the the region, +the segment containing the pointer will be highlighted. + +Proof General therefore assumes that the proof script has a series of +proofs which look something like this: +@lisp + goal @var{mythm} is @var{G} + @dots{} + save theorem @var{mythm} +@end lisp +interspersed with comments, definitions, and the like. Of course, the +exact syntax and terminology will depend on the proof assistant you use. + +The name @var{mythm} can appear in the menu for the proof script to help +quickly find a proof (@pxref{Support for function menus}). + +@c Proof General recognizes the goal-save sequences in proof scripts. +@c once a goal-save region has been fully processed by the proof assistant, +@c it is treated as atomic when undoing proof steps. This reflects the +@c fact that most proof assistants discard the history of a proof once a it +@c is completed or once a new proof is begun. + + +@node Active scripting buffer +@subsection Active scripting buffer +@cindex active scripting buffer + +You can edit as many script buffers as you want simultaneously, but only +one buffer at a time can be used to process a proof script +incrementally: this is the @dfn{active scripting buffer}. + +The active scripting buffer has a special indicator: the word +@code{Scripting} appears in its mode line. + +Proof General will give an error message: @code{Cannot have more than +one active scripting buffer!} if you attempt to use the script +processing commands in a new script buffer when there is already an +active scripting buffer which is only partly completed. If you get this +error message, you must choose either to assert the remainder of the +active buffer, or to retract what has been proved so far, before you can +start scripting in another buffer. + +@xref{Switching between proof scripts} for more explanation of this. + +@c A completed script buffer is one which is completely blue: the locked +@c region covers the whole buffer, indicating that all the commands been +@c successfully processed by the prover. + + +@node Summary of Proof General buffers +@section Summary of Proof General buffers +@cindex shell buffer +@cindex goals buffer +@cindex response buffer +@cindex proof by pointing + +Proof General manages several kinds of buffers in Emacs. Here is a +summary of the different kinds of buffers you will use when developing +proofs. -@table @kbd +@itemize @bullet +@item The @dfn{proof shell buffer} is an Emacs shell buffer + used to run your proof assistant. Usually it is hidden from view + (but see @xref{Working directly with the proof shell}). + Communication with the proof shell takes place via two or three + intermediate buffers. +@item A @dfn{script buffer}, as we have explained, is a buffer for editing a + proof script. The @dfn{active scripting buffer} is the script buffer + which is currently being used to send commands to the proof shell. +@item The @dfn{goals buffer} displays the list of subgoals to be + solved for a proof in progress. During a proof it is usually + displayed together with the script buffer. +@c FIXME: change when pbp is added back! + The goals buffer has facility for @dfn{proof-by-pointing}, although + this is disabled in Proof General @value{version}. +@item The @dfn{response buffer} displays other output from the proof + assistant, for example error messages or informative messages. + The response buffer is displayed whenever Proof General puts + a new message in it. +@end itemize -@item C-c C-b -assert the commands in the buffer. +Normally Proof General will automatically reveal and hide the goals and +response buffers as necessary during scripting. However there are ways +to customize the way the buffers are displayed, @pxref{Display +customization}. -@item C-c return -assert the commands in the editing region up to and -including the one containing the point. +The menu @code{Proof General -> Buffers} provides a convenient way to +display or switch to one of the four buffers: active scripting, goals, +response, or shell. -@item C-c u -retract the segments in the locked region back to and -including the one containing the point. If point is outside the *Locked* -region, the last segment is undone. +@c When +@c Proof General sees an error in the shell buffer, it will highlight the +@c error and display the buffer automatically. -@item C-c C-u -retract the last segment in the locked region, and kill the text in it. -@footnote{Be careful with this, as it may delete more than you anticipate. -However, you can always recover the killed text using Emacs Undo.} -@item C-c ' -move the point to the end of the locked region. If you are in a script -buffer other than the active scripting buffer, this will also transfer -you to the active one. +@c This facility was not added: +@c +@c Optionally, the goals buffer and script buffer can be identified +@c @pxref{Identify goals and response}. The disadvantage of this is that +@c the goals display can be replaced by other messages, so you must ask for +@c it to be refreshed. The advantage is that it is simpler to deal with +@c fewer Emacs buffers. -@item C-c C-e -move the point to the next terminator -@item C-c C-p -display the proof state in the goals buffer -@item C-c c -display the context in the process buffer +@node Script editing commands +@section Script editing commands -@item C-c h -print proof-system specific help text in the process buffer +Proof General provides a few functions for editing proof scripts. +Specific proof assistant code may elaborate on these basics. -@item C-c C-c -interrupt the process. This may leave script management or the -proof process (or both) in an inconsistent state. +@findex indent-for-tab-command +@vindex proof-script-indent +Indentation is controlled by the user option @code{proof-script-indent} +@pxref{User options}. When indentation is enabled, Proof General +will indent lines of proof script with the usual Emacs functions, +particularly @kbd{TAB}, @code{indent-for-tab-command}. -@item C-c C-z -move the end of the locked region backwards to the end of the segment -containing the point. @footnote{Don't try this one at home, kids.} +@c FIXME: remove when indentation is fixed. +Unfortunately, indentation in Proof General @value{version} is +somewhat slow and buggy. Therefore with large proof scripts, +we recommend @code{proof-script-index} is turned off. + +Here are the commands for moving around in a proof script, +with their default key bindings: +@kindex C-c C-e +@kindex C-c C-a +@kindex C-c ' +@table @kbd +@item C-c C-e +@code{proof-find-next-terminator} +@item C-c C-a +@code{proof-goto-command-start}. +@item C-c ' +@code{proof-goto-end-of-locked-interactive} +@end table + +@c TEXI DOCSTRING MAGIC: proof-find-next-terminator +@deffn Command proof-find-next-terminator +Set point after next @samp{@code{proof-terminal-char}}. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-goto-command-start +@deffn Command proof-goto-command-start +Move point to start of current command. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-goto-end-of-locked-interactive +@deffn Command proof-goto-end-of-locked-interactive +Switch to @code{proof-script-buffer} and jump to the end of the locked region. +Must be an active scripting buffer. +@end deffn + + +@node Script processing commands +@section Script processing commands +@kindex C-c C-n +@kindex C-c RET +@kindex C-c u +@kindex C-c C-u + +Here are the commands for asserting and retracting portions of the proof +script, together with their default key bindings. Note that assertion +and retraction commands can only be issued when the queue is empty. You +will get an error message @code{Proof Process Busy!} if you try to +assert an retract when the queue is being processed.@footnote{In fact, +this is an unnecessary restriction imposed by the original design of +Proof General. There is nothing to stop future versions of Proof +General allowing the queue region to be extended or shrunk, whilst the +prover is processing it.} + +@table @kbd +@item C-c C-n +@code{proof-assert-next-command} +@item C-c C-u +@code{proof-undo-last-successful-command} +@item C-c RET +@code{proof-assert-until-point} +@item C-c u +@code{proof-retract-until-point} +@item C-c b +@code{proof-process-buffer} +@item C-c @var{terminator-character} +@code{proof-active-terminator-minor-mode} +@end table -@item C-c C-t -Send the command at the point to the subprocess, not -recording it in the locked region. @footnote{This is supplied in order -to enable the user to test the types and values of expressions. There's -some checking that the command won't change the proof state, but it -isn't foolproof.} +The last command, @code{proof-active-terminator-minor-mode}, is +triggered using the character which terminates proof commands for your +proof assistant's script language. For LEGO and Isabelle, use @kbd{C-c +;}, for Coq, use @kbd{C-c .}. This not really a script processing +command. Instead, it causes subsequent key presses of @kbd{;} or +@kbd{.} to automatically send the line you've typed to the proof +assistant. + +Rather than use any other way of reading a proof script, a good reason +to use @kbd{C-c C-b} (@code{proof-process-buffer}) is that with a faulty +proof script (e.g., a script you are adapting to prove a different +theorem), Proof General will stop exactly where the proof script fails, +showing you the error message and the last processed command. So you +can easily continue development from exactly the right place in the +script. + + + +@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 + +@c TEXI DOCSTRING MAGIC: proof-undo-last-successful-command +@deffn Command proof-undo-last-successful-command &optional no-delete +Undo last successful command at end of locked region. +Unless optional @var{no-delete} is set, the text is also deleted from +the proof script. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-assert-until-point +@deffn Command 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 deffn + +@c TEXI DOCSTRING MAGIC: proof-retract-until-point +@deffn Command 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 actually 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 deffn + +@c TEXI DOCSTRING MAGIC: proof-process-buffer +@deffn Command proof-process-buffer +Process the current buffer and set point at the end of the buffer. +@end deffn + + +@c TEXI DOCSTRING MAGIC: proof-active-terminator-minor-mode +@deffn Command proof-active-terminator-minor-mode &optional arg +Toggle Proof General's active terminator minor mode. +With arg, turn on the Active Terminator minor mode if and only if arg +is positive. + +If active terminator mode is enabled, a terminator will process the +current command. +@end deffn + + +@node Toolbar commands +@section Toolbar commands + +The toolbar provides a selection of functions for asserting +and retracting portions of the script, and inserting +"goal" and "save" type commands. + +These functions are available only from the toolbar, menu Proof General +-> Scripting, or via @kbd{M-x}. There are no keybindings for them by +default. + + +@c TEXI DOCSTRING MAGIC: proof-toolbar-goal +@deffn Command proof-toolbar-goal +Insert a goal command into the script buffer, issue it to prover. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-toolbar-retract +@deffn Command proof-toolbar-retract +Retract entire buffer. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-toolbar-undo +@deffn Command proof-toolbar-undo +Undo last successful in locked region, without deleting it. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-toolbar-next +@deffn Command proof-toolbar-next +Assert next command in proof to proof process. +Move point if the end of the locked position is invisible. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-toolbar-use +@deffn Command proof-toolbar-use +Process the whole buffer +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-toolbar-restart +@deffn Command proof-toolbar-restart +Restart scripting via @code{proof-shell-restart}. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-toolbar-qed +@deffn Command proof-toolbar-qed +Insert a save theorem command into the script buffer, issue it. +@end deffn + + + +@node Proof assistant commands +@section Proof assistant commands +@kindex C-c C-p +@kindex C-c c +@kindex C-c h + +There are several commands for interacting with the proof assistant away +from a proof script. Here are the keybindings and functions. +@table @kbd +@item C-c C-p +@code{proof-prf} +@item C-c c +@code{proof-ctxt} +@item C-c h +@code{proof-help} +@item C-c C-c +@code{proof-interrupt-process} +@item C-c t +@code{proof-try-command} @item C-c C-v -Request a command from the minibuffer and send it to -the subprocess. Currently no checking whatsoever is done on the command. +@code{proof-execute-minibuffer-cmd} @end table -The command @code{proof-restart-script} can be used to completely -restart script management. +@c TEXI DOCSTRING MAGIC: proof-prf +@deffn Command proof-prf +List proof state. +@end deffn +@c TEXI DOCSTRING MAGIC: proof-ctxt +@deffn Command proof-ctxt +List context. +@end deffn -@node Multiple Files, An Active Terminator, Commands, Top -@unnumberedsec Multiple Files +@c TEXI DOCSTRING MAGIC: proof-help +@deffn Command proof-help +Print help message giving syntax. +@end deffn -Proof mode has a rudimentary facility for operating with multiple files -in a proof development. This is currently only supported for LEGO. If -the user invokes script management in a different buffer from the one in -which it is running, one of two prompts will appear: +@c TEXI DOCSTRING MAGIC: proof-interrupt-process +@deffn Command proof-interrupt-process +Interrupt the proof assistant. Warning! This may confuse Proof General. +@end deffn -@itemize @bullet -@item ``Steal script management?'' -if Emacs doesn't think the file is already part of the proof development -@item ``Reprocess this file?'' -if Emacs thinks the file is already included in the proof process. If -the user confirms, Emacs will cause the proof process to forget the -contents of the file, so that it is processed afresh. -@end itemize +@c TEXI DOCSTRING MAGIC: proof-try-command +@deffn Command proof-try-command &optional unclosed-comment-fun +Process the command at point, but don't add it to the locked region. -Currently this facility requires each script buffer to have a -corresponding file. +Supplied to let the user to test the types and values of +expressions. Checks via the function @code{proof-state-preserving-p} that the +command won't change the proof state, but this isn't guaranteed to be +foolproof and may cause Proof General to lose sync with the prover. -When working with script management in multiple buffers, it is easy -to lose track of which buffer is the current script buffer. As a mnemonic -aid, the word @samp{Scripting} appears in the minor mode list of the -active scripting buffer. +Default action if inside a comment is just to go until the start of +the comment. If you want something different, put it inside +@var{unclosed-comment-fun}. +@end deffn -Caveats: -@itemize @minus -@item Note that if processing a buffer causes other files to be loaded -into the LEGO process, those files will be imported from disk rather -than from any Emacs buffer in which it is being edited, i.e.@: if your -file is going to be included indirectly, save it. +@c TEXI DOCSTRING MAGIC: proof-execute-minibuffer-cmd +@deffn Command proof-execute-minibuffer-cmd +Prompt for a command in the minibuffer and send it to proof assistant. +The command isn't added to the locked region. -@item However much you move around the file system in Emacs, the -LEGOPATH will be the LEGOPATH you started with. No concept of -"current directory" is currently supported. -@end itemize +Warning! No checking whatsoever is done on the command, so this is +even more dangerous than @code{proof-try-command}. +@end deffn + +As if the last few commands weren't dangerous enough, there's also a +command which explicitly adjusts the end of the locked region, to be +used in extreme circumstances only. @pxref{Working directly with the +proof shell}. + +@c Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working +@c directly with the proof shell} + +There are a few commands for stopping, starting, and restarting the +proof assistant process which have menu entries but no key bindings. +As with any Emacs command, you can invoke these with @kbd{M-x}. + +@c TEXI DOCSTRING MAGIC: proof-shell-start +@deffn Command proof-shell-start +Initialise a shell-like buffer for a proof assistant. + +Also generates goal and response buffers. +Does nothing if proof assistant is already running. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-shell-restart +@deffn Command proof-shell-restart +Clear script buffers and send @code{proof-shell-restart-cmd}. +All locked regions are cleared and the active scripting buffer +deactivated. The restart command should re-synchronize +Proof General with the proof assitant. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-shell-exit +@deffn Command proof-shell-exit +Query the user and exit the proof process. -@node An Active Terminator, Proof by Pointing, Multiple Files, Top -@unnumberedsec An Active Terminator +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 -Proof mode has a minor mode which causes the terminator to become -active. When this mode is active, pressing the terminator key (@kbd{;} -for LEGO, @kbd{.} for Coq) outside a comment or quote will cause the -character to be entered into the buffer, and all the commands in the -editing region up to the point to be asserted. -This mode can be toggled with the command -`proof-active-terminator-minor-mode' (@kbd{C-c ;} or @kbd{C-c .}) -@node Proof by Pointing, Walkthrough, An Active Terminator, Top -@unnumberedsec Proof by Pointing -@emph{This mode is currently very unreliable, and we do not guarantee -that it will work as discussed in this document.} -Proof by pointing is a facility whereby proof commands can be generated -by using the mouse to select terms. When proving a goal, a summary of -the current proof state will appear in the goals buffer. By moving -the mouse over the buffer, the structure of the goal and hypothesis -terms will be shown by highlighting. -If a selection is made using the second (usually the middle) mouse -button, Emacs will generate the appropriate commands, insert them in the -script buffer, and send them to the proof process. These commands are -aggregated in the locked region as a single segment, so that a -mouse-generated command sequence can be retracted with a single -retraction command. +@c +@c CHAPTER: Advanced Script Management +@c +@node Advanced Script Management +@chapter Advanced Script Management +@cindex Multiple Files + +What we really mean by @emph{advanced} is that Proof General supports +large proof developments. These are typically spread across various +files which depend on each other in some way. Proof General knows enough +about the dependencies to allow script management across multiple files. -Further Information about proof by pointing may be found in the paper -@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent -Thery, to appear in @cite{Information and Computation}, from which -the following example is taken. @menu -* Proof by Pointing Example:: An example using proof by pointing +* Switching between proof scripts:: +* View of processed files :: +* Retracting across files:: +* Asserting across files:: +* Working directly with the proof shell:: @end menu -@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing +@node Switching between proof scripts +@section Switching between proof scripts +@cindex Switching between proof scripts + +Basic modularity in large proof developments can be achieved by +splitting proof scripts across various files. Let's assume that you are +in the middle of a proof development. You are working on a soundness +proof of Hoare Logic in a file called@footnote{The suffix may depend of +the specific proof assistant you are using e.g, LEGO's proof script +files have to end with @file{.l}.} @file{HSound.l}. It +depends on a number of other files which develop underlying +concepts e.g. syntax and semantics of expressions, assertions, +imperative programs. You notice that the current lemma is too difficult +to prove because you have forgotten to prove some more basic properties +about determinism of the programming language. Or perhaps a previous +definition is too cumbersome or even wrong. + +At this stage, you would like to visit the appropriate file, say +@file{sos.l} and retract to where changes are required. For further +details on how to accomplish this, we refer to @ref{Retracting across +files}. Then, using script management, you want to develop some more +basic theory in @file{sos.l}. Once this task has been completed +(possibly involving retraction across even earlier files) and the new +development has been asserted, you want to swich back to @file{HSound.l} +and replay to the point you got stuck previously. + +Some hours (or days) later you have completed the soundness proof and +are ready to tackle new challenges. Perhaps, you want to prove a +property that builds on soundness or you want to prove an orthogonal +property such as completeness. + +Proof General lets you do all of this while maintaining the consistency +between proof script buffers and the state of the proof assistant. +However, you cannot have more than one buffer where only a fraction of +the proof script contains a locked region. Before you can employ script +management in another proof script buffer, you must either fully assert +or retract the current script buffer. + +@node View of processed files +@section View of processed files + +Proof General is aware of all files that the proof assistant has +processed or is currently processing. In fact, it relies on the proof +assistant explicitly telling Proof General whenever it processes a +new file which corresponds@footnote{For example, LEGO generates additional compiled +(optimised) proof script files for efficiency.} to a file containing a proof +script. For further technical +details, @pxref{Handling multiple files}. + +If the current proof script buffer depends on background material from +other files, proof assistants typically process these files +automatically. If you visit such a file, the whole file is locked as +having been processed in a single step. From the user's point of view, +you can only retract but not assert in this buffer. Furthermore, +retraction is only possible to the @emph{beginning} of the buffer. + +To be more precise, buffers are locked as soon the proof assistant +notifies Proof General of processing a file different from the +current proof script. Thus, if you visit the file while the proof +assitant is still processing the file, it is already completely locked. +If the proof assistant is not happy with the contents and +complains with an error message, the buffer will still be marked as +having been completely processed. Sorry. You need to visit the +troublesome file, retract (which will always retract to the beginning of +the file) and debug the problem e.g., by asserting all of the buffer +under the supervision of Proof General, @pxref{Script processing +commands}. + +In case you wondered, inconsistencies may arise when you have unsaved +changes in a proof script buffer and the proof assistant suddenly +decides to automatically process the corresponding file. The good news +is that Proof General detects this problem and flashes up a warning in +the response buffer. You might then want to visit the modified buffer, +save it and retract to the beginning. Then you are back on track. + +@node Retracting across files +@section Retracting across files +@cindex Retraction -Suppose we wish to prove the lego term: +Make sure that the current script buffer has either been completely +asserted or retracted. Then you can retract proof scripts in a different +file. Simply visit a file that has been processed earlier and retract in +it, using the retraction commands from @ref{Script processing commands}. Apart from removing parts of the locked region in this +buffer, all files which depend on it will be retracted (and thus +unlocked) automatically. Proof General reminds you that now is a good +time to save any unmodified buffers. -@example -(((p a) \/ (q b)) /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x))); -@end example +@node Asserting across files +@section Asserting across files +@cindex Assertion -Asserting this goal will result in the proof state +Make sure that the current script buffer has either been completely +asserted or retracted. Then you can assert proof scripts in a different +file. Simply visit a file that contains no locked region and assert some +command with the usual assertion commands, @pxref{Script processing +commands}. Proof General reminds you that now is a good time to save any +unmodified buffers. This is particularly useful as assertion may cause +the proof assistant to automatically process other files. -@example -?0 : ((p a \/ q b) /\ @{x:Prop@}(p x)->q x)->Ex ([x:Prop]q x) -@end example -appearing in the goals buffer. Suppose our strategy is to use a -case analysis on the disjunction, starting with the @samp{p(a)} subterm. -Clicking on this term will cause script management to insert the following -command sequence in the script buffer, and execute it. +@node Working directly with the proof shell +@section Working directly with the proof shell +@cindex Shell -@example -Intros H; Refine H; Intros H0 H1; -Refine or_elim H0 Then Intros H2; Try Refine H2; -@end example +Occasionally you may want to review the dialogue of the entire session +with the proof assistant, or check that it hasn't done something +unexpected. Experienced users may also want to directly communicate with +the proof assistant rather than sending commands via the minibuffer, +@pxref{Proof assistant commands}. +Although the proof shell is usually hidden from view, it is run in a +buffer which provides the usual full editing and history facilities of +Emacs shells (see the package @file{comint.el} distributed with your +version of Emacs). You can switch to it using the menu: -The goals buffer will then read +@lisp + Proof-General -> Switch to buffers -> Proof Shell +@end lisp -@example - H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x - H0 : p a \/ q b - H1 : @{x:Prop@}(p x)->q x - H2 : p a - ?10 : Ex ([x:Prop]q x) -@end example +@b{Warning:} you can probably cause confusion by typing in the shell +buffer! Proof General may lose track of the state of the proof +assistant. -Clicking on the subterm @samp{(p x)} in the hypothesis H1 will instruct -script management to prove an instance of @samp{(p x)} and deduce the -corresponding @samp{(q x)}. The commands +Proof General watches the output from the proof assistant to guess when +a file is loaded or when a proof step is taken or undone, but it may not +be guaranteed when the restricted interface is by-passed. What happens +depends on how complete the communication is between Proof General and +the prover (which depends on the particular instantion of Proof +General). -@example -allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption; -@end example +To resynchronise, you have two options. If you are lucky, it might +suffice to -are inserted and executed, leaving the proof state as +@table @kbd +@item C-c C-z +move the end of the locked region backwards to the end of the segment +containing the point. +@end table -@example - H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x - H0 : p a \/ q b - H1 : @{x:Prop@}(p x)->q x - H2 : p a - H3 : (p a)->q a - ?20 : (q a)->Ex ([x:Prop]q x) -@end example +Otherwise, you will need to restart script management altogether, +@pxref{Toolbar commands}. -Now clicking on the @samp{q x)} subterm in ?20 will prove the subgoal. We are -left with the other half of the original case analysis: -@example - H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x - H0 : p a \/ q b - H1 : @{x:Prop@}(p x)->q x - H2 : q b - ?26 : Ex ([x:Prop]q x) -@end example -Clicking on @samp{q x} proves the goal. +@node Support for other Packages +@chapter Support for other Packages +Proof General makes some configuration for other Emacs packages which +provide various useful facilities. Sometimes this configuration is at +the proof assistant specific level, but we suggest that it should be +made for all proof assistants, as a convention. +The packages currently supported are @code{fume-func}, +@code{outline-mode} and @code{etags}. -@node Walkthrough, LEGO mode, Proof by Pointing, Top -@unnumberedsec A Walkthrough +@menu +* Support for function menus:: +* Support for outline mode:: +* Support for tags:: +@end menu -Here's a LEGO example of how script management is used. +@node Support for function menus +@section Support for function menus +@vindex proof-goal-with-hole-regexp +@cindex fume-func + +The Emacs package @code{fume-func} is a provides the handy facility to +make a menu from the names of entities declared in a buffer. Proof +General configures @code{fume-func} so that you can quickly jump to +particular proofs in a script buffer. (This is done with the +configuration variables @code{proof-goal-with-hole-regexp} and +@code{proof-save-with-hole-regexp}.) +@c , @pxref{Proof script mode} for further details. + +If you want to use fume-func, you may need to enable it for yourself. +It is distributed with XEmacs but by not enabled by default. To enable +it you should find the file @file{func-menu.el} and follow the +instructions there. At the time of writing, the current version of +XEmacs is 20.4, supplied with function menu version 2.45, which suggests +the following code for your @file{.emacs} file: + +@lisp + (require 'func-menu) + (define-key global-map 'f8 'function-menu) + (add-hook 'find-file-hooks 'fume-add-menubar-entry t) + (define-key global-map "\C-cl" 'fume-list-functions) + (define-key global-map "\C-cg" 'fume-prompt-function-goto) + (define-key global-map '(shift button3) 'mouse-function-menu) + (define-key global-map '(meta button1) 'fume-mouse-function-goto) +@end lisp + +If you have another version of Emacs, you should check the +@file{fume-func.el} file supplied with it. + +@node Support for outline mode +@section Support for outline mode +@cindex outline mode + +Proof General configures Emacs variables (@code{outline-regexp} and +@code{outline-heading-end-regexp}) so that outline minor mode can be +used on proof script files. The headings taken for outlining are the +"goal" statements at the start of goal-save sequences, +@xref{Goal-save sequences}. + +Use @kbd{M-x outline-minor-mode} to turn on outline minor mode. +Functions for navigating, hiding, and revealing the proof script are +available in menus. + +See @inforef{Outline Mode, ,(xemacs)} for more information about +outline mode. + + +@node Support for tags +@section Support for tags +@cindex tags + +A "tags table" is a description of how a multi-file program is broken up +into files. It lists the names of the component files and the names and +positions of the functions (or other named subunits) in each file. +Grouping the related files makes it possible to search or replace +through all the files with one command. Recording the function names +and positions makes possible the @kbd{M-.} command which finds the +definition of a function by looking up which of the files it is in. + +Some instantiations of Proof General (currently LEGO and Coq) are +supplied with external programs for making tags tables. Once a tag +table has been made for your proof developments, you can use the Emacs +tags mechanisms to find tags, and complete symbols from tags table. + +One useful key binding you might want to make is to set the usual +completion key @kbd{M-tab} to run @code{tag-complete-symbol} to use +completion from names in the tag table. To set this binding in Proof +General script buffers, put this code in your @file{.emacs} file: +@lisp +(add-hook 'proof-mode-hook + (lambda () (local-set-key '(meta tab) 'tag-complete-symbol))) +@end lisp +(Since this key binding interfers with a default binding that users may +already have customized, Proof General doesn't do this automatically). + +For more information on how to use tags, @inforef{Tags, ,(xemacs)}. + + + +@node Customizing Proof General +@chapter Customizing Proof General +@cindex Customization + + +There are two kinds of customization for Proof General: it can be +customized for a user's preferences using a particular proof assistant, +or it can be customized by an Emacs expert to add a new proof assistant. +Here we cover the user-level customization for Proof General. + +We only consider settings for Proof General itself. The support for a +particular proof assistant can provide extra customization settings. +See the chapters covering each assistant for details. -First, we turn on active terminator minor mode by typing @kbd{C-c ;} -Then we enter -`Module Walkthrough Import lib_logic;' +@menu +* Easy customization:: +* Display customization:: +* User options:: +* Changing faces:: +* Tweaking configuration settings:: +@end menu -The command should be lit in pink (or inverse video if you don't have a -colour display). As LEGO imports each module, a line will appear in the -minibuffer showing the creation of context marks. Eventually the -command should turn blue, indicating that LEGO has successfully -processed it. Then type (on a separate line if you like) +@node Easy customization +@section Easy customization +@cindex Using Customize +@cindex Emacs customization library + +Proof General uses the Emacs customization library extensively to +provide a friendly interface. + +You can access a menu of the customization settings for Proof General +via the menu: + +@lisp + Options -> Customize -> Emacs -> External -> Proof General +@end lisp +in XEmacs. + +In FSF Emacs, use the menu: +@c FIXME +@lisp + Help -> Customize -> Specific group +@end lisp +and type @kbd{proof-general RET}. + +The complete set of customization settings will only be availabe after +Proof General has been fully loaded. Proof General is fully loaded when +you visit a script file for the first time. + +When visiting a script file, there is a more direct route to the +settings: +@lisp + Proof-General -> Customize +@end lisp + +Using the customize facility is straightforward. You can select the +setting to customize via the menus, or with @code{M-x +customize-variable}. When you have selected a setting, you are shown a +buffer with its current value, and facility to edit it. Once you have +edited it, you can use the special buttons @var{set}, @var{save} and +@var{done}. You must use one of @var{set} or @var{save} to get any +effect. The @var{save} button stores the setting in your @file{.emacs} +file. + +Notice that in the customize menus, variable names mentioned later may +be abbreviated by omitting the "@code{proof}-" prefix. Also, some of +the option settings may have more descriptive names (for example, +@var{on} and @var{off}) than the low-level lisp values (non-@code{nil}, +@code{nil}) which are mentioned in this chapter. + +For more help, see @inforef{Easy Customization, ,xemacs}. + + + +@node Display customization +@section Display customization +@cindex display customization +@cindex multiple windows +@cindex buffer display customization +@cindex frames +@cindex multiple frames + +If you are working on a workstation with a window system, you can use +Emacs to manage several @i{frames} on the display, to keep the goals +buffer displayed in a fixed place on your screen and in a certain font, +for example. A convenient way to do this is via +@code{special-display-regexps}. + + +@c TEXI DOCSTRING MAGIC: proof-auto-delete-windows +@defopt proof-auto-delete-windows +If non-nil, automatically remove windows when they are cleaned. +For example, at the end of a proof the goals buffer window will +be cleared; if this flag is set it will automatically be removed. +If you want to fix the sizes of your windows you may want to set this +variable to @code{nil'} to avoid windows being deleted automatically. +If you use multiple frames, only the windows in the currently +selected frame will be automatically deleted. + +The default value is @code{nil}. +@end defopt + + + + +@node User options +@section User options +@c Index entries for each option 'concept' +@cindex User options +@cindex Strict read-only +@cindex Query program name +@cindex Dedicated windows +@cindex Remote host +@cindex Toolbar follow mode +@cindex Toolbar disabling +@cindex Proof script indentation +@cindex Indentation +@cindex Remote shell +@cindex Running proof assistant remotely +@c @cindex formatting proof script + +Here are the remaining user options for Proof General. These can be set +via the customization system, via the old-fashioned @code{M-x +edit-options} mechanism, or simply by adding @code{setq}'s to your +@file{.emacs} file. The first approach is strongly recommended. + + +@c TEXI DOCSTRING MAGIC: proof-prog-name-ask +@defopt proof-prog-name-ask +If non-nil, query user which program to run for the inferior process. + +The default value is @code{nil}. +@end defopt + + +@c TEXI DOCSTRING MAGIC: proof-rsh-command +@defopt proof-rsh-command +Shell command prefix to run a command on a remote host. +For example, +@lisp + ssh bigjobs +@end lisp +Would cause Proof General to issue the command @samp{ssh bigjobs isabelle} +to start Isabelle remotely on our large compute server called @samp{bigjobs}. + +The protocol used should be configured so that no user interaction +(passwords, or whatever) is required to get going. + +The default value is @code{""}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-toolbar-wanted +@defopt proof-toolbar-wanted +Whether to use toolbar in proof mode. + +The default value is @code{t}. +@end defopt + + +@c TEXI DOCSTRING MAGIC: proof-toolbar-follow-mode +@defopt proof-toolbar-follow-mode +Choice of how point moves with toolbar commands. +One of the symbols: @code{locked}, @code{follow}, @code{ignore}. +If @code{locked}, point sticks to the end of the locked region with toolbar commands. +If @code{follow}, point moves just when needed to display the locked region end. +If @code{ignore}, point is never moved after toolbar movement commands. + +The default value is @code{locked}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-window-dedicated +@defopt proof-window-dedicated +Whether response and goals buffers have dedicated windows. +If t, windows displaying responses from the prover will not +be switchable to display other windows. This may help manage +your display, but can sometimes be inconvenient, especially +for experienced Emacs users. +Moreover, this option may cause problems with multi-frame +use because of a bug. + +The default value is @code{nil}. +@end defopt + +@c FIXME needs to mention that without dedicated windows, buffers may be +@c hidden. Refer to the XEmacs manual on customising buffer display. + +@c TEXI DOCSTRING MAGIC: proof-strict-read-only +@defopt proof-strict-read-only +Whether Proof General is strict about the read-only region in buffers. +If non-nil, an error is given when an attempt is made to edit the +read-only region. If nil, Proof General is more relaxed (but may give +you a reprimand!) + +The default value is @code{15}. +@end defopt + + +@c TEXI DOCSTRING MAGIC: proof-script-indent +@defopt proof-script-indent +If non-nil, enable indentation code for proof scripts. +Currently the indentation code can be rather slow for large scripts, +and is critical on the setting of regular expressions for particular +provers. Enable it if it works for you. + +The default value is @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-one-command-per-line +@defopt proof-one-command-per-line +If non-nil, format for newlines after each proof command in a script. +This option is not fully-functional at the moment. + +The default value is @code{nil}. +@end defopt + + +@c TEXI DOCSTRING MAGIC: proof-splash-inhibit +@defopt proof-splash-inhibit +Non-nil prevents splash screen display when Proof General is loaded. + +The default value is @code{nil}. +@end defopt + + +@node Changing faces +@section Changing faces + +The fonts and colours that Proof General uses are configurable. If you +alter these through the customize menus, only the particular kind of +display in use (colour window system, monochrome window system, console, +@dots{}) will be affected. + +@c TEXI DOCSTRING MAGIC: proof-queue-face +@deffn Face proof-queue-face +Face for commands in proof script waiting to be processed. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-locked-face +@deffn Face proof-locked-face +Face for locked region of proof script (processed commands). +@end deffn -@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);} +@c TEXI DOCSTRING MAGIC: proof-declaration-name-face +@deffn Face proof-declaration-name-face +Face for declaration names in proof scripts. +Exactly what uses this face depends on the proof assistant. +@end deffn -The goal should be echoed in the goals buffer. -@samp{Intros;} +@c TEXI DOCSTRING MAGIC: proof-tacticals-name-face +@deffn Face proof-tacticals-name-face +Face for names of tacticals in proof scripts. +Exactly what uses this face depends on the proof assistant. +@end deffn -Whoops! @kbd{C-c C-u} to pretend that didn't happen. +@c TEXI DOCSTRING MAGIC: proof-error-face +@deffn Face proof-error-face +Face for error messages from proof assistant. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-warning-face +@deffn Face proof-warning-face +Face for warning messages. +Warning messages can come from proof assistant or from Proof General itself. +@end deffn -@samp{intros; andI;} +@c Maybe this detail of explanation belongs in the internals, +@c with just a hint here. +The slightly bizarre name of the next face comes from the idea that +while large amounts of output are being sent from the prover, some +messages should be displayed to the user while the bulk of the output is +hidden. The messages which are displayed may have a special annotation +to help Proof General recognize them, and this is an "eager" annotation +in the sense that it should be processed as soon as it is observed +by Proof General. -A proof summary will appear in the goals buffer. We could solve the -goal by pointing now, but we'll stay with the keyboard. +@c TEXI DOCSTRING MAGIC: proof-eager-annotation-face +@deffn Face proof-eager-annotation-face +Face for messages from proof assistant. +@end deffn -@samp{Refine H; intros; Immed; Refine H; intros; Immed;} -finishes the Goal. -@samp{Save bland_commutes;} -Moving the mouse pointer over the locked region now reveals that the -entire proof has been aggregated into a single segment. Suppose we -decide to call the goal something more sensible. Moving the cursor up -into the locked region, somewhere between `Goal' and `Save', we enter -@kbd{C-c u}. The segment is transferred back into the editing -region. Now we correct the goal name, move the cursor to the end of the -buffer, and type @kbd{C-c return}. Proof mode queues the commands for -processing and executes them. +@node Tweaking configuration settings +@section Tweaking configuration settings + +This section is a note for advanced users. + +Configuration settings are the per-prover customizations of Proof +General. These are not intended to be adjusted by the user. But +occasionally you may like to test changes to these settings to improve +the way Proof General works. You may want to do this when a proof +assistant has a flexible proof script language in which one can define +new tactics or even operations, and you want Proof General to recognize +some of these which the default settings don't mention. So please feel +free to try adjusting the configuration settings and report to us if you +find better default values than the ones we have provided. + +The configuration settings appear in the customization group +@code{prover-config}, or via the menu +@lisp + Proof-General -> Internals -> Prover Config +@end lisp + +One basic example of a setting you may like to tweak is: + +@c TEXI DOCSTRING MAGIC: proof-assistant-home-page +@defvar proof-assistant-home-page +Web address for information on proof assistant +@end defvar + +Most of the others are more complicated. More details of the settings +are given in @xref{Adapting Proof General to New Provers}. To browse +them, you can look through the customization groups +@code{prover-config}, @code{proof-script} and @code{proof-shell}. The +group @code{proof-script} contains the configuration variables for +scripting, and the group @code{proof-shell} contains those for +interacting with the proof assistant. + +Unfortunately, although you can use the customization mechanism to set +and save these variables, saving them may have no effect because the +default settings are often hard-wired into the proof assistant code. +Ones we expect may need changing appear as proof assistant specific +configurations. For example, @code{proof-assistant-home-page} is set in +the LEGO code from the value of the customization setting +@code{lego-www-home-page}. At present there is no easy way to save +changes to other configuration variables across sessions, other than by +editing the source code. Please contact us if this proves to be a +problem for any variable. + + + + + +@c +@c CHAPTER: LEGO Proof General +@c +@node LEGO Proof General +@chapter LEGO Proof General +@cindex LEGO Proof General + +LEGO proof script mode is a mode derived from proof script mode for +editing LEGO scripts. An important convention is that proof script +buffers @emph{must} start with a module declaration. If the proof script +buffer's file name is @file{fermat.l}, then it must commence with a +declaration of the form + +@lisp +Module fermat; +@end lisp + +If, in the development of the module @samp{fermat}, you require material +from other module e.g., @samp{lib_nat} and @samp{galois}, you need to +specify this dependency as part of the module declaration: + +@lisp +Module fermat Import lib_nat galois; +@end lisp + +No need to worry too much about effeciency. When you retract back to a +module declaration to add a new import item, LEGO does not actually +retract the previously imported modules. Therefore, reasserting the +extended module declaration really only processes the newly imported +modules. + +Using the LEGO Proof General, you never ever need to use administrative +LEGO commands such as @samp{Forget}, @samp{ForgetMark}, @samp{KillRef}, +@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again +@footnote{And please, don't even think of including those in your LEGO +proof script!}. You can concentrate on your actual proof developments. +Script management in Proof General will invoke the appropriate commands +for you. Proving with LEGO has never been easier. + +@menu +* LEGO specific commands:: +* LEGO tags:: +* LEGO customizations:: +@end menu + -@node LEGO mode, Coq mode, Walkthrough, Top -@unnumberedsec LEGO mode +@node LEGO specific commands +@section LEGO specific commands -LEGO mode is a mode derived from proof mode for editing LEGO scripts. -There are some abbreviations for common commands, which -add text to the buffer: +In addition to the commands provided by the generic Proof General, see +the previous sections, the LEGO Proof General provides a few extensions. +In proof scripts, there are some abbreviations for common commands: @table @kbd @item C-c i @@ -429,130 +1769,859 @@ Intros Refine @end table +@node LEGO tags +@section LEGO tags -@node Coq mode, Known Problems, LEGO mode, Top -@unnumberedsec Coq mode +The LEGO Proof General provides the program @file{legotags} to generate +tags for LEGO proof scripts. Invoking @samp{legotags *.l} produces a +file @file{TAGS} for all LEGO modules in the current directory. The LEGO +library itself is shipped out with all its modules already being tagged. +See @ref{Support for tags} for further details. -Coq mode is a mode derived from proof mode for editing Coq scripts. -As well as custom popup menus, it has the following commands: -@table @kbd +@node LEGO customizations +@section LEGO customizations -@item C-c C-s -search for items in the library of a given type. This runs the -@kbd{Search} command of Coq. +We refer to chapter @ref{Customizing Proof General} for an introduction +to the customisation mechanism. In addition to customizations at the +generic level, for LEGO you can also customize: -@end table +@c TEXI DOCSTRING MAGIC: lego-tags +@defopt lego-tags +The directory of the @var{tags} table for the @var{lego} library -In addition, there are some abbreviations for common commands, which -add text to the buffer: +The default value is @code{"/usr/lib/lego/lib_Type/"}. +@end defopt -@table @kbd -@item C-c I -Intros -@item C-c a -Apply -@end table +@c TEXI DOCSTRING MAGIC: lego-help-menu-list +@defvar lego-help-menu-list +List of menu items, as defined in @samp{@code{easy-menu-define}} for @var{lego} +@lisp + specific help. +@end lisp +@end defvar -@node Known Problems, Internals, Coq mode, Top -@unnumberedsec Known Problems +@c We don't worry about the following for now. These are too obscure. +@c lego-indent +@c lego-test-all-name -Since Emacs is pretty flexible, there are a whole bunch of things you -can do to confuse script management. When it gets confused, it may -become distressed, and may eventually sulk. In such instances -@code{proof-restart-script-management} may be of use. +@c We also don't document any of the internal variables which have been +@c set to configure the generic Proof General and which the user should +@c not tamper with -A few things to avoid: +In Xemacs 20.4, LEGO script buffer are coloured (fontified as they say) +by default. To automatically switch on fontification in FSF Emacs 20.2, +you need to set +@vindex lego-mode-hooks +@cindex font-lock colour -@itemize @minus -@item If you're using script management with multiple files, don't start -changing the file names. +@lisp + (add-hook 'lego-mode-hooks 'turn-on-font-lock) +@end lisp -@item Script Management doesn't understand how to undo @code{Discharge} -commands in LEGO, and any attempts it makes to do so may leave it in an -inconsistent state. If you're undoing the effects of a @code{Discharge} -command, retract back to the declaration of whatever gets discharged. +in your @file{~/.emacs} file. -@item Proof by Pointing doesn't work very well, and is inefficiently -implemented. -@item The locked and queue regions are not quite read-only: in particular -Emacs Undo can insert text into them. -@item When a LEGO import command fails, the created "Mark" is not -forgotten, and the proof process thinks the file has been included. So -if you assert the command again, it will probably be accepted by LEGO, -because the relevant mark is in the namespace. -@end itemize +@node Coq Proof General +@chapter Coq Proof General + +Sorry, there is no specific documentation written yet for Coq Proof +General. -Fixes for some of these may be provided in a future release. +If any Coq user would like to contribute, please send a message to +@code{proofgen@@dcs.ed.ac.uk}. -@node Internals, Variable Index, Known Problems, Top -@comment node-name, next, previous, up -@unnumberedsec Internals +Type @kbd{C-h C-m} to get a list of Coq specific commands and +browse the customize menus to find out what customization +options there are for Coq. @menu -* Granularity of Atomic Command Sequences:: -* Handling Multiple Files:: -* Adding A New Proof Assistant:: -* Literature:: +* Coq specific commands:: +* Coq customizations:: @end menu -@node Granularity of Atomic Command Sequences, Handling Multiple Files, Internals, Internals -@comment node-name, next, previous, up -@unnumberedsubsec Granularity of Atomic Commands -@cindex Granularity of Atomic Sequences -@cindex Retraction -@cindex Goal -@cindex ACS (Atomic Command Sequence) +@node Coq specific commands +@section Coq specific commands -The *Locked* region of a script buffer contains the initial segment of -the proof script which has been processed successfully. It consists of -atomic sequences of commands (ACS). Retraction is supported to the -beginning of every ACS. By default, every command is an ACS. But the -granularity of atomicity can be adjusted for different proof assistants. -This is essential when arbitrary retraction is not supported. Usually, -after a theorem has been proved, one may only retract to the start of -the goal. One needs to mark the proof of the theorem as an ACS. +@node Coq customizations +@section Coq customizations -@vtable @code -@item proof-atomic-sequents-list -is a list of instructions for setting up ACSs. Each instruction is a -list of the form @code{(@var{end} @var{start} &optional -@var{forget-command})}. @var{end} is a regular expression to recognise -the last command in an ACS. @var{start} is a function. Its input is the -last command of an ACS. Its output is a regular expression to recognise -the first command of the ACS. It is evaluated once and the output is -successively matched against previously processed commands until a match -occurs (or the beginning of the current buffer is reached). The region -determined by (@var{start},@var{end}) is locked as an ACS. Optionally, -the ACS is annotated with the actual command to retract the ACS. This is -computed by applying @var{forget-command} to the first and last command -of the ACS. -@end vtable -@node Handling Multiple Files, Adding A New Proof Assistant, Granularity of Atomic Command Sequences, Internals -@comment node-name, next, previous, up -@unnumberedsubsec Handling Multiple Files +@c +@c CHAPTER: Isabelle Proof General +@c -@cindex Multiple Files +@node Isabelle Proof General +@chapter Isabelle Proof General +@cindex Isabelle Proof General + +Isabelle Proof General includes a mode for editing theory files taken +from David Aspinall's Isamode interface, +@uref{http://www.dcs.ed.ac.uk/home/da/Isamode}. Detailed documentation +for the theory file mode is included with @code{Isamode}, there are some +notes on the special functions available and customization setttings +below. + +@menu +* Theory files:: +* Isabelle specific commands:: +* Isabelle customizations:: +@end menu + + +@node Theory files +@section Theory files +@cindex Theory files (in Isabelle) +@cindex ML files (in Isabelle) + +Isabelle Proof General attempts to lock theory files as well as ML files +when they are loaded. Theory files are always completely locked or +completely unlocked, because they are processed atomically. + +Proof General attempts to load the theory file for a @file{.ML} file +automatically before you start scripting. This is tricky because +Isabelle's theory loader assumes that @file{.ML} files are always read +together with theory files. At the moment Proof General uses an altered +version of @code{use_thy} which doesn't load the top-level ML file in +this case. + +@c FIXME: should say something about this: +@c This can cause confusion in the theory loader later, +@c especially with @code{update()}. To be safe, try to use just the Proof +@c General interface, and report any repeatable problems to +@c @code{isabelle@dcs.ed.ac.uk}. + +Compared to Isamode's theory editing mode, some of the functions and key +bindings for interacting with Isabelle have been removed, and two new +functions are available. + +The key @kbd{C-c C-b} (@code{isa-process-thy-file}) will cause Isabelle +to read the theory file being edited. This causes the file and all its +children (both theory and ML files) to be read. Any top-level ML file +associated with this theory file is also read. + +The key @kbd{C-c C-u} (@code{isa-retract-thy-file}) will retract +(unlock) the theory file being edited. This unlocks the file and all +its children (theory and ML files); no changes occur in Isabelle itself. + + +@c TEXI DOCSTRING MAGIC: isa-process-thy-file +@deffn Command isa-process-thy-file file +Process the theory file @var{file}. If interactive, use @code{buffer-file-name}. +@end deffn + +@c TEXI DOCSTRING MAGIC: isa-retract-thy-file +@deffn Command isa-retract-thy-file file +Retract the theory file @var{file}. If interactive, use @code{buffer-file-name}. +@end deffn + + +@node Isabelle specific commands +@section Isabelle specific commands + + +@unnumberedsubsec Switching to theory files +@cindex Switching to theory files +@kindex C-c C-o + +In Isabelle proofscript mode, @kbd{C-c C-o} (@code{thy-find-other-file}) +finds and switches to the associated theory file, that is, the file with +the same base name but extension @file{.thy} swapped for @file{.ML}. + +The same function (and keybinding) switches back to an ML file from the +theory file. + + +@c TEXI DOCSTRING MAGIC: thy-find-other-file +@deffn Command thy-find-other-file &optional samewindow +Find associated .ML or .thy file. +Finds and switch to the associated ML file (when editing a theory file) +or theory file (when editing an ML file). +If @var{samewindow} is non-nil (interactively, with an optional argument) +the other file replaces the one in the current window. +@end deffn + + +@node Isabelle customizations +@section Isabelle customizations + +Here are some of the user options specific to Isabelle. You can set +these with the customization mechanism as usual. + +@c TEXI DOCSTRING MAGIC: isabelle-web-page +@defvar isabelle-web-page +URL of web page for Isabelle. +@end defvar + + +@c @unnumberedsubsec Theory file editing customization + +@c TEXI DOCSTRING MAGIC: thy-use-sml-mode +@defopt thy-use-sml-mode +If non-nil, invoke sml-mode inside "ML" section of theory files. +This option is left-over from Isamode. Really, it would be more +useful if the script editing mode of Proof General itself could be based +on sml-mode, but at the moment there is no way to do this. + +The default value is @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: thy-indent-level +@defvar thy-indent-level +Indentation level for Isabelle theory files. An integer. +@end defvar + +@defopt thy-indent-level +Indentation level for Isabelle theory files. An integer. +@end defopt + +@c TEXI DOCSTRING MAGIC: thy-sections +@defvar thy-sections +Names of theory file sections and their templates. +Each item in the list is a pair of a section name and a template. +A template is either a string to insert or a function. Useful functions are: +@lisp + @code{thy-insert-header}, @code{thy-insert-class}, @code{thy-insert-default-sort}, + @code{thy-insert-const}, @code{thy-insert-rule}. +@end lisp +The nil template does nothing. +You can add extra sections to theory files by extending this variable. +@end defvar + +@c TEXI DOCSTRING MAGIC: thy-template +@defvar thy-template +Template for theory files. +Contains a default selection of sections in a traditional order. +You can use the following format characters: + +%t --- replaced by theory name. + +%p --- replaced by names of parents, separated by @samp{+} characters. +@end defvar + +@c ideal for above: +@c @defopt thy-template +@c Template for theory files. +@c Contains a default selection of sections in a traditional order. +@c You can use the following format characters: +@c @code{%t} -- replaced by theory name +@c @code{%p} -- replaced by names of parents, separated by @code{+}'s +@c @end defopt + + + + +@node Adapting Proof General to New Provers +@chapter Adapting Proof General to New Provers + +Proof General has about 60 configuration variables which are set on a +per-prover basis to configure the various features. However, many of +these variables occcur in pairs (typically regular expressions matching +the start and end of some text), and you can begin by setting just a few +variables to get the basic features working. + +The configuration variables are declared in the file +@file{generic/proof-config.el}. Documentation below is based on the +contents of that file. + +@menu +* Overview of adding a new prover:: +* Major modes used by Proof General:: +* Menus and user-level commands:: +* Proof script settings:: +* Proof shell settings:: +* Splash screen settings:: +* Goals buffer configuration:: +* Global constants:: +* Handling multiple files:: +@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. + +@itemize @bullet +@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 New 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 modes in @file{myassistant.el}, by looking at + the files for the currently supported assistants for example. + Basically you need to define some modes using @code{define-derived-mode} + and set the configuration variables. It's important that your modes + invoke the callbacks @code{proof-config-done} and + @code{proof-shell-config-done} once they've set the configuration + variables. +@end itemize + +You could begin by setting minimum number of the variables, then adjust +the settings via the customize menus, under Proof-General -> 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{@var{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{@var{proof-home-directory}} is the value of the +variable @code{proof-home-directory}. + +The default value is @code{((isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$"))}. +@end defopt + +@node Major modes used by Proof General +@section Major modes used by Proof General + +@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 in @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. +Usually customised for specific prover. +Suggestion: this can be set in @code{proof-pre-shell-start-hook}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-pbp +@defvar proof-mode-for-pbp +Mode for proof state display buffers. +Usually customised for specific prover. +Suggestion: this can be set in @code{proof-pre-shell-start-hook}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-script +@defvar proof-mode-for-script +Mode for proof script buffers. +This is used by Proof General to find out which buffers +contain proof scripts. +Suggestion: this can be set in the script mode configuration. +@end defvar + +@node Menus and user-level commands +@section Menus and user-level commands + +@c TEXI DOCSTRING MAGIC: proof-assistant-home-page +@defvar proof-assistant-home-page +Web address for information on proof assistant +@end defvar +@c TEXI DOCSTRING MAGIC: proof-ctxt-string +@defvar proof-ctxt-string +Command to display the context in proof assistant. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-help-string +@defvar proof-help-string +Command to ask for help in proof assistant. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-prf-string +@defvar proof-prf-string +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 %s will be replaced by the +goal string. If a function, should return a command string to +insert when called interactively. +@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 %s will be replaced by the +theorem name. If a function, should return a command string to +insert when called interactively. +@end defvar + +@c defgroup proof-script +@node Proof script settings +@section Proof script settings + +The following variables should be set before proof-config-done +is called. These configure the mode for the script buffer, +including highlighting, etc. + +@c TEXI DOCSTRING MAGIC: proof-terminal-char +@defvar proof-terminal-char +Character which terminates a proof command in a script buffer. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-comment-start +@defvar proof-comment-start +String which starts a comment in the proof assistant command language. +The script buffer's @code{comment-start} is set to this string plus a space. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-comment-end +@defvar proof-comment-end +String which starts a comment in the proof assistant command language. +The script buffer's @code{comment-end} is set to this string plus a space. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-save-command-regexp +@defvar proof-save-command-regexp +Matches a save command +@end defvar +@c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp +@defvar proof-save-with-hole-regexp +Regexp which matches a command to save a named theorem. +Match number 2 should be the name of the theorem saved. +Used for setting names of goal..save regions and for default +func-menu configuration in proof-script-find-next-goalsave. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-goal-command-regexp +@defvar proof-goal-command-regexp +Matches a goal command. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp +@defvar proof-goal-with-hole-regexp +Regexp which matches a command used to issue and name a goal. +Match number 2 should be the name of the goal issued. +Used for setting names of goal..save regions and for default +func-menu configuration in proof-script-find-next-goalsave. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps +@defvar proof-script-next-entity-regexps +Regular expressions to control finding definitions in script. +This is the list of the form +@lisp + (@var{anyentity-regexp} + @var{discriminator-regexp} ... @var{discriminator-regexp}) +@end lisp +The idea is that @var{anyentity-regexp} matches any named entity in the +proof script, on a line where the name appears. This is assumed to be +the start or the end of the entity. The discriminators then test +which kind of entity has been found, to get its name. A +@var{discriminator-regexp} has one of the forms +@lisp + (@var{regexp} @var{matchno}) + (@var{regexp} @var{matchno} @code{backward} @var{backregexp}) + (@var{regexp} @var{matchno} @code{forward} @var{forwardregexp}) +@end lisp +If @var{regexp} matches the string captured by @var{anyentity-regexp}, then +@var{matchno} is the match number for the substring which names the entity. + +If @code{backward} @var{backregexp} is present, then the start of the entity +is found by searching backwards for @var{backregexp}. + +Conversely, if @code{forward} @var{forwardregexp} is found, then the end of +the entity is found by searching forwards for @var{forwardregexp}. + +Otherwise, the start and end of the entity will be the region matched +by @var{anyentity-regexp}. + +This mechanism allows fairly complex parsing of the buffer, in +particular, it allows for goal..save regions which are named +only at the end. However, it does not parse strings, +comments, or parentheses. + +This variable may not need to be set: a default value which should +work for goal..saves is calculated from @code{proof-goal-with-hole-regexp}, +@code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}. +@end defvar +@c TEXI DOCSTRING MAGIC: nilproof-goal-command-p nil +@c TEXI DOCSTRING MAGIC: proof-lift-global +@defvar proof-lift-global +This function lifts local lemmas from inside goals out to top level. +This function takes the local goalsave span as an argument. Set this +to @samp{nil} of the proof assistant does not support nested goals. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-count-undos-fn +@defvar proof-count-undos-fn +Compute number of undos in a target segment +@end defvar +@c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn +@defvar proof-find-and-forget-fn +Function returning a command string to forget back to before its argument span. +The special string @code{proof-no-command} means there is nothing to do. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn +@defvar proof-goal-hyp-fn +Function which returns cons cell if point is at a goal/hypothesis. +First element of cell is a symbol, @code{goal'} or @code{hyp'}. The second +element is a string: the goal or hypothesis itself. This is used +when parsing the proofstate output +@end defvar +@c TEXI DOCSTRING MAGIC: proof-kill-goal-command +@defvar proof-kill-goal-command +Command to kill a goal. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-global-p +@defvar proof-global-p +Whether a command is a global declaration. Predicate on strings or nil. +This is used to handle nested goals allowed by some provers. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-state-preserving-p +@defvar proof-state-preserving-p +A predicate, non-nil if its argument preserves the proof state. +@end defvar +@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. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-stack-to-indent +@defvar proof-stack-to-indent +Prover-specific code for indentation. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-parse-indent +@defvar proof-parse-indent +Proof-assistant specific function for parsing. +Invoked in @samp{proof-parse-to-point}. Must be a +function taking two arguments, a character (the current character) +and a stack reflecting indentation, and must return a stack. The +stack is a list of the form (c . p) where @samp{c} is a character +representing the type of indentation and @samp{p} records the column for +indentation. The generic @samp{proof-parse-to-point} function supports +parentheses and commands. It represents these with the characters +@samp{?(}, @samp{?[} and @samp{@code{proof-terminal-char}}. +@end defvar + + + +@node Proof shell settings +@section Proof shell settings + +The variables in this section are the largest group. They concern the +proof shell mode. The first group of variables are hooks invoked at +various points. The second group of variables are concerned with +matching the output from the proof assistant. + +Variables here are put into the customize group @code{proof-shell}. + +These should be set in the shell mode configuration, again, +before @code{proof-shell-config-done} is called. + +@menu +* Proof shell commands:: +* Settings for matching output from proof process:: +* Hooks and function variables:: +@end menu + +@node Proof shell commands +@subsection Commands + +@c TEXI DOCSTRING MAGIC: proof-prog-name +@defvar proof-prog-name +System command to run program name in proof shell. +Suggestion: this can be set in @code{proof-pre-shell-start-hook} from +a variable which is in the proof assistant's customization +group. This allows different proof assistants to coexist +(albeit in separate Emacs sessions). +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-init-cmd +@defvar proof-shell-init-cmd +The command for initially configuring the proof process. +@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-cd +@defvar proof-shell-cd +Command to the proof assistant to change the working directory. +@end defvar + +@node Settings for matching output from proof process +@subsection Settings for matching output from proof process +@c TEXI DOCSTRING MAGIC: proof-shell-wakeup-char +@defvar proof-shell-wakeup-char +A special character which terminates an annotated prompt. +Set to nil if proof assistant does not support annotated prompts. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-first-special-char +@defvar proof-shell-first-special-char +First special character. +Codes above this character can have special meaning to Proof General, +and are stripped from the prover's output strings. +@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. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp +@defvar proof-shell-annotated-prompt-regexp +Regexp matching a (possibly annotated) prompt pattern. +Output is grabbed between pairs of lines matching this regexp. +To help matching you may be able to annotate the proof assistant +prompt with a special character not appearing in ordinary output. +The special character should appear in this regexp, 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. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp +@defvar proof-shell-interrupt-regexp +Regexp matching output indicating the assistant was interrupted. +Similar notes apply as for @code{proof-shell-error-regexp}, which see. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp +@defvar proof-shell-proof-completed-regexp +Regexp matching output indicating a finished proof. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp +@defvar proof-shell-clear-response-regexp +Regexp matching output telling Proof General to clear the response buffer. +This feature is useful to give the prover more control over what output +is shown to the user. Set to nil to disable. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp +@defvar proof-shell-start-goals-regexp +Regexp matching the start of the proof state output. +@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. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start +@defvar proof-shell-eager-annotation-start +Eager annotation field start. A regular expression or nil. +An eager annotation indicates to Emacs that some following output +should be displayed immediately and not accumulated for parsing. +Set to nil to disable this feature. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end +@defvar proof-shell-eager-annotation-end +Eager annotation field end. A regular expression or nil. +An eager annotation indicates to Emacs that some following output +should be displayed immediately and not accumulated for parsing. + +The default value is "\n" to match up to the end of the line. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp +@defvar proof-shell-assumption-regexp +A regular expression matching the name of assumptions. +@end defvar + + +@node Hooks and function variables +@subsection Hooks and function variables + +@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, setting the line width of output). +Any text inserted by these hooks will be sent to the proof process +before every command issued by Proof General. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-pre-shell-start-hook +@defvar proof-pre-shell-start-hook +Hooks run before proof shell is started. +Usually this is set to a function which configures the proof shell +variables. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-hook +@defvar proof-shell-handle-error-hook +Hooks run after an error has been reported in the response buffer. +@end defvar +@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 a script file name (with complete +path) the system is currently processing. 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 +A @var{regexp} to match that the prover has retracted across file boundaries. + +At this stage, Proof General's view of the processed files is out of +date and needs to be updated with the help of the function +@samp{@code{proof-shell-compute-new-files-list}}. +@end defvar +@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 +@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 Splash screen settings +@section Splash screen settings + +The splash screen can be configured, in a rather limited way. + +@c TEXI DOCSTRING MAGIC: proof-splash-time +@defvar proof-splash-time +Minimum number of seconds to display splash screen for. +The splash screen may be displayed for a couple of seconds longer than +this, depending on how long it takes the machine to initialise proof mode. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-splash-contents +@defvar proof-splash-contents +Evaluated to configure splash screen displayed when entering Proof General. +If an element is a string or an image specifier, it is displayed +centred on the window on its own line. If it is nil, a new line is +inserted. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-splash-extensions +@defvar proof-splash-extensions +Prover specific extensions of splash screen. +These are evaluated and appended to @code{proof-splash-contents}, which see. +@end defvar + + + + +@node Goals buffer configuration +@section Goals buffer configuration + +The goals buffer configuration will allow configuration of Proof General +for proof by pointing or similar features. At the moment these settings +are disabled. + +@c TEXI DOCSTRING MAGIC: pbp-change-goal +@defvar pbp-change-goal +Command to change to the goal %s +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-goal-command +@defvar pbp-goal-command +Command informing the prover that @samp{@code{pbp-button-action}} has been +requested on a goal. +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-hyp-command +@defvar pbp-hyp-command +Command informing the prover that @samp{@code{pbp-button-action}} has been +requested on an assumption. +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-error-regexp +@defvar pbp-error-regexp +Regexp indicating that the proof process has identified an error. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-result-start +@defvar proof-shell-result-start +Regexp matching start of an output from the prover after pbp commands. +In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-result-end +@defvar proof-shell-result-end +Regexp matching end of output from the prover after pbp commands. +In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +@end defvar + + + +@node Global constants +@section Global constants + +The settings here are internal constants used by Proof General. +You don't need to configure these for your proof assistant +unless you want to modify or extend the defaults. + +@c TEXI DOCSTRING MAGIC: proof-general-name +@defvar proof-general-name +Proof General name used internally and in menu titles. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-proof-general-home-page +@defopt proof-proof-general-home-page +Web address for Proof General + +The default value is @code{"http://www.dcs.ed.ac.uk/home/proofgen"}. +@end defopt +@c TEXI DOCSTRING MAGIC: proof-universal-keys +@defvar proof-universal-keys +List of keybindings which for the script and response buffer. +Elements of the list are tuples (k . f) +where @samp{k} is a keybinding (vector) and @samp{f} the designated function. +@end defvar + + + +@node Handling multiple files +@section Handling multiple files +@cindex Multiple files Large proof developments are typically spread across multiple files. Many provers support such developments by keeping track of dependencies and automatically processing scripts. Proof General supports this -mechanism. - -However, the prover must let the Proof General know whenever -it processes a file directly. Such files are being marked by Proof -General as having been processed by an atomic action (regardless of -whether an error occurs or not). The file can then only be edited after -retracting to the beginning of the file. +mechanism. The user's point of view is +explored further in @ref{Advanced Script Management}. Here, we +describe the more technical nitty gritty. This is what you need to know +when you customise another proof assistant to work with Proof General. -When retraction is requested in a buffer which is not the current -script, Proof General duely retracts in this buffer. It then arranges a -little conference with the prover to find out which other files have -also been retracted. With this strategy, Proof General doesn't have a -hard time to keep track of dependencies. +The key idea is that we leave it to the specific proof assistant to +worry about managing multiple files. But whenever the proof assistant +processes or retracts a file it must clearly say so. @vindex proof-shell-eager-annotation-start @vindex proof-shell-eager-annotation-end @@ -568,25 +2637,27 @@ file and retracts across file boundaries. @vtable @code @item proof-included-files-list -records the file history. Whenever a new file is being processed, it -gets added to the +records the file history. Whenever a new file is being processed, Proof +General adds it to the front of the list. When the prover retracts across file boundaries, this -list is resynchronised. It contains files in canonical truename format -@inforef{Truenames,,lispref}. - -@item proof-shell-process-file -is either nil or a tuple of the -form (@var{regexp}, @var{function}). If @var{regexp} matches a substring -of @var{str}, -then the function @var{function} is invoked with input @var{str}. It must return a script file -name (with complete path) -the system is currently processing. In practice, @var{function} is -likely to inspect the match data. @inforef{Match Data,,lispref}. -Care has to be taken in case the prover only reports on compiled -versions of files it is processing. In this case, @var{function} needs -to reconstruct the corresponding script file name. -The -new (true) file name is added to the front of @code{proof-included-files-list}. +list is resynchronised. It contains files in canonical truename format. +@inforef{Truenames,,lispref}. You should not set this variable directly. +The generic Proof General will modify @code{proof-included-files-list} +itself. Instead, for a specific proof assistant you need to customise +@code{proof-shell-process-file}. @code{proof-shell-retract-files-regexp} +and @code{proof-shell-compute-new-files-list}. + +@item proof-shell-process-file +is either nil or a tuple of the form (@var{regexp}, @var{function}). If +@var{regexp} matches a substring of @var{str}, then the function +@var{function} is invoked with input @var{str}. It must return a script +file name (with complete path) the system is currently processing. In +practice, @var{function} is likely to inspect the match +data. @inforef{Match Data,,lispref}. Care has to be taken in case the +prover only reports on compiled versions of files it is processing. In +this case, @var{function} needs to reconstruct the corresponding script +file name. The new (true) file name is then automatically added to the +front of @code{proof-included-files-list} by the generic code. @item proof-shell-retract-files-regexp is a regular expression. It indicates that the prover has retracted @@ -598,80 +2669,1099 @@ the function @code{proof-shell-compute-new-files-list}. @ftable @code @item proof-shell-compute-new-files-list Takes as argument the current output of the prover. It needs to return -an up to date list of all processed files. Its output is stored in -@code{proof-included-files-list}. In practice, this function is likely +an up to date list of all processed files. Its output is then +automatically stored in +@code{proof-included-files-list} by the generic Proof General. In practice, this function is likely to inspect the previous (global) variable @code{proof-included-files-list} and the match data @inforef{Match Data,,lispref} triggered by @code{proof-shell-retract-files-regexp}. @end ftable -@node Adding A New Proof Assistant, Literature, Handling Multiple Files, Internals -@comment node-name, next, previous, up -@unnumberedsubsec Adding Support for a New Proof Assistant -Suppose your new assistant is -called myassistant. -@itemize @minus -@item Make a directory called 'myassistant' under the Proof General home -directory, to put the specific customization and associated files in. -@item Add a file myassistant.el to the new directory. -@item Edit proof-site.el to add a new entry to the - @var{proof-internal-assistants-table} variable. The new entry should -look like this: - (myassistant "My New Assistant" "\\.myasst$") +@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:: +* Proof General site configuration:: +* Global variables:: +* Proof script mode:: +* Proof shell mode:: +@end menu + + + +@node Spans +@section Spans +@cindex spans +@cindex extents +@cindex overlays + +@dfn{Spans} are an abstraction of XEmacs @dfn{extents} used to help +bridge the gulf between FSF Emacs and XEmacs. In FSF 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 PROOFGENERAL_@var{home} if set, +otherwise based on where the file proof-site 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. +@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 assitants to use with Proof General. +A list of symbols chosen from: @code{isa} @code{lego} @code{coq}. +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. +@var{note}: to change proof assistant, you must start a new Emacs session. + +The default value is @code{(isa lego coq)}. +@end defopt + +The file @file{proof-site.el} also defines a version variable. + +@c TEXI DOCSTRING MAGIC: proof-version +@defvar proof-version +Version string identifying Proof General release. +@end defvar + + -The first item is used to form the name of the internal variables -for the new mode as well as the directory and file where it loads -from. The second is a string, naming the proof assistant. -The third item is a regular expression to match names of -proof script files for this assistant. See the documentation -of @var{proof-internal-assistants-table} for more details. -@item Define the new modes in myassistant.el, by looking at - the files for the currently supported assistants for example. - Basically you need to define some modes using @code{define-derived-mode} - and set the configuration variables. You could begin by setting - a minimum number of the variables, then adjust the - settings via the customize menus, under Proof-General -> Internals. -@end itemize -@node Literature, , Adding A New Proof Assistant, Internals -@comment node-name, next, previous, up -@unnumberedsubsec Literature +@node Global variables +@section Global variables -The current version supports Script Management as documented in: +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-goals-buffer +@defvar proof-goals-buffer +The goals buffer (also known as the pbp buffer). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-buffer-type +@defvar proof-buffer-type +Symbol indicating the type of this buffer: @code{script}, @code{shell}, or @code{pbp}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-included-files-list +@defvar proof-included-files-list +List of files currently included in proof process. +Whenever a new file is being processed, it gets added. +When the prover retracts across file boundaries, this list +is resynchronised. It contains files in canonical truename format +@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. +@end defvar + +The @file{proof.el} also loads @file{proof-config.el} which declares the +proof assistant configuration variables for Proof General, +@xref{Adapting Proof General to New Provers} for details. + + +@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, keybindings, and user-level +functions. + +Proof scripts have two important variables for the locked and queue +regions. These variables are local to each script buffer (although we +only really need one queue span in total rather than one per buffer). + +@c TEXI DOCSTRING MAGIC: proof-locked-span +@defvar proof-locked-span +The locked span of the buffer. +Each script buffer has its own locked span, which may be detached +from the buffer. +Proof General allows buffers in other modes also to be locked; +these also have a non-nil value for this variable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-queue-span +@defvar proof-queue-span +The queue span of the buffer. May be detached if inactive or empty. +@end defvar + +Various utility functions manipulate and examine the spans. An +important one is @code{proof-init-segmentation}. + +@c TEXI DOCSTRING MAGIC: proof-init-segmentation +@defun proof-init-segmentation +Initialise the queue and locked spans in a proof script buffer. +No harm if the spans have already been allocated. +@end defun + +For locking files loaded by a proof assistant, we use the next function. + +@c TEXI DOCSTRING MAGIC: proof-mark-buffer-atomic +@defun proof-mark-buffer-atomic buffer +Mark @var{buffer} as having been processed in 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 +(@xref{Handling multiple files} and @xref{Global variables}). + +@c TEXI DOCSTRING MAGIC: proof-register-possibly-new-processed-file +@defun proof-register-possibly-new-processed-file file +Register a possibly new @var{file} as having been processed by the prover. +@end defun + +Another important function activates scripting for the current script +buffer. This may involve switching from one scripting buffer to +another. + +@c TEXI DOCSTRING MAGIC: proof-activate-scripting +@defun proof-activate-scripting +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 current scripting buffer provided the current +scripting buffer has either no locked region or everything in it has +been processed. + +If we're changing scripting buffer and the old one is associated with +a file, add it to @code{proof-included-files-list}. + +When a new script buffer has scripting minor mode turned on, +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. + +Finally, this may be a good time to ask if the user wants to save some +buffers. +@end defun + +The next function is the main one used for parsing the proof script +buffer. + +@c TEXI DOCSTRING MAGIC: proof-segment-up-to +@defun proof-segment-up-to pos &optional next-command-end +Create a list of (type,int,string) tuples from end of locked region to @var{pos}. +Each tuple denotes the command and the position of its terminator, +type is one of @code{comment}, or @code{cmd}. @code{unclosed-comment} may be consed onto +the start if the segment finishes with an unclosed comment. +If optional @var{next-command-end} is non-nil, we contine past @var{pos} until +the next command end. +@end defun + +The function @code{proof-semis-to-vanillas} is used to convert +a parsed region of the script into a series of commands to +be sent to the proof assistant. + +@c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas +@defun proof-semis-to-vanillas semis &optional callback-fn +Convert a sequence of terminator positions to a set of vanilla extents. +Proof terminator positions @var{semis} has the form returned by +the function @code{proof-segment-up-to}. +@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, active 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 +@deffn Command 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 deffn + +@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 +@deffn Command 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 actually 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 deffn + +To clean up when scripting is stopped 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). + +Clever process handling is a tricky issue. Proof General attempts to +manage the process strictly, by mainting 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 @code{proof-start-queue} and proof-exec-loop. +@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. +Value for @code{kill-buffer-hook} in shell buffer. +Attempt to shut down the proof process nicely and +clears up all the locked regions and state variables. +@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, kill the shell buffer, +ensuring that script buffers are cleaned up neatly. +@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. The restart command should re-synchronize +Proof General with the proof assitant. +@end deffn + +@c +@c INPUT +@c + +Input to the proof shell via the queue region is dealt with 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. +@end defun + +@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, 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 + +A useful utility function for sending a single command to the process is +@code{proof-shell-invisible-command}. This should be used to implement +user-level functions rather than attempting to manipulate the proof +action list directly. + +@c +@c OUTPUT +@c + +Two main functions deal with output, @code{proof-shell-process-output} +and @code{proof-shell-process-urgent-message}. In effect we consider +the output to be two streams intermingled: the "urgent" messages which +have "eager" annotations, as well as the ordinary ruminations from the +prover. + +The idea is to conceal as much irrelevant information from the user as +possible; only the remaining output between prompts and after the last +urgent message will be a candidate for the goal or response buffer. +The variable @code{proof-shell-urgent-message-marker} tracks +the last urgent message seen. + +@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. +This function deals with errors, start of proofs, abortions of +proofs and completions of proofs. All other output from the proof +engine is simply reported to the user in the response buffer +by setting @code{proof-shell-delayed-output} to a cons cell of +(@var{insert} . @var{text}) where @var{text} is the text to be inserted. + +To extend this function, set +@code{proof-shell-process-output-system-specific}. + +This function - it can return one of 4 things: @code{error}, @code{interrupt}, +@code{loopback}, or nil. @code{loopback} means this was output from pbp, and +should be inserted into the script buffer and sent back to the proof +assistant. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker +@defvar proof-shell-urgent-message-marker +Marker in proof shell buffer pointing to end of last urgent message. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message +@defun proof-shell-process-urgent-message message +Analyse urgent @var{message} for various cases. +Included file, retracted file, cleared response buffer, or +if none of these apply, display. +@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}. + +Process 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, then +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 + @var{prompt} @var{input} + @var{output-1} + @var{urgent-message} + @var{output-2} + @var{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. + +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. +@end defun + + + + + + + + + + + + + + + + + + + +@c +@c +@c CHAPTER: Obtaining and Installing Proof General +@c +@c +@node Credits and References +@chapter Credits and References + +@menu +* Credits:: +* References:: +@end menu + +@node Credits +@unnumberedsec Credits + +LEGO Proof General was written by Thomas Kleymann and Dilip Sequeira. + +Coq Proof General was written by Healfdene Goguen. + +Isabelle Proof General was written by David Aspinall. + +The generic base for Proof General was developed by all four of us. + +Thomas Kleymann provided the impetus to develop a generic Emacs +interface, following ideas used in Projet CROAP, and with the help of +Yves Bertot. David Aspinall provided the Proof General name and images. + +An early version of this manual was prepared by Dilip Sequeira. The +present version was written by David Aspinall and Thomas Kleymann. + +During the development of Proof General, the following people helped +by providing feedback, testing, or code: +Pascal Brisset, +Rod Burstall, +Paul Callaghan, +Martin Hofmann, +James McKinna, +and Markus Wenzel. Thanks to all of you! + + +@node References +@unnumberedsec References + +Script management as used in Proof General is described in the paper: @itemize @bullet @item -Yves Bertot and Laurent Th@'ery. A generic approach to building -user interfaces for theorem provers. To appear in Journal of +Yves Bertot and Laurent Th@'ery. @i{A generic approach to building +user interfaces for theorem provers}. To appear in Journal of Symbolic Computation. @end itemize -It has the beginnings of support for Proof by Pointing, as documented in: +Proof General has the beginnings of support for proof by pointing, +as described in the document: @itemize @bullet @item -Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing +Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. @i{Implementing Proof by Pointing without a -Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de +Structure Editor}. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis RR-3286 @end itemize -@node Variable Index, Function Index, Internals, Top -@comment node-name, next, previous, up -@unnumbered Variable Index -@printindex vr -@node Function Index, Concept Index,Variable Index, Top -@comment node-name, next, previous, up -@unnumbered Function Index +@c +@c +@c APPENDIX: Obtaining and Installing Proof General +@c +@c +@node Obtaining and Installing Proof General +@appendix Obtaining and Installing Proof General + +Proof General has its own +@uref{http://www.dcs.ed.ac.uk/home/proofgen,home page} hosted at +Edinburgh. Visit this page for the latest news! + +@menu +* Obtaining Proof General:: +* Installing Proof General from tarball:: +* Installing Proof General from RPM package:: +* Notes for syssies:: +@end menu + + +@node Obtaining Proof General +@section Obtaining Proof General + +You can obtain Proof General from the URL +@example +@uref{http://www.dcs.ed.ac.uk/home/proofgen/download.html}. +@end example + +The distribution is available in three forms +@itemize @bullet +@item A source tarball, @* +@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz} +@item A Linux RPM package (for any architecture), @* +@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm} +@item A developer's tarball, @* +@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz} +@end itemize + +Both the tarball and the RPM package include the generic elisp code, +code for LEGO, Coq, and Isabelle, installation instructions (reproduced +below) and this documentation. + +@c was Installing Proof General from @file{.tar.gz} +@node Installing Proof General from tarball +@section Installing Proof General from tarball + +Copy the distribution to some directory @var{mydir}. +Unpack it there. For example: +@example +# cd @var{mydir} +# gunzip ProofGeneral-@var{version}.tar.gz +# tar -xpf ProofGeneral-@var{version}.tar +@end example +If you downloaded the version called @var{latest}, you'll find it +unpacks to a numeric version number. + +Proof General will now be in some subdirectory of @var{mydir}. The name +of the subdirectory will depend on the version number of Proof General. +For example, it might be @file{ProofGeneral-2.0}. It's convenient to +link it to a fixed name: +@example +# ln -sf ProofGeneral-2.0 ProofGeneral +@end example +Now put this line in your @file{.emacs} file: +@lisp + (load-file "@var{mydir}/ProofGeneral/generic/proof-site.el") +@end lisp + +This command will load @file{proof-site} which sets the Emacs load path +for Proof General and add auto-loads and modes for the assistants below: + +@multitable @columnfractions .3 .3 .4 +@item @b{Prover} @tab @b{Extensions} @tab @b{Modes} +@item Coq @tab @file{.v} @tab @code{coq-mode} +@item LEGO @tab @file{.l} @tab @code{lego-mode} +@item Isabelle @tab @file{.thy},@file{.ML} @tab @code{isa-mode} +@end multitable +When you load a file with one of these extensions, the corresponding +Proof General mode will be entered. You can also invoke the mode +command directly. + +The default names for proof assistant binaries may work on your system. +If not, you will need to set the appropriate variables. The easiest way +to do this (and most other customization of Proof General) is via the +Customize mechanism, see the menu item: +@example + Proof-General -> Customize -> @var{Name of Assistant} -> Prog Name +@end example +The Proof-General menu is available from script buffers after +Proof General is loaded. To load it manually, type +@lisp + M-x load-library RET proof RET +@end lisp + +Notice that the customization mechanism is only available in Emacs 20.x +and XEmacs. If you cannot use customize, simply add a line like this: +@lisp + (setq isabelle-prog-name "/usr/bin/isabelle FOL") +@end lisp +to your @file{.emacs} file. + + +@node Installing Proof General from RPM package +@section Installing Proof General from RPM package + +To install an RPM package you need to be root. Then type +@example +# rpm -Uvh ProofGeneral-latest.noarch.rpm +@end example + +Now add the line: +@lisp + (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") +@end lisp +to your @file{.emacs} or the site-wide initialisation file +@file{site-start.el}. + + +@node Notes for syssies +@section Notes for syssies + +Here are some more notes for installing Proof General in more complex +ways. Only attempt things in this section if you really understand what +you're doing. + +@unnumberedsubsec Byte compilation + +Compilation of the Emacs lisp files improves efficiency but can +sometimes cause compatibility problems (especially if you use more than +one version of Emacs at the same time). + +You can compile Proof General by typing @code{make} in the directory +where you installed it. + + +@unnumberedsubsec Site-wide installation + +If you are installing Proof General site-wide, you can put the +components in the standard directories of the filesystem if you prefer, +providing the variables in @file{proof-site.el} are adjusted +accordingly, @xref{Proof General site configuration}. Make sure that +the @file{generic} and assistant-specific elisp files are kept in +subdirectories (@file{coq}, @file{isa}, @file{lego}) of +@code{proof-home-directory} so that the autoload directory calculations +are correct. + +To prevent every user needing to edit their own @file{.emacs} files, you +can put the @code{load-file} command to load @file{proof-site.el} into +@file{site-start.el} or similar. Consult the Emacs documention for more +details if you don't know where to find this file. + +@unnumberedsubsec Removing support for unwanted provers + +You cannot run more than one instance of Proof General at a time: so if +you're using Coq, visiting an @file{.ML} file will not load Isabelle +Proof General, and the buffer remains in fundamental mode. If there are +some assistants supported that you never want to use, you can adjust the +variable @code{proof-assistants} in @file{proof-site.el} to solve this +problem, @xref{Proof General site configuration}. + +@c Via the Customize mechanism, see the menu: +@c @example +@c Options -> Customize -> Emacs -> External -> Proof General +@c @end example +@c or, after loading Proof General, in a proof script buffer +@c @example +@c Proof-General -> Customize +@c @end example + + + +@c +@c +@c APPENDIX: Known bugs and workarounds +@c +@c +@node Known bugs and workarounds +@appendix Known bugs and workarounds + +We only mention a few important problems here. The list is not a +description of all bugs and may be out of date. @* +Please consult the file +@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}} +in the distribution for more detailed and up-to-date information. @* +If you discover a problem which isn't mentioned in @file{BUGS}, please +let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. + +@menu +* Bugs at the generic level:: +* Bugs specific to LEGO Proof General:: +* Bugs specific to Coq Proof General:: +* Bugs specific to Isabelle Proof General:: +@end menu + +@node Bugs at the generic level +@section Bugs at the generic level + +@unnumberedsubsec Undo in XEmacs + +When @code{proof-strict-read-only} is non-nil, ordinary undo in script +buffer can edit the "uneditable region" in XEmacs. This doesn't happen +in FSFmacs. Test case: Insert some nonsense text after the locked +region. Kill the line. Process to the next command. Press @kbd{C-x u}, +nonsense text appears in locked region. + +@strong{Workaround:} be careful with undo. + +@unnumberedsubsec Font locking and read-only in FSF Emacs + +When @code{proof-strict-read-only} is set and font lock is switched on, +spurious "Region read only" errors are given which break font lock. + +@strong{Workaround:} turn off @code{proof-strict-read-only}, font lock, +or for the best of all possible worlds, switch to XEmacs. + + +@unnumberedsubsec Pressing keyboard quit @kbd{C-g} + +Using @kbd{C-g} can leave script management in a mess. The code is not +properly protected from Emacs interrupts. + +@strong{Workaround:} Don't type @kbd{C-g} while script management is +processing. If you do, use @code{proof-restart-scripting} to restart +the system. + +@unnumberedsubsec One prover at a time +You can't use more than one proof assistant at a time in the same Emacs +session. Attempting to load Proof General for a second prover will +fail, leaving a buffer in fundamental mode instead of the Proof General +mode for proof scripts. + +@strong{Workaround:} stick to one prover per Emacs session, make sure +that the proof-assistants variables only enables Proof General for the +provers you need. + + +@node Bugs specific to LEGO Proof General +@section Bugs specific to LEGO Proof General + +@menu +* Retraction and Discharge:: +* Retraction and proving:: +@end menu + +@node Retraction and Discharge +@subsection Retraction and Discharge + +After a @code{Discharge}, retraction ought to only be possible back to +the first declaration/definition which is discharged. However, LEGO +Proof General does not know that @code{Discharge} has such a non-local +effect. See @ref{Granularity of atomic command sequences} for a proposal +on how to fix this bug. + +@strong{Workaround:} retract back to the first declaration/definition +which is discharged. + +@node Retraction and proving +@subsection Retraction and proving +@cindex Retraction + +Getting retracting right is tricky when working on proofs. + +@unnumberedsubsec Definitions in a proof state +A thorny issues are local +definitions in a proof state. LEGO cannot undo them explicitly. + +@strong{Workaround:} retract back to a command before a definition. + +@unnumberedsubsec Normalisation in proofs +Normalisation commands such as @samp{Dnf}, @samp{Hnf} @samp{Normal} +cannot be undone in a proof state by Proof General. + +@strong{Workaround:} retract back to the start of the proof. + +@unnumberedsubsec Not saving proofs. +After LEGO has issued a @samp{*** +QED ***} you may undo steps in the proof as long as you don't issue a +@samp{Save} command or start a new proof. The LEGO Proof General assumes +that all proofs are terminated with a proper @samp{Save} command. + +@strong{Workaround:} Always issue a @samp{Save} command after completing +a proof. If you forget one, you should retract to a point before the +offending proof development. + +@node Bugs specific to Coq Proof General +@section Bugs specific to Coq Proof General + +@unnumberedsubsec Hard-wired tactics + +The collection of tactics which Proof General is aware of is hard-wired. +Thus, user-defined tactics cannot be retracted. + +@strong{Workaround:} You may need to retract to the start of the proof. + +@unnumberedsubsec Sections + +The Coq Proof General does not know about Coq's section mechansim. + +@node Bugs specific to Isabelle Proof General +@section Bugs specific to Isabelle Proof General + +@unnumberedsubsec Indentation + +Isabelle Proof General doesn't support Proof General's indentation +code to indent proof scripts. In any case, Proof General's +indentation code is somewhat broken. + +@strong{Workaround:} indent your script by hand. + +@unnumberedsubsec Scripting lanugage limitations + +Since Isabelle uses ML as a top-level language for writing +proof-scripts, Proof General may have difficulty understanding scripts +which stray too far away from the standard functions, tactics, and +tacticals. You will usually notice when a function, or whatever, +doesn't get highlighted as you might expect. This probably has no +detrimental impact on the interface unless you use your own variants +of the @code{goal} or @code{qed} forms. + +@strong{Workaround:} Restrict yourself to standard proof script +functions, or customize some of the variables from @file{isa.el} and +@file{isa-syntax.el} appropriately. + +@unnumberedsubsec Interaction with theory database + +Isabelle Proof General has a fragment written in ML which defines a +modified interface to the theory database. In particular, some internal +state records which files have been retracted by the interface, although +no changes are made inside Isabelle itself. This means that +re-asserting a retracted file does not need to re-load it if it has not +changed. (It is a shame that the standard theory loader provides no +such "retraction" mechanism for unlinking loaded theories). + +This means that Proof General can get confused if you use the theory +loader primitives directly in the proof shell, and the state inside +Emacs may not agree with Isabelle. You have been warned! + +@node Plans and ideas +@appendix Plans and ideas + +This section contains some tentative plans and ideas for improving Proof +General. Please send us contributions to this wish list, or better +still, offers to implement something from it! + +@menu +* 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. + +In fact, Proof General already contains code for proof by pointing, for +a reference @xref{Credits and References}. However, it is slightly LEGO +specific and not robust enough. + +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 might be specific to a +particular logic in use, if we hope to generate a proof command +unambiguously for any particular click. However, it 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. + +@node Granularity of atomic command sequences +@section Granularity of atomic command sequences +@c @cindex Granularity of Atomic Sequences +@c @cindex Retraction +@c @cindex Goal +@cindex ACS (Atomic Command Sequence) + +This is a proposal by Thomas Kleymann for generalising the way Proof +General handles sequences of proof commands @pxref{Goal-save sequences}, +particularly to make retraction more flexible. + +The locked region of a script buffer contains the initial segment of +the proof script which has been processed successfully. It consists of +atomic sequences of commands (ACS). Retraction is supported to the +beginning of every ACS. By default, every command is an ACS. But the +granularity of atomicity can be adjusted for different proof assistants. +This is essential when arbitrary retraction is not supported. Usually, +after a theorem has been proved, one may only retract to the start of +the goal. One needs to mark the proof of the theorem as an ACS. + +@vtable @code +@item proof-atomic-sequents-list +is a list of instructions for setting up ACSs. Each instruction is a +list of the form @code{(@var{end} @var{start} &optional +@var{forget-command})}. @var{end} is a regular expression to recognise +the last command in an ACS. @var{start} is a function. Its input is the +last command of an ACS. Its output is a regular expression to recognise +the first command of the ACS. It is evaluated once and the output is +successively matched against previously processed commands until a match +occurs (or the beginning of the current buffer is reached). The region +determined by (@var{start},@var{end}) is locked as an ACS. Optionally, +the ACS is annotated with the actual command to retract the ACS. This is +computed by applying @var{forget-command} to the first and last command +of the ACS. +@end vtable + +@node Browser mode for script files and theories +@section Browser mode for script files and theories + +This is a proposal by David Aspinall for a browser window. + +A browser window should provide support for browsing script files and +theories. We should be able to inspect data in varying levels of +detail, perhaps using outlining mechanisms. For theories, it would be +nice to query the running proof assistant. This may require support +from the assistant in the form of output which has been specially +marked-up with an SGML like syntax, for example. + +A browser would be useful to: +@itemize @bullet +@item Provide impoverished proof assistants with a browser +@item Extend the uniform interface of Proof General to theory browsing +@item Interact closely with proof script-writing +@end itemize +The last point is the most important. We should be able to integrate a +search mechanism for proofs of similar theorems, theorems containing +particular constants, etc. + + + + +@node Function Index +@unnumbered Function and Command Index @printindex fn -@node Concept Index,,Function Index, Top -@comment node-name, next, previous, up -@unnumbered Concept Index +@node Variable Index +@unnumbered Variable and User Option Index +@printindex vr + +@node Keystroke Index +@unnumbered Keystroke Index +@printindex ky + +@node Index +@unnumbered Index @printindex cp +@page +@contents @bye + + |