From 25d7353efb82929c008a04c14cd91cda6ddef4f8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 31 Aug 2023 15:26:09 +0200
Subject: [PATCH] update dependencies

---
 coq-actris.opam                                |  2 +-
 theories/channel/channel.v                     |  4 +++-
 theories/examples/basics.v                     |  2 ++
 theories/examples/par_map.v                    |  2 ++
 theories/examples/pizza.v                      |  2 ++
 theories/logrel/examples/compute_client_list.v |  4 +++-
 theories/logrel/examples/par_recv.v            |  2 ++
 theories/logrel/lib/mutex.v                    | 16 +++++++++-------
 8 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/coq-actris.opam b/coq-actris.opam
index 6a4adc2..ddd01db 100644
--- a/coq-actris.opam
+++ b/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-08-03.5.fe2b6d61") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-08-29.5.af0a091b") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 86d2ce9..e17e6b7 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -28,6 +28,8 @@ From actris.channel Require Export proto.
 From actris.utils Require Import llist skip.
 Set Default Proof Using "Type".
 
+Local Existing Instance spin_lock.
+
 (** * The definition of the message-passing connectives *)
 Definition new_chan : val :=
   λ: <>,
@@ -69,7 +71,7 @@ Class chanG Σ := {
   chanG_lockG :: lockG Σ;
   chanG_protoG :: protoG Σ val;
 }.
-Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
+Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 29b7e32..ba010b6 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -4,6 +4,8 @@ From actris.channel Require Import proofmode.
 From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import contribution.
 
+Local Existing Instance spin_lock.
+
 (** Basic *)
 Definition prog : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" #42) in
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index cd84a10..525e0e9 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
+Local Existing Instance spin_lock.
+
 (** * Distributed version (aka the implementation) *)
 Definition par_map_worker : val :=
   rec: "go" "map" "l" "c" :=
diff --git a/theories/examples/pizza.v b/theories/examples/pizza.v
index 6180e22..b567488 100644
--- a/theories/examples/pizza.v
+++ b/theories/examples/pizza.v
@@ -3,6 +3,8 @@ From actris.utils Require Import llist.
 From actris.channel Require Import proofmode.
 From stdpp Require Import list.
 
+Local Existing Instance spin_lock.
+
 Inductive pizza :=
   | Margherita
   | Calzone.
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 6f9494b..47d04d9 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -22,6 +22,8 @@ From actris.logrel Require Import session_typing_rules napp.
 From actris.logrel.lib Require Import list par_start.
 From actris.logrel.examples Require Import compute_service.
 
+Local Existing Instance spin_lock.
+
 Definition send_all_par : val :=
   rec: "go" "c" "xs" "lk" "counter" :=
     if: lisnil "xs" then
@@ -56,7 +58,7 @@ Definition compute_client : val :=
     recv_all_par "c" "ys" "n" "lk" "counter");; "ys".
 
 Section compute_example.
-  Context `{heapGS Σ, chanG Σ, lockG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, spin_lockG Σ, spawnG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition compute_type_client_aux (rec : lsty Σ) : lsty Σ :=
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 5b72a10..446ea7c 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -18,6 +18,8 @@ From iris.heap_lang.lib Require Export par spin_lock.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Export term_typing_judgment session_types.
 
+Local Existing Instance spin_lock.
+
 Definition prog : val := λ: "c",
   let: "lock" := newlock #() in
   (
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index eb5ca71..73df8f1 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -24,11 +24,13 @@ This type former is strongly inspired by the [Mutex] type in the standard
 library of Rust, which has also been semantically modelled in the LambdaRust
 project.
 *)
-From iris.heap_lang.lib Require Export spin_lock.
+From iris.heap_lang.lib Require Import spin_lock.
 From iris.heap_lang Require Import metatheory.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Export term_types term_typing_judgment subtyping.
 
+Local Existing Instance spin_lock.
+
 (** Mutex functions *)
 Definition mutex_alloc : val := λ: "x", (newlock #(), ref "x").
 Definition mutex_acquire : val := λ: "x", acquire (Fst "x");; ! (Snd "x").
@@ -37,15 +39,15 @@ Definition mutex_release : val :=
 
 (** Semantic types *)
 Definition lty_mutex `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-  ∃ (γ : gname) (l : loc) (lk : val),
+  ∃ (γ : lock_name) (l : loc) (lk : val),
     ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I.
 
 Definition lty_mutex_guard `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-  ∃ (γ : gname) (l : loc) (lk : val) (v : val),
+  ∃ (γ : lock_name) (l : loc) (lk : val) (v : val),
     ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
-    spin_lock.locked γ ∗ l ↦ v)%I.
+    lock.locked γ ∗ l ↦ v)%I.
 
 Global Instance: Params (@lty_mutex) 3 := {}.
 Global Instance: Params (@lty_mutex_guard) 3 := {}.
@@ -73,7 +75,7 @@ Section properties.
   Proof.
     iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv".
     iExists γ, l, lk. iSplit; first done.
-    iApply (spin_lock.is_lock_iff with "Hinv").
+    iApply (is_lock_iff with "Hinv").
     iIntros "!> !>". iSplit.
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
@@ -90,7 +92,7 @@ Section properties.
     iIntros "#[Hle1 Hle2]" (v) "!>".
     iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]".
     iExists γ, l, lk, w. iSplit; first done.
-    iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv").
+    iFrame "Hlock Hinner". iApply (is_lock_iff with "Hinv").
     iIntros "!> !>". iSplit.
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
@@ -98,7 +100,7 @@ Section properties.
 End properties.
 
 Section rules.
-  Context `{heapGS Σ, lockG Σ}.
+  Context `{heapGS Σ, spin_lockG Σ}.
 
   (** Mutex properties *)
   Lemma ltyped_mutex_alloc Γ A :
-- 
GitLab