From 822c986ef286928c1364c255ffcbb48e68080e26 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. --- ci/simple-tests/coq-test-proof-stat.el | 6 ++++-- ci/simple-tests/proof_stat.v | 4 ++++ 2 files changed, 8 insertions(+), 2 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.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.