Info file is easily generated from texinfo, so doesn't belong in CVS

1 files changed, 0 insertions, 433 deletions

diff --git a/script-management.info b/script-management.info
deleted file mode 100644
index 8640a092..00000000
--- a/script-management.info
+++ /dev/null
@@ -1,433 +0,0 @@
-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