branch: elpa/proof-general
commit 51696277a4dc30acd61e9ebb400d99934955e450
Author: Hendrik Tews <hend...@askra.de>
Commit: Pierre Courtieu <mata...@users.noreply.github.com>
Test that the Proof General prelude is correct
Add a test that checks that the commands that Proof General sends
to Coq before the first script command do not raise an error. See
also #567.
---
ci/simple-tests/README.md | 11 ++++
ci/simple-tests/test-prelude-correct.el | 92 +++++++++++++++++++++++++++++++++
2 files changed, 103 insertions(+)
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index 1a6e8c9..34812cf 100644
--- a/ci/simple-tests/README.md
+++ b/ci/simple-tests/README.md
@@ -10,3 +10,14 @@ test-omit-proofs
coq-par-job-needs-compilation-quick
: test coq-par-job-needs-compilation-quick by enumerating all
possible cases
+test-prelude-correct
+: test that the Proof General prelude is correct
+
+
+# Important conventions
+
+The Makefile runs all ERT tests in all `test-*.el` files.
+Therefore, the test should be written in a file matching this
+pattern.
+
+To run all tests in a single file, do `make test-*.success`.
diff --git a/ci/simple-tests/test-prelude-correct.el
b/ci/simple-tests/test-prelude-correct.el
new file mode 100644
index 0000000..84c0625
--- /dev/null
+++ b/ci/simple-tests/test-prelude-correct.el
@@ -0,0 +1,92 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2021 Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hend...@askra.de>
+;;
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Test that the Proof General prelude is correct.
+;;
+;; I use Proof General prelude here to refer to the initialization
+;; commands that Proof General sends to Coq before the first command
+;; of the script.
+
+;; This test shows different behaviour before 8.10. When the problem
+;; is fixed, I expect that the version distinction is no longer
+;; necessary and can be deleted.
+;;
+;; Load stuff for `coq--version<'
+(require 'proof-site)
+(proof-ready-for-assistant 'coq)
+(require 'coq-system)
+
+(defconst coq--post-v810 (coq--post-v810)
+ "t if Coq is more recent than 8.9")
+
+(message "goal present tests run with Coq version %s; post-v810: %s"
+ (coq-version t) coq--post-v810)
+
+
+;;; Coq source code for tests
+
+(defconst coq-src-proof
+ "Check 1."
+ "Coq source code for checking the prelude.")
+
+
+;;; utility functions
+
+(defun record-buffer-content (buf)
+ "Record buffer content of BUF via `message' for debugging.
+BUF should be a string."
+ (with-current-buffer buf
+ (let ((content (buffer-substring-no-properties (point-min) (point-max))))
+ (message "%s buffer contains %d chars: %s" buf (length content)
content))))
+
+(defun wait-for-coq ()
+ "Wait until processing is complete."
+ (while (or proof-second-action-list-active
+ (consp proof-action-list))
+ ;; (message "wait for coq/compilation with %d items queued\n"
+ ;; (length proof-action-list))
+ ;;
+ ;; accept-process-output without timeout returns rather quickly,
+ ;; apparently most times without process output or any other event
+ ;; to process.
+ (accept-process-output nil 0.1)))
+
+
+;;; define the test
+
+(ert-deftest prelude-correct ()
+ :expected-result (if coq--post-v810 :passed :failed)
+ "Test that the Proof Genneral prelude is correct.
+Check that all the commands that Proof General sends as
+initialization before the first script command to Coq do not
+yield an error."
+ (message "prelude-correct test: Check the Proof General prelude")
+ (setq proof-three-window-enable nil)
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "goals.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-proof)
+ (proof-goto-point)
+ (wait-for-coq)
+ (record-buffer-content "*coq*")
+
+ ;; check that there is no error in *coq*
+ (with-current-buffer "*coq*"
+ (goto-char (point-min))
+ (should (not (re-search-forward "Error:" nil t)))))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
