perf: use a small dequeue in freeing objects

This PR fixes several issues in `Init.Data.String`, most of them typos.

We also move the remaining material out of `Init.Data.String.Lemmas` to
`Init.Data.String.Lemmas.StringOrder`, which shortens the pole.

.claude/commands/release.md

@@ -157,16 +157,6 @@ Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail)
 fail while others are still running, `--watch` will continue until everything settles, then exit
 with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
 
-## Mathlib Bump Branches
-
-Mathlib `bump/v4.X.0` branches live on the **fork** `leanprover-community/mathlib4-nightly-testing`,
-NOT on `leanprover-community/mathlib4`.
-
-## Never Force-Update Remote Refs Without Confirmation
-
-Never force-update an existing remote branch or tag via `git push --force` or the GitHub API
-without explicit user confirmation.
-
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

src/Init/Data/Ord/String.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.Order.Ord
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas
-import Init.Data.String.Lemmas
+import Init.Data.String.Lemmas.StringOrder
 
 public section
 

src/Init/Data/String/Iter/Intercalate.lean

@@ -17,6 +17,7 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
+@[inline]
 public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)

src/Init/Data/String/Lemmas.lean

@@ -20,49 +20,4 @@ public import Init.Data.String.Lemmas.Intercalate
 public import Init.Data.String.Lemmas.Iter
 public import Init.Data.String.Lemmas.Hashable
 public import Init.Data.String.Lemmas.TakeDrop
