7. Graphical Proof-Tree Visualization
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.
|7.1 Starting and Stopping Proof-Tree Visualization|
|7.2 Features of Prooftree|
|7.3 Prooftree Customization|
7.1 Starting and Stopping Proof-Tree Visualization
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
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
proof-tree-external-display-toggle by one of the
three indicated means again. Alternatively you can also close the
Proof General launches only one instance of Prooftree, which can manage an arbitrary amount of proof-tree windows.
7.2 Features of Prooftree
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:
- Navigation in the proof tree and display of all previous proof states and proof commands.
- Display branches of the proof in different colors according to
their proof state, distinguishing branches with open, partially
or fully instantiated existential variables as well as branches
that have been finished by a cheating command such as
- Display the status of existential variables and their dependencies.
- Mark proof commands that introduce or instantiate a given existential variable.
- Snapshots of proof trees for reference when you retract your proof to try a different approach.
- Trigger a retract (undo) operation with a selected sequent as target.
- Insert proof scripts from the proof tree in the current buffer.
For a more elaborated description please consult the help dialog of Prooftree or the Prooftree man page.
7.3 Prooftree Customization
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
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.
This document was generated by Erik Martin-Dorel on April 2, 2020 using texi2html 1.82.