Ubuntu Manpage: prooftree - proof-tree display for Proof General

Provided by: prooftree_0.12-2build1_amd64

NAME

       prooftree - proof-tree 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  proof-tree  display, hit the Prooftree icon in the Proof General tool-bar or
       select the menu entry Proof-General -> Start/Stop Prooftree or type C-c  C-d  (which  runs
       proof-tree-external-display-toggle).  Inside a proof, this will immediately start a proof-
       tree display for the current proof. Outside a proof, Proof General remembers to start  the
       proof-tree 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  proof-tree 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.

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

MAIN PROOF DISPLAY

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.

Colors
The branches in the proof-tree 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 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 shift-click displays any goal or proof command in an additional
window. These additional windows are deleted when the main proof-tree window disappears,
unless their Sticky button is pressed.

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 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.

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 item moves the viewport to the proof tree such that the current proof
goal (if there is any) will be visible.

The Exit item terminates Prooftree and closes all proof-tree displays.

The remaining three items display, respectively, 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. Then 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
       Changes in the configuration dialog take only effect  when  the  Apply  or  OK  button  is
       pressed.  The  Save button stores the current configuration (as marshaled OCaml record) in
       ~/.prooftree, which will overwrite the built-in default configuration  for  the  following
       Prooftree runs. The Restore button loads and applies the saved configuration.

   Proof General Customization
       The  location  of  the  Prooftree  executable  and  the  command line arguments are in the
       customization group proof-tree.  Prover specific points, such as the  regular  expressions
       for  navigation and cheating commands are in the customization group proof-tree-internals.
       To visit a customization group, type M-x customize-group  followed  by  the  name  of  the
       customization group inside Proof General.

LIMITATIONS

       For  Coq,  proofs  must  be  started with command Proof, which is the recommended practice
       anyway (see Coq problem report 2776).

PREREQUISITES

       This version of Prooftree requires Coq 8.4beta or better and Proof General 4.3pre130327 or
       better.

FILES

       ~/.prooftree
              Saved  Prooftree  configuration.  Is loaded at application start-up for overwriting
              the built-in default configuration. Must contain a  marshaled  OCaml  configuration
              record.

CREDITS

       Prooftree has been inspired by the proof tree display of PVS.

AUTHOR

       Hendrik Tews <prooftree at askra.de>