Merge branch 'ralf/coq-8.20' into 'master'

test Coq 8.20

See merge request iris/iris!1073

.gitlab-ci.yml

@@ -45,10 +45,10 @@ variables:
 ## Build jobs
 
 # The newest version runs with timing.
-build-coq.8.19.1:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.19.1"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     OPAM_PKG: "1"
@@ -59,22 +59,28 @@ build-coq.8.19.1:
   interruptible: false
 
 # The newest version also runs in MRs, without timing.
-build-coq.8.19.1-mr:
+build-coq.8.20.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.19.1"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
 # Also ensure Dune works.
-build-coq.8.19.1-dune:
+build-coq.8.20.0-dune:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.19.1   dune version 3.15.2"
+    OPAM_PINS: "coq version 8.20.0   dune version 3.15.2"
     MAKE_TARGET: "dune"
 
+build-coq.8.19.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.19.1"
+    DENY_WARNINGS: "1"
+
 # The oldest version runs in MRs, without name mangling.
 build-coq.8.18.0:
   <<: *template

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 $@

README.md

@@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.18.0 / 8.19.1
+ - Coq 8.18.0 / 8.19.1 / 8.20.0
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
 Generally we always aim to support the last two stable Coq releases. Support for

_CoqProject

@@ -21,6 +21,8 @@
 -arg -w -arg -unknown-warning
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
+# https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
 
 iris/prelude/options.v
 iris/prelude/prelude.v

coq-iris.opam

@@ -27,7 +27,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.18" & < "8.21~") | (= "dev") }
   "coq-stdpp" { (= "dev.2024-09-11.0.f6973baf") | (= "dev") }
 ]
 

iris/bi/notation.v

@@ -33,7 +33,7 @@ which successfully undergoes automatic left-factoring. *)
 
 (** * BI connectives *)
 Reserved Notation "'emp'".
-Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
+Reserved Notation "'⌜' φ '⌝'" (at level 0, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").
 Reserved Notation "P -∗ Q"
   (at level 99, Q at level 200, right associativity,

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:

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⌝ ∗ ⌜

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
   --------------------------------------∗