Update to rely on Coq 8.17

.github/workflows/build.yml

@@ -20,10 +20,9 @@ jobs:
           - "dev"
           - "8.18"
           - "8.17"
-          - "8.16"
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: "iris-simp-lang.opam"
@@ -35,18 +34,16 @@ jobs:
             startGroup "Print opam config"
               opam config list; opam repo list; opam list
             endGroup
-  # NOTE: re-enable this job once Iris releases something after 4.0.0. (The only
-  # issue is that `iSolveTC` was moved to `tc_solve` in stdpp.)
-  #build-release:
-  #  name: build (released iris, coq dev)
-  #  runs-on: ubuntu-latest
-  #  strategy:
-  #    fail-fast: false
-  #  steps:
-  #    - uses: actions/checkout@v2
-  #    - uses: coq-community/docker-coq-action@v1
-  #      with:
-  #        custom_image: "coqorg/coq:dev"
+  build-release:
+    name: build (released iris, coq dev)
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v4
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: "coqorg/coq:dev"
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

README.md

@@ -52,8 +52,8 @@ There are a few files that are optional reading which make the tutorial work:
 
 ## Compiling
 
-This development relies on a development version of Iris and Coq 8.14 or later.
-We test Coq 8.14, 8.15, 8.16, and master with Iris dev in CI. (The released
+This development relies on a development version of Iris and Coq 8.17 or later.
+We test Coq 8.17, 8.18, and master with Iris dev in CI. (The released
 version of Iris is currently incompatible.)
 
 You'll need to install Iris, which is easiest done through opam. There are

_CoqProject

@@ -2,10 +2,7 @@
 
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overriden
-# Fixing this one requires Coq 8.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
-# Fixing this requires Coq 8.17
--arg -w -arg -future-coercion-class-field
+-arg -w -arg -deprecated-since-8.19
 
 src/lang.v
 src/notation.v

src/adequacy.v

@@ -33,8 +33,8 @@ ghost name and associated state.
 (** These assumptions are just functors in Σ, unlike simpGS which also has a
 ghost name. *)
 Class simpGpreS Σ := SimpPreG {
-  simp_preG_iris :> invGpreS Σ;
-  simp_preG_heap :> heap_mapGpreS loc val Σ;
+  simp_preG_iris :: invGpreS Σ;
+  simp_preG_heap :: heap_mapGpreS loc val Σ;
 }.
 
 Definition simpΣ : gFunctors :=

src/examples/spawn.v

@@ -23,7 +23,7 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 (* Not bundling simpGS, as it may be shared with other users. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
@@ -78,4 +78,4 @@ Proof.
 Qed.
 End proof.
 
-Typeclasses Opaque join_handle.
+#[export] Typeclasses Opaque join_handle.

src/heap_lib.v

@@ -19,11 +19,11 @@ directly in the IPM).
 |*)
 
 Class heap_mapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  heap_mapGpreS_inG :> inG Σ (heap_mapR L V);
+  heap_mapGpreS_inG :: inG Σ (heap_mapR L V);
 }.
 
 Class heap_mapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  heap_map_inG :> heap_mapGpreS L V Σ;
+  heap_map_inG :: heap_mapGpreS L V Σ;
   heap_map_name : gname;
 }.
 Global Arguments GenHeapGS L V Σ {_ _ _} _ : assert.

src/primitive_laws.v

@@ -61,7 +61,7 @@ them in `adequacy.v`.
 
 Class simpGS Σ := SimpGS {
   simp_invGS : invGS Σ;
-  simp_heap_mapG :> heap_mapGS loc val Σ;
+  simp_heap_mapG :: heap_mapGS loc val Σ;
 }.
 
 (* Observe that this instance assumes [simpGS Σ], which already has a fixed ghost