proof-stat: add test for proof-check-annotate

hendriktews · May 2, 2024 · e58c693 · e58c693
1 parent cc8db24
commit e58c693
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile
@@ -34,8 +34,11 @@ coq-proof-stat-batch-test:
 	      --eval '(proof-check-report nil "proof_stat.human.gen-out")'
 	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
 	      --eval '(proof-check-report t "proof_stat.tap.gen-out")'
+	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
+	      --eval '(proof-check-annotate nil t)'
 	cmp proof_stat.human.gen-out proof_stat.human.exp-out && \
 	        cmp proof_stat.tap.gen-out proof_stat.tap.exp-out && \
+		git diff --exit-code -- proof_stat.v && \
 		touch coq-proof-stat-batch-test
 
 .PHONY: clean

diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
@@ -1,7 +1,7 @@
 
 Definition a : nat := 4.
 
-Lemma a1_equal_4 : a = 2 * 2.
+Lemma a1_equal_4 : a = 2 * 2.                               (* FAIL *)
 Proof using.
   simpl.
   zzzz.                         (* this proof should fail *)
@@ -18,7 +18,7 @@ Proof using.
   trivial.
 Qed.
 
-Lemma b2_equal_6 : b = 2 * 3.
+Lemma b2_equal_6 : b = 2 * 3.                               (* FAIL *)
 Proof using.                    (* this proof should fail *)
 Qed.