branch: elpa/proof-general
commit bb147dc0732157f0b93b8be75a04ef3981db302e
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
CI: add proof-check tests
---
ci/simple-tests/README.md | 4 +-
ci/simple-tests/coq-test-proof-stat.el | 89 ++++++++++++++++++++++++++++++++++
2 files changed, 92 insertions(+), 1 deletion(-)
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index 523975c6ef..140e729875 100644
--- a/ci/simple-tests/README.md
+++ b/ci/simple-tests/README.md
@@ -15,9 +15,11 @@ coq-test-prelude-correct
coq-test-goals-present
: test that Proof General shows goals correctly in various
situations
-coq-test-three-window.el
+coq-test-three-window
: Test three-pane mode for different frame sizes, including ones that
are too small for three windows.
+coq-test-proof-stat
+: test proof-check-proofs
# Overview of existing tests for qRHL
diff --git a/ci/simple-tests/coq-test-proof-stat.el
b/ci/simple-tests/coq-test-proof-stat.el
new file mode 100644
index 0000000000..d725d01e53
--- /dev/null
+++ b/ci/simple-tests/coq-test-proof-stat.el
@@ -0,0 +1,89 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2024 Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hend...@askra.de>
+;;
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+;;
+;; Test proof-check-proofs.
+
+;; For seq-group-by inside `proof-check-report'. This is
+;; apparently not automatically loaded in Emacs 26.3. Though in a real
+;; PG session it is apparently present.
+(require 'seq)
+
+(defun reset-coq ()
+ "Reset Coq and Proof General.
+Do `proof-shell-exit' to kill Coq and reset the locked region and
+a lot of other internal state of Proof General. Used at the
+beginning of the test when several tests work on the same Coq
+source file."
+ (when (and (boundp 'proof-shell-buffer)
+ (buffer-live-p proof-shell-buffer))
+ (proof-shell-exit t)
+ (message "Coq and Proof General reseted")))
+
+
+(ert-deftest proof-check-correct-stat ()
+ "Test `proof-check-proofs' 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)
+ (reset-coq)
+ (find-file "proof_stat.v")
+
+ ;; run check on file where all errors are in opaque parts
+ (proof-check-proofs)
+
+ ;; the result buffer should exist
+ (should (buffer-live-p (get-buffer "*proof-check-report*")))
+ (with-current-buffer "*proof-check-report*"
+ ;; the summary should be correct
+ (goto-char (point-min))
+ (should
+ (search-forward "3 opaque proofs recognized: 1 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"))))
+
+
+(ert-deftest proof-check-error-on-error ()
+ "Test `proof-check-proofs' with errors in non-opaque parts.
+Check that `proof-check-proofs' signals an error with the expected message."
+ (setq proof-three-window-enable nil)
+ (reset-coq)
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "proof_stat.v")
+ (setq buffer (current-buffer))
+
+ ;; insert an error in non-opaque part
+ (goto-char (point-min))
+ (should (search-forward "automatic test marker 1" nil t))
+ (end-of-line)
+ (insert " X ")
+
+ ;; proof-check-proofs should abort now with an error
+ (condition-case err-desc
+ (progn
+ (proof-check-proofs)
+ ;; Still here? Make test fail!
+ (should nil))
+ (error
+ (should
+ (equal (error-message-string err-desc)
+ "Error encountered outside opaque proofs after line
10")))))
+
+ ;; clean-up modified file in any case
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
