CI.

.gitlab-ci.yml

@@ -27,37 +27,11 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
-  <<: *template
-  variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version dev"
-
-build-coq.8.9.0:
+build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.9.0"
-    OPAM_PKG: "coq-lambda-rust"
+    OPAM_PINS: "coq version 8.9.0 coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#ci/robbert/faster_iDestruct2"
     TIMING_CONF: "coq-8.9.0"
   tags:
   - fp-timing
 
-build-coq.8.8.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.8.2"
-
-build-coq.8.7.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.7.2"
-
-build-iris.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
-  except:
-  only:
-  - triggers
-  - schedules
-  - api

theories/lang/lib/spawn.v

@@ -105,7 +105,7 @@ Proof.
   iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
   { iMod ("Hclose" with "[Hc]").
     - iNext. iRight. iExists _. iFrame.
-    - iModIntro. wp_if. iApply ("IH" with "Hj H†"). auto. }
+    - iModIntro. wp_if. iApply ("IH" with "[HΦ] Hj H†"). auto. }
   iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
   iMod ("Hclose" with "[Hj Hf]") as "_".
   { iNext. iLeft. iFrame. }

theories/lifetime/frac_borrow.v

@@ -142,7 +142,7 @@ Proof.
     iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
     iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
   - iIntros "H†'".
-    iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
+    iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]"; try done.
     iDestruct "H" as (q') "[>Hκ' _]".
     iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
 Qed.

theories/lifetime/model/creation.v

@@ -69,7 +69,7 @@ Proof.
   destruct (decide (Kalive = ∅)) as [HKalive|].
   { iModIntro. rewrite /Iinv. iFrame.
     iApply (@big_sepS_impl with "[$HK]"); iAlways.
-    rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _]". set_solver. }
+    rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _] //". set_solver. }
   destruct (minimal_exists_L (⊂) Kalive)
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
   iDestruct (@big_sepS_delete with "HK") as "[[Hκinv Hκ] HK]"; first done.

theories/lifetime/model/primitive.v

@@ -244,12 +244,12 @@ Qed.
 
 Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
 Proof.
-  rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".
+  rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]] //".
   by destruct (lft_alive_and_dead_in A κ).
 Qed.
 Lemma lft_inv_dead_in A κ : lft_dead_in A κ → lft_inv A κ -∗ lft_inv_dead κ.
 Proof.
-  rewrite /lft_inv. iIntros (?) "[[_ %]|[$ _]]".
+  rewrite /lft_inv. iIntros (?) "[[_ %]|[$ _]] //".
   by destruct (lft_alive_and_dead_in A κ).
 Qed.
 

theories/typing/cont_context.v

@@ -71,7 +71,7 @@ Section cont_context.
   Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
   Proof.
     split.
-    - iIntros (??) "_ _ $".
+    - by iIntros (??) "_ _ $".
     - iIntros (??? H1 H2 ?) "#LFT #HE HC".
       iApply (H2 with "LFT HE"). by iApply (H1 with "LFT HE").
   Qed.
@@ -109,7 +109,7 @@ Section cont_context.
     iIntros (?) "_ #HE HC".
     rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
     iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
