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.
This document was generated on April 25, 2024 using texi2html 1.82.