Bump Iris; bump minimal Coq version to 8.17.

.gitlab-ci.yml

@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.15.1:
+build-coq.8.17.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1"
+    OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
     OPAM_PKG: "1"
   tags:

README.md

@@ -10,7 +10,7 @@ the paper
 
 It has been built and tested with the following dependencies
 
- - Coq 8.15.1
+ - Coq 8.17.0
  - The version of Iris in the [opam file](opam)
 
 In order to build, install the above dependencies and then run

_CoqProject

 -Q theories actris
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
-# Coq emits warnings when a custom entry is reimported, this is too noisy.
--arg -w -arg -custom-entry-overriden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection

coq-actris.opam

@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/channel/channel.v

@@ -66,8 +66,8 @@ Definition recv : val :=
 
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
-  chanG_lockG :> lockG Σ;
-  chanG_protoG :> protoG Σ val;
+  chanG_lockG :: lockG Σ;
+  chanG_protoG :: protoG Σ val;
 }.
 Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.

theories/channel/proto.v

@@ -56,7 +56,7 @@ Export action.
 
 (** * Setup of Iris's cameras *)
 Class protoG Σ V :=
-  protoG_authG :>
+  protoG_authG ::
     inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
 
 Definition protoΣ V := #[

theories/examples/map_reduce.v

@@ -90,8 +90,8 @@ End map_reduce.
 
 (** * Correctness proofs of the distributed version *)
 Class map_reduceG Σ A B `{Countable A, Countable B} := {
-  map_reduce_mapG :> mapG Σ A;
-  map_reduce_reduceG :> mapG Σ (Z * list B);
+  map_reduce_mapG :: mapG Σ A;
+  map_reduce_reduceG :: mapG Σ (Z * list B);
 }.
 
 Section mapper.

theories/examples/par_map.v

@@ -54,8 +54,8 @@ Definition par_map_client : val := λ: "n" "map" "xs",
 
 (** * Correctness proofs of the distributed version *)
 Class mapG Σ A `{Countable A} := {
-  map_contributionG :> contributionG Σ (gmultisetUR A);
-  map_lockG :> lockG Σ;
+  map_contributionG :: contributionG Σ (gmultisetUR A);
+  map_lockG :: lockG Σ;
 }.
 
 Section map.

theories/logrel/model.v

@@ -44,7 +44,7 @@ Arguments lsty_car {_} _ : simpl never.
 Global Instance lty_inhabited Σ k : Inhabited (lty Σ k) := populate $
   match k with
   | tty_kind => Ltty inhabitant
-  | lty_kind => Lsty inhabitant
+  | sty_kind => Lsty inhabitant
   end.
 
 Section lty_ofe.
@@ -53,12 +53,12 @@ Section lty_ofe.
   Instance lty_equiv k : Equiv (lty Σ k) :=
     match k with
     | tty_kind => λ A B, ∀ w, ltty_car A w ≡ ltty_car B w
-    | lty_kind => λ S T, lsty_car S ≡ lsty_car T
+    | sty_kind => λ S T, lsty_car S ≡ lsty_car T
     end.
   Instance lty_dist k : Dist (lty Σ k) :=
     match k with
     | tty_kind => λ n A B, ∀ w, ltty_car A w ≡{n}≡ ltty_car B w
-    | lty_kind => λ n S T, lsty_car S ≡{n}≡ lsty_car T
+    | sty_kind => λ n S T, lsty_car S ≡{n}≡ lsty_car T
     end.
 
   Lemma lty_ofe_mixin k : OfeMixin (lty Σ k).

theories/logrel/subtyping.v

@@ -8,7 +8,7 @@ From actris.logrel Require Export model term_types.
 Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
   match k with
   | tty_kind => λ A1 A2, ■ ∀ v, ltty_car A1 v -∗ ltty_car A2 v
-  | lty_kind => λ P1 P2, ■ iProto_le (lsty_car P1) (lsty_car P2)
+  | sty_kind => λ P1 P2, ■ iProto_le (lsty_car P1) (lsty_car P2)
   end%I.
 Arguments lty_le : simpl never.
 Infix "<:" := lty_le (at level 70) : bi_scope.

theories/utils/contribution.v

@@ -21,7 +21,7 @@ From iris.algebra Require Import excl auth csum gmultiset numbers.
 From iris.algebra Require Export local_updates.
 
 Class contributionG Σ (A : ucmra) `{!CmraDiscrete A} := {
-  contribution_inG :> inG Σ
+  contribution_inG :: inG Σ
     (authR (optionUR (csumR (prodR positiveR A) (exclR unitO))))
 }.