[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 25c2d37376 01/11: prooftree: Update proof tr
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general 25c2d37376 01/11: prooftree: Update proof tree display support for Coq 8.10 |
|
Date: |
Fri, 23 Feb 2024 10:01:19 -0500 (EST) |
branch: elpa/proof-general
commit 25c2d3737651e2983501ae77241cd8ead3274cf1
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
prooftree: Update proof tree display support for Coq 8.10
This is a major change, because the new Show Goal command in Coq
8.10 can print goals for previous states and therefore permits to
remove all the code that was tracking goals and existential from
PG and to rely on prooftree to request goals and goal updates.
This change does break compatibility for the proof tree display
for Coq 8.6 and before. (The old Coq versions themselves work,
it's just that proof tree display won't work.)
In paricular:
- delete urgent proof tree actions, the hooks and all the
corresponding code
- delete sequent hash and existentials info and all the corresponding code
- adopt prooftree regular expressions and show goal functions to
Coq 8.10 (implemented in coq/coq#10489)
- new hooks proof-tree-start-display-hook and
proof-tree-stop-display-hook for switching Coq's dependent evar
line on and off
- forward the new show goal commands from prooftree to Coq
- proof tree display starts with the Lemma command, because Proof
does not display anything anymore
- deleted superfluous proof tree code in hol-light and
deconfigured prooftree for Hol-Light, IIRC, it was never
working. But I am happy to provide support, if anybody wants to
pick this up.
---
coq/coq.el | 177 ++++----------------
generic/proof-shell.el | 11 +-
generic/proof-tree.el | 435 ++++++++++++-------------------------------------
3 files changed, 141 insertions(+), 482 deletions(-)
diff --git a/coq/coq.el b/coq/coq.el
index 54ae01ad00..52907a69f7 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -38,7 +38,6 @@
(require 'outline)
(require 'newcomment)
(require 'etags))
-(defvar proof-info) ; dynamic scope in proof-tree-urgent-action
(defvar action) ; dynamic scope in coq-insert-as stuff
(defvar string) ; dynamic scope in coq-insert-as stuff
(defvar old-proof-marker)
@@ -189,14 +188,8 @@ It is mostly useful in three window mode, see also
:group 'coq-config
:package-version '(ProofGeneral . "4.2"))
-;; Ignore all commands that start a proof. Otherwise "Proof" will appear
-;; as superfluous node in the proof tree. Note that we cannot ignore Proof,
-;; because, Fixpoint does not display the proof goal, see Coq bug #2776.
(defcustom coq-proof-tree-ignored-commands-regexp
- (concat "^\\(\\(Show\\)\\|\\(Locate\\)\\|"
- "\\(Theorem\\)\\|\\(Lemma\\)\\|\\(Remark\\)\\|\\(Fact\\)\\|"
- "\\(Corollary\\)\\|\\(Proposition\\)\\|\\(Definition\\)\\|"
- "\\(Let\\)\\|\\(Fixpoint\\)\\|\\(CoFixpoint\\)\\)")
+ "^\\(\\(Show\\)\\|\\(Locate\\)\\)"
"Regexp for `proof-tree-ignored-commands-regexp'."
:type 'regexp
:group 'coq-proof-tree)
@@ -231,7 +224,7 @@ It is mostly useful in three window mode, see also
:group 'coq-proof-tree)
(defcustom coq-proof-tree-update-goal-regexp
- (concat "^goal / evar \\([0-9]+\\) is:\n"
+ (concat "^goal ID \\([0-9]+\\) at state \\([0-9]+\\)\n"
"\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")
"Regexp for `proof-tree-update-goal-regexp'."
:type 'regexp
@@ -243,17 +236,6 @@ It is mostly useful in three window mode, see also
:type 'regexp
:group 'coq-proof-tree)
-(defcustom coq-proof-tree-existential-regexp "\\(\\?[0-9]+\\)"
- "Regexp for `proof-tree-existential-regexp'."
- :type 'regexp
- :group 'coq-proof-tree)
-
-(defcustom coq-proof-tree-instantiated-existential-regexp
- (concat coq-proof-tree-existential-regexp " using")
- "Regexp for recognizing an instantiated existential variable."
- :type 'regexp
- :group 'coq-proof-tree)
-
(defcustom coq-proof-tree-existentials-state-start-regexp
"^(dependent evars:"
"Coq instance of `proof-tree-existentials-state-start-regexp'."
@@ -2038,7 +2020,6 @@ at `proof-assistant-settings-cmds' evaluation time.")
proof-tree-new-layer-command-regexp coq-proof-tree-new-layer-command-regexp
proof-tree-current-goal-regexp coq-proof-tree-current-goal-regexp
proof-tree-update-goal-regexp coq-proof-tree-update-goal-regexp
- proof-tree-existential-regexp coq-proof-tree-existential-regexp
proof-tree-existentials-state-start-regexp
coq-proof-tree-existentials-state-start-regexp
proof-tree-existentials-state-end-regexp
@@ -2046,8 +2027,6 @@ at `proof-assistant-settings-cmds' evaluation time.")
proof-tree-additional-subgoal-ID-regexp
coq-proof-tree-additional-subgoal-ID-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
proof-tree-find-undo-position 'coq-proof-tree-find-undo-position
)
@@ -2207,78 +2186,9 @@ Set Diffs setting if Coq is running and has a version >=
8.10."
;; * the name of the current proof or nil
(list (car info) (nth 3 info))))
-(defun coq-extract-instantiated-existentials (start end)
- "Coq specific function for `proof-tree-extract-instantiated-existentials'.
-Return the list of currently instantiated existential variables."
- (proof-tree-extract-list
- start end
- coq-proof-tree-existentials-state-start-regexp
- coq-proof-tree-existentials-state-end-regexp
- coq-proof-tree-instantiated-existential-regexp))
-
-(defun coq-show-sequent-command (sequent-id)
+(defun coq-show-sequent-command (sequent-id state)
"Coq specific function for `proof-tree-show-sequent-command'."
- (format "Show Goal \"%s\"." sequent-id))
-
-(defun coq-proof-tree-get-new-subgoals ()
- "Check for new subgoals and issue appropriate Show commands.
-This is a hook function for `proof-tree-urgent-action-hook'. This
-function examines the current goal output and searches for new
-unknown subgoals. Those subgoals have been generated by the last
-proof command and we must send their complete sequent text
-eventually to prooftree. Because subgoals may change with
-the next proof command, we must execute the additionally needed
-Show commands before the next real proof command.
-
-The ID's of the open goals are checked with
-`proof-tree-sequent-hash' in order to find out if they are new.
-For any new goal an appropriate Show Goal command with a
-'proof-tree-show-subgoal flag is inserted into
-`proof-action-list'. Then, in the normal delayed output
-processing, the sequent text is send to prooftree as a sequent
-update (see `proof-tree-update-sequent') and the ID of the
-sequent is registered as known in `proof-tree-sequent-hash'.
-
-Searching for new subgoals must only be done when the proof is
-not finished, because Coq 8.5 lists open existential variables
-as (new) open subgoals. For this test we assume that
-`proof-marker' has not yet been moved.
-
-The `proof-tree-urgent-action-hook' is also called for undo
-commands. For those, nothing is done.
-
-The not yet delayed output is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
- ;; (message "CPTGNS start %s end %s"
- ;; proof-shell-delayed-output-start
- ;; proof-shell-delayed-output-end)
- (let ((start proof-shell-delayed-output-start)
- (end proof-shell-delayed-output-end)
- (state (car proof-info)))
- (when (> state proof-tree-last-state)
- (with-current-buffer proof-shell-buffer
- ;; The message "All the remaining goals are on the shelf" is processed as
- ;; urgent message and is therefore before
- ;; proof-shell-delayed-output-start. We therefore need to go back to
- ;; proof-marker.
- (goto-char proof-marker)
- (unless (proof-re-search-forward
- coq-proof-tree-branch-finished-regexp end t)
- (goto-char start)
- (while (proof-re-search-forward
- coq-proof-tree-additional-subgoal-ID-regexp end t)
- (let ((subgoal-id (match-string-no-properties 1)))
- (unless (gethash subgoal-id proof-tree-sequent-hash)
- ;; (message "CPTGNS new sequent %s found" subgoal-id)
- (push (proof-shell-action-list-item
- (coq-show-sequent-command subgoal-id)
- (proof-tree-make-show-goal-callback (car proof-info))
- '(no-goals-display
- no-response-display
- proof-tree-show-subgoal))
- proof-action-list)))))))))
-
-(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals)
+ (format "Show Goal %s at %d." sequent-id state))
(defun coq-find-begin-of-unfinished-proof ()
@@ -2318,13 +2228,18 @@ This is the Coq incarnation of
`proof-tree-find-undo-position'."
;; crash with a parsing error. Proof General must therefore turn on the evar
;; output with the command "Set Printing Dependent Evars Line". Of course,
;; after the proof, the evar line must be set back to what it was before the
-;; proof. I therefore look in the urgent action hook if proof display is
-;; switched on or off. When switched on, I test the current evar printing
-;; status with the undocumented command "Test Printing Dependent Evars Line" to
-;; remember if I have to switch evar printing off eventually.
+;; proof. I therefore test in proof-tree-start-display-hook the state of the
+;; Dependent Evars Line flag and remember the Coq state number in
+;; coq--proof-tree-must-disable-evars if the flag was off. When the proof tree
+;; display is switched off and the state is bigger, I reset the flag. This way
+;; the flag is not unnecessarily reset on undo. The only exception is, when you
+;; switch on the proof tree display a few commands before starting the proof.
(defvar coq--proof-tree-must-disable-evars nil
- "Remember if evar printing must be disabled when leaving the current proof.")
+ "Remember if evar printing must be disabled when leaving the current proof.
+When nil, evar printing does not need to be disabled. When
+non-nil, contains the state number where evar printing was
+enabled, to only disable it, when there was not undo.")
(defun coq-proof-tree-enable-evar-callback (_span)
"Callback for the evar printing status test.
@@ -2344,70 +2259,50 @@ fact in `coq--proof-tree-must-disable-evars'."
(if (looking-at "off")
(progn
;; (message "CPTEEC evar line mode was off")
- (setq coq--proof-tree-must-disable-evars t))
+ (setq coq--proof-tree-must-disable-evars
+ (car (coq-last-prompt-info-safe))))
;; (message "CPTEEC evar line mode was on")
(setq coq--proof-tree-must-disable-evars nil))))))
(defun coq-proof-tree-insert-evar-command (cmd &optional callback)
"Insert an evar printing command at the head of `proof-action-list'."
- (push (proof-shell-action-list-item
- (concat cmd " Printing Dependent Evars Line.")
- (if callback callback 'proof-done-invisible)
- (list 'invisible))
- proof-action-list))
+ (proof-add-to-queue
+ (list
+ (proof-shell-action-list-item
+ (concat cmd " Printing Dependent Evars Line.")
+ (if callback callback 'proof-done-invisible)
+ (list 'invisible 'no-response-display)))))
(defun coq-proof-tree-enable-evars ()
"Enable the evar status line for Coq >= 8.6.
Test the status of evar printing to be able to set it back
properly after the proof and enable the evar printing."
(when (coq--post-v86)
- ;; We push to proof-action-list --- therefore we need to push in reverse
- ;; order!
- (coq-proof-tree-insert-evar-command "Set")
+ (proof-shell-ready-prover)
(coq-proof-tree-insert-evar-command
"Test"
- 'coq-proof-tree-enable-evar-callback)))
+ 'coq-proof-tree-enable-evar-callback)
+ (coq-proof-tree-insert-evar-command "Set")))
+
+(add-hook 'proof-tree-start-display-hook #'coq-proof-tree-enable-evars)
(defun coq-proof-tree-disable-evars ()
"Disable evar printing if necessary.
This function switches off evar printing after the proof, if it
-was off before the proof. For undo commands, we rely on the fact
-that Coq itself undoes the effect of the evar printing change that
-we inserted after the goal statement. We also rely on the fact
-that Proof General never backtracks into the middle of a
+was off before the proof. For undo commands, I rely on the fact
+that Coq itself undoes the effect of the evar printing change
+that I inserted before the goal statement and on the state number
+stored in coq--proof-tree-must-disable-evars. I also rely on the
+fact that Proof General never backtracks into the middle of a
proof. (If this would happen, Coq would switch evar printing on
-and the code here would not switch it off after the proof.)
-
-Being called from `proof-tree-urgent-action-hook', this function
-can rely on `proof-info' being dynamically bound to the last
-result of `coq-proof-tree-get-proof-info'."
+and the code here would not switch it off after the proof.)"
(when coq--proof-tree-must-disable-evars
- (when (> (car proof-info) proof-tree-last-state)
+ (when (> (car (coq-last-prompt-info-safe))
+ coq--proof-tree-must-disable-evars)
(coq-proof-tree-insert-evar-command "Unset"))
(setq coq--proof-tree-must-disable-evars nil)))
-(defun coq-proof-tree-evar-display-toggle ()
- "Urgent action hook function for changing the evar printing status in Coq.
-This function is for `proof-tree-urgent-action-hook' (which is
-called only if external proof display is switched on). It checks
-whether a proof was started or stopped and inserts commands for
-enableing and disabling the evar status line for Coq 8.6 or
-later. Without the evar status line being enabled, prooftree
-crashes.
-
-Must only be called via `proof-tree-urgent-action-hook' to ensure
-that the dynamic variable `proof-info' is bound to the current
-result of `coq-proof-tree-get-proof-info'."
- (let ((current-proof-name (cadr proof-info)))
- (cond
- ((and (null proof-tree-current-proof) current-proof-name)
- ;; started a new proof
- (coq-proof-tree-enable-evars))
- ((and proof-tree-current-proof (null current-proof-name))
- ;; finished the current proof
- (coq-proof-tree-disable-evars)))))
-
-(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-evar-display-toggle)
+(add-hook 'proof-tree-stop-display-hook #'coq-proof-tree-disable-evars)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3de1c87684..52e8ff24d1 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -60,7 +60,6 @@
;; declare a few functions and variables from proof-tree - if we
;; require proof-tree the compiler complains about a recusive
;; dependency.
-(declare-function proof-tree-urgent-action "proof-tree" (flags))
(declare-function proof-tree-handle-delayed-output "proof-tree"
(old-proof-marker cmd flags span))
;; without the nil initialization the compiler still warns about this variable
@@ -143,7 +142,8 @@ and to be executed last is at the head.")
(condition-case err
(funcall (nth 2 listitem) (car listitem))
(error
- (message "error escaping proof-shell-invoke-callback: %s" err)
+ (message "error escaping proof-shell-invoke-callback %s for command %s:
%s"
+ (nth 2 listitem) (nth 1 listitem) err)
nil)))
(defvar proof-second-action-list-active nil
@@ -1235,11 +1235,7 @@ contains only invisible elements for Prooftree
synchronization."
;; proof-action-list and where the next item has not yet been
;; sent to the proof assistant. This is therefore one of the
;; few points where it is safe to manipulate
- ;; proof-action-list. The urgent proof-tree display actions
- ;; must therefore be called here, because they might add some
- ;; Show actions at the front of proof-action-list.
- (if proof-tree-external-display
- (proof-tree-urgent-action flags))
+ ;; proof-action-list.
;; Add priority actions to the front of proof-action-list.
;; Delay adding of priority items until there is no priority
@@ -1363,6 +1359,7 @@ ends with text matching
`proof-shell-eager-annotation-end'."
((proof-looking-at-safe proof-shell-theorem-dependency-list-regexp)
(proof-shell-process-urgent-message-thmdeps))
+ ;;XXX duplication?
((proof-looking-at-safe proof-shell-theorem-dependency-list-regexp)
(proof-shell-process-urgent-message-thmdeps))
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 6ddefead45..5ac537ed84 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -179,14 +179,16 @@ prooftree."
:group 'proof-tree-internals)
(defcustom proof-tree-update-goal-regexp nil
- "Regexp to match a goal and its ID.
+ "Regexp to match a goal and its ID and the corresponding state.
The regexp is matched against the output of additional show-goal
-commands inserted by Proof General with a command returned by
-`proof-tree-show-sequent-command'. Proof General inserts such
-commands to update the goal text in prooftree. This is necessary,
+commands inserted by prooftree with a command returned by
+`proof-tree-show-sequent-command'. Prooftree inserts such
+commands to update the goal texts. This is necessary,
for instance, when existential variables get instantiated. This
-regexp must have 2 grouping constructs, the first matching the ID
-of the goal, the second the complete sequent text."
+regexp must have 3 grouping constructs, the first matching the ID
+of the goal, the second the proof assistant state to which the
+sequent text corresponds, which must be a number, and the third
+the complete sequent text."
:type 'regexp
:group 'proof-tree-internals)
@@ -198,20 +200,6 @@ subgoal ID with subgroup 1."
:type 'regexp
:group 'proof-tree-internals)
-(defcustom proof-tree-existential-regexp nil
- "Regexp to match existential variables.
-Existential variables exist for instance in Isabelle/Hol and in
-Coq. They are placeholders for terms that might (for Coq they
-must) get instantiated in a later stage of the proof. This regexp
-should match one existential variable in subgroup 1. It is used
-inside a while loop to extract all existential variables from the
-goal text or from a list of existential variables.
-
-Leave this variable at nil for proof assistants that do not have
-existential variables."
- :type '(choice regexp (const nil))
- :group 'proof-tree-internals)
-
(defcustom proof-tree-existentials-state-start-regexp nil
"Regexp to match the start of the state display of existential variables.
Together with `proof-tree-existentials-state-end-regexp', this
@@ -269,31 +257,15 @@ is retracted (but no stuff before X)."
:type 'function
:group 'proof-tree-internals)
-(defcustom proof-tree-extract-instantiated-existentials nil
- "Proof assistant specific function for instantiated existential variables.
-This function must only be defined if the prover has existential
-variables, that is, if `proof-tree-existential-regexp' is
-non-nil.
-
-If defined, this function should return the list of currently
-instantiated existential variables as a list of strings. The
-function is called with `proof-shell-buffer' as current
-buffer and with two arguments start and stop, which designate the
-region containing the last output from the proof assistant.
-
-`proof-tree-extract-list' might be useful for writing this
-function."
- :type '(choice function (const nil))
- :group 'proof-tree-internals)
-
(defcustom proof-tree-show-sequent-command nil
"Proof assistant specific function for a show-goal command.
-This function is applied to an ID of a goal and should return a
-command (as string) that will display the complete sequent with
-that ID. The regexp `proof-tree-update-goal-regexp' should match
-the output of the proof assistant for the returned command, such
-that `proof-tree-update-sequent' will update the sequent ID
-inside prooftree.
+This function is applied to a goal ID and a state number and
+should return a command (as string) that will display the
+complete sequent with that ID in the given state. The regexp
+`proof-tree-update-goal-regexp' should match the output of the
+proof assistant for the returned command, such that
+`proof-tree-update-sequent' will update the sequent ID inside
+prooftree.
If the proof assistant is unable to redisplay sequent ID the
function should return nil and prooftree will not get updated."
@@ -321,25 +293,30 @@ must return a buffer position."
:type 'function
:group 'proof-tree-internals)
-(defcustom proof-tree-urgent-action-hook ()
- "Normal hook for prooftree actions that cannot be delayed.
-This hook is called (indirectly) from inside
-`proof-shell-exec-loop' after the preceeding command and any
-comments that follow have been choped off `proof-action-list' and
-before the next command is sent to the proof assistant. This hook
-can therefore be used to insert additional commands into
-`proof-action-list' that must be executed before the next real
-proof command.
-
-Functions in this hook can rely on `proof-info' being bound to
-the result of `proof-tree-get-proof-info'.
-
-This hook is used, for instance, for Coq to insert Show commands
-for newly generated subgoals. (The normal Coq output does not
-contain the complete sequent text of newly generated subgoals.)"
+(defcustom proof-tree-start-display-hook ()
+ "Normal hook for prooftree when external display starts.
+This hook is called when the external display is startet, more
+precisely, when the proof assistant is in the state that Proof
+General starts to send display commands to prooftree. This means,
+retraction to the start of the proof, in case it was necessary,
+has been done and `proof-action-list` is empty.
+
+This hook is used, for instance, for Coq to enable the dependent
+evars line."
:type 'hook
:group 'proof-tree-internals)
+(defcustom proof-tree-stop-display-hook ()
+ "Normal hook for prooftree when external display stops.
+This hook is called when the external display is stoped either
+because the proof has been finished, the script was retracted to
+a point before the proof, or the external prooftree process
+requested to stop.
+
+This hook is used, for instance, for Coq to disable the dependent
+evars line."
+ :type 'hook
+ :group 'proof-tree-internals)
;;
;; Internal variables
@@ -373,6 +350,10 @@ Controlled by `proof-tree-external-display-toggle'.")
"\nemacs exec: \\([-a-z]+\\) *\\([^\n]*\\)\n"
"Regular expression to match callback commands from the prooftree process.")
+(defconst proof-tree--show-goal-command-regexp
+ "\"\\([^\"]*\\)\" at \\([0-9]*\\) for \"\\([^\"]*\\)\""
+ "Regular expression to match the data part of the prooftree show-goal
command.")
+
(defvar proof-tree-last-state 0
"Last state of the proof assistant.
Used for undoing in prooftree.")
@@ -382,37 +363,6 @@ Used for undoing in prooftree.")
This variable is only maintained and meaningful if
`proof-tree-external-display' is t.")
-(defvar proof-tree-sequent-hash nil
- "Hash table to remember sequent ID's.
-Needed because some proof assistants do not distinguish between
-new subgoals, which have been created by the last proof command,
-and older, currently unfocussed subgoals. If Proof General meets
-a goal, it is treated as new subgoal if it is not in this hash yet.
-
-The hash is mostly used as a set of sequent ID's. However, for
-undo operations it is necessary to delete all those sequents from
-the hash that have been created in a state later than the undo
-state. For this purpose this hash maps sequent ID's to the state
-number in which the sequent has been created.
-
-The hash table is initialized in `proof-tree-start-process'.")
-
-(defvar proof-tree-existentials-alist nil
- "Alist mapping existential variables to sequent ID's.
-Used to remember which goals need a refresh when an existential
-variable gets instantiated. To support undo commands the old
-contents of this list must be stored in
-`proof-tree-existentials-alist-history'. To ensure undo is
-properly working, this variable should only be changed by using
-`proof-tree-delete-existential-assoc',
-`proof-tree-add-existential-assoc' or
-`proof-tree-clear-existentials'.")
-
-(defvar proof-tree-existentials-alist-history nil
- "Alist mapping state numbers to old values of
`proof-tree-existentials-alist'.
-Needed for undo.")
-
-
;;
;; process filter function that receives prooftree output
;;
@@ -428,6 +378,28 @@ because not all data from Prooftee has yet arrived. In
this case
the continuation is stored in this variable and will be called
from `proof-tree-process-filter' when more output arrives.")
+
+(defun proof-tree-handle-goal-request (data)
+ "Handle a show-goal command from prooftree.
+The command from prooftree has the form \"emacs exec: show-goal
+\"29\" at 21\"."
+ (if (string-match proof-tree--show-goal-command-regexp data)
+ (let ((goal-id (match-string 1 data))
+ (state (string-to-number (match-string 2 data)))
+ (proof-name (match-string 3 data))
+ show-cmd)
+ ;; (message "show goal %s at %d for %s" goal-id state proof-name)
+ (setq show-cmd (funcall proof-tree-show-sequent-command goal-id state))
+ (when show-cmd
+ (proof-add-to-priority-queue
+ (proof-shell-action-list-item
+ show-cmd
+ (proof-tree-make-show-goal-callback proof-name)
+ '(no-goals-display no-response-display proof-tree-show-subgoal)))))
+ (display-warning
+ '(proof-general proof-tree)
+ (format "Malformed prooftree show-goal command") :warning)))
+
(defun proof-tree-stop-external-display ()
"Prooftree callback for the command \"stop-displaying\"."
(if proof-tree-current-proof
@@ -500,7 +472,10 @@ In this case they store a continuation function in
piece of output arrives. `proof-tree-output-marker' points to the
next piece of Prooftree output that needs to get processed. If
everything is processed, the marker is deleted and
-`proof-tree-insert-output' sets it again for the next output."
+`proof-tree-insert-output' sets it again for the next output.
+
+This function relies on the POSIX guarantee that up to 512 bytes
+are transmitted atomically over a pipe."
(proof-tree-insert-output string)
(let ((continuation proof-tree-filter-continuation)
command-found command data)
@@ -528,6 +503,8 @@ everything is processed, the marker is deleted and
(set-marker proof-tree-output-marker (point-max)))))
(when command-found
(cond
+ ((equal command "show-goal")
+ (proof-tree-handle-goal-request data))
((equal command "stop-displaying")
(proof-tree-stop-external-display))
((equal command "undo")
@@ -589,10 +566,6 @@ variables."
(set-process-sentinel proof-tree-process #'proof-tree-process-sentinel)
(set-process-query-on-exit-flag proof-tree-process nil)
;; other initializations
- (setq proof-tree-sequent-hash (make-hash-table :test 'equal)
- proof-tree-last-state 0
- proof-tree-existentials-alist nil
- proof-tree-existentials-alist-history nil)
(proof-tree-send-configure)))
@@ -643,8 +616,9 @@ DATA as data sections to Prooftree."
current-sequent-text additional-sequent-ids
existential-info)
"Send the current goal state to prooftree."
- ;; (message "PTSGS id %s sequent %s ex-info %s"
- ;; current-sequent-id current-sequent-text existential-info)
+ ;; (message "PTSGS id %s command %s sequent %s ex-info %s"
+ ;; current-sequent-id command-string current-sequent-text
+ ;; existential-info)
(let* ((add-id-string (mapconcat #'identity additional-sequent-ids " "))
(second-line
(format
@@ -668,6 +642,7 @@ DATA as data sections to Prooftree."
(defun proof-tree-send-update-sequent (state proof-name sequent-id
sequent-text)
"Send the updated sequent text to prooftree."
+ ;; (message "ptsus state %d proof %s sequent %s" state proof-name sequent-id)
(let ((second-line
(format
(concat "update-sequent state %d sequent %s proof-name-bytes %d "
@@ -723,192 +698,32 @@ DATA as data sections to Prooftree."
;;
-;; proof-tree-existentials-alist manipulations and history
-;;
-
-(defun proof-tree-record-existentials-state (state &optional dont-copy)
- "Store the current state of `proof-tree-existentials-alist' for undo.
-Usually this involves making a copy of
-`proof-tree-existentials-alist' because of the destructive
-updates used on that list. If optional argument DONT-COPY is
-non-nil no copy is done."
- (setq proof-tree-existentials-alist-history
- (cons (cons state
- (if dont-copy
- proof-tree-existentials-alist
- (copy-alist proof-tree-existentials-alist)))
- proof-tree-existentials-alist-history)))
-
-(defun proof-tree-undo-state-var (proof-state var-symbol history-symbol)
- "Undo changes to VAR-SYMBOL using HISTORY-SYMBOL.
-This is a general undo function for variables that keep their
-undo information in a alist that maps state numbers to old
-values. Argument PROOF-STATE is the state to reestablish,
-VAR-SYMBOL is (the symbol of) the variable to undo and
-HISTORY-SYMBOL is (the symbol of) the undo history alist."
- (let ((undo-not-finished t)
- (history (symbol-value history-symbol))
- (var (symbol-value var-symbol)))
- (while (and undo-not-finished history)
- (if (> (caar history) proof-state)
- (progn
- (setq var (cdr (car history)))
- (setq history (cdr history)))
- (setq undo-not-finished nil)))
- (set var-symbol var)
- (set history-symbol history)))
-
-(defun proof-tree-undo-existentials (proof-state)
- "Undo changes in `proof-tree-existentials-alist'.
-Change `proof-tree-existentials-alist' back to its contents in
-state PROOF-STATE."
- (proof-tree-undo-state-var proof-state
- 'proof-tree-existentials-alist
- 'proof-tree-existentials-alist-history))
-
-(defun proof-tree-delete-existential-assoc (state ex-assoc)
- "Delete mapping EX-ASSOC from ‘proof-tree-existentials-alist’."
- (proof-tree-record-existentials-state state)
- (setq proof-tree-existentials-alist
- (delq ex-assoc proof-tree-existentials-alist)))
-
-(defun proof-tree-add-existential-assoc (state ex-var sequent-id)
- "Add the mapping EX-VAR -> SEQUENT-ID to ‘proof-tree-existentials-alist’.
-Do nothing if this mapping does already exist."
- (let ((ex-var-assoc (assoc ex-var proof-tree-existentials-alist)))
- (if ex-var-assoc
- (unless (member sequent-id (cdr ex-var-assoc))
- (proof-tree-record-existentials-state state)
- (setcdr ex-var-assoc (cons sequent-id (cdr ex-var-assoc))))
- (proof-tree-record-existentials-state state)
- (setq proof-tree-existentials-alist
- (cons (cons ex-var (list sequent-id))
- proof-tree-existentials-alist)))))
-
-(defun proof-tree-clear-existentials ()
- "Clear the mapping in `proof-tree-existentials-alist' and its history."
- (setq proof-tree-existentials-alist nil)
- (setq proof-tree-existentials-alist-history nil))
-
-
-;;
-;; Process urgent output from the proof assistant
+;; Process output from the proof assistant
;;
-(defun proof-tree-show-goal-callback (state)
+(defun proof-tree-show-goal-callback (proof-name)
"Callback for display-goal commands inserted by this package.
Update the sequent and run hooks in `proof-state-change-hook'.
-Argument STATE is the state number (i.e., an integer) with which
-the update sequent command should be associated.
-
-The STATE is necessary, because a comment following a branching
-command cat get retired together with the branching command
-before the show-goal commands that update sequents are processed.
-The effect of the sequent update would therefore be undone when
-the comment alone is retracted.
+Argument PROOF-NAME is necessary, because show goal commands can
+be delayed until after the proof.
You CANNOT put this function directly as callback into
`proof-action-list' because callbacks receive the span as
-argument and this function expects an integer! Rather you should
+argument and this function expects a string! Rather you should
call `proof-tree-make-show-goal-callback', which evaluates to a
lambda expressions that you can put into `proof-action-list'."
- ;;(message "PTSGC %s" state)
- (proof-tree-update-sequent state)
+ (proof-tree-update-sequent proof-name)
(run-hooks 'proof-state-change-pre-hook)
(run-hooks 'proof-state-change-hook))
-(defun proof-tree-make-show-goal-callback (state)
+(defun proof-tree-make-show-goal-callback (proof-name)
"Create the callback for display-goal commands."
- (lambda (_span) (proof-tree-show-goal-callback state)))
-
-(defun proof-tree-urgent-action (flags)
- "Handle urgent points before the next item is sent to the proof assistant.
-Schedule goal updates when existential variables have changed and
-call `proof-tree-urgent-action-hook'. All this is only done if
-the current output does not come from a command (with the
-'proof-tree-show-subgoal flag) that this package inserted itself.
-
-Urgent actions are only needed if the external proof display is
-currently running. Therefore this function should not be called
-when `proof-tree-external-display' is nil.
-
-This function assumes that the prover output is not suppressed.
-Therefore, `proof-tree-external-display' being t is actually a
-necessary precondition.
-
-The not yet delayed output is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
- ;; (message "PTUA flags %s start %s end %s pal %s ptea %s"
- ;; flags
- ;; proof-shell-delayed-output-start
- ;; proof-shell-delayed-output-end
- ;; proof-action-list
- ;; proof-tree-existentials-alist)
- (let* ((proof-info (funcall proof-tree-get-proof-info))
- (state (car proof-info))
- (start proof-shell-delayed-output-start)
- (end proof-shell-delayed-output-end)
- inst-ex-vars)
- (unless (memq 'proof-tree-show-subgoal flags)
- (when (and (> state proof-tree-last-state)
- proof-tree-existential-regexp
- proof-tree-existentials-alist)
- ;; Only deal with existentials if this is not and undo
- ;; command, if the proof assistant actually has existentials
- ;; (i.e., proof-tree-existential-regexp is set) and if there
- ;; are some goals with existentials.
- (setq inst-ex-vars
- (with-current-buffer proof-shell-buffer
- (funcall proof-tree-extract-instantiated-existentials
- start end)))
- (dolist (ex-var inst-ex-vars)
- (let ((var-goal-assoc (assoc ex-var proof-tree-existentials-alist)))
- (when var-goal-assoc
- (dolist (sequent-id (cdr var-goal-assoc))
- (let ((show-cmd
- (funcall proof-tree-show-sequent-command sequent-id)))
- (if show-cmd
- (setq proof-action-list
- (cons (proof-shell-action-list-item
- show-cmd
- (proof-tree-make-show-goal-callback state)
- '(no-goals-display no-response-display
- proof-tree-show-subgoal))
- proof-action-list)))))
- (proof-tree-delete-existential-assoc state var-goal-assoc)))))
- (run-hooks 'proof-tree-urgent-action-hook))
- ;; (message "PTUA END pal %s ptea %s"
- ;; proof-action-list
- ;; proof-tree-existentials-alist)
- ))
-
-
-;;
-;; Process output from the proof assistant
-;;
+ `(lambda (_span) (proof-tree-show-goal-callback ,proof-name)))
(defun proof-tree-quit-proof ()
- "Reset internal state when there is no current proof any more.
-Because currently it is not possible to undo into the middle of a
-proof, we can safely flush the `proof-tree-sequent-hash' and
-`proof-tree-existentials-alist-history' when the current proof is
-finished or quit."
- (clrhash proof-tree-sequent-hash)
- (proof-tree-clear-existentials)
- (setq proof-tree-current-proof nil))
-
-(defun proof-tree-register-existentials (current-state sequent-id sequent-text)
- "Register existential variables that appear in SEQUENT-TEXT.
-If SEQUENT-TEXT contains existential variables, then SEQUENT-ID
-is stored in `proof-tree-existentials-alist'."
- (if proof-tree-existential-regexp
- (let ((start 0))
- (while (proof-string-match proof-tree-existential-regexp
- sequent-text start)
- (setq start (match-end 0))
- (proof-tree-add-existential-assoc current-state
- (match-string 1 sequent-text)
- sequent-id)))))
+ "Reset internal state when there is no current proof any more."
+ (setq proof-tree-current-proof nil)
+ (run-hooks 'proof-tree-stop-display-hook))
(defun proof-tree-extract-goals (start end)
"Extract the current goal state information from the delayed output.
@@ -932,29 +747,6 @@ current buffer."
nil))
-(defun proof-tree-extract-list (start end start-regexp end-regexp item-regexp)
- "Extract items between START-REGEXP and END-REGEXP.
-In the region given by START and END, determine the subregion
-between START-REGEXP and END-REGEXP and return the list of all
-items in the subregion. An item is a match of subgroub 1 of
-ITEM-REGEXP. The items in the returned list have the same order
-as in the text.
-
-Return nil if START-REGEXP or ITEM-REGEXP is nil. The subregion
-extends up to END if END-REGEXP is nil."
- (let (result)
- (when (and start-regexp item-regexp)
- (goto-char start)
- (when (proof-re-search-forward start-regexp end t)
- (setq start (point))
- (if (and end-regexp (proof-re-search-forward end-regexp end t))
- (setq end (match-beginning 0)))
- (goto-char start)
- (while (proof-re-search-forward item-regexp end t)
- (setq result (cons (match-string-no-properties 1)
- result)))))
- (nreverse result)))
-
(defun proof-tree-extract-existential-info (start end)
"Extract the information display of existential variables.
This function cuts out the text between
@@ -1025,13 +817,7 @@ command was sent to the proof assistant."
current-sequent-id
current-sequent-text
(nth 2 current-goals)
- (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))))))
+ (proof-tree-extract-existential-info start end)))))))
(defun proof-tree-handle-navigation (proof-info)
"Handle a navigation command.
@@ -1068,23 +854,9 @@ The delayed output of the navigation command is in the
region
(setq proof-tree-last-state (car proof-info))))
(defun proof-tree-handle-undo (proof-info)
- "Undo prooftree to current state.
-Send the undo command to prooftree and undo changes to the
-internal state of this package. The latter involves currently two
-points:
-* delete those goals from `proof-tree-sequent-hash' that have
- been generated after the state to which we undo now;
-* change proof-tree-existentials-alist back to its previous content."
+ "Undo prooftree to current state."
;; (message "PTHU info %s" proof-info)
(let ((proof-state (car proof-info)))
- ;; delete sequents from the hash
- (maphash
- (lambda (sequent-id state)
- (if (> state proof-state)
- (remhash sequent-id proof-tree-sequent-hash)))
- proof-tree-sequent-hash)
- ;; undo changes in other state vars
- (proof-tree-undo-existentials proof-state)
(unless (equal (cadr proof-info) proof-tree-current-proof)
;; went back to a point before the start of the proof that we
;; are displaying;
@@ -1099,20 +871,19 @@ points:
(setq proof-tree-last-state (- proof-state 1))))
-(defun proof-tree-update-sequent (proof-state)
+(defun proof-tree-update-sequent (proof-name)
"Prepare an update-sequent command for prooftree.
This function processes delayed output that the proof assistant
-generated in response to commands that Proof General inserted in
-order to keep prooftree up-to-date. Such commands are tagged with
-a 'proof-tree-show-subgoal flag.
+generated in response to commands that prooftree inserted in
+order to keep its display up-to-date. Such commands are tagged
+with a 'proof-tree-show-subgoal flag. Argument PROOF-NAME
+originally comes from prooftree and is passed back now, because
+processing a show goal command might happen after the proof.
This function uses `proof-tree-update-goal-regexp' to find a
-sequent and its ID in the delayed output. If something is found
-an appropriate update-sequent command is sent to prooftree.
-
-The update-sequent command is associated with state PROOF-STATE
-for proper undo effects, see also the comments for
-`proof-tree-show-goal-callback'.
+sequent, its ID and the corresponding state in the delayed
+output. If something is found an appropriate update-sequent
+command is sent to prooftree.
The delayed output is in the region
\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
@@ -1123,21 +894,16 @@ The delayed output is in the region
(if (proof-tree-is-running)
(with-current-buffer proof-shell-buffer
(let* ((start proof-shell-delayed-output-start)
- (end proof-shell-delayed-output-end)
- (proof-info (funcall proof-tree-get-proof-info))
- (proof-name (cadr proof-info)))
+ (end proof-shell-delayed-output-end))
(goto-char start)
(if (proof-re-search-forward proof-tree-update-goal-regexp end t)
(let ((sequent-id (match-string-no-properties 1))
- (sequent-text (match-string-no-properties 2)))
+ (proof-state
+ (string-to-number (match-string-no-properties 2)))
+ (sequent-text (match-string-no-properties 3)))
(proof-tree-send-update-sequent
- proof-state proof-name sequent-id sequent-text)
- ;; put current sequent into hash (if it is not there yet)
- (unless (gethash sequent-id proof-tree-sequent-hash)
- (puthash sequent-id proof-state proof-tree-sequent-hash))
- (proof-tree-register-existentials proof-state
- sequent-id
- sequent-text)))))))
+;; XXX existentials info??
+ proof-state proof-name sequent-id sequent-text)))))))
(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags _span)
@@ -1275,6 +1041,7 @@ display is switched off."
;; inside an unfinished proof -> start for this proof
(proof-tree-display-current-proof proof-start)
;; outside a proof -> wait for the next proof
+ (run-hooks 'proof-tree-start-display-hook)
(setq proof-tree-external-display t)
(proof-tree-send-undo proof-tree-last-state)
(message
- [nongnu] elpa/proof-general 7aaca43e29 05/11: prooftree: wait for show-goal commands at proof end, (continued)
- [nongnu] elpa/proof-general 7aaca43e29 05/11: prooftree: wait for show-goal commands at proof end, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 5fbc5d3030 09/11: prooftree: fix single step undo, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 1f0724813a 11/11: proof-tree: protect against internal errors, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 1dc76dbb65 02/11: prooftree: complete evar info, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 5b10c7e1ea 04/11: prooftree: fix spurious undo recognition for show goal, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 0615eecc88 06/11: PG-adapting: delete some outdated prooftree information, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general b95c2087e9 03/11: prooftree: simplify evar printing management, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general b96927ed0f 10/11: prooftree: fix Unshelve and delete new layer recognition, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general eb468a9f8f 08/11: user doc, CHANGES: update for prooftree, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general cef4d1cf12 07/11: prooftree: polish, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 25c2d37376 01/11: prooftree: Update proof tree display support for Coq 8.10,
ELPA Syncer <=