From 370567111db1805916e7d7ff31efda43390cdae2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 08:52:17 +0200
Subject: [PATCH] Bump Iris.
---
coq-gpfsl.opam | 2 +-
coq-orc11.opam | 2 +-
gpfsl-examples/list_helper.v | 2 +-
gpfsl-examples/queue/proof_ms_abs_graph.v | 4 ++--
gpfsl-examples/stack/proof_treiber_history.v | 2 +-
5 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 4793653a..165eace9 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
- "coq-iris" { (= "dev.2023-10-03.0.70b30af7") | (= "dev") }
+ "coq-iris" { (= "dev.2023-10-05.2.da1ec123") | (= "dev") }
"coq-orc11" {= version}
]
diff --git a/coq-orc11.opam b/coq-orc11.opam
index fbca1bde..dbaff5cf 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
depends: [
- "coq-stdpp" { (= "dev.2023-10-03.0.83c8fcbf") | (= "dev") }
+ "coq-stdpp" { (= "dev.2023-10-05.1.c57a2eed") | (= "dev") }
]
build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index d5c39964..3c7ea936 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -458,7 +458,7 @@ Proof.
have EqL: length L11 = length L21.
{ revert ND HL1 HL2. rewrite -Eq. by apply NoDup_lookup. }
have Eq1: L11 = L21.
- { rewrite -(take_app L11 ([a] ++ L12)) -(take_app L21 ([a] ++ L22)).
+ { rewrite -(take_app_length L11 ([a] ++ L12)) -(take_app_length L21 ([a] ++ L22)).
by rewrite Eq EqL. }
by simplify_list_eq.
Qed.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 659b6a82..ddb84f16 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -3431,8 +3431,8 @@ Proof.
have Eq': (D2' ++ [(η2, n2)] ++ [(η2', n2')]).*1
= (D20 ++ [(η2, n2)] ++ D22).*1. { by f_equal. }
move : Eq'. by rewrite !fmap_app. }
- have EqL1 := take_app D2' ([(η2, n2)] ++ [(η2', n2')]).
- have EqL2 := take_app D20 ([(η2, n2)] ++ D22).
+ have EqL1 := take_app_length D2' ([(η2, n2)] ++ [(η2', n2')]).
+ have EqL2 := take_app_length D20 ([(η2, n2)] ++ D22).
rewrite EqD2' (_: length D2' = length D20) in EqL1.
- by rewrite EqL1 in EqL2.
- by rewrite -(fmap_length fst D2') -(fmap_length fst D20) Eq1. }
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 6b93d641..d615e490 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -212,7 +212,7 @@ Lemma length_concat_fmap_take_plus_S (f : _ → list event_id) gen1' emo x N
Proof.
apply lookup_lt_Some in GEN1 as LEgen1'.
rewrite -{1}(take_drop gen1' emo).
- rewrite take_add_app; last first. { rewrite take_length. lia. }
+ rewrite take_app_add'; last first. { rewrite take_length. lia. }
rewrite fmap_app concat_app app_length.
rewrite (drop_S _ _ _ GEN1). rewrite firstn_cons fmap_cons /=.
rewrite app_length. done.
--
GitLab