From 7c8418fb0225bfbce4154edebfd621955fdf39c6 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 8 Jul 2024 16:35:46 +0200 Subject: [PATCH] Fix #779 regression-cannot-step-Fail-correctly. As suggested by @hendriktews: added a "no-error" regexp. Also adapted the tests so that they pass with coq pre-8.20 and post-8.20. No need to ass more tests case imho. --- ci/coq-tests.el | 24 ++++++++++++++---------- coq/coq-syntax.el | 22 +++------------------- coq/coq.el | 1 + generic/proof-config.el | 13 +++++++++++++ generic/proof-shell.el | 5 ++++- 5 files changed, 35 insertions(+), 30 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 7f4291b16..9b2a96d66 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -183,6 +183,10 @@ For example, COMMENT could be (*test-definition*)" "Particular case of `coq-should-buffer-regexp'." (coq-should-buffer-regexp (regexp-quote str) buffer-name)) +(defun coq-should-buffer-contain-string (str &optional buffer-name) + "Particular case of `coq-should-buffer-regexp'." + (coq-should-buffer-regexp (concat ".*\\(" (regexp-quote str) "\\).*") buffer-name)) + ;; TODO: Use https://github.com/rejeep/ert-async.el ;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html @@ -327,12 +331,12 @@ For example, COMMENT could be (*test-definition*)" (proof-assert-next-command-interactive) ;; pas the comment (proof-assert-next-command-interactive) (proof-shell-wait) + ;; The order of these messages has changed btween 8.19 and 8.20 + ;; so we check each part separatelty + (coq-should-buffer-contain-string "The command has indeed failed with message:") + (coq-should-buffer-contain-string "Tactic failure: Cannot solve this goal." "*coq*") (if (coq--version< (coq-version) "8.10.0") - (coq-should-buffer-string "The command has indeed failed with message: -In nested Ltac calls to \"now (tactic)\" and \"easy\", last call failed. -Tactic failure: Cannot solve this goal.") - (coq-should-buffer-string "The command has indeed failed with message: -Tactic failure: Cannot solve this goal." "*coq*"))))) + (coq-should-buffer-contain-string "In nested Ltac calls to \"now (tactic)\" and \"easy\", last call failed."))))) ;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*") @@ -348,11 +352,11 @@ Tactic failure: Cannot solve this goal." "*coq*"))))) (proof-assert-next-command-interactive) ;; pas the comment (proof-assert-next-command-interactive) (proof-shell-wait) - ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof." - (coq-should-buffer-string "The command has indeed failed with message: -In nested Ltac calls to \"now (tactic)\" and \"easy\", last call failed. -Tactic failure: Cannot solve this goal.")))) - + ;; The order of these messages has changed btween 8.19 and 8.20 + ;; so we check each part separatelty + (coq-should-buffer-contain-string "The command has indeed failed with message:") + (coq-should-buffer-contain-string "Tactic failure: Cannot solve this goal." "*coq*") + (coq-should-buffer-contain-string "In nested Ltac calls to \"now (tactic)\" and \"easy\", last call failed.")))) (ert-deftest 100_coq-test-proof-using-proof () "Test for insertion of Proof using annotations" diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index fbb5398f9..a3e7f3ab0 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1296,19 +1296,6 @@ Very similar to `coq-omit-proof-admit-command', but without the dot." (defvar coq-symbols-regexp (regexp-opt coq-symbols)) -;; HACKISH: This string matches standard error regexp UNLESS there is -;; the standard header of the "Fail" command (which is "The command -;; blah has indeed failed with message:\n"). The case where the error -;; header has nothing before it is treated using "empty string at -;; start" regexp. BUT coq-error-regexp (and hence -;; proof-shell-error-regexp) must be correct either when searching in -;; a string or when searching in the proof-shell-buffer when point is -;; at the start of the last output. Hence when we use \\` (empty -;; string at start of the string) we should also accept \\= (empty -;; string at point). -(defvar coq--prefix-not-regexp "\\(\\(\\`\\|\\=\\)\n?\\)\\|\\(?:\\(?:[^:]\\|[^e]:\\|[^g]e:\\|[^a]ge:\\|[^s]age:\\|[^s]sage:\\|[^e]ssage:\\|[^m]essage:\\)\n\\)" - "A regexp matching allowed text before coq error.") - (defvar coq--error-header-re-list '("In nested Ltac call" "Discarding pattern" @@ -1321,13 +1308,10 @@ Very similar to `coq-omit-proof-admit-command', but without the dot." "\\ and around all messages except errors. diff --git a/coq/coq.el b/coq/coq.el index 28d1be288..9d23dafca 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1985,6 +1985,7 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-shell-clear-goals-regexp coq-shell-proof-completed-regexp proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp proof-shell-error-regexp coq-error-regexp + proof-shell-no-error-regexp coq-no-error-regexp proof-shell-interrupt-regexp coq-interrupt-regexp proof-shell-assumption-regexp coq-id proof-shell-theorem-dependency-list-regexp coq-shell-theorem-dependency-list-regexp diff --git a/generic/proof-config.el b/generic/proof-config.el index aa79b85c4..07e338599 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1190,6 +1190,19 @@ error message is displayed. The engine matches interrupts before errors, see `proof-shell-interrupt-regexp'. +It is safe to leave this variable unset (as nil)." + :type '(choice (const nil) regexp) + :group 'proof-shell) + +(defcustom proof-shell-no-error-regexp nil + "Regexp matching a non-error from the proof assistant. + +Some commands of the proof assistant may display error message as +information messages. E.g. in Coq: \"Fail \" shows the error +message thrown by without failing itself. + +Matching this regexp disables error message detection. + It is safe to leave this variable unset (as nil)." :type '(choice (const nil) regexp) :group 'proof-shell) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index e2bf02301..14e1ede31 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -854,7 +854,10 @@ after a completed proof." (setq proof-shell-last-output-kind 'interrupt) (proof-shell-handle-error-or-interrupt 'interrupt flags)) - ((proof-re-search-forward-safe proof-shell-error-regexp end t) + ((and (save-excursion + (proof-re-search-forward-safe proof-shell-error-regexp end t)) + (not (proof-re-search-forward-safe proof-shell-no-error-regexp end t))) + (setq proof-shell-last-output-kind 'error) (proof-shell-handle-error-or-interrupt 'error flags))