Basic description of script management, compiled for emacs info mode.

1 files changed, 433 insertions, 0 deletions

diff --git a/script-management.info b/script-management.info
new file mode 100644
index 00000000..8640a092
--- /dev/null
+++ b/script-management.info
@@ -0,0 +1,433 @@
+This is Info file script-management.info, produced by Makeinfo version
+1.68 from the input file script-management.texinfo.
+
+
+File: script-management.info,  Node: Top,  Next: Introduction,  Prev: (dir),  Up: (dir)
+
+A *proof script* is a sequence of commands to a proof assistant.  Proof
+mode is a mode designed to be customised for a particular proof
+assistant, to manage communication with a proof process and thereby
+support building and secure editing of proof scripts.  Currently custom
+modes exist for LEGO and Coq.
+
+* Menu:
+
+* Introduction::          Introduction to Script Management
+* Commands::              Proof mode Commands
+* Multiple Files::        Proof developments spanning several files
+* Proof by Pointing::     Proof using the Mouse
+* An Active Terminator::  Active Terminator minor mode
+* Walkthrough::           An example of using proof mode
+* LEGO mode::             Extra Bindings for LEGO
+* Coq mode::              Extra Bindings for Coq
+* Internals::             The Seedy Underside of Proof mode
+* Known Problems::        Caveat Emptor
+
+
+File: script-management.info,  Node: Introduction,  Next: Commands,  Prev: Top,  Up: Top
+
+Introduction
+============
+
+Each script resides in an Emacs buffer, called a *script buffer*, which
+is divided into three regions:
+
+   * The *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.
+
+   * The *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.
+
+   * The *Editing* region contains the commands the user is working on,
+     and can be edited as normal Emacs text.
+
+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, and Emacs will summarise the results in the
+*Response Buffer*.
+
+*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.  *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.
+
+
+File: script-management.info,  Node: Commands,  Next: Multiple Files,  Prev: Introduction,  Up: Top
+
+Proof Mode Commands
+===================
+
+`C-c C-b'
+     assert the commands in the buffer.
+
+`C-c return'
+     assert the commands in the editing region up to and including the
+     one containing the point.
+
+`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-c C-u'
+     retract the last segment in the locked region, and kill the text
+     in it.  (1)
+
+`C-c ''
+     move the point to the end of the locked region
+
+`C-c C-e'
+     move the point to the next terminator
+
+`C-c C-c'
+     interrupt the process process. This may leave script management or
+     the proof process (or both) in an inconsistent state.
+
+`C-c C-z'
+     move the end of the locked region backwards to the end of the
+     segment containing the point. (2)
+
+`C-c C-t'
+     Send the command at the point to the subprocess, not recording it
+     in the locked region. (3)
+
+`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.
+
+The command `proof-restart-script' can be used to completely restart
+script management.
+
+---------- Footnotes ----------
+
+(1) Be careful with this, as it may delete more than you anticipate.
+However, you can always recover the killed text using Emacs Undo.
+
+(2) Don't try this one at home, kids.
+
+(3) 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.
+
+
+File: script-management.info,  Node: Multiple Files,  Next: An Active Terminator,  Prev: Commands,  Up: Top
+
+Multiple Files
+==============
+
+Proof mode has a rudimentary facility for operating with multiple files
+in a LEGO proof development. If the user invokes script management in a
+different buffer from the one in which it is running, one of two prompts
+will appear:
+
+   * "Steal script management?"  if Emacs doesn't think the file is
+     already part of the proof development
+
+   * "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.
+
+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 `Scripting' appears in the minor mode list of the active
+scripting buffer.
+
+Caveats:
+   - 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.
+
+   - 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.
+
+
+File: script-management.info,  Node: An Active Terminator,  Next: Proof by Pointing,  Prev: Multiple Files,  Up: Top
+
+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 (`;' for
+LEGO, `.' 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' (`C-c ;' or `C-c .')
+
+
+File: script-management.info,  Node: Proof by Pointing,  Next: Walkthrough,  Prev: An Active Terminator,  Up: Top
+
+Proof by Pointing
+=================
+
+*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 response 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
+`User Interfaces for Theorem Provers' by Yves Bertot and Laurent Thery,
+to appear in `Information and Computation', from which the following
+example is taken.
+
+* Menu:
+
+* Proof by Pointing Example::          An example using proof by pointing
+
+
+File: script-management.info,  Node: Proof by Pointing Example,  Prev: Proof by Pointing,  Up: Proof by Pointing
+
+Suppose we wish to prove the lego term:
+
+     (((p a) \/ (q b))  /\ {x:Prop}(p x) -> (q x)) -> (Ex ([x:Prop] q(x)));
+
+Asserting this goal will result in the proof state
+
+     ?0 : ((p a \/ q b) /\ {x:Prop}(p x)->q x)->Ex ([x:Prop]q x)
+
+appearing in the response buffer. Suppose our strategy is to use a case
+analysis on the disjunction, starting with the `p(a)' subterm.
+Clicking on this term will cause script management to insert the
+following command sequence in the script buffer, and execute it.
+
+     Intros H; Refine H; Intros H0 H1;
+     Refine or_elim H0 Then Intros H2; Try Refine H2;
+
+The response buffer will then read
+
+       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)
+
+Clicking on the subterm `(p x)' in the hypothesis H1 will instruct
+script management to prove an instance of `(p x)' and deduce the
+corresponding `(q x)'. The commands
+
+     allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption;
+
+are inserted and executed, leaving the proof state as
+
+       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)
+
+Now clicking on the `q x)' subterm in ?20 will prove the subgoal. We are
+left with the other half of the original case analysis:
+
+       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)
+
+Clicking on `q x' proves the goal.
+
+
+File: script-management.info,  Node: Walkthrough,  Next: LEGO mode,  Prev: Proof by Pointing,  Up: Top
+
+A Walkthrough
+=============
+
+Here's a LEGO example of how script management is used.
+
+First, we turn on active terminator minor mode by typing `C-c ;' Then
+we enter
+
+`Module Walthrough 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
+response buffer 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)
+
+`Goal bland_commutes: {A,b:Prop} and A B -> and B A;'
+
+The goal should be echoed in the response buffer.
+
+`Intros;'
+
+Whoops! `C-c C-u' to pretend that didn't happen.
+
+`intros; andI;'
+
+A proof summary will appear in the response buffer. We could solve the
+goal by pointing now, but we'll stay with the keyboard.
+
+`Refine H; intros; Immed; Refine H; intros; Immed;'
+
+finishes the Goal.
+
+`Save;'
+
+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
+`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 `C-c return'.  Proof mode queues the commands for processing and
+executes them.
+
+
+File: script-management.info,  Node: LEGO mode,  Next: Coq mode,  Prev: Walkthrough,  Up: Top
+
+LEGO mode
+=========
+
+LEGO mode is a mode derived from proof mode for editing LEGO scripts.
+As well as custom popup menus, it has the following commands:
+
+`C-c C-p'
+     display the proof state in the response buffer
+
+`C-c c'
+     display the context in the response buffer
+
+`C-c c'
+     print LEGO help text in the response buffer
+
+In addition, there are some abbreviations for common commands
+
+`C-c i'
+     intros
+
+`C-c I'
+     Intros
+
+`C-c R'
+     Refine
+
+
+File: script-management.info,  Node: Coq mode,  Next: Known Problems,  Prev: LEGO mode,  Up: Top
+
+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:
+
+`C-c C-p'
+     display the proof state in the response buffer
+
+`C-c c'
+     display the context in the response buffer
+
+In addition, there are some abbreviations for common commands:
+
+`C-c I'
+     Intros
+
+`C-c a'
+     Apply
+
+
+File: script-management.info,  Node: Known Problems,  Next: Internals,  Prev: Coq mode,  Up: Top
+
+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
+`proof-restart-script-management' may be of use.
+
+A few things to avoid:
+
+   - If you're using script management with multiple files, don't start
+     changing the file names.
+
+   - Script Management doesn't understand how to undo `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
+     `Discharge' command, retract back to the declaration of whatever
+     gets discharged.
+
+   - Proof by Pointing doesn't work very well, and is inefficiently
+     implemented.
+
+   - The locked and queue regions are not quite read-only: in particular
+     Emacs Undo can insert text into them.
+
+   - 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.
+
+Fixes for some of these may be provided in a future release.
+
+
+File: script-management.info,  Node: Internals,  Prev: Known Problems,  Up: Top
+
+Internals
+=========
+
+I may one day document the script management internals here. Until then,
+UtSL.
+
+
+
+Tag Table:
+Node: Top124
+Node: Introduction1065
+Node: Commands3509
+Node: Multiple Files5229
+Node: An Active Terminator6730
+Node: Proof by Pointing7309
+Node: Proof by Pointing Example8569
+Node: Walkthrough10244
+Node: LEGO mode11791
+Node: Coq mode12346
+Node: Known Problems12822
+Node: Internals14161
+
+End Tag Table