Next: Customizing Proof General, Previous: Subterm Activation and Proof by Pointing, Up: Top [Contents][Index]
Since version 4.2, Proof General supports proof-tree visualization on graphical desktops via the additional program Prooftree. Currently, proof-tree visualization is only supported for the Coq proof assistant.
This version of Proof General requires Prooftree version 0.11. Check the Prooftree website, to see if some later versions are also compatible. (Because of the communication protocol, Proof General is always only compatible with certain versions of Prooftree.)
For installation instructions and more detailed information about Prooftree, please refer to the Prooftree website and the Prooftree man page. For information about how to support proof-tree visualization for a different proof assistant, see Section Configuring Proof-Tree Visualization in the Adapting Proof General manual.
When proof-tree visualization is supported (currently only for the Coq proof assistant), you can start the visualization via the proof-tree button in the tool-bar, via the menu
Proof-General -> Start/Stop Prooftree
or via the keyboard shortcut C-c C-d, all of which invoke
proof-tree-external-display-toggle
.
If you are inside a proof, the graphical display is started immediately for your current proof. Otherwise the display starts as soon as you start the next proof. Starting the proof-tree display in the middle of a proof involves an automatic reexecution of your current proof script in the locked region, which should be almost unnoticeable, except for the time it takes.
The proof-tree display stops at the end of the proof or when you
invoke proof-tree-external-display-toggle
by one of the
three indicated means again. Alternatively you can also close the
proof-tree window.
Proof General launches only one instance of Prooftree, which can manage an arbitrary amount of proof-tree windows.
The proof-tree window provides visual information about the status of the different branches in your proof (by coloring completely proved branches in green, for example) and means for inspecting previous proof states without the need to retract parts of your proof script. Currently, Prooftree provides the following features:
admit
.
For a more elaborated description please consult the help dialog of Prooftree or the Prooftree man page.
The location of the Prooftree program and command line
arguments can be configured in the customization group
proof-tree
. You can visit this customization group inside
a running instance of Proof General by typing M-x
customize-group <RET> proof-tree <RET>
.
The graphical aspects of the proof-tree rendering, fonts and
colors can be changed inside Prooftree by invoking the
Configuration
item of the main menu.
Prover specific parts such as the regular expressions for
recognizing subgoals, existential variables and navigation and
cheating commands are in the customization group
proof-tree-internals
. Under normal circumstances there
should be no need to change one of these internal settings.
Previous: Features of Prooftree, Up: Graphical Proof-Tree Visualization [Contents][Index]