1PROOFTREE(1)                     User Manuals                     PROOFTREE(1)
2
3
4

NAME

6       prooftree - proof-tree display for Proof General
7

SYNOPSIS

9       prooftree [Options...]
10

DESCRIPTION

12       Prooftree  visualizes  proof  trees during proof development with Proof
13       General.  Currently it only works for Coq, though  adding  support  for
14       other proof assistants should be relatively easy.
15
16       To start a proof-tree display, hit the Prooftree icon in the Proof Gen‐
17       eral tool-bar or select the  menu  entry  Proof-General  ->  Start/Stop
18       Prooftree  or type C-c C-d (which runs proof-tree-external-display-tog‐
19       gle).  Inside a proof, this will immediately start a proof-tree display
20       for  the  current  proof.  Outside  a proof, Proof General remembers to
21       start the proof-tree display for the next proof.
22
23       Under normal circumstances Prooftree is started by Proof General as  an
24       Emacs  subprocess.  The  user interacts with Prooftree only through the
25       graphical user interface. A substantial part of the proof-tree  visual‐
26       ization  task  is  done  by  Proof  General.   Therefore  not  only the
27       Prooftree command line arguments but also other  aspects  can  only  be
28       configured inside Proof General, see Proof General Customization below.
29

OPTIONS

31       -help  Print synopsis and exit.
32
33       -config
34              Open  the configuration dialog on startup (if you want to change
35              the configuration without starting Proof General).
36
37       -geometry spec
38              Sets the X geometry of the main window.  spec is  a  standard  X
39              geometry string in the form xposxypos[+xoff[+yoff]].
40
41       -tee file
42              Write all input to file (usually for debugging purposes).
43
44       -debug Provide more details on errors.
45
46       -help-dialog
47              Open  the help dialog on startup. Mainly useful for proofreading
48              the help text.
49

MAIN PROOF DISPLAY

51       Prooftree opens one window for each proof that it is requested to  dis‐
52       play.   This  window  contains the proof-tree graph and a small display
53       for sequents and proof commands.
54
55   Colors
56       The branches in the proof-tree graph are  colored  according  to  their
57       state.  Prooftree distinguishes between the following states.
58
59       current (blue by default)
60              The current branch is the branch from the root of the proof tree
61              to the current goal.
62
63       unproven (default foreground color)
64              A branch is unproven if it contains open proof goals.
65
66       proved incomplete (cyan by default)
67              An incompletely proved branch has its proof finished,  but  some
68              of  the  existential variables that have been introduced in this
69              branch are not (yet) instantiated.
70
71       proved partially (dark green by default)
72              In a partially proved branch all existential  variables  of  the
73              branch itself are instantiated, but some of those instantiations
74              contain existential variables that are not (yet) instantiated.
75
76       proved complete (green by default)
77              A branch is proved complete if all its existential variables are
78              instantiated with terms that themselves do not contain any exis‐
79              tential variables.
80
81       cheated (red by default)
82              A cheated branch contains a  cheating  proof  command,  such  as
83              admit
84
85       The colors as well as many other Prooftree parameters can be changed in
86       the Prooftree Configuration Dialog (see below).
87
88   Navigation
89       When the proof tree grows large one can navigate by a variety of means.
90       In  addition  to  scroll bars and the usual keys one can move the proof
91       tree by dragging with mouse button  1  pressed.  By  default,  dragging
92       moves  the viewport (i.e., the proof tree underneath moves in the oppo‐
93       site direction). After setting a negative value for  Drag  acceleration
94       in  the  Prooftree  Configuration  Dialog, dragging will move the proof
95       tree instead (i.e, the proof tree moves in the same  direction  as  the
96       mouse).
97
98   Sequent Display
99       The  sequent  display  below the proof tree normally shows the ancestor
100       sequent of the current goal. With a single left  mouse  click  one  can
101       display  any  goal  or  proof  command in the sequent display. A single
102       click outside the proof tree will switch back to default behavior.  The
103       initial size of the sequent display can be set in the Prooftree Config‐
104       uration Dialog.  A value of 0 hides the sequent display.
105
106   Tool Tips
107       Abbreviated proof commands and sequents are shown in full as tool  tips
108       when  the mouse pointer rests over them. Both, the tool tips for abbre‐
109       viated proof commands and for sequents can  be  independently  switched
110       off  in  the Prooftree Configuration Dialog.  The length at which proof
111       commands are abbreviated can be configured as well.
112
113   Additional Displays
114       A double click or a shift-click displays any goal or proof  command  in
115       an  additional  window.  These  additional  windows  are  automatically
116       updated, for instance, if an existential variable is instantiated.  For
117       additional sequent displays one can browse the instantiation history of
118       the sequent using the forward and backward  buttons.  These  additional
119       windows can be detached from the proof tree. A detached display is nei‐
120       ther automatically updated nor automatically deleted.
121
122   Existential Variables
123       Prooftree keeps track of existential variables, whether they have  been
124       instantiated and whether they depend on some other, not (yet) instanti‐
125       ated existential. It uses different colors  for  proved  branches  that
126       contain  non-instantiated  existential variables and branches that only
127       depend on some not instantiated existential.  The list of currently not
128       (yet)  instantiated existential variables is appended to proof commands
129       and sequents in tool-tips and the other displays.
130
131       The Existential Variable Dialog displays a table with  all  existential
132       variables of the current proof and their dependencies. Each line of the
133       table contains a button that marks the proof  command  that  introduced
134       this variable (with yellow background, by default) and, if present, the
135       proof command that instantiated this variable (with orange  background,
136       by default).
137
138   Main Menu
139       The  Menu button displays the main menu. The Clone item clones the cur‐
140       rent proof tree in an additional window. This additional window contin‐
141       ues to display a snapshot of the cloned proof tree, no matter what hap‐
142       pens with the original proof.
143
144       The Show current and Show selected items move the viewport of the proof
145       tree  such  that the current proof goal, or, respectively, the selected
146       node will be visible (if they exist).
147
148       The Exit item terminates Prooftree and closes all proof-tree displays.
149
150       The remaining three items display, respectively, the Prooftree Configu‐
151       ration Dialog, and the Help and About windows.
152
153   Context Menu
154       A  right  click  displays  the  Context Menu, which contains additional
155       items.
156
157       The item Undo to point is active over sequent nodes in the proof  tree.
158       There,  it  sends  an  retract  or  undo  request to Proof General that
159       retracts the scripting buffer up to that sequent.
160
161       The items Insert command and Insert subproof are active over proof com‐
162       mands. They sent, respectively, the selected proof command or all proof
163       commands in the selected subtree, to Proof General, which inserts  them
164       at point.
165