-import Init.Data.Order.Lemmas
-public import Init.Data.String.Basic
-import Init.Data.Char.Lemmas
-import Init.Data.Char.Order
-import Init.Data.List.Lex
-
-public section
-
-open Std
-
-namespace String
-
-@[deprecated toList_inj (since := "2025-10-30")]
-protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.toList = b.toList :=
-  h ▸ rfl
-@[deprecated toList_inj (since := "2025-10-30")]
-protected theorem ne_of_data_ne {a b : String} (h : a.toList ≠ b.toList) : a ≠ b := by
-  simpa [← toList_inj]
-
-@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
-@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
-@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
-@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
-
-attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
-
-protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
-protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
-protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
-protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
-protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
-protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
-  have := String.lt_irrefl a
-  intro h; subst h; contradiction
-
-instance instIsLinearOrder : IsLinearOrder String := by
-  apply IsLinearOrder.of_le
-  case le_antisymm => constructor; apply String.le_antisymm
-  case le_trans => constructor; apply String.le_trans
-  case le_total => constructor; apply String.le_total
-
-instance : LawfulOrderLT String where
-  lt_iff a b := by
-    simp [← String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
-
-end String
+public import Init.Data.String.Lemmas.StringOrder

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -40,7 +40,7 @@ framework.
 /--
 This data-carrying typeclass is used to give semantics to a pattern type that implements
 {name}`ForwardPattern` and/or {name}`ToForwardSearcher` by providing an abstract, not necessarily
-decidable {name}`PatternModel.Matches` predicate that implementates of {name}`ForwardPattern`
+decidable {name}`PatternModel.Matches` predicate that implementations of {name}`ForwardPattern`
 and {name}`ToForwardSearcher` can be validated against.
 
 Correctness results for generic functions relying on the pattern infrastructure, for example the
@@ -151,7 +151,7 @@ theorem IsLongestMatch.le_of_isMatch {pat : ρ} [PatternModel pat] {s : Slice} {
 
 /--
 Predicate stating that the region between the start of the slice {name}`s` and the position
-{name}`pos` matches the patten {name}`pat`, and that there is no longer match starting at the
+{name}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
 beginning of the slice. This is what a correct matcher should match.
 
 In some cases, being a match and being a longest match will coincide, see
@@ -228,7 +228,7 @@ theorem isLongestRevMatch_iff_isRevMatch {ρ : Type} (pat : ρ) [PatternModel pa
   exact ht₅ (NoSuffixPatternModel.eq_empty _ _ ht₂ (ht₅'' ▸ ht₂'))
 
 /--
-Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match
+Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains a match
 of {name}`pat` in {name}`s` and it is longest among matches starting at {name}`startPos`.
 -/
 structure IsLongestMatchAt (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
@@ -411,7 +411,7 @@ theorem not_revMatchesAt_startPos {pat : ρ} [PatternModel pat] {s : Slice} :
   intro h
   simpa [← Pos.ofSliceTo_inj] using h.ne_endPos
 
-theorem revMatchesAt_iff_revMatchesAt_ofSliceto {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
+theorem revMatchesAt_iff_revMatchesAt_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
     {pos : (s.sliceTo base).Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat (Pos.ofSliceTo pos) := by
   simp only [revMatchesAt_iff_exists_isLongestRevMatchAt]
   constructor
@@ -505,8 +505,8 @@ theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ}
 /--
 Predicate stating compatibility between {name}`PatternModel` and {name}`BackwardPattern`.
 
-This extends {name}`LawfulForwardPattern`, but it is much stronger because it forces the
-{name}`ForwardPattern` to match the longest prefix of the given slice that matches the property
+This extends {name}`LawfulBackwardPattern`, but it is much stronger because it forces the
+{name}`BackwardPattern` to match the longest prefix of the given slice that matches the property
 supplied by the {name}`PatternModel` instance.
 -/
 class LawfulBackwardPatternModel {ρ : Type} (pat : ρ) [BackwardPattern pat]

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Pred.lean

@@ -65,7 +65,7 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slic
     s.startsWith P = s.copy.toList.head?.any (decide <| P ·) := by
   simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_head?]
 
-theorem eq_append_of_dropPrefix_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
+theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
     ∃ c, s.copy = singleton c ++ res.copy ∧ P c := by
   rw [dropPrefix?_prop_eq_dropPrefix?_decide] at h
   simpa using eq_append_of_dropPrefix?_bool_eq_some h
@@ -162,7 +162,7 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Stri
 theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice}
     (h : s.dropPrefix? P = some res) : ∃ c, s = singleton c ++ res.copy ∧ P c := by
   rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
-  simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
+  simpa using Slice.eq_append_of_dropPrefix?_prop_eq_some h
 
 theorem skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
     s.skipSuffix? p = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) = true := by

src/Init/Data/String/Lemmas/StringOrder.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+public import Init.Data.Order.Classes
+import Init.Data.List.Lex
+import Init.Data.Char.Lemmas
+import Init.Data.Char.Order
+import Init.Data.Order.Factories
+import Init.Data.Order.Lemmas
+
+public section
+
+open Std
+
+namespace String
+
+@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
+@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
+@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
+@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
+
+attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
+
+protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
+protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
+protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
+protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
+protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
+protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
+  have := String.lt_irrefl a
+  intro h; subst h; contradiction
+
+instance instIsLinearOrder : IsLinearOrder String := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply String.le_antisymm
+  case le_trans => constructor; apply String.le_trans
+  case le_total => constructor; apply String.le_total
+
+instance : LawfulOrderLT String where
+  lt_iff a b := by
+    simp [← String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
+
+end String

src/Init/Data/String/Slice.lean

@@ -706,14 +706,14 @@ Returns {name}`none` otherwise.
 This function is generic over all currently supported patterns.
 -/
 @[inline]
-def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
-  ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom
+def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
+  ((s.sliceFrom pos).skipSuffix? pat).map Pos.ofSliceFrom
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
 Use {name (scope := "Init.Data.String.Slice")}`String.Slice.dropSuffix` to return the slice
-unchanged when {name}`pat` does not match a prefix.
+unchanged when {name}`pat` does not match a suffix.
 
 This function is generic over all currently supported patterns.
 
@@ -775,7 +775,7 @@ def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat]
 termination_by pos.down
 
 /--
-Returns the position a the start of the longest suffix of {name}`s` for which {name}`pat` matches
+Returns the position at the start of the longest suffix of {name}`s` for which {name}`pat` matches
 (potentially repeatedly).
 -/
 @[inline]

src/Init/Data/String/TakeDrop.lean

@@ -314,7 +314,7 @@ Returns {name}`none` otherwise.
 This function is generic over all currently supported patterns.
 -/
 @[inline]
-def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
   (pos.toSlice.revSkip? pat).map Pos.ofToSlice
 
 /--
@@ -461,7 +461,7 @@ def dropPrefix? (s : String) (pat : ρ) [ForwardPattern pat] : Option String.Sli
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
 Use {name (scope := "Init.Data.String.TakeDrop")}`String.dropSuffix` to return the slice
-unchanged when {name}`pat` does not match a prefix.
+unchanged when {name}`pat` does not match a suffix.
 
 This is a cheap operation because it does not allocate a new string to hold the result.
 To convert the result into a string, use {name}`String.Slice.copy`.

src/Init/Omega/LinearCombo.lean

@@ -36,9 +36,6 @@ private local instance : ToString Int where
 private local instance : Repr Int where
   reprPrec i prec := if i < 0 then Repr.addAppParen (toString i) prec else toString i
 
-private local instance : Append String where
-  append := String.Internal.append
-
 /-- Internal representation of a linear combination of atoms, and a constant term. -/
 structure LinearCombo where
   /-- Constant term. -/

src/Lean/Data/Trie.lean

@@ -60,7 +60,7 @@ instance : EmptyCollection (Trie α) :=
 instance : Inhabited (Trie α) where
   default := empty
 
-/-- Insert or update the value at a the given key `s`.  -/
+/-- Insert or update the value at the given key `s`.  -/
 partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :=
   let rec insertEmpty (i : Nat) : Trie α :=
     if h : i < s.utf8ByteSize then
@@ -100,7 +100,7 @@ partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :
         node (f v) cs ts
   loop 0 t
 
-/-- Inserts a value at a the given key `s`, overriding an existing value if present. -/
+/-- Inserts a value at the given key `s`, overriding an existing value if present. -/
 partial def insert (t : Trie α) (s : String) (val : α) : Trie α :=
   upsert t s (fun _ => val)
 

src/Std/Data/String/ToInt.lean

@@ -183,7 +183,8 @@ public theorem toInt?_repr (a : Int) : a.repr.toInt? = some a := by
   rw [repr_eq_if]
   split <;> (simp; omega)
 
-public theorem isInt?_repr (a : Int) : a.repr.isInt = true := by
+@[simp]
+public theorem isInt_repr (a : Int) : a.repr.isInt = true := by
   simp [← String.isSome_toInt?]
 
 public theorem repr_injective {a b : Int} (h : Int.repr a = Int.repr b) : a = b := by

src/Std/Time/Internal/Bounded.lean

@@ -239,7 +239,7 @@ def ofFin' {lo : Nat} (fin : Fin (Nat.succ hi)) (h : lo ≤ hi) : Bounded.LE lo
     else ofNat' lo (And.intro (Nat.le_refl lo) h)
 
 /--
-Creates a new `Bounded.LE` using a the modulus of a number.
+Creates a new `Bounded.LE` using the modulus of a number.
 -/
 @[inline]
 def byEmod (b : Int) (i : Int) (hi : i > 0) : Bounded.LE 0 (i - 1) := by
@@ -252,7 +252,7 @@ def byEmod (b : Int) (i : Int) (hi : i > 0) : Bounded.LE 0 (i - 1) := by
     exact Int.emod_lt_of_pos b hi
 
 /--
-Creates a new `Bounded.LE` using a the Truncating modulus of a number.
+Creates a new `Bounded.LE` using the Truncating modulus of a number.
 -/
 @[inline]
 def byMod (b : Int) (i : Int) (hi : 0 < i) : Bounded.LE (- (i - 1)) (i - 1) := by

src/runtime/object.cpp

@@ -415,17 +415,128 @@ static void lean_del_core(object * o, object * & todo) {
     }
 }
 
+// Adaptive deque for lean_dec_ref_cold.
+// Uses a small stack-allocated circular buffer processed in FIFO (BFS) order
+// for better cache locality when freeing wide structures (arrays, multi-field
+// constructors). When the buffer is full, excess objects overflow to the
+// existing in-object linked list (DFS order).
+#define LEAN_DEC_DEQUE_CAP 32u
+#define LEAN_DEC_DEQUE_MASK (LEAN_DEC_DEQUE_CAP - 1u)
+
+struct lean_del_deque {
+    lean_object * buf[LEAN_DEC_DEQUE_CAP];
+    unsigned head;
+    unsigned tail;
+    lean_object * overflow;
+};
+
+static inline void deque_enqueue(lean_del_deque & dq, lean_object * o) {
+    unsigned next_tail = (dq.tail + 1) & LEAN_DEC_DEQUE_MASK;
+    if (LEAN_LIKELY(next_tail != dq.head)) {
+        dq.buf[dq.tail] = o;
+        dq.tail = next_tail;
+    } else {
+        push_back(dq.overflow, o);
+    }
+}
+
+static inline lean_object * deque_pop(lean_del_deque & dq) {
+    if (LEAN_LIKELY(dq.head != dq.tail)) {
+        lean_object * r = dq.buf[dq.head];
+        dq.head = (dq.head + 1) & LEAN_DEC_DEQUE_MASK;
+        return r;
+    }
+    return pop_back(dq.overflow);
+}
+
+static inline bool deque_empty(lean_del_deque const & dq) {
+    return dq.head == dq.tail && dq.overflow == nullptr;
+}
+
+static inline void dec_deque(lean_object * o, lean_del_deque & dq) {
+    if (lean_is_scalar(o))
+        return;
+    if (LEAN_LIKELY(o->m_rc > 1)) {
+        o->m_rc--;
+    } else if (o->m_rc == 1) {
+        deque_enqueue(dq, o);
+    } else if (o->m_rc == 0) {
+        return;
+    } else if (std::atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_acq_rel) == -1) {
+        deque_enqueue(dq, o);
+    }
+}
+
+static void lean_del_core_deque(object * o, lean_del_deque & dq) {
+    uint8 tag = lean_ptr_tag(o);
+    if (tag <= LeanMaxCtorTag) {
+        object ** it  = lean_ctor_obj_cptr(o);
+        object ** end = it + lean_ctor_num_objs(o);
+        for (; it != end; ++it) dec_deque(*it, dq);
+        lean_free_small_object(o);
+    } else {
+        switch (tag) {
+        case LeanClosure: {
+            object ** it  = lean_closure_arg_cptr(o);
+            object ** end = it + lean_closure_num_fixed(o);
+            for (; it != end; ++it) dec_deque(*it, dq);
+            lean_dealloc(o, lean_closure_byte_size(o));
+            break;
+        }
+        case LeanArray: {
+            object ** it  = lean_array_cptr(o);
+            object ** end = it + lean_array_size(o);
+            for (; it != end; ++it) dec_deque(*it, dq);
+            lean_dealloc(o, lean_array_byte_size(o));
+            break;
+        }
+        case LeanScalarArray:
+            lean_dealloc(o, lean_sarray_byte_size(o));
+            break;
+        case LeanString:
+            lean_dealloc(o, lean_string_byte_size(o));
+            break;
+        case LeanMPZ:
+            to_mpz(o)->m_value.~mpz();
+            lean_free_small_object(o);
+            break;
+        case LeanThunk:
+            if (object * c = lean_to_thunk(o)->m_closure) dec_deque(c, dq);
+            if (object * v = lean_to_thunk(o)->m_value) dec_deque(v, dq);
+            lean_free_small_object(o);
+            break;
+        case LeanRef:
+            if (object * v = lean_to_ref(o)->m_value) dec_deque(v, dq);
+            lean_free_small_object(o);
+            break;
+        case LeanTask:
+            deactivate_task(lean_to_task(o));
+            break;
+        case LeanPromise:
+            deactivate_promise(lean_to_promise(o));
+            break;
+        case LeanExternal:
+            lean_to_external(o)->m_class->m_finalize(lean_to_external(o)->m_data);
+            lean_free_small_object(o);
+            break;
+        default:
+            lean_unreachable();
+        }
+    }
+}
+
 extern "C" LEAN_EXPORT void lean_dec_ref_cold(lean_object * o) {
     if (o->m_rc == 1 || std::atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_acq_rel) == -1) {
 #ifdef LEAN_LAZY_RC
         push_back(g_to_free, o);
 #else
-        object * todo = nullptr;
-        while (true) {
-            lean_del_core(o, todo);
-            if (todo == nullptr)
-                return;
-            o = pop_back(todo);
+        lean_del_deque dq;
+        dq.head = 0;
+        dq.tail = 0;
+        dq.overflow = nullptr;
+        deque_enqueue(dq, o);
+        while (!deque_empty(dq)) {
+            lean_del_core_deque(deque_pop(dq), dq);
         }
 #endif
     }