From e2c661db941cd47ecc5e74e3e31b0878f59a09a6 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 17 Apr 2024 16:44:00 +0200 Subject: [PATCH] coq: run silently and explicitly Show when necessary This is a step towards fixing #568. It fixes the cases after Proof, comments, auto, errors, Search and Check, leaving now 2 instead of 8 failing tests in ci/simple-tests/test-goals-present.el. Admitted is not handled correctly any more, which is a regression. Using proof-shell-handle-delayed-output-hook and proof-shell-handle-error-or-interrupt-hook we issue a Show command as a priority action item when the last (normal) action item has been processed. The new action item flag 'keep-response tells the generic machinery to not clear the response buffer and to keep it present in two-pane mode in case an error was detected or the last command was a Search or Check that produced a response. The new action item flag 'coq-show-when-silent is used to distinguish the additional Show commands and to avoid an endless loop of Show commands. Set proof-shell-last-output-kind now in proof-shell-handle-delayed-output such that it correctly reflects the cases of goals and response (which has not been the case since commit 037dc9be9ba1f62fb831fd478e5ab3b63df7eaaf from 2009. This commit breaks coq-show-proof-stepwise to some extend. Expect 080_coq-test-regression-show-proof-stepwise to fail. Additionally: - update manuals - expect errors in tests 020_coq-test-definition, 090_coq-test-regression-Fail and 091_coq-test-regression-Fail because messages are not printed in silent mode --- ci/coq-tests.el | 16 +++ ci/simple-tests/coq-test-goals-present.el | 8 +- coq/coq.el | 128 ++++++++++++++++++---- doc/PG-adapting.texi | 5 + generic/pg-goals.el | 17 ++- generic/proof-shell.el | 28 +++-- 6 files changed, 161 insertions(+), 41 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 7f4291b16..e28350a2d 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -196,6 +196,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 020_coq-test-definition () + ;; There are no infomsgr when running silent. + :expected-result :failed "Test *response* output after asserting a Definition." (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") @@ -291,6 +293,9 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 080_coq-test-regression-show-proof-stepwise() "Regression test for the \"Show Proof\" option" + ;; When running silent, the Show Proof command is issued, but its + ;; output is not (yet) kept in the response buffer. + :expected-result :failed (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") (lambda () @@ -317,6 +322,10 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 090_coq-test-regression-Fail() + ;; When running silent, the message about indeed failing is not + ;; shown. One might fix this test by checking that there is no + ;; error, which would be shown without Fail. + :expected-result :failed "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") @@ -338,6 +347,13 @@ Tactic failure: Cannot solve this goal." "*coq*"))))) ;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*") (ert-deftest 091_coq-test-regression-Fail() + ;; XXX What is the difference between this test and + ;; 090_coq-test-regression-Fail? + + ;; When running silent, the message about indeed failing is not + ;; shown. One might fix this test by checking that there is no + ;; error, which would be shown without Fail. + :expected-result :failed "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index 6ba07db71..33866747c 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -260,17 +260,14 @@ which action the goals buffer should have been reset." (ert-deftest goals-after-proof () "Test goals are present after ``Proof''." - :expected-result (if coq--post-v87 :failed :passed) (goals-after-test coq-src-proof "Proof" nil)) (ert-deftest goals-after-comment () "Test goals are present after a comment." - :expected-result :failed (goals-after-test coq-src-comment "comment" nil)) (ert-deftest goals-after-auto () "Test goals are present after ``auto''." - :expected-result (if coq--post-v87 :failed :passed) (goals-after-test coq-src-auto "auto" nil)) (ert-deftest goals-after-simpl () @@ -279,11 +276,11 @@ which action the goals buffer should have been reset." (ert-deftest goals-after-error () "Test goals are present after an error." - :expected-result :failed (goals-after-test coq-src-error "error" t)) (ert-deftest goals-reset-after-admitted () "The goals buffer is reset after an Admitted." + :expected-result :failed (goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted")) (ert-deftest goals-reset-no-more-goals () @@ -359,7 +356,6 @@ two-pane mode." (ert-deftest goals-up-to-date-at-error () "Check that goals are updated before showing the error." - :expected-result :failed (update-goals-when-response coq-src-update-goal-after-error "Lemma foo" "H : eq_one 1 -> False" @@ -382,7 +378,6 @@ This test checks several commands inside a proof with a final Search command. After processing these commands, the goals buffer should have been updated and the response buffer should contain something and be visible in two-pane mode." - :expected-result :failed (update-goals-when-response coq-src-update-goal-after-search "Lemma g" "2 = 2" @@ -405,7 +400,6 @@ This test checks several commands inside a proof with a final Check command. After processing these commands, the goals buffer should have been updated and the response buffer should contain something and be visible in two-pane mode." - :expected-result :failed (update-goals-when-response coq-src-update-goal-after-check "Lemma h" "3 = 3" diff --git a/coq/coq.el b/coq/coq.el index a036acde3..74019e808 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -122,8 +122,21 @@ Namely, goals that do not fit in the goals window." ;; should re-intialize to coq-search-blacklist-string instead of ;; keeping the current value (that may come from another file). ,(format "Add Search Blacklist %s. " coq-search-blacklist-current-string)) - '("Set Suggest Proof Using. ") coq-user-init-cmd) - "Command to initialize the Coq Proof Assistant.") + '("Set Suggest Proof Using. " + "Set Silent. ") + coq-user-init-cmd) + "Commands for initial Coq configuration, Coq variant of `proof-shell-init-cmd'. +List of commands sent to the Coq background process just after it +has been started. This happens inside `proof-shell-config-done', +when the major mode `coq-shell-mode' is configured in the `*coq*' +buffer. + +Sets silent mode. + +In normal interaction, Coq is started because the user asserts +some commands. Therefore the commands here are followed by those +inserted inside `proof-assert-command-hook', respectively, +`coq-adapt-printing-width'.") ;; FIXME: Even if we don't use coq-indent for indentation, we still need it for ;; coq-script-parse-cmdend-forward/backward and coq-find-real-start. @@ -1207,12 +1220,15 @@ Printing All set." ;; command and *not* have the goal redisplayed, the command must be tagged with ;; 'empty-action-list. (defun coq-empty-action-list-command (cmd) - "Return the list of commands to send to Coq after CMD -if it is the last command of the action list. -If CMD is tagged with 'empty-action-list then this function won't -be called and no command will be sent to Coq. + "Return the list of commands to send to Coq if CMD is last in the action list. +Return the list of commands to be sent to Coq when +`proof-action-list' is empty, CMD was the last command just sent +to Coq and CMD was not tagged with `'empty-action-list'. Note: the last command added if `coq-show-proof-stepwise' is set -should match the `coq-show-proof-diffs-regexp'." +should match the `coq-show-proof-diffs-regexp'. + +This function is called from `proof-shell-exec-loop' via +`proof-shell-empty-action-list-command'." (cond ((or ;; If closing a nested proof, Show the enclosing goal. @@ -1225,28 +1241,29 @@ should match the `coq-show-proof-diffs-regexp'." . ,(coq--show-proof-stepwise-cmds))) ((or - ;; If we go back in the buffer and the number of abort is less than - ;; the number of nested goals, then Unset Silent and Show the goal + ;; If we go back in the buffer and the number of abort is less than the + ;; number of nested goals, that is, if we are inside a proof, then Show + ;; the goal. (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) - `("Unset Silent." - ,(if (coq--post-v810) (coq-diffs) "Show.") - . ,(coq--show-proof-stepwise-cmds))) + (append + (if (coq--post-v810) (list (coq-diffs)) ()) + ;; '("Show.") + (coq--show-proof-stepwise-cmds))) ((or - ;; If we go back in the buffer and not in the above case, then only Unset - ;; silent (there is no goal to show). Still, we need to "Set Diffs" again + ;; If we go back in the buffer and not in the above case, i.e., outside a + ;; proof, then only set the Diffs option. (string-match-p "BackTo\\s-" cmd)) - (if (coq--post-v810) - (list "Unset Silent." (coq-diffs) ) - (list "Unset Silent."))) + (if (coq--post-v810) (list (coq-diffs)) ())) + ((or ;; If starting a proof, Show Proof if need be (coq-goal-command-str-p cmd) ;; If doing (not closing) a proof, Show Proof if need be (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0))) - (coq--show-proof-stepwise-cmds)))) + (coq--show-proof-stepwise-cmds)))) ;; This does not Set Printing Width, it rather tells pg to do that before each ;; command (if necessary) @@ -1326,7 +1343,9 @@ redisplayed." (let ((wdth (or width (coq-guess-goal-buffer-at-next-command)))) ;; if no available width, or unchanged, do nothing (when (and wdth (not (equal wdth coq-shell-current-line-width))) - (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t) + (proof-shell-invisible-command + (format "Set Printing Width %S." (- wdth 1)) + t) (setq coq-shell-current-line-width wdth) ;; Show iff show non nil and some proof is under way (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe))))) @@ -1846,7 +1865,7 @@ at `proof-assistant-settings-cmds' evaluation time.") (let ((pt2 (point))) (re-search-backward "Goal:\\|^TcDebug\\|^" nil t) (when (looking-at "Goal") - (pg-goals-display (buffer-substring (point) pt2) nil)))))))) + (pg-goals-display (buffer-substring (point) pt2) nil nil)))))))) ;; overwrite the generic one, interactive prompt is Debug mode;; try to display ;; the debug goal in the goals buffer. @@ -1943,8 +1962,11 @@ at `proof-assistant-settings-cmds' evaluation time.") ;; span menu (setq proof-script-span-context-menu-extensions #'coq-create-span-menu) - (setq proof-shell-start-silent-cmd "Set Silent. " - proof-shell-stop-silent-cmd "Unset Silent. ") + ;; When proof-shell-start-silent-cmd and proof-shell-stop-silent-cmd stay at + ;; their default value nil, the generic code won't switch Coq to silent and + ;; noisy at, respectively, the beginning and end of longer asserted regions. + ;; (setq proof-shell-start-silent-cmd "Set Silent. " + ;; proof-shell-stop-silent-cmd "Unset Silent. ") ;; prooftree config (setq @@ -1969,6 +1991,21 @@ at `proof-assistant-settings-cmds' evaluation time.") ) (defun coq-shell-mode-config () + "Initialization of `coq-shell-mode' that runs in the `*coq*' buffer. +The interaction buffer with Coq, `*coq*', uses a major mode that +is derived via `proof-shell-mode' from `scomint-mode'. This +function runs as the body of `coq-shell-mode' when the `*coq*' +buffer is initialized, which happens when the Coq background +process is started. This function intitalizes the Coq +personalization of Proof General in the interaction buffer with +Coq. At the end, this function calls `proof-shell-config-done', +which initializes the Coq session, e.g., by sending +`proof-shell-init-cmd', respectively, `coq-shell-init-cmd' to Coq. + +In normal interaction, the proof assistant is started because the +user assert some commands. Therefore this function runs only +shortly before `proof-assert-command-hook', respectively, +`coq-adapt-printing-width'." (setq proof-shell-cd-cmd coq-shell-cd proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) @@ -3017,6 +3054,53 @@ buffer." (add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t) +(defun coq-show-goals-inside-proof (keep-response) + "Update goals buffer when action item list has been processed. +Add a Show command as priority action, such that it will still be +processed if the generic machinery inside `proof-shell-filter' +believes it has processed the last item from the action list. +When Coq runs in silent mode, we need to update the goals +precisely when everything else from the action list has been +processed. + +The Show command is only added inside proofs and only if the last +processed command was not a show command from this function. The +action item flag `'coq-show-when-silent' is used for the latter. + +KEEP-RESPONSE should be set if the last command produced some +error or response that should be kept and shown to the user. If +set, the flag `'keep-response' is added to the action item." + (when (and coq-last-but-one-proofstack + (not (member 'coq-show-when-silent + proof-shell-delayed-output-flags))) + (let* ((flags-1 (list 'coq-show-when-silent 'invisible 'empty-action-list)) + (flags (if keep-response (cons 'keep-response flags-1) flags-1))) + (proof-add-to-priority-queue + (proof-shell-action-list-item "Show. " 'proof-done-invisible flags))))) + +(defun coq-show-goals-on-error () + "Update goals after error. +This function is intended for +`proof-shell-handle-error-or-interrupt-hook' to update the goals +buffer after an error has been detected. See also +`coq-show-goals-inside-proof'." + (coq-show-goals-inside-proof t)) + +(defun coq-show-goals-standard-case () + "Update goals after last command when no error was detected. +This function is intended for +`proof-shell-handle-delayed-output-hook' to update the goals +buffer after the last command has been processed and no error has +been detected. Take care to keep the response buffer visible if +the last command was a Search, a Check or something similar. See +also `coq-show-goals-inside-proof'." + (coq-show-goals-inside-proof (eq proof-shell-last-output-kind 'response))) + +(add-hook 'proof-shell-handle-error-or-interrupt-hook + #'coq-show-goals-on-error) +(add-hook 'proof-shell-handle-delayed-output-hook + #'coq-show-goals-standard-case) + ;; ;; Scroll response buffer to maximize display of first goal ;; diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 3e5e72e39..c83d2b228 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3888,8 +3888,13 @@ bother the user. They may include @code{'no-response-display} do not display messages in @strong{response} buffer @code{'no-error-display} do not display errors/take error action @code{'no-goals-display} do not goals in @strong{goals} buffer + @code{'keep-response} do not erase the response buffer when goals are shown @code{'proof-tree-show-subgoal} item inserted by the proof-tree package @code{'priority-action} item added via @code{proof-add-to-priority-queue} + @code{'empty-action-list} @code{proof-shell-empty-action-list-command} should not be + called if this is the last item in the action list + @code{'coq-show-when-silent} Coq specific flag used for the final Show when + running completely silent. @end lisp Note that @code{'invisible} does not imply any of the others. If flags are non-empty, interactive cues will be surpressed. (E.g., diff --git a/generic/pg-goals.el b/generic/pg-goals.el index f7cb9b3c7..0bba1553c 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -79,7 +79,7 @@ May enable proof-by-pointing or similar features. ;; ;; Goals buffer processing ;; -(defun pg-goals-display (string keepresponse) +(defun pg-goals-display (string keepresponse nodisplay) "Display STRING in the `proof-goals-buffer', properly marked up. Converts term substructure markup into mouse-highlighted extents. @@ -90,7 +90,13 @@ function tries to do that by calling `pg-response-maybe-erase'. If KEEPRESPONSE is non-nil, we assume that a response message corresponding to this goals message has already been displayed before this goals message (see `proof-shell-handle-delayed-output'), -so the response buffer should not be cleared." +so the response buffer should not be cleared. + +IF NODISPLAY is non-nil, do not display the goals buffer in some +window (but the goals buffer is updated as described above and +any window currently showing it will keep it). In two-pane mode, +NODISPLAY has the effect that the goals are updated but the +response buffer is displayed." ;; Response buffer may be out of date. It may contain (error) ;; messages relating to earlier proof states @@ -114,8 +120,11 @@ so the response buffer should not be cleared." (set-buffer-modified-p nil) ;; Keep point at the start of the buffer. - (proof-display-and-keep-buffer - proof-goals-buffer (point-min)))) + ;; (For Coq, somebody sets point to the conclusion in the goal, so the + ;; position argument in proof-display-and-keep-buffer has no effect.) + (unless nodisplay + (proof-display-and-keep-buffer + proof-goals-buffer (point-min))))) ;; ;; Actions in the goals buffer diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 4de85ddf9..34b2640e4 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -38,6 +38,8 @@ ;; -> proof-shell-process-urgent-message ;; -> proof-shell-filter-manage-output ;; -> proof-shell-handle-immediate-output +;; -> proof-shell-handle-error-or-interrupt +;; -> proof-shell-error-or-interrupt-action ;; -> proof-shell-exec-loop ;; -> proof-tree-check-proof-finish ;; -> proof-shell-handle-error-or-interrupt @@ -113,8 +115,13 @@ bother the user. They may include 'no-response-display do not display messages in *response* buffer 'no-error-display do not display errors/take error action 'no-goals-display do not goals in *goals* buffer + 'keep-response do not erase the response buffer when goals are shown 'proof-tree-show-subgoal item inserted by the proof-tree package 'priority-action item added via proof-add-to-priority-queue + 'empty-action-list proof-shell-empty-action-list-command should not be + called if this is the last item in the action list + 'coq-show-when-silent Coq specific flag used for the final Show when + running completely silent. Note that 'invisible does not imply any of the others. If flags are non-empty, interactive cues will be surpressed. (E.g., @@ -1070,7 +1077,9 @@ being processed." (unless (eq proof-shell-busy queuemode) (proof-debug "proof-append-alist: wrong queuemode detected for busy shell") - (cl-assert (eq proof-shell-busy queuemode))))) + (cl-assert + (eq proof-shell-busy queuemode) nil + "wrong queuemode in proof-add-to-queue: %s instead expected %s")))) (let ((nothingthere (null proof-action-list))) @@ -1716,10 +1725,9 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) - (if (proof-shell-exec-loop) - (setq proof-shell-last-output-kind - ;; only display result for last output - (proof-shell-handle-delayed-output))) + (when (proof-shell-exec-loop) + ;; only display result for last output + (proof-shell-handle-delayed-output)) ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) @@ -1814,14 +1822,18 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output both)) + (pg-goals-display proof-shell-last-goals-output + (or both (member 'keep-response flags)) + (member 'keep-response flags))) ;; indicate a goals output has been given - 'goals)) + (setq proof-shell-last-output-kind 'goals))) (t (proof-shell-display-output-as-response flags proof-shell-last-output) ;; indicate that (only) a response output has been given - 'response)) + (if (equal proof-shell-last-output "") + (setq proof-shell-last-output-kind nil) + (setq proof-shell-last-output-kind 'response)))) ;; FIXME (CPC 2015-12-31): The documentation of this hook suggests that it ;; only gets run after new output has been displayed, but this isn't true at