From 9e9f499e62d8fcef3b5cf7421edb6b1e70e81f8c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 12 Jun 2024 10:46:16 +0200 Subject: [PATCH] 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 86470f954..8ec4e25fb 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 82346b541..901c8b382 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 7903afc6a..1735d29f7 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 c436431b0..415b18bc2 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.