From 911cf014b899212815c2ec8d3e8c8b88be0df57b Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Sun, 19 Mar 2023 18:59:30 +0100
Subject: [PATCH] test-omit-proofs: skip for Coq 8.8 or older

Test omit-proofs-never-omit-hints uses a feature ('#[local]') that has
only been introduced in Coq 8.9. If we continue our current support
policy, we will stop to support Coq 8.10 and older in April 2023.
Instead of a proper fix, I therefore decided to simply skip the test
for Coq 8.8 or older.
---
 ci/simple-tests/omit_test.v         | 19 ++++++++++---------
 ci/simple-tests/test-omit-proofs.el | 17 ++++++++++++++++-
 coq/coq-system.el                   | 12 ++++++++++++
 3 files changed, 38 insertions(+), 10 deletions(-)

diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v
index 417e23951..f0382c5e3 100644
--- a/ci/simple-tests/omit_test.v
+++ b/ci/simple-tests/omit_test.v
@@ -41,15 +41,6 @@ Qed.
 
 (* automatic test marker 4 *)
 
-Lemma never_omit_hints : 1 + 1 = 2.
-Proof using.
-  #[local] Hint Resolve classic_excluded_middle : core.
-  (* automatic test marker 5 *)
-  auto.
-Qed.
-
-(* automatic test marker 6 *)
-
 Section let_test.
 
   Let never_omit_let : 1 + 1 = 2.
@@ -61,3 +52,13 @@ Section let_test.
 End let_test.
 
 (* automatic test marker 8 *)
+
+Lemma never_omit_hints : 1 + 1 = 2.
+Proof using.
+  (* Note that attributes such as #[local] were only introduced in Coq 8.9. *)
+  #[local] Hint Resolve classic_excluded_middle : core.
+  (* automatic test marker 5 *)
+  auto.
+Qed.
+
+(* automatic test marker 6 *)
diff --git a/ci/simple-tests/test-omit-proofs.el b/ci/simple-tests/test-omit-proofs.el
index 45a99ffb5..891343370 100644
--- a/ci/simple-tests/test-omit-proofs.el
+++ b/ci/simple-tests/test-omit-proofs.el
@@ -18,6 +18,17 @@
 ;; - the proof has omitted color then
 ;; - stuff before the proof still has normal color
 
+;; Load stuff for `coq--version<'
+(require 'proof-site)
+(proof-ready-for-assistant 'coq)
+(require 'coq-system)
+
+(defconst coq--post-v809 (coq--post-v809)
+  "t if Coq is more recent than 8.8")
+
+(message "omit tests run with Coq version %s; post-v809: %s"
+         (coq-version t) coq--post-v809)
+
 ;; reimplement seq-some from the seq package
 ;; seq-some not present in emacs 24
 ;; XXX consider to switch to seq-some when support for emacs 24 is dropped
@@ -170,7 +181,11 @@ In particular, test that with proof-omit-proofs-option configured:
   :expected-result :failed
   "Test that proofs containing Hint are never omitted.
 This test only checks that the face in the middle of the proof is
-the normal `proof-locked-face'."
+the normal `proof-locked-face'.
+
+The sources for the test contain a local attribute in form of
+'#[local]', which has been introduced only in Coq version 8.9."
+  (skip-unless coq--post-v809)
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
   (reset-coq)
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 1ee3b5698..f21334d3f 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -182,6 +182,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-v809 ()
+  "Return t if the auto-detected version of Coq is >= 8.9.
+Return nil if the version cannot be detected."
+  (let ((coq-version-to-use (or (coq-version t) "8.8")))
+    (condition-case err
+	(not (coq--version< coq-version-to-use "8.10alpha"))
+      (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--post-v810 ()
   "Return t if the auto-detected version of Coq is >= 8.10.
 Return nil if the version cannot be detected."