branch: elpa/proof-general
commit d4d2465d0184d9c7aab51eeeac407c22b13ae7e7
Merge: 964a5958e7 a1b2941ff4
Author: hendriktews <hend...@askra.de>
Commit: GitHub <nore...@github.com>
Merge pull request #833 from hendriktews/test-sec-error
CI: add new tests for error messages at Qed
---
ci/simple-tests/README.md | 5 +-
ci/simple-tests/coq-test-goals-present.el | 81 ++++++++++++++++++++++++++++++-
2 files changed, 83 insertions(+), 3 deletions(-)
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index 721fa99459..e961328737 100644
--- a/ci/simple-tests/README.md
+++ b/ci/simple-tests/README.md
@@ -13,8 +13,9 @@ coq-test-par-job-needs-compilation-quick
coq-test-prelude-correct
: test that the Proof General prelude is correct
coq-test-goals-present
-: test that Proof General shows goals correctly in various
- situations
+: Test that Proof General shows goals correctly in various situations.
+ Test also that in other situations the response buffer contains the
+ right output and is visible in two-pane mode.
coq-test-three-window
: Test three-pane mode for different frame sizes, including ones that
are too small for three windows.
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index a00e0a0cdb..e26d16f5de 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -9,7 +9,9 @@
;;; Commentary:
;;
-;; Test that Proof General shows goals correctly in various situations.
+;; Test that Proof General shows goals correctly in various
+;; situations. Test also that in other situations the response buffer
+;; contains the right output and is visible in two-pane mode.
;; gloabal configuration for this file
;; all tests in this file shall run in two-pane mode
@@ -161,6 +163,19 @@ Qed.
"Coq source code for response buffer visibility tests.
Used in `check-response-present' for all `response-buffer-visible-*' tests.")
+(defconst coq-src-not-declared-section-variable
+ "Section A.
+ Variable P : Prop.
+ Hypothesis p_true : P.
+
+ Lemma a : P.
+ Proof using.
+ trivial.
+ (* marker A *)
+ Qed.
+"
+ "Coq source for ert-deftest error-message-visible-at-proof-end")
+
;;; utility functions
@@ -425,6 +440,70 @@ something and be visible in two-pane mode."
"3 = 3"
"Check"))
+(defun check-error-at-qed (intermediate-pos)
+ "Check that Qed correctly shows an error.
+Run a script that provokes an error at Qed about a not declared section
+variable and check that the error message is displayed."
+ (let (buffer
+ (proof-omit-proofs-option nil))
+ (unwind-protect
+ (progn
+ (find-file "goals.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-not-declared-section-variable)
+ (goto-char (point-min))
+
+ (if intermediate-pos
+ (progn
+ (message "process up to %s" intermediate-pos)
+ (should (re-search-forward intermediate-pos nil t))
+ (beginning-of-line)
+ (forward-line 1)
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content "*coq*")
+ )
+ (message "process complete script in one step"))
+
+ (goto-char (point-max))
+ (message "process complete script to end")
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content "*coq*")
+ ;; (record-buffer-content "*response*")
+
+ ;; check that the goals buffer is empty
+ (with-current-buffer proof-goals-buffer
+ (should (equal (point-min) (point-max))))
+
+ (with-current-buffer proof-response-buffer
+ (goto-char (point-min))
+ (should
+ (re-search-forward
+ "The following section variable is used but not declared:"
+ nil t))))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+(ert-deftest error-message-visible-at-qed-complete-script ()
+ :expected-result :failed
+ "Check that the error message is present at the end of the proof.
+Run a complete script that provokes an error at Qed about a not declared
+section variable and check that the error message is displayed."
+ (message "Check that the error message is present at Qed for complete
script.")
+ (check-error-at-qed nil))
+
+(ert-deftest error-message-visible-at-qed-one-step ()
+ "Check that the error message is present for Qed.
+Run a proof that uses an undeclared section variable. Check that the
+error message is displayed when running Qed alone as single step."
+ (message "Check that the error message is present at Qed for single step.")
+ (check-error-at-qed "marker A"))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; response buffer visibility tests
