[nongnu] elpa/proof-general 8215623 4/5: Merge pull request #607 from Matafou/fix-#597-Fail-backtrace

[ELPA Syncer]

branch: elpa/proof-general
commit 82156237e97480101225bb53a45425ea146fb6ba
Merge: f6df849 3b765b4
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #607 from Matafou/fix-#597-Fail-backtrace
    
    Fix #597; ProofGeneral cannot step over `Fail` correctly
---
 ci/coq-tests.el    | 38 ++++++++++++++++++++++++++++++++++++++
 ci/test_stepwise.v | 16 ++++++++++++++++
 coq/coq-syntax.el  |  2 +-
 3 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index fb5635f..160312c 100644
--- a/ci/coq-tests.el
+++ b/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
diff --git a/ci/test_stepwise.v b/ci/test_stepwise.v
index 3812adb..af451ff 100644
--- a/ci/test_stepwise.v
+++ b/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.
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b8b498a..a2266db 100644
--- a/coq/coq-syntax.el
+++ 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