prooftree.1

.\" groff -man -Tascii prooftree.1
.\"
.TH PROOFTREE 1 "August 2011" PROOFTREE "User Manuals"
.SH NAME
prooftree \- proof-tree display for Proof General
.SH SYNOPSIS
.B prooftree \fR[\fIOptions...\fR]
.SH DESCRIPTION
.\" ============= paragraph general purpose ===================================
.B Prooftree
visualizes proof trees during proof development with 
.B Proof General\fR. 
Currently it only works for \fBCoq\fR, though adding
support for other proof assistants should be relatively easy.
.\" ==========================================================================
.P
To start a proof-tree display, hit the 
.B Prooftree
icon in the 
.B Proof General
tool-bar or select the menu entry
.I Proof-General
-> 
.I Start/Stop Prooftree
or type
.I C-c C-d
(which runs
.I proof-tree-external-display-toggle\fR).
Inside a proof, this will immediately start a proof-tree display
for the current proof. Outside a proof, 
.B Proof General
remembers to start the proof-tree display for the next proof.
.\" ==========================================================================
.P
Under normal circumstances
.B Prooftree
is started by 
.B Proof General
as an
.B Emacs
subprocess. The user interacts with 
.B Prooftree
only through the graphical user interface. A substantial part of
the proof-tree visualization task is done by
.B Proof General\fR.
Therefore not only the 
.B Prooftree
command line arguments but also other aspects can only be
configured inside 
.B Proof General\fR,
see 
.B Proof General Customization
below.
.\"
.\" ==========================================================================
.\" ================ Options =================================================
.\" ==========================================================================
.\"
.SH OPTIONS
.\" ======================================= -help ============================
.IP "-help"
Print synopsis and exit.
.\" ======================================= -config ==========================
.IP "-config"
Open the configuration dialog on startup (if you want to change
the configuration without starting 
.B Proof General\fR).
.\" ======================================= -geometry ========================
.IP "-geometry \fIspec\fR"
Sets the X geometry of the main window.
.I spec
is a standard X geometry string in the form 
\fIxpos\fRx\fIypos\fR[+\fIxoff\fR[+\fIyoff\fR]].
.\" ======================================= -tee =============================
.IP "-tee \fIfile\fR"
Write all input to
.I file
(usually for debugging purposes).
.\" ======================================= -debug ===========================
.IP "-debug"
Provide more details on errors.
.\" ======================================= -help-dialog =====================
.IP "-help-dialog"
Open the help dialog on startup. Mainly useful for proofreading
the help text.
.\"
.\" ==========================================================================
.\" ================ Main Window =============================================
.\" ==========================================================================
.\"
.SH MAIN PROOF DISPLAY
.B Prooftree
opens one window for each proof that it is requested to display.
This window contains the proof-tree graph and a small display for
sequents and proof commands. 
.\" ==========================================================================
.SS Colors
The branches in the proof-tree graph are colored
according to their state. 
.B Prooftree
distinguishes between the following states.
.IP "current (blue by default)"
The current branch is the branch from the root of the proof tree
to the current goal.
.IP "unproven (default foreground color)"
A branch is unproven if it contains open proof goals.
.IP "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.
.IP "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 that are not (yet) instantiated.
.IP "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.
.IP "cheated (red by default)"
A cheated branch contains a cheating proof command, such as 
.I admit\f.
.P
The colors as well as many other
.B Prooftree
parameters can be changed in the 
.B Prooftree Configuration Dialog
(see below). 
.\" ==========================================================================
.SS 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 
.I Drag acceleration 
in the 
.B Prooftree Configuration Dialog\fR,
dragging will move the proof tree instead (i.e, the proof tree
moves in the same direction as the mouse).
.\" ==========================================================================
.SS 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
.B Prooftree Configuration Dialog\fR.
A value of 0 hides the sequent display.
.\" ==========================================================================
.SS 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
.B Prooftree Configuration Dialog\fR.
The length at which proof commands are abbreviated can be
configured as well.
.\" ==========================================================================
.SS Additional Displays
A double click or a shift-click 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
.I detached
from the proof tree. A detached display is neither automatically
updated nor automatically deleted.
.\" ==========================================================================
.SS Existential Variables
.B 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 contain non-instantiated existential variables and
branches that only depend on some not instantiated existential.
The list of currently not (yet) instantiated existential
variables is appended to proof commands and sequents in tool-tips
and the other displays.
.\" ==========================================================================
.P
The
.B 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). 
.\" ==========================================================================
.SS Main Menu
The
.I Menu
button displays the main menu. The 
.I 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.
.\" ==========================================================================
.P
The 
.I Show current
and
.I 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).
.\" ==========================================================================
.P
The
.I Exit
item terminates 
.B Prooftree
and closes all proof-tree displays.
.\" ==========================================================================
.P
The remaining three items display, respectively, the
.B Prooftree Configuration Dialog\fR,
and the 
.B Help
and 
.B About
windows.
.\" ==========================================================================
.SS Context Menu
A right click displays the 
.I Context Menu\fR,
which contains additional items.
.\" ==========================================================================
.P
The item
.I 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.
.\" ==========================================================================
.P
The items
.I Insert command
and
.I 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 ===========================================
.\" ==========================================================================
.\"
.SH CONFIGURATION
.SS Prooftree Configuration Dialog
The 
.I Save 
button stores the current configuration (as marshaled 
.B OCaml
record) in 
.I ~/.prooftree\fR,
which will overwrite the built-in default configuration for the
following 
.B Prooftree
runs. The 
.I Revert
button loads and applies the saved configuration.
The
.I Cancel
and
.I OK
buttons close the dialog, but
.I Cancel
additionally resets the configuration to the state before the
start of the dialog. To avoid opening partial file names, the
.I Log Proof General input
check box is deactivated when typing the log file name.
.\" ==========================================================================
.SS Proof General Customization
The location of the 
.B Prooftree
executable and the command line arguments are in the
customization group
.I proof-tree\fR.
Prover specific points, such as the regular expressions for
navigation and cheating commands are in the customization group
.I proof-tree-internals\fR.
To visit a customization group, type 
.I M-x customize-group
followed by the name of the customization group inside 
.B Proof General\fR.
.\"
.\" ==========================================================================
.\" ================ Limitations =============================================
.\" ==========================================================================
.\"
.SH LIMITATIONS
For
.B Coq
>= 8.5, existential variables in
.B Prooftree
are severely broken because
.B Coq
does not provide the necessary information, see
.B Coq
bug 4504.
.\" ==========================================================================
.P
In
.B Coq\fR,
proofs must be started with command 
.I Proof\fR,
which is the recommended practice anyway (see Coq problem report
2776).
.\" ==========================================================================
.P
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 current
communication protocol between
.B Proof General
and
.B Prooftree
does not permit more.
.\"
.\" ==========================================================================
.\" ================ Prerequisites ===========================================
.\" ==========================================================================
.\"
.SH PREREQUISITES
This version of
.B Prooftree
requires
.B Coq
8.4beta or better
and 
.B Proof General
4.3pre130327 or better.
.\"
.\" ==========================================================================
.\" ================ Files ===================================================
.\" ==========================================================================
.\"
.SH FILES
.IP "~/.prooftree"
Saved
.B Prooftree
configuration. Is loaded at application start-up for overwriting
the built-in default configuration. Must contain a marshaled
.B OCaml
configuration record.
.\"
.\" ==========================================================================
.\" ================ SEE ALSO ================================================
.\" ==========================================================================
.\"
.SH SEE ALSO
.TP
The \fBProoftree\fR web page, \fIhttp://askra.de/software/prooftree/\fR

.TP
The \fBProof General Adapting Manual\fR
contains information about adapting 
.B Prooftree
for a new proof assistant (see
.I http://proofgeneral.inf.ed.ac.uk/adaptingman-latest.html\fR).
.\"
.\" ==========================================================================
.\" ================ Credits =================================================
.\" ==========================================================================
.\"
.SH CREDITS
.B Prooftree
has been inspired by the proof tree display of
.B PVS\fR.
.\"
.\" ==========================================================================
.\" ================ Author ==================================================
.\" ==========================================================================
.\"
.SH AUTHOR
Hendrik Tews <prooftree at askra.de>