ci/coq-tests: expect 060_coq-test-wholefile to fail for 8.17

See also ProofGeneral#698.
hendriktews · Apr 8, 2023 · 1891f09 · 1891f09
1 parent 911cf01
commit 1891f09
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git 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
@@ -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)