[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

8. Handling Multiple Files

Large proof developments are typically spread across multiple files. Many provers support such developments by keeping track of dependencies and automatically processing scripts. Proof General supports this mechanism. The user’s point of view is considered in the user manual. Here, we describe the more technical nitty gritty. This is what you need to know when you customise another proof assistant to work with Proof General.

Documentation for the configuration settings mentioned here appears in the previous sections, this section is intended to help explain the use of those settings.

Proof General maintains a list proof-included-files-list of files which it thinks have been processed by the proof assistant. When a file which is on this list is visited in Emacs, it will be coloured entirely blue to indicate that it has been processed. No editing of the file will be allowed (unless proof-strict-read-only allows it).

Variable: proof-included-files-list

List of files currently included in proof process.
This list contains files in canonical truename format (see ‘file-truename’).

Whenever a new file is being processed, it gets added to this list via the ‘proof-shell-process-file’ configuration settings. When the prover retracts a file, this list is resynchronised via the ‘proof-shell-retract-files-regexp’ and ‘proof-shell-compute-new-files-list’ configuration settings.

Only files which have been fully processed should be included here. Proof General itself will automatically add the filenames of a script buffer which has been completely read when scripting is deactivated. It will automatically remove the filename of a script buffer which is completely unread when scripting is deactivated.

NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant should only output a processed message when a file has been successfully read.

The way that proof-included-files-list is maintained is the key to multiple file management. Ideally you should not set this variable directly, but instead use (some of) the various configuration settings that enable functionality inside Proof General for managing proof-included-files-list (see below if the configuration setting do not suffice).

There is a range of strategies for managing multiple files. Ideally, file dependencies should be managed by the proof assistant. Proof General will use the prover’s low-level commands to process a whole file and its requirements non-interactively, without going through script management. So that the user knows which files have been processed, the proof assistant should issue messages which Proof General can recognize (“file foo has been processed”) — see proof-shell-process-file. When the user wants to edit a file which has been processed, the file must be retracted (unlocked). The proof assistant should provide a command corresponding to this action, which undoes a given file and all its dependencies. As each file is undone, a message should be issued which Proof General can recognize (“file foo has been undone”) – see proof-shell-retract-files-regexp. (The function proof-shell-compute-new-files-list should be set to calculate the new value for proof-included-files-list after a retract message has been seen).

As well as this communication from the assistant to Proof General about processed or retracted files, Proof General can communicate the other way: it will tell the proof assistant when it has processed or retracted a file via script management. This is because during script management, the proof assistant may not be aware that it is actually dealing with a file of proof commands (rather than just terminal input).

Proof General will provide this information in two special instances. First, when scripting is turned off in a file that has been completely processed, Proof General will tell the proof assistant using proof-shell-inform-file-processed-cmd. Second, when scripting is turned on in a file which is completely processed, Proof General will tell the proof assistant to reconsider: the file should not be considered completely processed yet. This uses the setting proof-shell-inform-file-retracted-cmd. This second, retracting, case might lead to a series of messages from the prover telling Proof General to unlock files which depend on the present one, again via proof-shell-retract-files-regexp.

The special case for retracting is the primary file the user wishes to edit: this is automatically removed from proof-included-files-list, but it depends on the proof assistant whether or not it is possible to revert to a partially processed version of the file (or "undo into" it). This is the reason for the setting proof-cannot-reopen-processed-files. If this is non-nil, any attempt to undo a fully processed file will unlock the entire file (whether or not Proof General itself has history information for the file).

What we have described so far is the ideal case, but it may require some support from the proof assistant to set up (for example, if file-level undo is not normally supported, or the messages during file processing are not suitable). Moreover, some proof assistants may not have file handling with dependencies, or may have a particularly simple case of a linear context: each file depends on all the ones processed before it. Proof General allows you a shortcut to get automatic management of multiple files in these cases by setting the flag proof-auto-multiple-files. This setting is probably an approximation to the right thing for any proof assistant. More files than necessary will be retracted if the prover has a tree-like file dependency rather than a linear one.

Finally, we should mention how Proof General recognizes file processing messages from the proof assistant. Proof General considers output delimited by the the two regular expressions proof-shell-eager-annotation-start and proof-shell-eager-annotation-end as being important. It displays the output in the Response buffer and analyses the contents further. Among other important messages characterised by these regular expressions (warnings, errors, or information), the prover can tell the interface whenever it processes or retracts a file.

To summarize, the settings for multiple file management that may be customized are as follows. To recognize file-processing, proof-shell-process-file. To recognize messages about file undoing, proof-shell-retract-files-regexp and proof-shell-compute-new-files-list. See section Settings for matching urgent messages from proof process. To tell the prover about files handled with script management, use proof-shell-inform-file-processed-cmd and proof-shell-inform-file-retracted-cmd. See section Commands. If your prover does not allow re-opening of closed files, set proof-cannot-reopen-processed-files to t. Finally, set the flag proof-auto-multiple-files for a automatic approximation to multiple file handling. See section Proof Script Settings.

Internally Proof General uses proof-register-possibly-new-processed-file to add a file to proof-included-files-list and to possibly inform the prover about this fact, See section Proof script mode. The function proof-shell-process-urgent-message-retract is responsible for taking (possibly several) files off proof-included-files-list. It relies on proof-shell-compute-new-files-list (see section Settings for matching urgent messages from proof process) to compute the new value of proof-included-files-list and then calls proof-restart-buffers on all those buffers that have been taken off from proof-included-files-list, See section Proof script mode.

[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

This document was generated on April 14, 2023 using texi2html 1.82.