branch: elpa/proof-general
commit 82156237e97480101225bb53a45425ea146fb6ba
Merge: f6df849 3b765b4
Author: Pierre Courtieu <mata...@users.noreply.github.com>
Commit: GitHub <nore...@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
