diff options
| -rw-r--r-- | doc/NewDoc.texi | 836 |
1 files changed, 232 insertions, 604 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index a8c18e31..941c35a6 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -17,9 +17,19 @@ @c . finish incomplete sections @c . polish mark-up @c . add more index entries -@c . screenshots might be nice +@c . screenshots might be nice (one day) @c +@c NB: try keep full node lines out of this file because Emacs makes a +@c mess of updating them in general. Instead, rely on makeinfo +@c and friends to do the equivalent job. For this to work, +@c we write nodes in the form: +@c +@c @node node-name +@c <section-command> +@c +@c + @set version 2.0 @set xemacsversion 20.4 @@ -34,6 +44,14 @@ END-INFO-DIR-ENTRY @end format @end ifinfo +@c +@c MACROS +@c +@c define one here for a command with a keybinding? +@c +@c I like the idea, but it's maybe against the texinfo +@c style to fix together a command and its keybinding. + @c merge functions and variables into concept index. @syncodeindex fn cp @@ -130,7 +148,7 @@ Basic Script Management * Script editing commands:: * Script processing commands:: * Toolbar commands:: -* Other commands:: +* Proof assistant commands:: * Walkthrough example in LEGO:: Proof scripts @@ -152,7 +170,7 @@ Support for other Packages Customizing Proof General * Easy customization:: -* Setting user options:: +* Setting the user options:: * Running on another machine:: * Tweaking configuration settings:: @@ -183,9 +201,9 @@ Proof shell settings Internals of Proof General -* Proof Script Mode:: -* Proof Shell Mode:: -* Handling Multiple Files:: +* Proof script mode:: +* Proof shell mode:: +* Handling multiple files:: Credits and References @@ -206,8 +224,8 @@ Obtaining and Installing Proof General @node Introducing Proof General @chapter Introducing Proof General -@cindex{proof assistant} -@cindex{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. @@ -271,8 +289,8 @@ see @pxref{Obtaining and Installing Proof General}. @node Features of Proof General @section Features of Proof General -@cindex{Features} -@cindex{Why use Proof General?} +@cindex Features +@cindex Why use Proof General? Why would you want to use Proof General? @@ -312,7 +330,7 @@ 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{Other commands}, +For more details, see @pxref{Toolbar commands}, @pxref{Proof assistant commands}, and @pxref{Customizing Proof General}. @c not yet @@ -367,7 +385,7 @@ for more details of how to do this. @c @c CHAPTER: Basic Script Management @c -@node Basic Script Management, Advanced Script Management, Introducing Proof General, Top +@node Basic Script Management @chapter Basic Script Management @menu @@ -377,11 +395,11 @@ for more details of how to do this. * Script editing commands:: * Script processing commands:: * Toolbar commands:: -* Other commands:: +* Proof assistant commands:: * Walkthrough example in LEGO:: @end menu -@node Proof scripts, The buffer model, Basic Script Management, Basic Script Management +@node Proof scripts @section Proof scripts @cindex proof script @@ -413,7 +431,7 @@ file, while it is written and edited. * Goals and saves:: @end menu -@node Goals and saves, , Proof scripts, Proof scripts +@node Goals and saves @unnumberedsubsec Goals and saves @cindex goal @cindex save @@ -437,7 +455,7 @@ once a goal-save region has been processed by the proof assistant, it is treated as atomic when undoing proof steps. -@node The buffer model, Regions in a proof script, Proof scripts, Basic Script Management +@node The buffer model @section The buffer model @cindex script buffer @cindex goals buffer @@ -480,9 +498,37 @@ assistant, for example warning or informative messages. @node Script editing commands @section Script editing commands +@kindex C-c C-e + + @node Script processing commands @section Script processing commands +@kindex C-c C-n +@kindex C-c C-p +@kindex C-c RET +@kindex C-c u +@kindex C-c C-u + + +@deffn Command proof-assert-next-command +@end deffn + +@deffn Command proof-undo-last-successful-command +@end deffn + +@deffn Command proof-try-command +@end deffn + +@deffn Command proof-retract-until-point +@end deffn + +@deffn Command proof-process-buffer +@end deffn + + + + @c FIXME: requires formatting Why is C-c C-b useful? Could just use the file to read it one go @@ -495,13 +541,41 @@ continue development from there. @node Toolbar commands @section Toolbar commands -@node Other commands -@section Other commands +@node Proof assistant commands +@section Proof assistant commands +@kindex C-c C-p +@kindex C-c c +@kindex C-c h + +@deffn Command proof-prf +List proof state. +@end deffn + +@deffn Command proof-ctxt +List context. +@end deffn + +@deffn Command proof-help +Print help message giving syntax. +@end deffn + +@deffn Command proof-execute-minibuffer-cmd +Prompt for a command in the minibuffer and send it to proof assistant. +@end deffn + +@deffn Command proof-interrupt-process +Interrupt the proof assistant. WARNING! This may confuse Proof General. +@end deffn + + + +@c Please explain C-c C-v here. + +@c Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working +@c directly with the proof shell} + -Please explain C-c C-v here. -Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working -directly with the proof shell} @node Walkthrough example in LEGO @section Walkthrough example in LEGO @@ -575,7 +649,7 @@ assistant explicitly telling the Proof General whenever it processes a new file which corresponds@footnote{For example, LEGO generates additional compiled (optimised) proof script files for efficiency.} to a file containing a proof script. For further technical -details, @pxref{Handling Multiple Files}. +details, @pxref{Handling multiple files}. If the current proof script buffer depends on background material from other files, proof assistants typically process these files @@ -636,8 +710,7 @@ 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{Other commands}. - +@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 @@ -691,7 +764,7 @@ fume-func is a handy package which makes a menu from the function declarations in a buffer. Proof General configures fume-func so that you can quickly jump to particular proofs in a script buffer. This is done with the configuration variable @code{proof-goal-with-hole-regexp}, -@pxref{Proof Script Mode} for further details. +@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 @@ -736,7 +809,7 @@ See the chapters covering each assistant for details. @menu * Easy customization:: -* Setting user options:: +* Setting the user options:: * Tweaking configuration settings:: @end menu @@ -783,21 +856,21 @@ file. For more help, see @inforef{Easy Customization, ,xemacs}. -@node Setting user options -@section Setting user options +@node Setting the user options +@section Setting the user options @c Index entries for each option 'concept' -@cindex{User options} -@cindex{Strict read-only} -@cindex{Query program name} -@cindex{Dedicated windows} -@cindex{Remote host} -@cindex{Toolbar follow mode} -@cindex{Toolbar disabling} -@cindex{Proof script indentation} -@cindex{Indentation} -@cindex{Remote shell} -@cindex{Running proof assistant remotely} -@c @cindex{formatting proof script} +@cindex User options +@cindex Strict read-only +@cindex Query program name +@cindex Dedicated windows +@cindex Remote host +@cindex Toolbar follow mode +@cindex Toolbar disabling +@cindex Proof script indentation +@cindex Indentation +@cindex Remote shell +@cindex Running proof assistant remotely +@c @cindex formatting proof script Here are the user options for Proof General. These can be set via the @@ -876,15 +949,17 @@ script. This option is not fully-functional at the moment. @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. Occasionally you may like to adjust some of these settings to -improve the way Proof General works. Ideally this should not be -necessary. One case when it may be necessary is 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. +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 @@ -896,7 +971,7 @@ One basic example of a setting you may like to tweak is: @defvar proof-assistant-home-page Web address for information on proof assistant. -@end var +@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 @@ -908,9 +983,15 @@ 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. At -present there is no easy way to get around this other than by editing -the source code. Please contact us if this proves to be a problem. +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. + @node LEGO Proof General @@ -1041,14 +1122,17 @@ in your @file{~/.emacs} file. @menu * Isabelle specific commands:: * Isabelle customizations:: -* Theory file editing @end menu + + @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 @@ -1060,15 +1144,55 @@ theory file. @deffn Command thy-find-other-file Find and switch to the associated ML file (when editing a theory file) or theory file (when editing an ML file). + +Usually the current window is split and the new file shown in the other +window. With an optional argument (@kbd{C-u} prefix), the other file +replaces the one in the current window. @end deffn -@node @node Isabelle customizations @section Isabelle customizations -@defopt -@end opt +Here are some of the user options specific to Isabelle. You can set +these with the customization mechanism as usual. + +@defopt isabelle-web-page +A string containing a URL for a web page for Isabelle. +@end defopt + + +@c @unnumberedsubsec Theory file editing customization + +@defopt thy-use-sml-mode +If non-nil, attempt to use sml-mode in ML section of theory files. +This option is left-over from Isamode. Really, it would be more +useful if the script editing mode of Proof General itself could be based +on sml-mode, but at the moment there is no way to do this. +@end defopt + +@defopt thy-indent-level +Indentation level for Isabelle theory files. An integer. +@end defopt + +@defopt thy-sections +A list containing names of theory file sections and their templates. +Each item in the list is a pair of a section name and a template. +A template is either a string to insert or a function. Useful functions are: +@code{thy-insert-header}, @code{thy-insert-class}, +@code{thy-insert-default-sort}, @code{thy-insert-const}, +@code{thy-insert-rule}. The nil template does nothing. +You can add extra sections to theory files by extending this variable. +@end defopt + +@defopt thy-template +Template for theory files. +Contains a default selection of sections in a traditional order. +You can use the following format characters: + @code{%t} -- replaced by theory name + @code{%p} -- replaced by names of parents, separated by @code{+}'s +@end defopt + @@ -1144,20 +1268,20 @@ of @var{proof-assistants-table} for more details. @chapter Internals of Proof General @menu -* Proof Script Mode:: -* Proof Shell Mode:: -* Handling Multiple Files:: +* Proof script mode:: +* Proof shell mode:: +* Handling multiple files:: @end menu -@node Proof Script Mode -@section Proof Script Mode +@node Proof script mode +@section Proof script mode -@node Proof Shell Mode -@section Proof Shell Mode +@node Proof shell mode +@section Proof shell mode -@node Handling Multiple Files -@section Handling Multiple Files -@cindex Multiple Files +@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 @@ -1589,505 +1713,25 @@ functions, or customize some of the variables from @file{isa.el} and @node Plans and ideas @appendix Plans and ideas - - -@node Keystroke Index -@unnumbered Keystroke Index -@printindex ky - -@node Index -@unnumbered Index -@printindex cp - -@page -@contents -@bye - - -@c -@c OLD TEXI STUFF HERE -@c -@c WARNING --- DO NOT EDIT BELOW HERE!! -@c - - - - - - - -@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: - -@itemize @bullet -@item -@b{LEGO Proof General} for LEGO Version 1.3.1@* -by Thomas Kleymann and Dilip Sequeira -@item -@b{Coq Proof General} for Coq Version 6.2@* -by Healfdene Goguen -@item -@b{Isabelle Proof General} for Isabelle 98-1@* -by David Aspinall -@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. - -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. - - - - -****************** - - - -@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:: -@end menu - - -@node Introduction, Commands, Top, Top -@comment node-name, next, previous, up -@unnumberedsec Introduction - -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: - -@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 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! - - - -@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. - -@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 -@section Proof Mode Commands - -@table @kbd - -@item C-c C-b -assert the commands in the buffer. - -@item C-c return -assert the commands in the editing region up to and -including the one containing the point. - -@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. - -@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. - -@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 - -@item C-c h -print proof-system specific help text in the process buffer - -@item C-c C-c -interrupt the process. This may leave script management or the -proof process (or both) in an inconsistent state. - -@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.} - -@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.} - -@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. -@end table - -The command @code{proof-restart-script} can be used to completely -restart script management. - - -@node Multiple Files, An Active Terminator, Commands, Top -@section Multiple Files - -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: - -@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 - -Currently this facility requires each script buffer to have a -corresponding file. - -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. - -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. - -@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 - -@node An Active Terminator, Proof by Pointing, Multiple Files, Top -@section An Active Terminator - -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 -@section 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. - -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 -@end menu - -@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing - -Suppose we wish to prove the lego term: - -@example -(((p a) \/ (q b)) /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x))); -@end example - -Asserting this goal will result in the proof state - -@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. - -@example -Intros H; Refine H; Intros H0 H1; -Refine or_elim H0 Then Intros H2; Try Refine H2; -@end example - - -The goals buffer will then read - -@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 - -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 - -@example -allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption; -@end example - -are inserted and executed, leaving the proof state as - -@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 - -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 Walkthrough, LEGO mode, Proof by Pointing, Top -@section A Walkthrough - -Here's a LEGO example of how script management is used. - -First, we turn on active terminator minor mode by typing @kbd{C-c ;} -Then we enter - -`Module Walkthrough Import lib_logic;' - -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) - -@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);} - -The goal should be echoed in the goals buffer. - -@samp{Intros;} - -Whoops! @kbd{C-c C-u} to pretend that didn't happen. - -@samp{intros; andI;} - -A proof summary will appear in the goals buffer. We could solve the -goal by pointing now, but we'll stay with the keyboard. - -@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 LEGO mode, Coq mode, Walkthrough, Top -@section LEGO mode - -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: - -@table @kbd -@item C-c i -intros -@item C-c I -Intros -@item C-c R -Refine -@end table - - -@node Coq mode, Known Problems, LEGO mode, Top -@section Coq mode - -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 - -@item C-c C-s -search for items in the library of a given type. This runs the -@kbd{Search} command of Coq. - -@end table - -In addition, there are some abbreviations for common commands, which -add text to the buffer: - -@table @kbd -@item C-c I -Intros -@item C-c a -Apply -@end table - -@node Known Problems, Internals, Coq mode, Top -@section Known Problems - -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. - -A few things to avoid: - -@itemize @minus -@item If you're using script management with multiple files, don't start -changing the file names. - -@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. - -@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 - -Fixes for some of these may be provided in a future release. - -@node Internals, Variable Index, Known Problems, Top -@comment node-name, next, previous, up -@section Internals +This section contains some tentative plans and ideas for improving Proof +General. Please send us contributions to this wish list, or better +still, offers to implement something from it! @menu * Granularity of Atomic Command Sequences:: -* Handling Multiple Files:: -* Adding A New Proof Assistant:: -* Literature:: +* Browser mode for script files and theories:: @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 Granularity of Atomic Command Sequences +@section Granularity of Atomic Commands +@c @cindex Granularity of Atomic Sequences +@c @cindex Retraction +@c @cindex Goal +@c @cindex ACS (Atomic Command Sequence) + +This is a proposal by Thomas Kleymann for generalising the way Proof +General handles sequences of proof commands @pxref{Goals and saves}, +particularly to make retraction more flexible. The *Locked* region of a script buffer contains the initial segment of the proof script which has been processed successfully. It consists of @@ -2114,56 +1758,40 @@ computed by applying @var{forget-command} to the first and last command of the ACS. @end vtable -@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 +@node Browser mode for script files and theories +@section Browser mode for script files and theories -Suppose your new assistant is -called myassistant. +This is a proposal by David Aspinall for a browser window. -@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-assistants-table} variable. The new entry should -look like this: - - (myassistant "My New Assistant" "\\.myasst$") +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. -The first item is used to form the name of the internal variables -for the new mode as well as the directory and file where it loads -from. The second is a string, naming the proof assistant. -The third item is a regular expression to match names of -proof script files for this assistant. See the documentation -of @var{proof-assistants-table} for more details. -@item Define the new modes in myassistant.el, by looking at - the files for the currently supported assistants for example. - Basically you need to define some modes using @code{define-derived-mode} - and set the configuration variables. You could begin by setting - a minimum number of the variables, then adjust the - settings via the customize menus, under Proof-General -> Internals. +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 Literature, , Adding A New Proof Assistant, Internals -@comment node-name, next, previous, up -@unnumberedsubsec Literature -The current version supports Script Management as documented in: -@itemize @bullet -@item -Yves Bertot and Laurent Th@'ery. A generic approach to building -user interfaces for theorem provers. To appear in Journal of -Symbolic Computation. -@end itemize +@node Keystroke Index +@unnumbered Keystroke Index +@printindex ky + +@node Index +@unnumbered Index +@printindex cp + +@page +@contents +@bye -It has the beginnings of support for Proof by Pointing, as documented in: -@itemize @bullet -@item -Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. 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 |