branch: elpa/proof-general
commit dac9b5d32ec1404d35e3dd83070591806f8977b0
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
ci/coq-tests: expect 060_coq-test-wholefile to fail for 8.17
See also #698.
---
ci/coq-tests.el | 2 ++
coq/coq-system.el | 12 ++++++++++++
2 files changed, 14 insertions(+)
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 774cc989f5..a8c97be594 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -259,6 +259,8 @@ For example, COMMENT could be (*test-definition*)"
(ert-deftest 060_coq-test-wholefile ()
+ ;; test_wholefile.v triggers a fatal warning in 8.17, see also #698
+ :expected-result (if (coq--post-v817) :failed :passed)
"Test `proof-process-buffer'."
(coq-fixture-on-file
(coq-test-full-path "test_wholefile.v")
diff --git a/coq/coq-system.el b/coq/coq-system.el
index f21334d3f3..db8cbc6e6e 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -218,6 +218,18 @@ Return nil if the version cannot be detected."
(signal 'coq-unclassifiable-version coq-version-to-use))
(t (signal (car err) (cdr err))))))))
+(defun coq--post-v817 ()
+ "Return t if the auto-detected version of Coq is >= 8.17.
+Return nil if the version cannot be detected."
+ (let ((coq-version-to-use (or (coq-version t) "8.16")))
+ (condition-case err
+ (not (coq--version< coq-version-to-use "8.17"))
+ (error
+ (cond
+ ((equal (substring (cadr err) 0 15) "Invalid version")
+ (signal 'coq-unclassifiable-version coq-version-to-use))
+ (t (signal (car err) (cdr err))))))))
+
(defun coq--supports-topfile ()
"Return t if \"-topfile\" appears in coqtop options"
(string-match "-topfile" coq-autodetected-help)
