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

12. Configuring Proof-Tree Visualization

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.

To organize the layers, Prooftree must identify those proof commands that add new goals to a proof.

Variable: proof-tree-new-layer-command-regexp

Regexp to match proof commands that add new goals to a proof.
This regexp must match the command that turns the proof assistant into prover mode, which adds the initial goal to the proof. It must further match commands that add additional goals after all previous goals have been proved.


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. The Elisp code does also determine if additional output must be requested from the proof assistant. In that case it adds appropriate commands to proof-action-list, see section Proof script mode. These additional commands 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.

For the decision about which goals must be sent to Prooftree, the Elisp code maintains the following two state variables.

Variable: proof-tree-sequent-hash

Hash table to remember sequent ID’s.
Needed because some proof assistants do not distinguish between new subgoals, which have been created by the last proof command, and older, currently unfocussed subgoals. If Proof General meets a goal, it is treated as new subgoal if it is not in this hash yet.

The hash is mostly used as a set of sequent ID’s. However, for undo operations it is necessary to delete all those sequents from the hash that have been created in a state later than the undo state. For this purpose this hash maps sequent ID’s to the state number in which the sequent has been created.

The hash table is initialized in ‘proof-tree-start-process’.

Variable: proof-tree-existentials-alist

Alist mapping existential variables to sequent ID’s.
Used to remember which goals need a refresh when an existential variable gets instantiated. To support undo commands the old contents of this list must be stored in ‘proof-tree-existentials-alist-history’. To ensure undo is properly working, this variable should only be changed by using ‘proof-tree-delete-existential-assoc’, ‘proof-tree-add-existential-assoc’ or ‘proof-tree-clear-existentials’.

When retracting these two variables must be set to their previous state. For proof-tree-sequent-hash this is done with the state numbers that are stored in the hash. For proof-tree-existentials-alist a separate alist stores previous states.

Variable: proof-tree-existentials-alist-history

Alist mapping state numbers to old values of ‘proof-tree-existentials-alist’.
Needed for undo.

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-urgent-action flags

Handle urgent points before the next item is sent to the proof assistant.
Schedule goal updates when existential variables have changed and call ‘proof-tree-urgent-action-hook’. All this is only done if the current output does not come from a command (with the 'proof-tree-show-subgoal flag) that this package inserted itself.

Urgent actions are only needed if the external proof display is currently running. Therefore this function should not be called when ‘proof-tree-external-display’ is nil.

This function assumes that the prover output is not suppressed. Therefore, ‘proof-tree-external-display’ being t is actually a necessary precondition.

The not yet delayed output is in the region [proof-shell-delayed-output-start, proof-shell-delayed-output-end].

The function proof-tree-urgent-action 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.


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

This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.