Merge pull request ProofGeneral#607 from Matafou/fix-#597-Fail-backtrace

Fix ProofGeneral#597; ProofGeneral cannot step over `Fail` correctly

ci/coq-tests.el

@@ -303,6 +303,44 @@ For example, COMMENT could be (*test-definition*)"
    'show-proof-stepwise 'diffs-on))
 
 
+(ert-deftest 090_coq-test-regression-Fail()
+  "Test for Fail"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before "(*FailNoTrace*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (proof-assert-next-command-interactive) ;; pas the comment
+     (proof-assert-next-command-interactive)
+     (proof-shell-wait)
+     (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-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*")
+
+(ert-deftest 091_coq-test-regression-Fail()
+  "Test for Fail"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before "(*FailTrace*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (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."))))
+
+
 (provide 'coq-tests)
 
 ;;; coq-tests.el ends here

ci/test_stepwise.v

@@ -11,6 +11,22 @@ Proof using .
   exact proof_of_A.
 Qed. (*test-lemma*)
 
+Section failSection.
+  Local Unset Ltac Backtrace.
+  Goal False.
+  Proof. (*FailNoTrace*)
+    Fail (now auto).
+    auto.
+  Abort.
+
+  Local Set Ltac Backtrace.
+  Goal False. (*FailTrace*) 
+    Fail (now auto).
+    auto.
+  Abort.
+End failSection.
+
+
 Lemma false_proof : forall A B : bool, A = B. 
 Proof.
   intros A B.

coq/coq-syntax.el

@@ -1282,7 +1282,7 @@ different."
 (defvar coq-symbols-regexp (regexp-opt coq-symbols))
 
 ;; ----- regular expressions
-(defvar coq-error-regexp "^\\(In nested Ltac call\\|Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
+(defvar coq-error-regexp "\\(?:[^:]\\|[^e]:\\|[^g]e:\\|[^a]ge:\\|[^s]age:\\|[^s]sage:\\|[^e]ssage:\\|[^m]essage:\\)\n\\(In nested Ltac call\\|Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
   "A regexp indicating that the Coq process has identified an error.")
 
 ;; april2017: coq-8.7 removes special chars definitely and puts