path: root/script-management.info

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