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.

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.

Enabling

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 >: proof-autosend-toggle

Command: proof-autosend-toggle &optional arg: Toggle ‘proof-autosend-enable’. With arg, turn on iff ARG>0.
This function simply uses customize-set-variable to 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 pg-toggle-visibility.

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.

Command: pg-toggle-visibility: Toggle visibility of region under point.

Command: pg-show-all-proofs: Display all completed proofs in the buffer.

Command: pg-hide-all-proofs: Hide all completed proofs in the buffer.

User Option: proof-disappearing-proofs

Non-nil causes Proof General to hide proofs as they are completed.

The default value is nil.

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.v’. 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.v’ and retract to where changes are required. Then, using script management, you want to develop some more basic theory in ‘sos.v’. 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.v’ 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 Proof status statistic

The command proof-check-report (menu Proof-General -> Check Opaque Proofs) generates the proof status of all opaque proofs in the current buffer, i.e., it generates an overview that shows which of the opaque proofs in the current buffer are currently valid and which are failing. When used interactively, the proof status is shown in the buffer *proof-check-report* (as long as proof-check-report-buffer is not changed). Note that incomplete proofs, i.e., Admitted proofs for Coq, count as invalid.

The command proof-check-annotate (menu Proof-General -> Annotate Failing Proofs) modifies the current buffer and places comments containing FAIL on all failing opaque proofs. With prefix argument also the passing proofs are annotated with PASS. For configuring the position of these comments, see proof-check-annotate-position and proof-check-annotate-right-margin.

Currently proof-check-report and proof-check-annotate only work for Coq.

Command: proof-check-report tap &optional batch

Generate an overview about valid and invalid proofs.
This command completely processes the current buffer and generates an overview about all the opaque proofs in it and whether their proof scripts are valid or invalid. Note that proofs closed with a cheating command (see ‘proof-omit-cheating-regexp’), i.e., Admitted for Coq, count as invalid.

This command makes sense for a development process where invalid proofs are permitted and vos compilation and the omit proofs feature (see ‘proof-omit-proofs-configured’) are used to work at the most interesting or challenging point instead of on the first invalid proof.

Argument tap, which can be set by a prefix argument, controls the form of the generated overview. Nil, without prefix, gives an human readable overview, otherwise it’s test anything protocol (tap). Argument batch controls where the overview goes to. If nil, or in an interactive call, the overview appears in ‘proof-check-report-buffer’. If batch is a string, it should be a filename to write the overview to. Otherwise the overview is output via ‘message’ such that it appears on stdout when this command runs in batch mode.

In the same way as the omit-proofs feature, this command only tolerates errors inside scripts of opaque proofs. Any other error is reported to the user without generating an overview. The overview only contains those names of theorems whose proof scripts are classified as opaque by the omit-proofs feature. For Coq for instance, among others, proof scripts terminated with 'Defined' are not opaque and do not appear in the generated overview.

Note that this command does not (re-)compile required files. Dependencies must be compiled before running this commands, for instance by asserting all require commands beforehand.

Command: proof-check-annotate annotate-passing &optional save-buffer

Annotate failing proofs in current buffer with a "fail" comment.
This function modifies the current buffer in place. Use with care!

Similarly to ‘proof-check-report’, check all opaque proofs in the current buffer. Instead of generating a report, failing proofs are annotated with "fail" in a comment. Existing "pass" or "fail" comments (e.g., from a previous run) are deleted together with the surrounding white space. With prefix argument (or when annotate-passing is non-nil) also passing proofs are annotated with a "pass" comment. Pass and fail comments can be placed at the last or second last statement before the opaque proof. For Coq this corresponds to the proof using and the theorem statement, respectively. In both cases the comment is placed at the right margin of the first line, see ‘proof-check-annotate-position’ and ‘proof-check-annotate-right-margin’.

Interactively, this command does not save the current buffer after placing the annotations. With save-buffer non-nil, the current buffer is saved if it has been modified.

Variable: proof-check-annotate-position: Line for annotating proofs with "pass" or "fail" comments.
This option determines the line where ‘proof-check-annotate’ puts comments with "pass" and "fail". Value ‘’theoren’ uses the first line of the second last statement before the start of the opaque proof, which corresponds to the line containing a Theorem keyword for Coq. Value ‘’proof-using’ uses the first line of the last statement before the opaque proof, which corresponds to the Proof using line for Coq.

Variable: proof-check-annotate-right-margin: Right margin for "pass" and "fail" comments.
This option determines the right margin to which ‘proof-check-annotate’ right-aligns the comments with "pass" and "fail". If nil, the value of ‘fill-column’ is used.

See section Quick and inconsistent compilation for enabling vos compilation inside Proof General and see See section Omitting proofs for speed for the omit-proofs feature.

The interactive use of proof-check-report and proof-check-annotate is limited because they only work on the current buffer. However, these commands can also be run in batch mode in a script, for instance in a continuous integration environment. To run proof-check-report on a file in batch mode, use

emacs -batch -l <your-pg-dir>/generic/proof-site.el <file> \
      --eval '(proof-check-report <tap> <output>)'

where <tap> should be nil for human readable output and t for test anything protocol. If <output> is t the proof status appears in the standard output of the Emacs process. Otherwise <output> should be a filename as string in double quotes. Then the proof status is written to this file. (If output is nil or omitted, the proof status is only put into the *proof-check-report* buffer, which does not make much sense in a batch command as the one above.)

Using a similar command also proof-check-annotate can run in batch mode in a continuous integration environment, for instance for checking that all failing proofs are annotated with FAIL via git diff --exit-code.

3.9 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.10 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: proof-frob-locked-end

This command is disabled by default, to protect novices using it accidently.

If 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.11 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 entered once. The size of the ring is set by the variable pg-input-ring-size.

M-p: pg-previous-matching-input-from-input
M-n: pg-next-matching-input-from-input

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 on November 21, 2024 using texi2html 1.82.