From e1c67a6cb5ba78af5faf43b87c1869de5f3161b9 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 15 Jan 2013 14:40:18 +0000 Subject: - support bullets and braces in Prooftree - prooftree protocol change to version 3 --- CHANGES | 7 +++++ coq/coq.el | 19 ++++++++----- doc/ProofGeneral.texi | 20 +++++++++++--- generic/proof-shell.el | 5 ++-- generic/proof-tree.el | 73 +++++++++++++++++++++++++++++++------------------- hol-light/hol-light.el | 2 +- 6 files changed, 84 insertions(+), 42 deletions(-) diff --git a/CHANGES b/CHANGES index 8dd018e8..55034825 100644 --- a/CHANGES +++ b/CHANGES @@ -6,6 +6,12 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. * Changes of Proof General 4.3 from Proof General 4.2 +** Generic/misc changes + +*** Require Prooftree version 0.11 + Check the Prooftree website to see which other versions of + Prooftree are compatible with Proof General 4.3. + ** Coq changes *** Asynchronous parallel compilation of required modules @@ -15,6 +21,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. to compile modules in parallel in the background while Proof General stays responsive. +*** Support for bullets and braces for Prooftree. * Changes of Proof General 4.2 from Proof General 4.1 diff --git a/coq/coq.el b/coq/coq.el index 89a380ce..b0906f65 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -190,7 +190,8 @@ See also `coq-hide-additional-subgoals'." :group 'coq-proof-tree) (defcustom coq-navigation-command-regexp - "^\\(Focus\\)\\|\\(Unfocus\\)" + (concat "^\\(\\(Focus\\)\\|\\(Unfocus\\)\\|" + "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|\\({\\)\\|\\(}\\)\\)") "Regexp for `proof-tree-navigation-command-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -203,8 +204,8 @@ See also `coq-hide-additional-subgoals'." (defcustom coq-proof-tree-current-goal-regexp (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?" - "\\(?: (unfocused: [0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " - "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)") + "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " + "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?: .*\n\\)+\\)\\(?:\n\\|$\\)") "Regexp for `proof-tree-current-goal-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -244,9 +245,13 @@ See also `coq-hide-additional-subgoals'." :type 'regexp :group 'coq-proof-tree) -(defcustom coq-proof-tree-proof-finished-regexp - "^\\(?:Proof completed\\)\\|\\(?:No more subgoals\\)\\." - "Regexp for `proof-tree-proof-finished-regexp'." +(defcustom coq-proof-tree-branch-finished-regexp + (concat "^\\(\\(?:Proof completed\\.\\)\\|\\(?:No more subgoals\\.\\)\\|" + "\\(No more subgoals but non-instantiated " + "existential variables:\\)\\|" + "\\(This subproof is complete, but there are " + "still unfocused goals.\\)\\)") + "Regexp for `proof-tree-branch-finished-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -1195,7 +1200,7 @@ flag Printing All set." coq-proof-tree-existentials-state-end-regexp proof-tree-additional-subgoal-ID-regexp coq-proof-tree-additional-subgoal-ID-regexp - proof-tree-proof-finished-regexp coq-proof-tree-proof-finished-regexp + proof-tree-branch-finished-regexp coq-proof-tree-branch-finished-regexp proof-tree-extract-instantiated-existentials 'coq-extract-instantiated-existentials proof-tree-show-sequent-command 'coq-show-sequent-command diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index f5149df8..58119672 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3081,7 +3081,16 @@ Query the prover about the identifier near mouse click @var{event}. 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 +for the Coq proof assistant. + +This version of Proof General requires Prooftree version 0.11. +Check the @uref{http://askra.de/software/prooftree/, 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 @uref{http://askra.de/software/prooftree/, Prooftree website} and the @uref{http://askra.de/software/prooftree/prooftree.man.html, @@ -4879,10 +4888,13 @@ you want to save abbrevs; answer yes. 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}. +@pxref{Graphical Proof-Tree Visualization}. To find out which +versions of Prooftree are compatible with this version of Proof +General, @pxref{Graphical Proof-Tree Visualization} or the +@uref{http://askra.de/software/prooftree/, Prooftree website}. -Proof-tree visualization does currently neither support bullets -and braces nor the command ``Grab Existential Variables''. +Proof-tree visualization does currently not support the command +``Grab Existential Variables''. For the visualization to work properly, proofs must be started with ``Proof.'', which is encouraged practice anyway (see Coq Bug diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c304f61d..cc7e56f8 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1513,7 +1513,8 @@ After processing the current output, the last step undertaken by the filter is to send the next command from the queue." (let ((span (caar proof-action-list)) (cmd (nth 1 (car proof-action-list))) - (flags (nth 3 (car proof-action-list)))) + (flags (nth 3 (car proof-action-list))) + (old-proof-marker (marker-position proof-marker))) ;; A copy of the last message, verbatim, never modified. (setq proof-shell-last-output @@ -1532,7 +1533,7 @@ by the filter is to send the next command from the queue." (proof-shell-handle-delayed-output))) ;; send output to the proof tree visualizer (if proof-tree-external-display - (proof-tree-handle-delayed-output cmd flags span))))) + (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) (defsubst proof-shell-display-output-as-response (flags str) diff --git a/generic/proof-tree.el b/generic/proof-tree.el index b73c2308..969dce05 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -211,8 +211,13 @@ the state display expands to the end of the prover output." :type '(choice regexp (const nil)) :group 'proof-tree-internals) -(defcustom proof-tree-proof-finished-regexp nil - "Regexp to match the no-more-subgoals message." +(defcustom proof-tree-branch-finished-regexp nil + "Regexp to recognize that the current branch has been finished. +This must match in precisely the following cases: +- The current branch has been finished but there is no current + open subgoal because the prover has not switched to the next + subgoal. +- The last open goal has been proved. " :type 'regexp :group 'proof-tree-internals) @@ -472,7 +477,7 @@ variables." ;; Low-level communication primitives ;; -(defconst proof-tree-protocol-version 2 +(defconst proof-tree-protocol-version 3 "Version of the communication protocol between Proof General and Prooftree. Must be increased if one of the low-level communication primitives is changed.") @@ -547,12 +552,12 @@ DATA as data sections to Prooftree." (1+ (string-bytes proof-name))))) (proof-tree-send-message second-line (list proof-name)))) -(defun proof-tree-send-proof-finished (state proof-name cmd-string +(defun proof-tree-send-branch-finished (state proof-name cmd-string cheated-flag existential-info) - "Send proof-finished to prooftree." + "Send branch-finished to prooftree." (proof-tree-send-message (format - (concat "proof-finished state %d %s proof-name-bytes %d command-bytes %d " + (concat "branch-finished state %d %s proof-name-bytes %d command-bytes %d " "existential-bytes %d") state (if cheated-flag "cheated" "not-cheated") @@ -820,6 +825,7 @@ This function cuts out the text between output, including the matches of these regular expressions. If the start regexp is nil, the empty string is returned. If the end regexp is nil, the match expands to the end of the prover output." + (goto-char start) (if (and proof-tree-existentials-state-start-regexp (proof-re-search-forward proof-tree-existentials-state-start-regexp end t)) @@ -832,7 +838,7 @@ regexp is nil, the match expands to the end of the prover output." (buffer-substring-no-properties start end)) "")) -(defun proof-tree-handle-proof-progress (cmd-string proof-info) +(defun proof-tree-handle-proof-progress (old-proof-marker cmd-string proof-info) "Send CMD-STRING and goals in delayed output to prooftree. This function is called if there is some real progress in a proof. This function sends the current state, the current goal @@ -840,9 +846,13 @@ and the list of additional open subgoals to Prooftree. Prooftree will sort out the rest. The delayed output is in the region -\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." - ;; (message "PTHPO cmd |%s| info %s flags %s start %s end %s" +\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]. +Urgent messages might be before that, following OLD-PROOF-MARKER, +which contains the position of `proof-marker', before the next +command was sent to the proof assistant." + ;; (message "PTHPO cmd |%s| info %s flags %s proof-marker %s start %s end %s" ;; cmd proof-info flags + ;; old-proof-marker ;; proof-shell-delayed-output-start ;; proof-shell-delayed-output-end) (let* ((start proof-shell-delayed-output-start) @@ -852,10 +862,17 @@ The delayed output is in the region (cheated-flag (and proof-tree-cheating-regexp (proof-string-match proof-tree-cheating-regexp cmd-string))) - (current-goals (proof-tree-extract-goals start end)) - (existential-info - (proof-tree-extract-existential-info start end))) - (if current-goals + current-goals) + ;; Check first for special cases, because Coq's output for finished + ;; branches is almost identical to proper goals. + (goto-char old-proof-marker) + (if (proof-re-search-forward proof-tree-branch-finished-regexp end t) + (proof-tree-send-branch-finished + proof-state proof-name cmd-string cheated-flag + (proof-tree-extract-existential-info start end)) + (goto-char start) + (setq current-goals (proof-tree-extract-goals start end)) + (when current-goals (let ((current-sequent-id (car current-goals)) (current-sequent-text (nth 1 current-goals)) ;; nth 2 current-goals contains the additional ID's @@ -867,21 +884,13 @@ The delayed output is in the region current-sequent-id current-sequent-text (nth 2 current-goals) - existential-info) + (proof-tree-extract-existential-info start end)) ;; put current sequent into hash (if it is not there yet) (unless (gethash current-sequent-id proof-tree-sequent-hash) (puthash current-sequent-id proof-state proof-tree-sequent-hash)) (proof-tree-register-existentials proof-state current-sequent-id - current-sequent-text)) - - ;; no current goal found, maybe the proof has been finished? - (goto-char start) - (if (proof-re-search-forward proof-tree-proof-finished-regexp end t) - (progn - (proof-tree-send-proof-finished - proof-state proof-name cmd-string - cheated-flag existential-info)))))) + current-sequent-text)))))) (defun proof-tree-handle-navigation (proof-info) "Handle a navigation command. @@ -901,7 +910,7 @@ The delayed output of the navigation command is in the region (proof-tree-send-switch-goal proof-state proof-name current-id))))) -(defun proof-tree-handle-proof-command (cmd proof-info) +(defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info) "Display current goal in prooftree unless CMD should be ignored." ;; (message "PTHPC") (let ((proof-state (car proof-info)) @@ -913,7 +922,8 @@ The delayed output of the navigation command is in the region (proof-string-match proof-tree-navigation-command-regexp cmd-string)) (proof-tree-handle-navigation proof-info) - (proof-tree-handle-proof-progress cmd-string proof-info))) + (proof-tree-handle-proof-progress old-proof-marker + cmd-string proof-info))) (setq proof-tree-last-state (car proof-info)))) (defun proof-tree-handle-undo (proof-info) @@ -989,13 +999,19 @@ The delayed output is in the region sequent-text))))))) -(defun proof-tree-handle-delayed-output (cmd flags span) +(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags span) "Process delayed output for prooftree. This function is the main entry point of the Proof General prooftree support. It examines the delayed output in order to take appropriate actions and maintains the internal state. -All arguments are (former) fields of the `proof-action-list' +The delayed output to handle is in the region +\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]. +Urgent messages might be before that, following OLD-PROOF-MARKER, +which contains the position of `proof-marker', before the next +command was sent to the proof assistant. + +All other arguments are (former) fields of the `proof-action-list' entry that is now finally retired. CMD is the command, FLAGS are the flags and SPAN is the span." ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags @@ -1035,7 +1051,8 @@ the flags and SPAN is the span." (when current-proof-name ;; we are inside a proof: display something (proof-tree-ensure-running) - (proof-tree-handle-proof-command cmd proof-info))))))) + (proof-tree-handle-proof-command old-proof-marker + cmd proof-info))))))) ;; diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index f3c983b0..3201e2ff 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -400,7 +400,7 @@ the currently open proof.") proof-tree-find-begin-of-unfinished-proof 'hol-light-find-begin-of-unfinished-proof ;; These ones belong in shell mode - proof-tree-proof-finished-regexp "No subgoals" + proof-tree-branch-finished-regexp "No subgoals" proof-tree-show-sequent-command (lambda (id) (format "print_xgoal_of_id \"%s\";;" id)) -- cgit v1.2.3