PROOFTREE
Section: User Manuals (1)
Updated: April 2020
Index
NAME
prooftree  prooftree display for Proof General
SYNOPSIS
prooftree [Options...]
DESCRIPTION
Prooftree
visualizes proof trees during proof development with
Proof General.
Currently it only works for Coq, though adding
support for other proof assistants should be relatively easy.
To start a prooftree display, hit the
Prooftree
icon in the
Proof General
toolbar or select the menu entry
ProofGeneral
>
Start/Stop Prooftree
or type
Cc Cd
(which runs
prooftreeexternaldisplaytoggle).
Inside a proof, this will immediately start a prooftree display
for the current proof. Outside a proof,
Proof General
remembers to start the prooftree display for the next proof.
Under normal circumstances
Prooftree
is started by
Proof General
as an
Emacs
subprocess. The user interacts with
Prooftree
only through the graphical user interface. A substantial part of
the prooftree visualization task is done by
Proof General.
Therefore not only the
Prooftree
command line arguments but also other aspects can only be
configured inside
Proof General,
see
Proof General Customization
below.
OPTIONS
 help

Print synopsis and exit.
 config

Open the configuration dialog on startup (if you want to change
the configuration without starting
Proof General).
 geometry spec

Sets the X geometry of the main window.
spec
is a standard X geometry string in the form
xposxypos[+xoff[+yoff]].
 tee file

Write all input to
file
(usually for debugging purposes).
 debug

Provide more details on errors.
 helpdialog

Open the help dialog on startup. Mainly useful for proofreading
the help text.
 testcoqevarparser data

Call the
Coq
evar parser on
data,
pretty print the result and exit. Useful for debugging the evar
parser only.
MAIN PROOF DISPLAY
Prooftree
opens one window for each proof that it is requested to display.
This window contains the prooftree graph and a small display for
sequents and proof commands.
Colors
The branches in the prooftree graph are colored
according to their state.
Prooftree
distinguishes between the following states.
 current (blue by default)

The current branch is the branch from the root of the proof tree
to the current goal.
 unproven (default foreground color)

A branch is unproven if it contains open proof goals.
 proved incomplete (cyan by default)

An incompletely proved branch has its proof finished, but some of
the existential variables that have been introduced in this
branch are not (yet) instantiated.
 proved partially (dark green by default)

In a partially proved branch all existential variables of the
branch itself are instantiated, but some of those instantiations
contain existential variables from other branches
that are not (yet) instantiated.
 proved complete (green by default)

A branch is proved complete if all its existential variables are
instantiated with terms that themselves do not contain any
existential variables.
 cheated (red by default)

A cheated branch contains a cheating proof command, such as
admit
The colors as well as many other
Prooftree
parameters can be changed in the
Prooftree Configuration Dialog
(see below).
Navigation
When the proof tree grows large one can navigate by a variety of
means. In addition to scroll bars and the usual keys one can move
the proof tree by dragging with mouse button 1 pressed. By
default, dragging moves the viewport (i.e., the proof tree
underneath moves in the opposite direction). After setting a
negative value for
Drag acceleration
in the
Prooftree Configuration Dialog,
dragging will move the proof tree instead (i.e, the proof tree
moves in the same direction as the mouse).
Sequent Display
The sequent display below the proof tree normally shows the
ancestor sequent of the current goal. With a single left mouse
click one can display any goal or proof command in the sequent
display. A single click outside the proof tree will switch back
to default behavior. The initial size of the sequent display can
be set in the
Prooftree Configuration Dialog.
A value of 0 hides the sequent display.
Tool Tips
Abbreviated proof commands and sequents are shown in full as
tool tips when the mouse pointer rests over them. Both, the tool
tips for abbreviated proof commands and for sequents can be
independently switched off in the
Prooftree Configuration Dialog.
The length at which proof commands are abbreviated can be
configured as well.
Additional Displays
A double click or a shiftclick displays any goal or proof
command in an additional window. These additional windows are
automatically updated, for instance, if an existential variable
is instantiated. For additional sequent displays one can browse
the instantiation history of the sequent using the forward and
backward buttons. These additional windows can be
detached
from the proof tree. A detached display is neither automatically
updated nor automatically deleted.
Existential Variables
Prooftree
keeps track of existential variables, whether they have been
instantiated and whether they depend on some other, not (yet)
instantiated existential. It uses different colors for proved
branches that created currently not instantiated existential
variables and branches that only depend on some not instantiated
existential created in different branches.
The list of currently not (yet) instantiated existential
variables is appended to proof commands and sequents in tooltips
and the other displays.
The
Existential Variable Dialog
displays a table with all existential variables of the current
proof and their dependencies. Each line of the table contains a
button that marks the proof command that introduced this variable
(with yellow background, by default) and, if present, the proof
command that instantiated this variable (with orange background,
by default).
Main Menu
The
Menu
button displays the main menu. The
Clone
item clones the current proof tree in an additional window. This
additional window continues to display a snapshot of the cloned
proof tree, no matter what happens with the original proof.
The
Show current
and
Show selected
items move the viewport of the proof tree such that the current
proof goal, or, respectively, the selected node will be visible
(if they exist).
The
Exit
item terminates
Prooftree
and closes all prooftree displays.
The remaining four items display, respectively, the
Existential Variable Dialog,
the
Prooftree Configuration Dialog,
and the
Help
and
About
windows.
Context Menu
A right click displays the
Context Menu,
which contains additional items.
The item
Undo to point
is active over sequent nodes in the proof tree. There, it sends an
retract or undo request to Proof General that retracts the
scripting buffer up to that sequent.
The items
Insert command
and
Insert subproof
are active over proof commands. They sent, respectively, the
selected proof command or all proof commands in the selected
subtree, to Proof General, which inserts them at point.
CONFIGURATION
Prooftree Configuration Dialog
The configuration dialog permits to change fonts, colors, layout
parameters for proof tree drawing, to configure tool tips,
initial window sizes and some other points. Changes in the
configuration dialog take immediate effect.
The
Save
button stores the current configuration (as marshaled
OCaml
record) in
~/.prooftree,
which will overwrite the builtin default configuration for the
following
Prooftree
runs. The
Revert
button loads and applies the saved configuration.
The
Cancel
and
OK
buttons close the dialog, but
Cancel
additionally resets the configuration to the state before the
start of the dialog. To avoid opening partial file names, the
Log Proof General input
check box is deactivated when typing the log file name.
Proof General Customization
The location of the
Prooftree
executable and the command line arguments are in the
customization group
prooftree.
Prover specific points, such as the regular expressions for
navigation and cheating commands are in the customization group
prooftreeinternals.
To visit a customization group, type
Mx customizegroup
followed by the name of the customization group inside
Proof General.
LIMITATIONS
In additional sequent displays, the information about existential
variables is only shown for the latest version of the sequent and
not for older versions in the instantiation history.
The synchronization between Proof General and Prooftree is not
perfect. There are a few race conditions which are unlikely to occur
during interactive proof development but can be triggered by asserting
larger parts of a proof or by very quick user actions.
 •

