diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py
index de38705e6def683844afd4bee6bf5f855b81c506..926b06ff0982cfe695dcf524e67f8d99616522c9 100755
--- a/benchmark/gitlab-extract.py
+++ b/benchmark/gitlab-extract.py
@@ -114,5 +114,5 @@ for commit in parse_log.parse_git_commits(args.commits):
             found_build = True
             print(" success")
             break
-    if not found_build:
+    if not found_build and not BREAK:
         print(" found no succeessful build")
diff --git a/ci b/ci
index d2edcd474159cc883d09c0a08dbd463c2d2780df..39c267a40904232496986518530eea6169fb8168 160000
--- a/ci
+++ b/ci
@@ -1 +1 @@
-Subproject commit d2edcd474159cc883d09c0a08dbd463c2d2780df
+Subproject commit 39c267a40904232496986518530eea6169fb8168
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 6235d121511b3ab21a1d910d6502aac828ae9614..9ee7222369e9d9f8d77cd8a79466a2812cb3fec1 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -38,9 +38,9 @@ Section proofs.
   Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
   Proof. rewrite /cinv; apply _. Qed.
 
-  Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
+  Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
   Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
-  Global Instance cinv_own_as_fractionnal γ q :
+  Global Instance cinv_own_as_fractional γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. split. done. apply _. Qed.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 37d03155767548ae08db44de84aef7a75a7a057e..7975845aa6c9c03876df8f770dff3a613103d2ec 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -94,6 +94,19 @@ Proof.
   iApply "HP'". iFrame.
 Qed.
 
+Lemma inv_open_strong E N P :
+  ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True.
+Proof.
+  iIntros (?) "Hinv".
+  iPoseProof (inv_open (↑ N) N P with "Hinv") as "H"; first done.
+  rewrite difference_diag_L.
+  iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
+  rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
+  iIntros (E') "HP". iSpecialize ("H" with "HP").
+  iPoseProof (fupd_mask_frame_r _ _ E' with "H") as "H"; first set_solver.
+  by rewrite left_id_L.
+Qed.
+
 Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance elim_inv_inv E N P Q Q' :
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 593bc540b0d161a8b3c0b01d6d1ee88a0aae843f..15bf8ab76e12c994f29a6121adb40b1e3421c2cd 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -158,6 +158,28 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
+  Lemma big_sepL_delete Φ l i x :
+    l !! i = Some x →
+    ([∗ list] k↦y ∈ l, Φ k y)
+    ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, if decide (k = i) then emp else Φ k y.
+  Proof.
+    intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
+    rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite decide_True // left_id.
+    rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
+    - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
+      rewrite take_length in Hk. by rewrite decide_False; last lia.
+    - apply big_sepL_proper=> k y _. by rewrite decide_False; last lia.
+  Qed.
+
+  Lemma big_sepL_delete' `{!BiAffine PROP} Φ l i x :
+    l !! i = Some x →
+    ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y.
+  Proof.
+    intros. rewrite big_sepL_delete //. (do 2 f_equiv)=> k y.
+    rewrite -decide_emp. by repeat case_decide.
+  Qed.
+
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.