CONFIGURATION

167   Prooftree Configuration Dialog
168       The  Save  button  stores the current configuration (as marshaled OCaml
169       record) in ~/.prooftree, which will overwrite the built-in default con‐
170       figuration  for  the  following Prooftree runs. The Revert button loads
171       and applies the saved configuration.  The Cancel and OK  buttons  close
172       the  dialog,  but  Cancel  additionally resets the configuration to the
173       state before the start of the dialog. To  avoid  opening  partial  file
174       names, the Log Proof General input check box is deactivated when typing
175       the log file name.
176
177   Proof General Customization
178       The location of the Prooftree executable and the command line arguments
179       are  in  the  customization  group proof-tree.  Prover specific points,
180       such as the regular expressions for navigation  and  cheating  commands
181       are  in  the customization group proof-tree-internals.  To visit a cus‐
182       tomization group, type M-x customize-group followed by the name of  the
183       customization group inside Proof General.
184

LIMITATIONS

186       For  Coq >= 8.5, existential variables in Prooftree are severely broken
187       because Coq does not provide the necessary  information,  see  Coq  bug
188       4504.
189
190       In  Coq, proofs must be started with command Proof, which is the recom‐
191       mended practice anyway (see Coq problem report 2776).
192
193       In additional sequent displays, the information about existential vari‐
194       ables  is  only shown for the latest version of the sequent and not for
195       older versions in the instantiation history. The current  communication
196       protocol between Proof General and Prooftree does not permit more.
197

PREREQUISITES

199       This version of Prooftree requires Coq 8.4beta or better and Proof Gen‐
200       eral 4.3pre130327 or better.
201

FILES

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

SEE ALSO

209       The Prooftree web page, http://askra.de/software/prooftree/
210
211
212       The Proof General Adapting Manual
213              contains information about adapting Prooftree for  a  new  proof
214              assistant (see http://proofgeneral.inf.ed.ac.uk/adaptingman-lat
215              est.html).
216

CREDITS

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

AUTHOR

221       Hendrik Tews <prooftree at askra.de>
222
223
224
225PROOFTREE                         August 2011                     PROOFTREE(1)
Impressum