1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<HTML><HEAD><TITLE>Man page of PROOFTREE</TITLE>
</HEAD><BODY>
<H1>PROOFTREE</H1>
Section: User Manuals (1)<BR>Updated: August 2011<BR><A HREF="#index">Index</A>
<HR>
<A NAME="lbAB"> </A>
<H2>NAME</H2>
prooftree - proof-tree display for Proof General
<A NAME="lbAC"> </A>
<H2>SYNOPSIS</H2>
<B>prooftree </B>[<I>Options...</I>]
<A NAME="lbAD"> </A>
<H2>DESCRIPTION</H2>
<B>Prooftree</B>
visualizes proof trees during proof development with
<B>Proof General</B>.
Currently it only works for <B>Coq</B>, though adding
support for other proof assistants should be relatively easy.
<P>
To start a proof-tree display, hit the
<B>Prooftree</B>
icon in the
<B>Proof General</B>
tool-bar or select the menu entry
<I>Proof-General</I>
->
<I>Start/Stop Prooftree</I>
or type
<I>C-c C-d</I>
(which runs
<I>proof-tree-external-display-toggle</I>).
Inside a proof, this will immediately start a proof-tree display
for the current proof. Outside a proof,
<B>Proof General</B>
remembers to start the proof-tree display for the next proof.
<P>
Under normal circumstances
<B>Prooftree</B>
is started by
<B>Proof General</B>
as an
<B>Emacs</B>
subprocess. The user interacts with
<B>Prooftree</B>
only through the graphical user interface. A substantial part of
the proof-tree visualization task is done by
<B>Proof General</B>.
Therefore not only the
<B>Prooftree</B>
command line arguments but also other aspects can only be
configured inside
<B>Proof General</B>,
see
<B>Proof General Customization</B>
below.
<A NAME="lbAE"> </A>
<H2>OPTIONS</H2>
<DL COMPACT>
<DT>-help<DD>
Print synopsis and exit.
<DT>-config<DD>
Open the configuration dialog on startup (if you want to change
the configuration without starting
<B>Proof General</B>).
<DT>-geometry <I>spec</I><DD>
Sets the X geometry of the main window.
<I>spec</I>
is a standard X geometry string in the form
<I>xpos</I>x<I>ypos</I>[+<I>xoff</I>[+<I>yoff</I>]].
<DT>-tee <I>file</I><DD>
Write all input to
<I>file</I>
(usually for debugging purposes).
<DT>-debug<DD>
Provide more details on errors.
<DT>-help-dialog<DD>
Open the help dialog on startup. Mainly useful for proofreading
the help text.
</DL>
<A NAME="lbAF"> </A>
<H2>MAIN PROOF DISPLAY</H2>
<B>Prooftree</B>
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.
<A NAME="lbAG"> </A>
<H3>Colors</H3>
The branches in the proof-tree graph are colored
according to their state.
<B>Prooftree</B>
distinguishes between the following states.
<DL COMPACT>
<DT>current (blue by default)<DD>
The current branch is the branch from the root of the proof tree
to the current goal.
<DT>unproven (default foreground color)<DD>
A branch is unproven if it contains open proof goals.
<DT>proved incomplete (cyan by default)<DD>
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.
<DT>proved partially (dark green by default)<DD>
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.
<DT>proved complete (green by default)<DD>
A branch is proved complete if all its existential variables are
instantiated with terms that themselves do not contain any
existential variables.
<DT>cheated (red by default)<DD>
A cheated branch contains a cheating proof command, such as
<I>admit</I>
</DL>
<P>
The colors as well as many other
<B>Prooftree</B>
parameters can be changed in the
<B>Prooftree Configuration Dialog</B>
(see below).
<A NAME="lbAH"> </A>
<H3>Navigation</H3>
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
<I>Drag acceleration </I>
in the
<B>Prooftree Configuration Dialog</B>,
dragging will move the proof tree instead (i.e, the proof tree
moves in the same direction as the mouse).
<A NAME="lbAI"> </A>
<H3>Sequent Display</H3>
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
<B>Prooftree Configuration Dialog</B>.
A value of 0 hides the sequent display.
<A NAME="lbAJ"> </A>
<H3>Tool Tips</H3>
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
<B>Prooftree Configuration Dialog</B>.
The length at which proof commands are abbreviated can be
configured as well.
<A NAME="lbAK"> </A>
<H3>Additional Displays</H3>
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
<I>detached</I>
from the proof tree. A detached display is neither automatically
updated nor automatically deleted.
<A NAME="lbAL"> </A>
<H3>Existential Variables</H3>
<B>Prooftree</B>
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.
<P>
The
<B>Existential Variable Dialog</B>
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).
<A NAME="lbAM"> </A>
<H3>Main Menu</H3>
The
<I>Menu</I>
button displays the main menu. The
<I>Clone</I>
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.
<P>
The
<I>Show current</I>
and
<I>Show selected</I>
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).
<P>
The
<I>Exit</I>
item terminates
<B>Prooftree</B>
and closes all proof-tree displays.
<P>
The remaining three items display, respectively, the
<B>Prooftree Configuration Dialog</B>,
and the
<B>Help</B>
and
<B>About</B>
windows.
<A NAME="lbAN"> </A>
<H3>Context Menu</H3>
A right click displays the
<I>Context Menu</I>,
which contains additional items.
<P>
The item
<I>Undo to point</I>
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.
<P>
The items
<I>Insert command</I>
and
<I>Insert subproof</I>
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.
<A NAME="lbAO"> </A>
<H2>CONFIGURATION</H2>
<A NAME="lbAP"> </A>
<H3>Prooftree Configuration Dialog</H3>
The
<I>Save </I>
button stores the current configuration (as marshaled
<B>OCaml</B>
record) in
<I>~/.prooftree</I>,
which will overwrite the built-in default configuration for the
following
<B>Prooftree</B>
runs. The
<I>Revert</I>
button loads and applies the saved configuration.
The
<I>Cancel</I>
and
<I>OK</I>
buttons close the dialog, but
<I>Cancel</I>
additionally resets the configuration to the state before the
start of the dialog. To avoid opening partial file names, the
<I>Log Proof General input</I>
check box is deactivated when typing the log file name.
<A NAME="lbAQ"> </A>
<H3>Proof General Customization</H3>
The location of the
<B>Prooftree</B>
executable and the command line arguments are in the
customization group
<I>proof-tree</I>.
Prover specific points, such as the regular expressions for
navigation and cheating commands are in the customization group
<I>proof-tree-internals</I>.
To visit a customization group, type
<I>M-x customize-group</I>
followed by the name of the customization group inside
<B>Proof General</B>.
<A NAME="lbAR"> </A>
<H2>LIMITATIONS</H2>
For
<B>Coq</B>
>= 8.5, existential variables in
<B>Prooftree</B>
are severely broken because
<B>Coq</B>
does not provide the necessary information, see
<B>Coq</B>
bug 4504.
<P>
In
<B>Coq</B>,
proofs must be started with command
<I>Proof</I>,
which is the recommended practice anyway (see Coq problem report
2776).
<P>
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
<B>Proof General</B>
and
<B>Prooftree</B>
does not permit more.
<A NAME="lbAS"> </A>
<H2>PREREQUISITES</H2>
This version of
<B>Prooftree</B>
requires
<B>Coq</B>
8.4beta or better
and
<B>Proof General</B>
4.3pre130327 or better.
<A NAME="lbAT"> </A>
<H2>FILES</H2>
<DL COMPACT>
<DT>~/.prooftree<DD>
Saved
<B>Prooftree</B>
configuration. Is loaded at application start-up for overwriting
the built-in default configuration. Must contain a marshaled
<B>OCaml</B>
configuration record.
</DL>
<A NAME="lbAU"> </A>
<H2>SEE ALSO</H2>
<DL COMPACT>
<DT>The <B>Prooftree</B> web page, <I><A HREF="http://askra.de/software/prooftree/">http://askra.de/software/prooftree/</A></I><DD>
<P>
<DT>The <B>Proof General Adapting Manual</B><DD>
contains information about adapting
<B>Prooftree</B>
for a new proof assistant (see
<I><A HREF="http://proofgeneral.inf.ed.ac.uk/adaptingman-latest.html">http://proofgeneral.inf.ed.ac.uk/adaptingman-latest.html</A></I>).
</DL>
<A NAME="lbAV"> </A>
<H2>CREDITS</H2>
<B>Prooftree</B>
has been inspired by the proof tree display of
<B>PVS</B>.
<A NAME="lbAW"> </A>
<H2>AUTHOR</H2>
Hendrik Tews <prooftree at askra.de>
<P>
<HR>
<A NAME="index"> </A><H2>Index</H2>
<DL>
<DT><A HREF="#lbAB">NAME</A><DD>
<DT><A HREF="#lbAC">SYNOPSIS</A><DD>
<DT><A HREF="#lbAD">DESCRIPTION</A><DD>
<DT><A HREF="#lbAE">OPTIONS</A><DD>
<DT><A HREF="#lbAF">MAIN PROOF DISPLAY</A><DD>
<DL>
<DT><A HREF="#lbAG">Colors</A><DD>
<DT><A HREF="#lbAH">Navigation</A><DD>
<DT><A HREF="#lbAI">Sequent Display</A><DD>
<DT><A HREF="#lbAJ">Tool Tips</A><DD>
<DT><A HREF="#lbAK">Additional Displays</A><DD>
<DT><A HREF="#lbAL">Existential Variables</A><DD>
<DT><A HREF="#lbAM">Main Menu</A><DD>
<DT><A HREF="#lbAN">Context Menu</A><DD>
</DL>
<DT><A HREF="#lbAO">CONFIGURATION</A><DD>
<DL>
<DT><A HREF="#lbAP">Prooftree Configuration Dialog</A><DD>
<DT><A HREF="#lbAQ">Proof General Customization</A><DD>
</DL>
<DT><A HREF="#lbAR">LIMITATIONS</A><DD>
<DT><A HREF="#lbAS">PREREQUISITES</A><DD>
<DT><A HREF="#lbAT">FILES</A><DD>
<DT><A HREF="#lbAU">SEE ALSO</A><DD>
<DT><A HREF="#lbAV">CREDITS</A><DD>
<DT><A HREF="#lbAW">AUTHOR</A><DD>
</DL>
<HR>
This document was created by
<A HREF="http://www.nongnu.org/man2html/">man2html</A>,
using the manual pages.<BR>
Time: 10:35:43 GMT, January 03, 2017
</BODY>
</HTML>
|
