From f1f3836dcc6d5ea90407ff81a1f954c41562fac9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Feb 2017 21:44:35 +0100
Subject: [PATCH] Bump Iris and fix several TODOs and FIXMEs.
---
opam.pins | 2 +-
theories/lang/lifting.v | 3 +--
theories/lifetime/model/raw_reborrow.v | 3 +--
theories/typing/own.v | 7 ++-----
theories/typing/programs.v | 5 ++---
theories/typing/type_context.v | 6 +-----
theories/typing/unsafe/spawn.v | 10 ++--------
7 files changed, 10 insertions(+), 26 deletions(-)
diff --git a/opam.pins b/opam.pins
index 7da43734..2e1903eb 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 8b9f59ab3630176149621661c8f3ee7b456dfe5f
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9ea6fa453f1b9ef1cd4b5b8a167d1fab717c895e
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 9e0263e9..887fbc2c 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -51,8 +51,7 @@ Proof.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
iModIntro; iSplit=> //. iFrame.
- (* FIXME: Merging these two into one "iApply" doesn't work. *)
- iSpecialize ("HΦ" $! _ (length init)). iApply ("HΦ" $! (list_to_vec init)).
+ iApply ("HΦ" $! _ _ (list_to_vec init)).
rewrite vec_to_list_of_list. auto.
Qed.
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
index e563a17e..fadea3d2 100644
--- a/theories/lifetime/model/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -40,8 +40,7 @@ Proof.
iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
{ by rewrite lookup_fmap HB. }
iMod (own_bor_update_2 with "HBâ— Hi") as "[HBâ— Hi]".
- { eapply auth_update. (* FIXME: eapply singleton_local_update loops. *)
- apply: singleton_local_update; last eapply
+ { eapply auth_update, singleton_local_update; last eapply
(exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iAssert (▷?q lft_inv A κ)%I with "[H◯ HB◠HB Hvs' Hinh' Hbox]" as "Hκ".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index af0840fc..94192e2c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -155,8 +155,7 @@ Section own.
iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
- iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
- iMod "Hfin" as "[Hshr $]". by iApply Hsync.
+ iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
Qed.
End own.
@@ -225,9 +224,7 @@ Section typing.
typed_body E L C T (let: x := new [ #n ] in e).
Proof.
intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
- iIntros (v). iApply typed_body_mono; [done| |done|].
- (* FIXME : why can't we iApply Htyp? *)
- 2:by iDestruct (Htyp v) as "$".
+ iIntros (v). iApply typed_body_mono; [done| |done|by iApply (Htyp v)].
by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
Qed.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 16be9ec8..d82cf7b1 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -262,9 +262,8 @@ Section typing_rules.
Proof.
iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL HT".
iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
- (* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
- { iPoseProof Hwrt as "Hwrt". done. }
- { iPoseProof Hread as "Hread". done. }
+ { iApply Hwrt. }
+ { iApply Hread. }
{ by rewrite tctx_interp_cons tctx_interp_singleton. }
rewrite tctx_interp_cons tctx_interp_singleton. auto.
Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 77a4aa7e..dc0d11b9 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -155,11 +155,7 @@ Section type_context.
Global Instance tctx_ty_copy T p ty :
CopyC T → Copy ty → CopyC ((p ◠ty) :: T).
- Proof.
- (* TODO RJ: Should we have instances that PersistentP respects equiv? *)
- intros ???. rewrite /PersistentP tctx_interp_cons.
- apply uPred.sep_persistent; by apply _.
- Qed.
+ Proof. intros ???. rewrite tctx_interp_cons. apply _. Qed.
(** Send typing contexts *)
Class SendC (T : tctx) :=
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index aa79c626..56a50af5 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -23,14 +23,8 @@ Section join_handle.
end%I;
ty_shr κ tid l := True%I |}.
Next Obligation. by iIntros (ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
- Next Obligation.
- (* FIXME: Replacing the % by a _ below fails. *)
- iIntros "* % _ _ $". auto.
- Qed.
- Next Obligation.
- (* FIXME: for some reason, `iIntros "*" does not do anything here. *)
- iIntros (?) "* _ _ _". auto.
- Qed.
+ Next Obligation. iIntros "* _ _ _ $". auto. Qed.
+ Next Obligation. iIntros (?) "**"; auto. Qed.
Lemma join_handle_subtype ty1 ty2 :
type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
--
GitLab