[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [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. (But you should not set this variable directly, it is managed via the configuration settings).

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.

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

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.