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 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  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 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 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. 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 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 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
       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  >= 8.5, existential variables in Prooftree are severely broken because Coq does not provide the
       necessary information, see Coq bug 4504.

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

       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 Proof General and Prooftree does not permit more.

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.

SEE ALSO

       The Prooftree web page, http://askra.de/software/prooftree/

       The Proof General Adapting Manual
              contains   information   about   adapting   Prooftree   for   a   new   proof    assistant    (see
              http://proofgeneral.inf.ed.ac.uk/adaptingman-latest.html).

CREDITS

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

AUTHOR

       Hendrik Tews <prooftree at askra.de>