12. Configuring Proof-Tree Visualization

Parts of this section are outdated. Please create an issue at github.com/ProofGeneral/Proof General if you have a question for adapting Prooftree for a new proof assistant.

The proof-tree visualization feature was written with the idea of supporting Coq as well as other proof assistants. Nevertheless, supporting proof-tree visualization for a second proof assistant will almost certainly require changes in the generic Elisp code in generic/proof-tree.el as well as in the Prooftree program.

12.1 A layered set of proof trees

Prooftree can actually display more than one proof tree per proof. This is necessary to support the Grab Existential Variables command in Coq. When the main goal has been proved, this command turns all open existential variables into new proof obligations. All these new proof obligations become root nodes for their own proof trees. When they all have been proved one can again grab the open existential variables...

For each proof, Prooftree can therefore display several layers, where each layer can contain several (graphically) independent proof trees. The first layer contains one tree for the original proof goal. The second layer contains proof trees for goals that have been added to the proof after the first proof tree was completed. And so on.

Prooftree assumes a new layer when it receives new goals in a state where the number of open goals is zero.

12.2 Prerequisites

Proof-tree visualization requires certain support from the proof assistant. Patching the proof assistant is therefore the first step of adding support for proof-tree visualization. The following features are needed.

Unique goal identification

The proof assistant must assign and output a unique string for each goal. For Coq the internal evar index number is used, which is printed for each goal in the form (ID XXX) when Coq is started with the option -emacs.

The unique goal identification is needed to distinguish newly spawned subgoals from older open subgoals and to mark the current goal in the proof-tree display.

Indication of newly generated subgoals

A proof command that spawns additional subgoals must somehow indicate the goal ID’s of these new subgoals. Otherwise the proof-tree display will not be able to reconstruct the proof-tree structure.

For Coq the newly spawned subgoals appear always in the list of additional subgoals below the current goal. Note, that it is not required to mark the newly spawned subgoals. They may appear in a mixed list with older open subgoals. Note further, that it is not required that always the complete set of all open subgoals is printed (which is indeed not the case after of Focus command in Coq). It is only required that the goal ID’s of all newly spawned subgoals is somehow printed.

State number for undo

There must be a state number that is strictly increasing when asserting proof commands and that is reset to the appropriate number after retracting some proof commands.

For Coq the state number in the extended prompt (visible only with option -emacs) is used.

Information about existential variables

Existential variables are placeholders that might or must be instantiated later in the proof. Prooftree supports existential variables with three features. Firstly, it can update goals when existential variables get instantiated. Secondly, it can mark the proof commands that introduced or instantiated existential variables and, thirdly, it can display and track dependencies between existential variables.

For the first feature, the proof assistant must list the currently instantiated existential variables for every goal. For the second feature it must additionally list the not instantiated existential variables. Finally, for the third feature, it must display the dependencies for instantiated existential variables.

For Coq, all necessary information is provided in the existential evar line, that is printed with the -emacs switch.

12.3 Proof-Tree Display Internals

This section gives some information about the inner structure of the code that realizes the proof-tree display. The idea here is that this section provides the background information to make the documentation of the customizable variables of the proof-tree Elisp code easy to understand.

12.3.1 Organization of the Code

The proof-tree display is realized by Proof General in cooperation with the external Prooftree program. The latter is a GTK application in OCaml. Both, the Elisp code in Proof General and the Prooftree OCaml code is divided into a generic and a proof assistant specific part.

The generic Elisp code lives in generic/proof-tree.el. As usual in Proof General, it contains various customizable variables, which the proof assistant specific code must set. Most of these variables contain regular expressions, but there are also some that hold functions. The Coq specific code for the proof-tree display is distributed in a few chunks over coq/coq.el.

The main task of the Elisp code is to extract goals, undo events and information about existential variables from the proof-assistant output and to send all this data to Prooftree. Additional commands inserted by Prooftree are flagged with proof-tree-show-subgoal, no-goals-display and no-response-display. The flag proof-tree-show-subgoal ensures that a number of internal functions ignore these additional commands. The other two flags ensure that their output is neither displayed in the goals nor the response buffer.

In Prooftree the separation between generic and proof-assistant specific code is less obvious. The Coq specific code is in the file coq.ml. All the remaining code is generic.

Prooftree opens for each proof a separate window. It reconstructs the proof tree and orders the existential variables in a dependency hierarchy. It stores a complete history of previous states to support arbitrary undo operations. Under normal circumstances one starts just one Prooftree process that keeps running for the remainder of the Proof General session, regardless of how many proof-tree windows are displayed.

A fair amount of the Prooftree code is documented with ocamldoc documentation comments. With make doc they can be converted into a set of html pages in the doc subdirectory.

12.3.2 Communication

Prooftree is a standard Emacs subprocess that reads goals and other proof status messages from its standard input. The communication between Proof General and Prooftree is almost one way only. Proof General sends proof status messages to Prooftree, from which Prooftree reconstructs the current proof status and the complete proof tree. Prooftree never requests additional information from Proof General.

There are only a few messages that Prooftree sends to Proof General. These messages communicate user requests to Proof General, for instance, when the user selects the undo menu item, or when he closes the Prooftree window.

The communication protocol is completely described in the ocamldoc documentation of input.ml in the Prooftree sources. All messages consist of UTF-8 encoded human-readable strings. The strings have either a fixed length or their byte-length is encoded in the message before the string itself.

