3. Advanced Script Management and Editing
If you are working with large proof developments, you may want to know about the advanced script management and editing features of Proof General covered in this chapter.
3.1 Document centred working
Proof scripts can be annotated with the output produced by the prover while they are checked. By hovering the mouse on the completed regions you can see any output that was produced when they were checked. Depending on the proof language (it works well with declarative languages), this may enable a “document centred” way of working, where you may not need to keep a separate window open for displaying prover output.
This way of working is controlled by several settings. To help configure things appropriately for document-centred working, there are two short-cut commands:
Proof-General -> Quick Options -> Display -> Document Centred Proof-General -> Quick Options -> Display -> Default
which change settings appropriately between a document centred mode and the original classic Proof General behaviour and appearance. The first command also engages automatic processing of the whole buffer, explained in the following section further below.
The behaviour can be fine-tuned with the individual settings. Starting with the classic settings, first, you may select
Proof-General -> Quick Options -> Processing -> Full Annotations
to ensure that the details are recorded in the script. This is not the default because it can cause long sequences of commands to execute more slowly as the output is collected from the prover eagerly when the commands are executed, and printing can be be slow for large and complex expressions. It also increases the space requirements for Emacs buffers. However, when interactively developing smaller files, it is very useful.
Next, you may deselect
Proof-General -> Quick Options -> Display -> Auto Raise
which will prevent the prover output being eagerly displayed. You can still manually arrange your Emacs windows and frames to ensure the output buffers are present if you want.
You may like to deselect
Proof General -> Quick Options -> Display -> Colour Locked
to prevent highlighting of the locked region. This text which has been checked and that which has not is less obvious, but you can see the position of the next command to be processed with the marker.
If you have no colouring on the locked region, it can be hard to see where processing has got to. Look for the “overlay marker”, a triangle in the left-hand fringe of the display, to see which line processing has stopped at. If it has stopped on a region with an error, you might want to see that. You can select
Proof-General -> Quick Options -> Display -> Sticky Errors
to add a highlight for regions which did not successfully process on the last attempt. Whenever the region is edited, the highlight is removed.
Finally, you may want to ensure that
Proof-General -> Quick Options -> Read Only -> Undo On Edit
Undo on edit is a setting for the
This allows you to freely edit the processed region, but first it
automatically retracts back to the point of the edit. Comments can
be edited freely without retraction.
The configuration variables controlled by the above menu items can be
customized as Emacs variables. The two settings which control
interaction with the prover are
proof-strict-read-only. Note that you can also record the
history of output from the prover without adding mouse hovers to the
script. This is controlled by
proof-output-tooltips which is
also on the Display menu in Quick Options. See section Display customization, for more information about customizing display options.
- User Option: proof-full-annotation
Non-nil causes Proof General to record output for all proof commands.
Proof output is recorded as it occurs interactively; normally if many steps are taken at once, this output is suppressed. If this setting is used to enable it, the proof script can be annotated with full details. See also ‘
proof-output-tooltips’ to enable automatic display of output on mouse hovers.
The default value is
- User Option: 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, except for the special value
'retractwhich means undo first. If nil, Proof General is more relaxed (but may give you a reprimand!).
The default value is
3.2 Automatic processing
If you like making your hair stand on end, the electric terminator mode is probably not enough. Proof General has another feature that will automatically send text to the prover, while you aren’t looking.
Proof-General -> Quick Options -> Processing -> Process Automatically
Causes Proof General to start processing text when Emacs is idle for a while. You can choose either to send just the next command beyond the point, or the whole buffer. See
Proof-General -> Quick Options -> Processing -> Automatic Processing Mode
for the choices.
The text will be sent in a fast loop that processes more quickly than
C-c C-b (i.e.,
proof-process-buffer, the down toolbar
button), but ignores user input and doesn’t update the display. But the
feature tries to be non-intrusive to the user: if you start to type
something or use the mouse, the fast loop will be interrupted and revert
to a slower interactive loop with display updates.
In the check next command mode, the successfully checked region will briefly flash up as green to indicate it is okay.
You can use C-c C-. (
proof-goto-end-of-locked) to find out
where processing got to, as usual. Text is only sent if the last
interactive command processed some text (i.e., wasn’t an undo step
backwards into the buffer) and processing didn’t stop with an error. To
start automatic processing again after an error, simply hit C-c
C-n after editing the buffer. To turn the automatic processing on or
off from the keyboard, you can use the key binding:
- C-c >
- Command: proof-autosend-toggle &optional arg
proof-autosend-enable’. With arg, turn on iff ARG>0.
This function simply uses
customize-set-variableto set the variable.
3.3 Visibility of completed proofs
Large developments may consist of large files with many proofs. To help see what has been proved without the detail of the proof itself, Proof General can hide portions of the proof script. Two different kinds of thing can be hidden: comments and (what Proof General designates as) the body of proofs.
You can toggle the visibility of a proof script portion by using the
context sensitive menu triggered by clicking the right mouse button
on a completed proof, or the key C-c v, which runs
You can also select the “disappearing proofs” mode from the menu,
Proof-General -> Quick Options -> Display -> Disappearing Proofs
This automatically hides each the body of each proof portion as it is completed by the proof assistant. Two further menu commands in the main Proof-General menu, Show all and Hide all apply to all the completed portions in the buffer.
Notice that by design, this feature only applies to completed proofs, after they have been processed by the proof assistant. When files are first visited in Proof General, no information is stored about proof boundaries.
The relevant elisp functions and settings are mentioned below.
- User Option: proof-disappearing-proofs
Non-nil causes Proof General to hide proofs as they are completed.
The default value is
3.4 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(5) ‘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 ‘sos.l’ and retract to where changes are required. Then, using script management, you want to develop some more basic theory in ‘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 switch back to ‘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.
3.5 View of processed files
Proof General tries to be aware of all files that the proof assistant has processed or is currently processing. In the best case, it relies on the proof assistant explicitly telling it whenever it processes a new file which corresponds(6) to a file containing a proof script.
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 beginning of the buffer.
Unlike a script buffer that has been processed step-by-step via Proof General, automatically loaded script buffers do not pass through a “red” phase to indicate that they are currently being processed. This is a limitation of the present implementation. Proof General locks a buffer as soon as it sees the appropriate message from the proof assistant. Different proof assistants may use different messages: either early locking when processing a file begins (e.g. LEGO) or late locking when processing a file ends (e.g. Isabelle).
With early locking, you may find that a script which has only been partly processed (due to an error or interrupt, for example), is wrongly completely locked by Proof General. Visit the file and retract back to the start to fix this.
With late locking, there is the chance that you can break synchronization by editing a file as it is being read by the proof assistant, and saving it before processing finishes.
In fact, there is a general problem of editing files which may be processed by the proof assistant automatically. Synchronization can be broken whenever you have unsaved changes in a proof script buffer and the proof assistant processes the corresponding file. (Of course, this problem is familiar from program development using separate editors and compilers). The good news is that Proof General can detect the problem and flashes up a warning in the response buffer. You can then visit the modified buffer, save it and retract to the beginning. Then you are back on track.
3.6 Retracting across files
Make sure that the current script buffer has either been completely asserted or retracted (Proof General enforces this). 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 see section 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.
3.7 Asserting across files
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, see section 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.
3.8 Automatic multiple file handling
To make it easier to adapt Proof General for a proof assistant, there is another possibility for multiple file support — that it is provided automatically by Proof General and not integrated with the file-management system of the proof assistant.
In this case, Proof General assumes that the only files processed are the ones it has sent to the proof assistant itself. Moreover, it (conservatively) assumes that there is a linear dependency between files in the order they were processed.
If you only have automatic multiple file handling, you’ll find that any files loaded directly by the proof assistant are not locked when you visit them in Proof General. Moreover, if you retract a file it may retract more than is strictly necessary (because it assumes a linear dependency).
For further technical details of the ways multiple file scripting is configured, see Handling multiple files in the Adapting Proof General manual.
3.9 Escaping script management
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, see section Proof assistant commands.
Although the proof shell is usually hidden from view, it is run in a buffer which you can use to interact with the prover if necessary. You can switch to it using the menu:
Proof-General -> Buffers -> Shell
Warning: you can probably cause confusion by typing in the shell buffer! Proof General may lose track of the state of the proof assistant. Output from the assistant is only fully monitored when Proof General is in control of the shell. When in control, 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. What happens when you type in the shell buffer directly depends on how complete the communication is between Proof General and the prover (which depends on the particular instantiation of Proof General).
If synchronization is lost, you have two options to resynchronize. If you are lucky, it might suffice to use the key:
- C-c C-z
This command is disabled by default, to protect novices using it accidently.
proof-frob-locked-end does not work, you will need to restart
script management altogether (see section Proof assistant commands).
- Command: proof-frob-locked-end
Move the end of the locked region backwards to regain synchronization.
Only for use by consenting adults.
This command can be used to repair synchronization in case something goes wrong and you want to tell Proof General that the proof assistant has processed less of your script than Proof General thinks.
You should only use it to move the locked region to the end of a proof command.
3.10 Editing features
To make editing proof scripts more productive, Proof General provides some additional editing commands.
One facility is the input ring of previously processed commands.
This allows a convenient way of repeating an earlier command or a small
edit of it. The feature is reminiscent of history mechanisms provided
in shell terminals (and the implementation is borrowed from the Emacs
Comint package). The input ring only contains commands which have been
successfully processed (coloured blue). Duplicated commands are only
The size of the ring is set by the variable
- Command: pg-previous-input arg
Cycle backwards through input history, saving input.
If called interactively, arg is given by the prefix argument.
- Command: pg-next-input arg
Cycle forwards through input history.
If called interactively, arg is given by the prefix argument.
- Command: pg-previous-matching-input regexp n
Search backwards through input history for match for regexp.
(Previous history elements are earlier commands.) With prefix argument n, search for Nth previous match. If n is negative, find the next or Nth next match.
- Command: pg-next-matching-input regexp n
Search forwards through input history for match for regexp.
(Later history elements are more recent commands.) With prefix argument n, search for Nth following match. If n is negative, find the previous or Nth previous match.
- Command: pg-previous-matching-input-from-input n
Search backwards through input history for match for current input.
(Previous history elements are earlier commands.) With prefix argument n, search for Nth previous match. If n is negative, search forwards for the -Nth following match.
- Command: pg-next-matching-input-from-input n
Search forwards through input history for match for current input.
(Following history elements are more recent commands.) With prefix argument n, search for Nth following match. If n is negative, search backwards for the -Nth previous match.
This document was generated by Erik Martin-Dorel on August 21, 2021 using texi2html 1.82.