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.
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.
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.
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.
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.
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.
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.
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.
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 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.
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
’.
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.
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.
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*
.
The proof-tree display code inside Proof General uses two guard variables.
Whether external proof-tree display is configured.
This boolean enables the proof-tree menu entry and the function
that starts external proof-tree 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 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.
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.
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.
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
.
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.
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.
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.
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.
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
.