For debugging purposes Prooftree can save all input in a file. This feature can be turned on in the Debug tab of the Prooftree configuration dialog or with option -tee. The text that Prooftree sends to Proof General can be found in buffer *proof-tree*.

12.3.3 Guards

The proof-tree display code inside Proof General uses two guard variables.

Variable: proof-tree-configured

Whether external proof-tree display is configured.
This boolean enables the proof-tree menu entry and the function that starts external proof-tree display.

Variable: proof-tree-external-display

Display proof trees in external prooftree windows if t.
Actually, if this variable is t then the user requested an external proof-tree display. If there was no unfinished proof when proof-tree display was requested and if no proof has been started since then, then there is obviously no proof-tree display. In this case, this variable stays t and the proof-tree display will be started for the next proof.

Controlled by ‘proof-tree-external-display-toggle’.

In Proof General, the code for the external proof-tree display is called from the proof-shell filter function in proof-shell-exec-loop and proof-shell-filter-manage-output, see section Proof shell mode. The variable proof-tree-external-display is a guard for these calls, to ensure that the proof-tree specific code is only called if the user requested a proof-tree display.

The whole proof-tree package contains only one function that can be called interactively: proof-tree-external-display-toggle, which switches proof-tree-external-display on and off. When proof-tree-configured is nil, proof-tree-external-display-toggle aborts with an error message.

Command: proof-tree-external-display-toggle

Toggle the external proof-tree display.
When called outside a proof the external proof-tree display will be enabled for the next proof. When called inside a proof the proof display will be created for the current proof. If the external proof-tree display is currently on, then this toggle will switch it off. At the end of the proof the proof-tree display is switched off.

12.3.4 Urgent and Delayed Actions

The proof-shell filter functions contains two calls to proof-tree specific code. One for urgent actions and one for all remaining actions, that can be delayed.

Urgent actions are those that must be executed before proof-shell-exec-loop sends the next item from proof-action-list to the proof assistant. For execution speed, the amount of urgent code should be kept small.

Function: proof-tree-check-proof-finish last-item

Urgent action to delay processing at proof end.
This function is called from ‘proof-shell-exec-loop’ after the old item has been removed and before the next item from ‘proof-action-list’ is sent to the proof assistant. Of course only when the proof-tree display is active. At the end of the proof, this function delays items just following the previous proof until all show-goal commands from prooftree and the ‘proof-tree-display-stop-command’ (which switches the dependent evar line off for Coq) have been processed.

If this function detects the end of the proof, it moves non-priority items following in ‘proof-action-list’ to ‘proof-tree--delayed-actions’ and sets ‘proof-second-action-list-active’. When later the command from ‘proof-tree-display-stop-command’ is recognized, the items are moved back. If no items follow the end of the previous proof, ‘proof-tree-display-stop-command’ is set to t.

The function proof-tree-check-proof-finish is called at a point where it is save to manipulate proof-action-list. This is essential, because proof-tree-urgent-action inserts goal display commands into proof-action-list when existential variables got instantiated and when the sequent text from newly created subgoals is missing.

Most of the proof-tree specific code runs when the proof assistant is already busy with the next item from proof-action-list.

Function: proof-tree-handle-delayed-output old-proof-marker cmd flags _span

Process delayed output for prooftree.
This function is the main entry point of the Proof General prooftree support. It examines the delayed output in order to take appropriate actions and maintains the internal state.

The delayed output to handle is in the region [proof-shell-delayed-output-start, proof-shell-delayed-output-end]. Urgent messages might be before that, following old-proof-marker, which contains the position of ‘proof-marker’, before the next command was sent to the proof assistant.

All other arguments are (former) fields of the ‘proof-action-list’ entry that is now finally retired. cmd is the command, flags are the flags and span is the span.

The function proof-tree-handle-delayed-output does all the communication with Prooftree.

12.3.5 Full Annotation

In the default configuration Proof General switches the proof assistant into quiet mode if there are more than proof-shell-silent-threshold items in proof-action-list, see Section Document centred working (in Chapter Advanced Script Management and Editing) in the Proof General users manual. The proof-tree display needs of course the full output from the proof assistant. Therefore proof-shell-should-be-silent keeps the proof assistant noisy when the proof-tree display is switched on.

12.4 Configuring Prooftree for a New Proof Assistant

To get the proof-tree display running for a new proof assistant one has to configure the proof-tree Elisp code and adapt the Prooftree program.

12.4.1 Proof Tree Elisp configuration

All variables that need to be configured are in the customization group proof-tree-internals. Most of these variables are regular expressions for extracting various parts from the proof assistant output. However, some are functions that need to be implemented as prover specific part of the proof display code.

The variables proof-tree-configured, proof-tree-get-proof-info and proof-tree-find-begin-of-unfinished-proof might be used before the proof assistant is running inside a proof shell. They must therefore be configured as part of the proof assistant editing mode.

The other variables are only used when the proof shell is running. They can therefore be configured with the proof assistant proof-shell mode.

12.4.2 Prooftree Adaption

To make the new proof assistant known to Prooftree, the match in function configure_prooftree in input.ml must be extended. If the new proof assistant does not support existential variables adding a line

  | "new-pa-name" -> ()

suffices.

If the new prover supports existential variables, Prooftree must be extended with a parser for the existential variable information printout of the proof assistant. The parser for Coq is contained in the file coq.ml. Then the function configure_prooftree must assign this new parser to the reference parse_existential_info.

This document was generated on November 21, 2024 using texi2html 1.82.