-      [iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
+      [by iDestruct "HC" as "[$ _]" | iApply "IH"; by iDestruct "HC" as "[_ $]"].
   Qed.
 End cont_context.
 

theories/typing/fixpoint.v

@@ -93,7 +93,7 @@ Section fixpoint.
   Proof.
     unfold eqtype, subtype, type_incl.
     setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
-    split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
+    split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; by iIntros "!#*$".
   Qed.
 End fixpoint.
 

theories/typing/function.v

@@ -260,7 +260,7 @@ Section typing.
       iInduction ps as [|p ps] "IH" forall (tys); first by simpl.
       simpl in tys. inv_vec tys=>ty tys. simpl.
       iDestruct "Hargs" as "[HT Hargs]". iSplitL "HT".
-      + iApply (wp_hasty with "HT"). iIntros (?). rewrite tctx_hasty_val. iIntros "? $".
+      + iApply (wp_hasty with "HT"). iIntros (?). rewrite tctx_hasty_val. by iIntros "? $".
       + iApply "IH". done.
     - simpl. change (@length expr ps) with (length ps).
       iIntros (vl'). inv_vec vl'=>kv vl; csimpl.

theories/typing/lib/arc.v

@@ -134,13 +134,13 @@ Section arc.
       { iDestruct "HP" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
       iDestruct "HX" as (γ ν q') "[#Hpersist H]".
       iMod ("Hclose2" with "[] H") as "[HX $]"; first by unfold shared_arc_own; auto 10.
-      iAssert C with "[>HX]" as "#$".
+      iAssert C with "[>HX]" as "#?".
       { iExists _, _, _. iFrame "Hpersist".
         iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
         iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
         { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
         iApply (bor_share with "Hrc"); solve_ndisj. }
-      iApply ("Hclose1" with "[]"). by auto.
+      iFrame "#". iApply ("Hclose1" with "[]"). by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by auto.
       iApply step_fupd_intro; first solve_ndisj. by iFrame.
   Qed.
@@ -253,9 +253,9 @@ Section arc.
       iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
       iDestruct "HP" as (γ ν) "[#Hpersist H]".
       iMod ("Hclose2" with "[] H") as "[HX $]"; first by auto 10.
-      iModIntro. iNext. iAssert C with "[>HX]" as "#$".
+      iModIntro. iNext. iAssert C with "[>HX]" as "#?".
       { iExists _, _. iFrame "Hpersist". iApply bor_share; solve_ndisj. }
-      iApply ("Hclose1" with "[]"). by auto.
+      iFrame "#". iApply ("Hclose1" with "[]"). by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by auto.
       iApply step_fupd_intro; first solve_ndisj. by iFrame.
   Qed.

theories/typing/lib/rc/rc.v

@@ -171,13 +171,13 @@ Section rc.
       iMod ("Hclose2" with "[] Hrctok") as "[HX $]".
       { unfold X. iIntros "!> [??] !>". iNext. iRight. do 3 iExists _.
         iFrame "#∗". }
-      iAssert C with "[>HX]" as "#$".
+      iAssert C with "[>HX]" as "#?".
       { iExists _, _, _. iFrame "Hpersist".
         iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
         iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
         { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
         iApply (bor_na with "Hrc"); solve_ndisj. }
-      iApply ("Hclose1" with "[]"). by auto.
+      iFrame "#". iApply ("Hclose1" with "[]"). by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by auto.
       iApply step_fupd_intro; first solve_ndisj. by iFrame.
   Qed.

theories/typing/lib/rc/weak.v

@@ -413,14 +413,14 @@ Section code.
       - iExists _. iDestruct "Hrcst" as "[Hlw >$]". iRight.
         iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
         iExists _. iFrame. simpl.
-        by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+        rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. iFrame.
       - iExists _. iDestruct "Hrcst" as "(>Hlw & >$ & >H† & >H)". destruct weakc.
         + iLeft. iSplitR; first done. iMod ("Hclose" with "[$Hna Hrc●]") as "$".
           { iExists _. iFrame. }
           rewrite Hszeq. auto with iFrame.
         + iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
           iFrame. iExists _. iFrame.
-          by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. }
+          rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. iFrame. }
     - subst. wp_read. wp_let. wp_op. wp_if.
       iApply (type_type _ _ _ [ w ◁ box (uninit 1); #lw ◁ box (uninit (2 + ty.(ty_size))) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.

theories/typing/sum.v

@@ -208,7 +208,7 @@ Section sum.
       + iIntros "Htl H". iDestruct "H" as (i') "[>Hown1 HownC1]".
         iDestruct ("Htlclose" with "Htl") as "Htl".
         iDestruct (heap_mapsto_agree with "[Hown1 Hown2]") as "#Heq".
-        { iDestruct "Hown1" as "[$ _]". iDestruct "Hown2" as "[$ _]". }
+        { iDestruct "Hown1" as "[$ _]". by iDestruct "Hown2" as "[$ _]". }
         iDestruct "Heq" as %[= ->%Z_of_nat_inj].
         iMod ("Hclose'" with "Htl [$HownC1 $HownC2]") as "[$ ?]".
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.

theories/typing/util.v

@@ -41,8 +41,8 @@ Section util.
     - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
       { rewrite bor_unfold_idx. eauto. }
       iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
-      iApply "Hclose". auto.
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#? $]"; first solve_ndisj.
+      iFrame "#". iApply "Hclose". auto.
     - iMod fupd_intro_mask' as "Hclose'"; first solve_ndisj. iModIntro.
       iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.