In a situation, where a goal contains an existential variable, this
variable is instantiated (in different branch of the proof), and the
goal is shelved and quickly unshelved, it might happen that the
updated sequent text (containing the instantiating of the existential
variable) is associated with the unshelved version of the goal.
 •

Spawned subgoals and the instantiating of existential variables cause
asynchronous updatesequent messages sent to
Prooftree.
When quickly retracting portions of the proof, the corresponding undo
message might overtake same updatesequent messages and thereby
confuse
Prooftree.
PREREQUISITES
This version of
Prooftree
requires
Coq
8.11 or better
and
Proof General
from March 2021 or later.
FILES
 ~/.prooftree

Saved
Prooftree
configuration. Is loaded at application startup for overwriting
the builtin default configuration. Must contain a marshaled
OCaml
configuration record.
SEE ALSO
 The Prooftree web page, http://askra.de/software/prooftree/

 The Proof General Adapting Manual

contains now partially outdated information about adapting
Prooftree
for a new proof assistant (see
https://proofgeneral.github.io/doc/master/adaptingman/).
HISTORY
Prooftree
was developed in 2011 to help to keep orientation in larger
Coq
proofs. The first versions required patches for
Coq.
After a meeting with the
Coq
development team at the third
Coq
workshop in Nijmegen, the Netherlands, in 2011, Arnaud Spiwack
added the necessary support for
Prooftree
to
Coq
and
Prooftree
version 0.8 was the first version that worked with
Coq
8.4beta and the
Proof General
development version.
The user friendly names for existential variables, introduced in
Coq
8.6 broke many
Prooftree
features for existential variables and the removal of the
Show Goal id
command in
Coq
8.7 broke
Prooftree
completely. In 2019, Jim Fehrle added the necessary support for
Prooftree
again to
Coq
8.11. The existential variable printout and the
Show Goal
command were slightly generalized, making it possible to simplify
the proof tree code in
Proof General
quite a bit.
CREDITS
Prooftree
has been inspired by the proof tree display of
PVS.
AUTHOR
Hendrik Tews <prooftree at askra.de>
Index
 NAME

 SYNOPSIS

 DESCRIPTION

 OPTIONS

 MAIN PROOF DISPLAY

 Colors

 Navigation

 Sequent Display

 Tool Tips

 Additional Displays

 Existential Variables

 Main Menu

 Context Menu

 CONFIGURATION

 Prooftree Configuration Dialog

 Proof General Customization

 LIMITATIONS

 PREREQUISITES

 FILES

 SEE ALSO

 HISTORY

 CREDITS

 AUTHOR

This document was created by
man2html,
using the manual pages.
Time: 13:27:19 GMT, February 23, 2024