branch: elpa/proof-general
commit 3b765b48ce7920cbd5a9a8771ee2d4905a901c47
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Adding tests for #597.
---
ci/coq-tests.el | 38 ++++++++++++++++++++++++++++++++++++++
ci/test_stepwise.v | 16 ++++++++++++++++
2 files changed, 54 insertions(+)
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.
