branch: elpa/proof-general
commit 71c807ced24371451341a3a9edeaec94f4e1b88e
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
proof-stat: admitted proofs should count as failing
Proofs terminated with Admitted should count as failing in the
statistics, even when Coq accepts the proofs without error.
The ERT test is marked expected fail, however, this is not possible
for the tests of goal coq-proof-stat-batch-test, therefore the
expected output is wrong, such that these tests succeed.
---
ci/simple-tests/coq-test-proof-stat.el | 6 ++++--
ci/simple-tests/proof_stat.human.exp-out | 3 ++-
ci/simple-tests/proof_stat.tap.exp-out | 3 ++-
ci/simple-tests/proof_stat.v | 4 ++++
4 files changed, 12 insertions(+), 4 deletions(-)
diff --git a/ci/simple-tests/coq-test-proof-stat.el
b/ci/simple-tests/coq-test-proof-stat.el
index 86470f9548..8ec4e25fb9 100644
--- a/ci/simple-tests/coq-test-proof-stat.el
+++ b/ci/simple-tests/coq-test-proof-stat.el
@@ -24,6 +24,7 @@ source file."
(ert-deftest proof-check-correct-stat ()
+ :expected-result :failed
"Test `proof-check-report' on a file that is correct in non-opaque parts.
Test that the report buffer contains the expected output."
(setq proof-three-window-enable nil)
@@ -39,14 +40,15 @@ Test that the report buffer contains the expected output."
;; the summary should be correct
(goto-char (point-min))
(should
- (search-forward "3 opaque proofs recognized: 1 successful 2 FAILING"
+ (search-forward "4 opaque proofs recognized: 2 successful 2 FAILING"
nil t))
;; results for all 3 test lemmas should be correct
(mapc
(lambda (s) (should (search-forward s nil t)))
'("FAIL a1_equal_4"
"OK b_equal_6"
- "FAIL b2_equal_6"))))
+ "FAIL b2_equal_6"
+ "FAIL use_admit"))))
(ert-deftest proof-check-error-on-error ()
diff --git a/ci/simple-tests/proof_stat.human.exp-out
b/ci/simple-tests/proof_stat.human.exp-out
index 82346b541f..901c8b3820 100644
--- a/ci/simple-tests/proof_stat.human.exp-out
+++ b/ci/simple-tests/proof_stat.human.exp-out
@@ -1,9 +1,10 @@
Proof check results for proof_stat.v
-3 opaque proofs recognized: 1 successful 2 FAILING
+4 opaque proofs recognized: 2 successful 2 FAILING
FAIL a1_equal_4
OK b_equal_6
FAIL b2_equal_6
+ OK use_admit
diff --git a/ci/simple-tests/proof_stat.tap.exp-out
b/ci/simple-tests/proof_stat.tap.exp-out
index 7903afc6aa..1735d29f79 100644
--- a/ci/simple-tests/proof_stat.tap.exp-out
+++ b/ci/simple-tests/proof_stat.tap.exp-out
@@ -1,7 +1,8 @@
TAP version 13
-1..3
+1..4
not ok 1 a1_equal_4
ok 2 b_equal_6
not ok 3 b2_equal_6
+ok 4 use_admit
diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
index c436431b02..415b18bc2d 100644
--- a/ci/simple-tests/proof_stat.v
+++ b/ci/simple-tests/proof_stat.v
@@ -22,3 +22,7 @@ Lemma b2_equal_6 : b = 2 * 3.
(* FAIL *)
Proof using. (* this proof should fail *)
Qed.
+Lemma use_admit : 0 = 1.
+Proof using. (* this proof succeeds but should count as failing
*)
+ admit.
+Admitted.
