Provided by: prooftree_0.13-1build3_amd64

**NAME**

prooftree - proof-tree display for Proof General

**SYNOPSIS**

prooftree[Options...]

**DESCRIPTION**

Prooftreevisualizes proof trees during proof development withProofGeneral. Currently it only works forCoq, though adding support for other proof assistants should be relatively easy. To start a proof-tree display, hit theProoftreeicon in theProofGeneraltool-bar or select the menu entryProof-General->Start/StopProoftreeor typeC-cC-d(which runsproof-tree-external-display-toggle). Inside a proof, this will immediately start a proof- tree display for the current proof. Outside a proof,ProofGeneralremembers to start the proof-tree display for the next proof. Under normal circumstancesProoftreeis started byProofGeneralas anEmacssubprocess. The user interacts withProoftreeonly through the graphical user interface. A substantial part of the proof-tree visualization task is done byProofGeneral. Therefore not only theProoftreecommand line arguments but also other aspects can only be configured insideProofGeneral, seeProofGeneralCustomizationbelow.

**OPTIONS**

-help Print synopsis and exit. -config Open the configuration dialog on startup (if you want to change the configuration without startingProofGeneral). -geometryspecSets the X geometry of the main window.specis a standard X geometry string in the formxposxypos[+xoff[+yoff]]. -teefileWrite all input tofile(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**

Prooftreeopens 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.ColorsThe branches in the proof-tree graph are colored according to their state.Prooftreedistinguishes 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 asadmitThe colors as well as many otherProoftreeparameters can be changed in theProoftreeConfigurationDialog(see below).NavigationWhen 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 forDragaccelerationin theProoftreeConfigurationDialog, dragging will move the proof tree instead (i.e, the proof tree moves in the same direction as the mouse).SequentDisplayThe 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 theProoftreeConfigurationDialog. A value of 0 hides the sequent display.ToolTipsAbbreviated 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 theProoftreeConfigurationDialog. The length at which proof commands are abbreviated can be configured as well.AdditionalDisplaysA 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 bedetachedfrom the proof tree. A detached display is neither automatically updated nor automatically deleted.ExistentialVariablesProoftreekeeps 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. TheExistentialVariableDialogdisplays 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).MainMenuTheMenubutton displays the main menu. TheCloneitem 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. TheShowcurrentandShowselecteditems move the viewport of the proof tree such that the current proof goal, or, respectively, the selected node will be visible (if they exist). TheExititem terminatesProoftreeand closes all proof-tree displays. The remaining three items display, respectively, theProoftreeConfigurationDialog, and theHelpandAboutwindows.ContextMenuA right click displays theContextMenu, which contains additional items. The itemUndotopointis 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 itemsInsertcommandandInsertsubproofare 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**

ProoftreeConfigurationDialogTheSavebutton stores the current configuration (as marshaledOCamlrecord) in~/.prooftree, which will overwrite the built-in default configuration for the followingProoftreeruns. TheRevertbutton loads and applies the saved configuration. TheCancelandOKbuttons close the dialog, butCanceladditionally resets the configuration to the state before the start of the dialog. To avoid opening partial file names, theLogProofGeneralinputcheck box is deactivated when typing the log file name.ProofGeneralCustomizationThe location of theProoftreeexecutable and the command line arguments are in the customization groupproof-tree. Prover specific points, such as the regular expressions for navigation and cheating commands are in the customization groupproof-tree-internals. To visit a customization group, typeM-xcustomize-groupfollowed by the name of the customization group insideProofGeneral.

**LIMITATIONS**

ForCoq>= 8.5, existential variables inProoftreeare severely broken becauseCoqdoes not provide the necessary information, seeCoqbug 4504. InCoq, proofs must be started with commandProof, 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 betweenProofGeneralandProoftreedoes not permit more.

**PREREQUISITES**

This version ofProoftreerequiresCoq8.4beta or better andProofGeneral4.3pre130327 or better.

**FILES**

~/.prooftree SavedProoftreeconfiguration. Is loaded at application start-up for overwriting the built-in default configuration. Must contain a marshaledOCamlconfiguration record.

**SEE** **ALSO**

TheProoftreeweb page,http://askra.de/software/prooftree/TheProofGeneralAdaptingManualcontains information about adaptingProoftreefor a new proof assistant (seehttp://proofgeneral.inf.ed.ac.uk/adaptingman-latest.html).

**CREDITS**

Prooftreehas been inspired by the proof tree display ofPVS.

**AUTHOR**

Hendrik Tews <prooftree at askra.de>