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
generic/proof-tree.el as well as in the
|12.1 A layered set of proof trees|
|12.3 Proof-Tree Display Internals|
|12.4 Configuring Prooftree for a New Proof Assistant|
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
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.
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
evarindex number is used, which is printed for each goal in the form
(ID XXX)when Coq is started with the option
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
Focuscommand 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
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|
|12.3.4 Urgent and Delayed Actions|
|12.3.5 Full Annotation|
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
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
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
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 ‘
- 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-add-existential-assoc’ or ‘
When retracting these two variables must be set to their previous
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
- Variable: proof-tree-existentials-alist-history
Alist mapping state numbers to old values of ‘
Needed for undo.
In Prooftree the separation between generic and proof-assistant
specific code is less obvious. The Coq specific code is in the
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
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
text that Prooftree sends to Proof General can be found in buffer
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 ‘
In Proof General, the code for the external proof-tree display is
called from the proof-shell filter function in
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-external-display-toggle aborts with an error
- 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-subgoalflag) 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-tree-urgent-action is called at a point
where it is save to manipulate
proof-action-list. This is
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
- 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-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.
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.
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|
|12.4.2 Prooftree Adaption|
12.4.1 Proof Tree Elisp configuration
All variables that need to be configured are in the customization
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.
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
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
input.ml must be
extended. If the new proof assistant does not support existential
variables adding a line
| "new-pa-name" -> ()
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
This document was generated by Erik Martin-Dorel on March 10, 2022 using texi2html 1.82.