From 8dac02feee6dab63693cd4ee352c3f5fbbdb9809 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Sep 2024 18:53:14 +0200
Subject: [PATCH] use Coq 8.20 for reftesting

---
 Makefile.coq.local  | 16 +++++++++-------
 tests/bi.ref        | 12 ++++--------
 tests/heap_lang.ref |  8 ++++----
 tests/proofmode.ref |  4 ++--
 4 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 4df3f5c55..4babb6f23 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -4,6 +4,11 @@ NO_TEST:=
 # use MAKE_REF=1 to generate new reference files
 MAKE_REF:=
 
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: style $(if $(NO_TEST),,test)
 
@@ -26,10 +31,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# These versions of Coq are known to have different output so we don't test them.
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-# Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
-COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -46,14 +47,15 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
 	$(HIDE)REF=$*".ref" && \
-	  echo "COQTEST$(if $(COQ_NOREF), [ref diff ignored],$(if $(MAKE_REF), [make ref],)) $< (ref: $$REF)" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref diff ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
 	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
 	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(COQ_NOREF), (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) , \
-	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE") \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) \
 	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@
diff --git a/tests/bi.ref b/tests/bi.ref
index faa15d658..9aed176aa 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -5,21 +5,17 @@ m : gmap nat nat
 The term "m" has type "gmap nat nat" while it is expected to have type
  "gmap nat Z" (cannot unify "nat" and "Z").
 The command has indeed failed with message:
-Unable to satisfy the following constraints:
 In environment:
 PROP : bi
 P : PROP
-
-?p : "Persistent (|==> P)"
-
+Could not find an instance for the following existential variables:
+?p : Persistent (|==> P)
 The command has indeed failed with message:
-Unable to satisfy the following constraints:
 In environment:
 PROP : bi
 P : PROP
-
-?p : "Persistent (â–  P)"
-
+Could not find an instance for the following existential variables:
+?p : Persistent (â–  P)
 "match_def_unfold_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 613d78114..8af930a4f 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -232,10 +232,10 @@ Tactic failure: wp_pure: "Hcred" is not fresh.
   q3 : Qp
   v4 : val
   q4 : Qp
-  H : ((✓ (DfracOwn q3 ⋅ DfracOwn q4) ∧ v3 = v4)
-       ∧ ✓ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)) ∧ v2 = v3)
-      ∧ ✓ (DfracOwn q1 ⋅ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)))
-        ∧ v1 = v2
+  H :
+    ((✓ (DfracOwn q3 ⋅ DfracOwn q4) ∧ v3 = v4)
+     ∧ ✓ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)) ∧ v2 = v3)
+    ∧ ✓ (DfracOwn q1 ⋅ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4))) ∧ v1 = v2
   ============================
   --------------------------------------∗
   ⌜(q1 + (q2 + (q3 + q4)) ≤ 1)%Qp⌝ ∗ ⌜v1 = v2⌝ ∗ ⌜
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 58da080bd..402665b1e 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -708,8 +708,8 @@ No applicable tactic.
   
   PROP : bi
   Ψ, Φ : nat → PROP
-  HP : ∀ (f : nat → nat) (y : nat),
-         TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
+  HP :
+    ∀ (f : nat → nat) (y : nat), TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
   ============================
   "H" : Ψ 11
   --------------------------------------∗
-- 
GitLab