From 34c15424cc454cd59c5e094093acd6ddbdcc5186 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 3 Jan 2012 09:36:05 +0000 Subject: merge ProofTreeBranch into main trunk: - add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof --- doc/ProofGeneral.texi | 136 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-) (limited to 'doc/ProofGeneral.texi') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 6f04c513..daa90e5d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -161,6 +161,7 @@ provided for several other provers. * Unicode symbols and special layout support:: * Support for other Packages:: * Subterm Activation and Proof by Pointing:: +* Graphical Proof-Tree Visualization:: * Customizing Proof General:: * Hints and Tips:: * LEGO Proof General:: @@ -514,7 +515,8 @@ Proof General is designed to be useful for novices and expert users alike. It will be useful to you if you use a proof assistant, and you'd like an interface with the following features: simplified interaction, script management, multiple file scripting, a script editing mode, proof -by pointing, toolbar and menus, syntax highlighting, real symbols, +by pointing, proof-tree visualization, +toolbar and menus, syntax highlighting, real symbols, functions menu, tags, and finally, adaptability. Here is an outline of some of these features. Look in the contents @@ -554,6 +556,7 @@ regions. For more details, @pxref{Basic Script Management}, @ref{Script processing commands}, and @ref{Advanced Script Management and Editing}. + @item @i{Script editing mode}@* Proof General provides useful facilities for editing proof scripts, including syntax hilighting and a menu to jump to particular goals, @@ -563,6 +566,21 @@ assistant, or undo previous proof steps. For more details, @pxref{Script editing commands}, and @ref{Script processing commands}. + +@item @i{Proof-tree visualization}@* +In cooperation with the external program Prooftree +(available from the @uref{http://askra.de/software/prooftree/, +Prooftree website}), Proof General can display proof trees +graphically and provide visual information about the proof status +of different branches in a proof. The proof-tree display provides +additional means for inspecting the proof tree and thus helps +against loosing track in proofs. + +The graphical proof-tree visualization is currently only +supported for Coq. For more details, @pxref{Graphical Proof-Tree +Visualization}. + + @item @i{Toolbar and menus}@* A script buffer has a toolbar with navigation buttons for processing parts of the proof script. A menu provides further functions for @@ -3031,6 +3049,113 @@ Query the prover about the identifier near mouse click @var{event}. +@c ================================================================= +@c +@c CHAPTER +@c +@node Graphical Proof-Tree Visualization +@chapter Graphical Proof-Tree Visualization +@cindex 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. For installation instructions and +more detailed information about Prooftree, please refer to the +@uref{http://askra.de/software/prooftree/, Prooftree website} and +the @uref{http://askra.de/software/prooftree/prooftree.man.html, +Prooftree man page}. For information about how to support +proof-tree visualization for a different proof assistant, see +Section @i{Configuring Proof-Tree Visualization} in the +@i{Adapting Proof General} manual. + +@menu +* Starting and Stopping Proof-Tree Visualization:: +* Features of Prooftree:: +* Prooftree Customization:: +@end menu + + +@node Starting and Stopping Proof-Tree Visualization +@section 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 +@lisp + Proof-General -> Start/Stop Prooftree +@end lisp +or via the keyboard shortcut @kbd{C-c C-d}, all of which invoke +@code{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 @code{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. + +@node Features of Prooftree +@section 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: + +@itemize @bullet +@item Navigation in the proof tree and display of all previous +proof states and proof commands. +@item 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 +@code{admit}. +@item Display the status of existential variables and their +dependencies. +@item Mark proof commands that introduce or instantiate a +given existential variable. +@item Snapshots of proof trees for reference when you retract +your proof to try an different approach. +@end itemize + +For a more elaborated description please consult the help dialog +of Prooftree or the +@uref{http://askra.de/software/prooftree/prooftree.man.html, +Prooftree man page}. + + +@node Prooftree Customization +@section Prooftree Customization + +The location of the Prooftree program and command line +arguments can be configured in the customization group +@code{proof-tree}. You can visit this customization group inside +a running instance of Proof General by typing @code{M-x +customize-group proof-tree }. + +The graphical aspects of the proof-tree rendering, fonts and +colors can be changed inside Prooftree by invoking the +@code{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 +@code{proof-tree-internals}. Under normal circumstances there +should be no need to change one of these internal settings. + + @c ================================================================= @c @c CHAPTER @@ -4033,6 +4158,7 @@ assistant. It supports most of the generic features of Proof General. * Editing multiple proofs:: * User-loaded tactics:: * Holes feature:: +* Proof-Tree Visualization:: @end menu @@ -4608,6 +4734,14 @@ select the file named @code{coq-abbrev.el} in the you want to save abbrevs; answer yes. +@node Proof-Tree Visualization +@section Proof-Tree Visualization + +Starting with Proof General version 4.2 and Coq version 8.4, Coq +Proof General has full support for proof-tree visualization, +@pxref{Graphical Proof-Tree Visualization}. + + @c ================================================================= @c @c CHAPTER: Isabelle Proof General -- cgit v1.2.3