bump iris

.gitlab-ci.yml

@@ -29,11 +29,11 @@ variables:
 
 ## Build jobs
 
-# build against known-working Coq 8.18.0
-build-coq.8.18.0:
+# build against known-working Coq 8.19.2
+build-coq.8.19.2:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.19.2"
     #DENY_WARNINGS: "1"
     #MANGLE_NAMES: "1"
     #OPAM_PKG: "1"
@@ -44,7 +44,7 @@ build-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.18.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.19.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   except:
   only:
   - triggers

semantics.opam

@@ -9,10 +9,10 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.18" & < "8.19~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2024-06-10.0.84ed8993") | (= "dev") }
-  "coq-equations" { (= "1.3+8.18") }
-  "coq-autosubst" { (= "1.8") | (= "dev")  }
+  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-08-20.0.657b34ad") | (= "dev") }
+  "coq-equations" { (= "1.3+8.18") | = "1.3+8.19" }
+  "coq-autosubst" { (= "1.8") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/program_logics/heap_lang/derived_laws.v

@@ -85,13 +85,13 @@ Proof.
   iDestruct (array_app with "Hl") as "[Hl1 Hl]".
   iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
   assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
-  rewrite take_length min_l; last by lia. iFrame "Hl2".
+  rewrite length_take min_l; last by lia. iFrame "Hl2".
   iIntros (w) "Hl2".
   clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
   { apply list_lookup_insert. lia. }
   rewrite -[in (l ↦∗{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
   iApply array_app. rewrite take_insert; last by lia. iFrame.
-  iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
+  iApply array_cons. rewrite length_take min_l; last by lia. iFrame.
   rewrite drop_insert_gt; last by lia. done.
 Qed.
 

theories/program_logics/heap_lang/primitive_laws.v

@@ -118,7 +118,7 @@ Proof.
   iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
-    rewrite replicate_length Z2Nat.id; auto with lia. }
+    rewrite length_replicate Z2Nat.id; auto with lia. }
   iApply step_fupd_intro; first done.
   iModIntro. iFrame "Hσ". do 2 (iSplit; first done).
   iApply wp_value_fupd. iApply "HΦ".