Commit 745b8584 authored by Dan Frumin's avatar Dan Frumin

bump std++ & iris

parent b9f71b10
Pipeline #15440 passed with stage
in 10 minutes and 19 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-02-25.0.9b44e889") | (= "dev") }
"coq-iris" { (= "dev.2019-03-06.2.f5d03e25") | (= "dev") }
]
......@@ -127,7 +127,7 @@ Section cwp_rules.
iApply (wp_wand with "Hcwp").
iIntros (v) "HΦ".
iIntros (γ env l I) "#Hflock Hres #Heq".
iMod (flock_res_alloc_strong _ (dom (gset lock_res_gname) I) with "Hflock HR1") as (ρ) "[% Hres']"; first done.
iMod (flock_res_alloc_cofinite _ (dom (gset lock_res_gname) I) with "Hflock HR1") as (ρ) "[% Hres']"; first done.
pose (I' := <[ρ:=(1%Qp,R1)]>I).
assert (I !! ρ = None) by by eapply not_elem_of_dom.
iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
......@@ -217,7 +217,7 @@ Section cwp_rules.
iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
wp_apply (newflock_spec cmonadN); first done.
iIntros (k γ') "#Hlock2".
iMod (flock_res_alloc_strong _ _ _ (env_inv env Q)%I with "Hlock2 [$HQ $Henv]") as (ρ) "[_ Hres]"; first done.
iMod (flock_res_alloc_cofinite _ _ _ (env_inv env Q)%I with "Hlock2 [$HQ $Henv]") as (ρ) "[_ Hres]"; first done.
wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hres]").
......@@ -337,7 +337,7 @@ Section cwp_run.
iSpecialize ("Hwp" $! amg). rewrite cwp_eq /cwp_def.
wp_apply (newflock_spec cmonadN); first done.
iIntros (k γ') "#Hlock". iApply wp_fupd.
iMod (flock_res_alloc_strong _ _ _ (env_inv env)%I
iMod (flock_res_alloc_cofinite _ _ _ (env_inv env)%I
with "Hlock [Henv Hσ]") as (ρ) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
wp_let.
......
......@@ -265,7 +265,7 @@ Section flock.
(** ** Spectral operations *)
Lemma flock_res_alloc_strong (X : gset lock_res_gname) γ lk R E :
Lemma flock_res_alloc_cofinite (X : gset lock_res_gname) γ lk R E :
N E
is_flock γ lk -
R ={E}= ρ, ⌜ρ X flock_res γ ρ 1 R.
......@@ -285,8 +285,8 @@ Section flock.
set (X := set_map flock_token2_name
(dom (gset lock_res_gname) (fp from_active fa)) : gset gname).
iMod (own_alloc_strong (Excl ()) X) as (γt Ht) "T1"; first done.
iMod (own_alloc_strong (Excl ()) X) as (γt Ht) "T2"; first done.
iMod (own_alloc_cofinite (Excl ()) X) as (γt Ht) "T1"; first done.
iMod (own_alloc_cofinite (Excl ()) X) as (γt Ht) "T2"; first done.
iMod (cinv_alloc _ (resN.@(γt,γt)) (R own γt (Excl ()) own γt (Excl ()))%I with "[HR T1]") as (γc) "[#HR Hρ]".
{ iNext. iLeft. by iFrame. }
set (ρ :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment