Merge pull request ProofGeneral#780 from Matafou/fix-779-regression-c…

…annot-step-Fail-correctly

Fixes ProofGeneral#779 regression cannot step Fail correctly.

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"

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.

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

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)

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))