Provided by: prooftree_0.13-1build3_amd64 bug


       prooftree - proof-tree display for Proof General


       prooftree [Options...]


       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.


       -help  Print synopsis and exit.

              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.

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


       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.

       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

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

       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

   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

       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.


   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.


       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.


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


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


       The Prooftree web page,

       The Proof General Adapting Manual
              contains information about adapting  Prooftree  for  a  new  proof  assistant  (see


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


       Hendrik Tews <prooftree at>