From 2de34a17ffbd920aba781365b3d8537fdd8cc69f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Wed, 21 Aug 2024 10:09:44 +0200
Subject: [PATCH] bump iris
---
.gitlab-ci.yml | 8 ++++----
semantics.opam | 8 ++++----
theories/program_logics/heap_lang/derived_laws.v | 4 ++--
theories/program_logics/heap_lang/primitive_laws.v | 2 +-
4 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 52fe123..9c89c72 100644
--- a/.gitlab-ci.yml
+++ b/.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
diff --git a/semantics.opam b/semantics.opam
index 41493c3..5649e4c 100644
--- a/semantics.opam
+++ b/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}%"]
diff --git a/theories/program_logics/heap_lang/derived_laws.v b/theories/program_logics/heap_lang/derived_laws.v
index e43905d..2586fc6 100644
--- a/theories/program_logics/heap_lang/derived_laws.v
+++ b/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.
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index 5d766c6..194a07d 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/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Φ".
--
GitLab