[nongnu] elpa/proof-general eca47ea8af 2/2: Merge pull request #780 from Matafou/fix-779-regression-cannot-step-Fail-correctly

[ELPA Syncer]

branch: elpa/proof-general
commit eca47ea8afdfcd94b4c8d88ee640f6631cfe5c5d
Merge: 837f587bd5 7c8418fb02
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #780 from 
Matafou/fix-779-regression-cannot-step-Fail-correctly
    
    Fixes #779 regression cannot step Fail correctly.
---
 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 7f4291b167..9b2a96d661 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 fbb5398f90..a3e7f3ab0e 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."
     "\\<Error:")
   "A list of regexps matching coq error headers.")
 
-(defvar coq--raw-error-regexp (coq--regexp-alt-list coq--error-header-re-list))
+(defvar coq-error-regexp (coq--regexp-alt-list coq--error-header-re-list))
 
-;; ----- regular expressions
-;; ignore "Error:" if preceded by \n[ ^]+\n
-(defvar coq-error-regexp
-  (concat "\\(?:" coq--prefix-not-regexp "\\)" coq--raw-error-regexp)
-  "A regexp indicating that the Coq process has identified an error.")
+(defvar coq-no-error-regexp "The command has indeed failed"
+  "see `proof-shell-no-error-regexp'.]")
 
 ;; april2017: coq-8.7 removes special chars definitely and puts
 ;; <infomsg> and <warning> around all messages except errors.
diff --git a/coq/coq.el b/coq/coq.el
index 28d1be2887..9d23dafca0 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 aa79b85c44..07e338599a 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 <cmd>\" shows the error
+message thrown by <cmd> 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 e2bf02301d..14e1ede318 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))