7. Graphical Proof-Tree Visualization

Since version 4.5, Proof General (again) supports proof-tree visualization on graphical desktops via the additional program Prooftree. Currently, proof-tree visualization is only supported for the Coq proof assistant. (Proof-tree visualization was already supported in version 4.2 but then discontinued in 2017 when Coq 8.7 dropped the variant of Show Goal that prooftree relied on.)

This version of Proof General requires Prooftree version 0.14. 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

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.

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 admit.
• 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 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.

This document was generated on April 18, 2024 using texi2html 1.82.