chore: generalize definition of extrinsicFix further to make a point

This reverts commit 2198b357f6.

CMakeLists.txt

@@ -129,6 +129,7 @@ if(USE_MIMALLOC)
     # cadical, it might be worth reorganizing the directory structure.
     SOURCE_DIR
     "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
+    EXCLUDE_FROM_ALL
   )
   FetchContent_MakeAvailable(mimalloc)
 endif()

src/CMakeLists.txt

@@ -110,6 +110,7 @@ option(RUNTIME_STATS "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
 option(USE_MIMALLOC "use mimalloc" ON)
+set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations (https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60)")
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
@@ -117,6 +118,7 @@ option(USE_LAKE "Use Lake instead of lean.mk for building core libs from languag
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
 set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_LAKE_OPTS "" CACHE STRING "extra options to lake")
 set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
@@ -126,7 +128,7 @@ string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
 # option used by the CI to fail on warnings
 option(WFAIL "Fail build if warnings are emitted by Lean" ON)
 if(WFAIL MATCHES "ON")
-  string(APPEND LAKE_EXTRA_ARGS " --wfail")
+  string(APPEND LEAN_EXTRA_LAKE_OPTS " --wfail")
   string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 

src/Init/Data/Array/QSort/Basic.lean

@@ -33,6 +33,7 @@ if necessary so that the middle (pivot) element is at index `hi`.
 We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
 swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
+@[inline]
 def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega)
     (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m ≤ hi} × Vector α n :=
   let mid := (lo + hi) / 2
@@ -44,7 +45,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
   -- elements in `[i, k)` are greater than or equal to `pivot`,
   -- elements in `[k, hi)` are unexamined,
   -- while `as[hi]` is (by definition) the pivot.
-  let rec loop (as : Vector α n) (i k : Nat)
+  let rec @[specialize] loop (as : Vector α n) (i k : Nat)
       (ilo : lo ≤ i := by omega) (ik : i ≤ k := by omega) (w : k ≤ hi := by omega) :=
     if h : k < hi then
       if lt as[k] pivot then

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

@@ -909,7 +909,7 @@ theorem Slice.Pos.skipWhile_copy {ρ : Type} {pat : ρ} [ForwardPattern pat] [Pa
   simp
 
 @[simp]
-theorem Pos.skipWhile_le {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
+theorem Pos.le_skipWhile {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
     [LawfulForwardPatternModel pat] {s : String} {pos : s.Pos} : pos ≤ pos.skipWhile pat := by
   simp [skipWhile_eq_skipWhile_toSlice, Pos.le_ofToSlice_iff]
 

src/Init/Internal/Order.lean

@@ -7,5 +7,7 @@ module
 
 prelude
 public import Init.Internal.Order.Basic
+public import Init.Internal.Order.ExtrinsicFix
 public import Init.Internal.Order.Lemmas
+public import Init.Internal.Order.MonadTail
 public import Init.Internal.Order.Tactic

src/Init/Internal/Order/ExtrinsicFix.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf, Robin Arnez
+-/
+module
+
+prelude
+public import Init.Internal.Order.Basic
+public import Init.Internal.Order.MonadTail
+import Init.Classical
+
+set_option linter.missingDocs true
+
+/-!
+This module provides a fixpoint combinator that combines advantages of `partial` and
+`partial_fixpoint` recursion.
+
+The combinator is similar to {lean}`CCPO.fix`, but does not require a CCPO instance or
+monotonicity proof at the definition site. Therefore, it can be used in situations in which
+these constraints are unavailable (e.g., when the monad does not have a `MonadTail` instance).
+Given a CCPO and monotonicity proof, there are theorems guaranteeing that it equals
+{lean}`CCPO.fix` and satisfies fixpoint induction.
+-/
+
+public section
+
+namespace Lean.Order
+
+/--
+The function implemented as the loop {lean}`opaqueFix f = f (opaqueFix f)`.
+{lean}`opaqueFix f` is the fixpoint of {name}`f`, as long as `f` is monotone with respect to
+some CCPO on `α`.
+
+The loop might run forever depending on {name}`f`. It is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+@[specialize]
+partial def opaqueFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
+  f (opaqueFix f)
+
+/-
+SAFE assuming that the code generated by iteration over `f` is equivalent to the CCPO
+fixpoint of `f` if there exists a CCPO making `f` monotone.
+-/
+open _root_.Classical in
+/--
+A fixpoint combinator that can be used to construct recursive definitions with an *extrinsic*
+proof of monotonicity.
+
+Given a fixpoint functional {name}`f`, {lean}`extrinsicFix f` is the recursive function obtained
+by having {name}`f` call itself recursively.
+
+If there is no CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` might run forever.
+In this case, nothing interesting can be proved about the result; it is opaque.
+
+If there _is_ a CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` is equivalent to
+{lean}`CCPO.fix f`, logically and regarding its termination behavior.
+-/
+@[cbv_opaque, implemented_by opaqueFix]
+def extrinsicFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
+  if h : ∃ x, x = f x then
+    h.choose
+  else
+    -- Return `opaqueFix f` so that `implemented_by opaqueFix` is sound.
+    -- In effect, `extrinsicFix` is opaque if no fixpoint exists.
+    opaqueFix f
+
+/--
+A fixpoint combinator that allows for deferred proofs of monotonicity.
+
+{lean}`extrinsicFix f` is a function implemented as the loop
+{lean}`extrinsicFix f = f (extrinsicFix f)`.
+
+If there is a CCPO making `f` monotone, {name}`extrinsicFix_eq` proves that it satisfies the
+fixpoint equation, and {name}`extrinsicFix_induct` enables fixpoint induction.
+Otherwise, {lean}`extrinsicFix f` is opaque, i.e., it is impossible to prove nontrivial
+properties about it.
+-/
+add_decl_doc extrinsicFix
+
+/-- Every CCPO has at least one element (the bottom element). -/
+noncomputable local instance CCPO.instNonempty [CCPO α] : Nonempty α := ⟨bot⟩
+
+/--
+The fixpoint equation for `extrinsicFix`: given a proof that the fixpoint exists, unfold
+`extrinsicFix`.
+-/
+theorem extrinsicFix_eq {f : α → α}
+    (x : α) (h : x = f x) :
+    letI : Nonempty α := ⟨x⟩; extrinsicFix f = f (extrinsicFix f) := by
+  letI : Nonempty α := ⟨x⟩
+  have h : ∃ x, x = f x := ⟨x, h⟩
+  simp only [extrinsicFix, dif_pos h]
+  exact h.choose_spec
+
+/--
+The fixpoint equation for `extrinsicFix`: given a CCPO instance and monotonicity of `f`,
+{lean}`extrinsicFix f = f (extrinsicFix f)`.
+-/
+theorem extrinsicFix_eq_mono [inst : CCPO α] {f : α → α}
+    (hf : monotone f) :
+    extrinsicFix f = f (extrinsicFix f) :=
+  extrinsicFix_eq (fix f hf) (fix_eq hf)
+
+abbrev discardR {C : α → Sort _} {R : α → α → Prop}
+    (f : ∀ a, (∀ a', R a' a → C a') → C a) : ((∀ a, C a) → (∀ a, C a)) :=
+  fun rec a => f a (fun a _ => rec a)
+
+theorem extrinsicFix_eq_wf {C : α → Sort _} [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {f : ∀ a, (∀ a', R a' a → C a') → C a} (h : WellFounded R) {a : α} :
+    extrinsicFix (discardR f) a = f a (fun a _ => extrinsicFix (discardR f) a) := by
+  suffices extrinsicFix (discardR f) = fun a => f a (fun a _ => extrinsicFix (discardR f) a) by
+    conv => lhs; rw [this]
+  apply extrinsicFix_eq (fun a => WellFounded.fix h f a) (funext fun a => (WellFounded.fix_eq h f a))
+
+end Lean.Order

src/Init/Internal/Order/MonadTail.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Internal.Order.Basic
+import all Init.System.ST  -- for EST.bind in MonadTail instance
+
+set_option linter.missingDocs true
+
+public section
+
+namespace Lean.Order
+
+/--
+A *tail monad* is a monad whose bind operation preserves any suitable ordering of the continuation.
+Specifically, `MonadTail m` asserts that every `m β` carries a chain-complete partial order (CCPO)
+and that `>>=` is monotone in its second (continuation) argument with respect to that order.
+
+This is a weaker requirement than `MonoBind`, which requires monotonicity in both arguments.
+`MonadTail` is sufficient for `partial_fixpoint`-based recursive definitions where the
+recursive call only appears in the continuation (second argument) of `>>=`.
+-/
+class MonadTail (m : Type u → Type v) [Bind m] where
+  /-- Every `m β` with `Nonempty β` has a chain-complete partial order. -/
+  instCCPO β [Nonempty β] : CCPO (m β)
+  /-- Bind is monotone in the second (continuation) argument. -/
+  bind_mono_right {a : m α} {f₁ f₂ : α → m β} [Nonempty β] (h : ∀ x, f₁ x ⊑ f₂ x) :
+    a >>= f₁ ⊑ a >>= f₂
+
+attribute [implicit_reducible] MonadTail.instCCPO
+attribute [instance] MonadTail.instCCPO
+
+@[scoped partial_fixpoint_monotone]
+theorem MonadTail.monotone_bind_right
+    (m : Type u → Type v) [Monad m] [MonadTail m]
+    {α β : Type u} [Nonempty β]
+    {γ : Sort w} [PartialOrder γ]
+    (f : m α) (g : γ → α → m β)
+    (hmono : monotone g) :
+    monotone (fun (x : γ) => f >>= g x) :=
+  fun _ _ h => MonadTail.bind_mono_right (hmono _ _ h)
+
+instance : MonadTail Id where
+  instCCPO _ := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
+  bind_mono_right h := h _
+
+instance {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] [Nonempty σ] :
+    MonadTail (StateT σ m) where
+  instCCPO α := inferInstanceAs (CCPO (σ → m (α × σ)))
+  bind_mono_right h := by
+    intro s
+    show StateT.bind _ _ s ⊑ StateT.bind _ _ s
+    simp only [StateT.bind]
+    apply MonadTail.bind_mono_right (m := m)
+    intro ⟨x, s'⟩
+    exact h x s'
+
+instance {ε : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (ExceptT ε m) where
+  instCCPO β := MonadTail.instCCPO (Except ε β)
+  bind_mono_right h := by
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    cases x with
+    | error => exact PartialOrder.rel_refl
+    | ok a => exact h a
+
+instance : MonadTail (Except ε) where
+  instCCPO β := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
+  bind_mono_right h := by
+    cases ‹Except _ _› with
+    | error => exact FlatOrder.rel.refl
+    | ok a => exact h a
+
+instance {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (OptionT m) where
+  instCCPO β := MonadTail.instCCPO (Option β)
+  bind_mono_right h := by
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    cases x with
+    | none => exact PartialOrder.rel_refl
+    | some a => exact h a
+
+instance : MonadTail Option where
+  instCCPO _ := inferInstance
+  bind_mono_right h := MonoBind.bind_mono_right h
+
+instance {ρ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (ReaderT ρ m) where
+  instCCPO α := inferInstanceAs (CCPO (ρ → m α))
+  bind_mono_right h := by
+    intro r
+    show ReaderT.bind _ _ r ⊑ ReaderT.bind _ _ r
+    simp only [ReaderT.bind]
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    exact h x r
+
+set_option linter.missingDocs false in
+noncomputable def ST.bot' [Nonempty α] (s : Void σ) : @FlatOrder (ST.Out σ α) (.mk Classical.ofNonempty (Classical.choice ⟨s⟩)) :=
+  .mk Classical.ofNonempty (Classical.choice ⟨s⟩)
+
+instance [Nonempty α] : CCPO (ST σ α) where
+  rel := PartialOrder.rel (α := ∀ s, FlatOrder (ST.bot' s))
+  rel_refl := PartialOrder.rel_refl
+  rel_antisymm := PartialOrder.rel_antisymm
+  rel_trans := PartialOrder.rel_trans
+  has_csup hchain := CCPO.has_csup (α := ∀ s, FlatOrder (ST.bot' s)) hchain
+
+instance : MonadTail (ST σ) where
+  instCCPO _ := inferInstance
+  bind_mono_right {_ _ a f₁ f₂} _ h := by
+    intro w
+    change FlatOrder.rel (ST.bind a f₁ w) (ST.bind a f₂ w)
+    simp only [ST.bind]
+    apply h
+
+instance : MonadTail BaseIO :=
+  inferInstanceAs (MonadTail (ST IO.RealWorld))
+
+instance [Nonempty ε] : MonadTail (EST ε σ) where
+  instCCPO _ := inferInstance
+  bind_mono_right h := MonoBind.bind_mono_right h
+
+instance [Nonempty ε] : MonadTail (EIO ε) :=
+  inferInstanceAs (MonadTail (EST ε IO.RealWorld))
+
+instance : MonadTail IO :=
+  inferInstanceAs (MonadTail (EIO IO.Error))
+
+instance {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [MonadTail m] :
+    MonadTail (StateRefT' ω σ m) :=
+  inferInstanceAs (MonadTail (ReaderT (ST.Ref ω σ) m))
+
+end Lean.Order

src/Init/While.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Core
+public import Init.Internal.Order.ExtrinsicFix
 
 public section
 
@@ -21,18 +22,38 @@ namespace Lean
 inductive Loop where
   | mk
 
+open Lean.Order in
 @[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop (b : β) : m β := do
+def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m]
+    (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  haveI : Nonempty (β → m β) := ⟨fun b => pure b⟩
+  Lean.Order.extrinsicFix (fun (cont : β → m β) (b : β) => do
     match ← f () b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop b
-  loop init
+    | .done val => pure val
+    | .yield val => cont val) init
 
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-syntax "repeat " doSeq : doElem
+open Lean.Order in
+theorem Loop.forIn_eq [Monad m] [MonadTail m]
+    {l : Loop} {b : β} {f : Unit → β → m (ForInStep β)} :
+    Loop.forIn l b f = (do
+      match ← f () b with
+      | .done val => pure val
+      | .yield val => Loop.forIn l val f) := by
+  haveI : Nonempty β := ⟨b⟩
+  simp only [Loop.forIn]
+  apply congrFun
+  apply extrinsicFix_eq
+  intro cont₁ cont₂ h b'
+  apply MonadTail.bind_mono_right
+  intro r
+  cases r with
+  | done => exact PartialOrder.rel_refl
+  | yield val => exact h val
+
+syntax (name := doRepeat) "repeat " doSeq : doElem
 
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)

src/Lean/Elab/BuiltinDo/For.lean

@@ -153,6 +153,9 @@ open Lean.Meta
 
   let body ←
     withLocalDeclsD xh fun xh => do
+    Term.addLocalVarInfo x xh[0]!
+    if let some h := h? then
+      Term.addLocalVarInfo h xh[1]!
     withLocalDecl s .default σ (kind := .implDetail) fun loopS => do
     mkLambdaFVars (xh.push loopS) <| ← do
     bindMutVarsFromTuple loopMutVarNames loopS.fvarId! do

src/Lean/Elab/Deriving/Inhabited.lean

@@ -89,7 +89,7 @@ where
       let val ←
         if isStructure (← getEnv) inductiveTypeName then
           withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
-            let stx ← `(structInst| {..})
+            let stx ← `(structInstDefault| struct_inst_default%)
             withoutErrToSorry <| elabTermAndSynthesize stx type
         else
           withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do

src/Lean/Elab/Do/Basic.lean

@@ -384,6 +384,7 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
   let k := dec.k
   -- The .ofBinderName below is mainly to interpret `__do_lift` binders as implementation details.
   let declKind := .ofBinderName x
+  let kResultTy ← mkFreshResultType `kResultTy
   withLocalDecl x .default eResultTy (kind := declKind) fun xFVar => do
     let body ← k
     let body' := body.consumeMData
@@ -411,7 +412,6 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
         -- else -- would be too aggressive
         --   return ← mapLetDecl (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k ref
 
-    let kResultTy ← mkFreshResultType `kResultTy
     let body ← Term.ensureHasType (← mkMonadicType kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
@@ -545,7 +545,10 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
-  discard <| joinRhsMVar.mvarId!.checkedAssign joinRhs
+  unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
+    joinRhsMVar.mvarId!.withContext do
+      throwError "Bug in a `do` elaborator. Failed to assign join point RHS{indentExpr joinRhs}\n\
+        to metavariable\n{joinRhsMVar.mvarId!}"
 
   let body ← body?.getDM do
     -- Here we unconditionally add a pending MVar.

src/Lean/Elab/Do/Legacy.lean

@@ -1782,6 +1782,10 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
+          else if k == `Lean.doRepeat then
+            let seq := doElem[1]
+            let expanded ← `(doElem| for _ in Loop.mk do $seq)
+            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/StructInst.lean

@@ -150,6 +150,8 @@ structure SourcesView where
   explicit : Array ExplicitSourceView
   /-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
   implicit : Option Syntax
+  /-- Use `Inhabited` instances inherited from parent structures, and use `default` instances for missing fields. -/
+  useInhabited : Bool
   deriving Inhabited
 
 /--
@@ -179,7 +181,7 @@ private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
         let structName ← getStructureName srcType
         return { stx, fvar := src, structName }
     let implicit := if implicitSource[0].isNone then none else implicitSource
-    return { explicit, implicit }
+    return { explicit, implicit, useInhabited := false }
 
 /--
 We say a structure instance notation is a "modifyOp" if it contains only a single array update.
@@ -579,6 +581,9 @@ private structure StructInstContext where
   /-- If true, then try using default values or autoParams for missing fields.
   (Considered after `useParentInstanceFields`.) -/
   useDefaults : Bool
+  /-- If true, then tries `Inhabited` instances as an alternative to parent instances,
+  and when default values are missing. -/
+  useInhabited : Bool
   /-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
   Only applies if `useDefaults` is true. -/
   unsynthesizedAsMVars : Bool
@@ -735,14 +740,27 @@ The arguments for the `_default` auxiliary function are provided by `fieldMap`.
 After default values are resolved, then the one that is added to the environment
 as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here.
 -/
-private partial def getFieldDefaultValue? (fieldName : Name) : StructInstM (NameSet × Option Expr) := do
+private def getFieldDefaultValue? (fieldName : Name) : StructInstM (Option (NameSet × Expr)) := do
   let some defFn := getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName
-    | return ({}, none)
+    | return none
   let fieldMap := (← get).fieldMap
   let some (fields, val) ← instantiateStructDefaultValueFn? defFn (← read).levels (← read).params (pure ∘ fieldMap.find?)
     | logError m!"default value for field `{fieldName}` of structure `{.ofConstName (← read).structName}` could not be instantiated, ignoring"
-      return ({}, none)
-  return (fields, val)
+      return none
+  return some (fields, val)
+
+/--
+If `useInhabited` is enabled, tries synthesizing an `Inhabited` instance for the field.
+-/
+private def getFieldDefaultValueUsingInhabited (fieldType : Expr) : StructInstM (Option (NameSet × Expr)) := do
+  if (← read).useInhabited then
+    try
+      let val ← mkDefault fieldType
+      return some ({}, val)
+    catch _ =>
+      return none
+  else
+    return none
 
 /--
 Auxiliary type for `synthDefaultFields`
@@ -751,8 +769,16 @@ private structure PendingField where
   fieldName : Name
   fieldType : Expr
   required : Bool
-  deps : NameSet
-  val? : Option Expr
+  /-- If present, field dependencies and the default value. -/
+  val? : Option (NameSet × Expr)
+
+private def PendingField.isReady (pendingField : PendingField) (hasDep : Name → Bool) : Bool :=
+  pendingField.val?.any fun (deps, _) => deps.all hasDep
+
+private def PendingField.val! (pendingField : PendingField) : Expr :=
+  match pendingField.val? with
+  | some (_, val) => val
+  | none          => panic! "PendingField has no value"
 
 private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
   registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
@@ -786,12 +812,15 @@ private def synthOptParamFields : StructInstM Unit := do
   -- Process default values for pending optParam fields.
   let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do
     if required || (← isFieldNotSolved? fieldName).isSome then
-      let (deps, val?) ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
-      if let some val := val? then
-        trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
-      else
-        trace[Elab.struct] "no default value for {fieldName}"
-      pure <| some { fieldName, fieldType, required, deps, val? }
+      let val? ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure none
+      let val? ← pure val? <||> if (← read).useInhabited then getFieldDefaultValueUsingInhabited fieldType else pure none
+      trace[Elab.struct]
+        if let some (deps, val) := val? then
+          m!"default value for {fieldName}:{inlineExpr val}" ++
+          if deps.isEmpty then m!"" else m!"(depends on fields {deps.toArray})"
+        else
+          m!"no default value for {fieldName}"
+      pure <| some { fieldName, fieldType, required, val? }
     else
       pure none
   -- We then iteratively look for pending fields that do not depend on unsolved-for fields.
@@ -799,12 +828,11 @@ private def synthOptParamFields : StructInstM Unit := do
   -- so we need to keep trying until no more progress is made.
   let mut pendingSet : NameSet := pendingFields.foldl (init := {}) fun set pending => set.insert pending.fieldName
   while !pendingSet.isEmpty do
-    let selectedFields := pendingFields.filter fun pendingField =>
-      pendingField.val?.isSome && pendingField.deps.all (fun dep => !pendingSet.contains dep)
+    let selectedFields := pendingFields.filter (·.isReady (!pendingSet.contains ·))
     let mut toRemove : Array Name := #[]
     let mut assignErrors : Array MessageData := #[]
     for selected in selectedFields do
-      let some selectedVal := selected.val? | unreachable!
+      let selectedVal := selected.val!
       if let some mvarId ← isFieldNotSolved? selected.fieldName then
         let fieldType := selected.fieldType
         let selectedType ← inferType selectedVal
@@ -1084,6 +1112,7 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
         addStructFieldAux fieldName mvar
         return ← loop
   -- Default case: natural metavariable, register it for optParams
+  let fieldType := fieldType.consumeTypeAnnotations
   discard <| addStructFieldMVar fieldName fieldType
   modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
   loop
@@ -1111,29 +1140,44 @@ private partial def loop : StructInstM Expr := withViewRef do
 For each parent class, see if it can be used to synthesize the fields that haven't been provided.
 -/
 private partial def addParentInstanceFields : StructInstM Unit := do
-  let env ← getEnv
   let structName := (← read).structName
-  let fieldNames := getStructureFieldsFlattened env structName (includeSubobjectFields := false)
+  let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
   let fieldViews := (← read).fieldViews
   if fieldNames.all fieldViews.contains then
     -- Every field is accounted for already
     return
 
-  -- We look at class parents in resolution order
+  -- We look at parents in resolution order
   let parents ← getAllParentStructures structName
-  let classParents := parents.filter (isClass env)
-  if classParents.isEmpty then return
+  let env ← getEnv
+  let parentsToVisit := if (← read).useInhabited then parents else parents.filter (isClass env)
+  if parentsToVisit.isEmpty then return
 
   let allowedFields := fieldNames.filter (!fieldViews.contains ·)
   let mut remainingFields := allowedFields
 
   -- Worklist of parent/fields pairs. If fields is empty, then it will be computed later.
-  let mut worklist : List (Name × Array Name) := classParents |>.map (·, #[]) |>.toList
+  let mut worklist : List (Name × Array Name) := parentsToVisit |>.map (·, #[]) |>.toList
   let mut deferred : List (Name × Array Name) := []
 
+  let trySynthParent (parentName : Name) (parentTy : Expr) : StructInstM (LOption Expr) := do
+    if isClass (← getEnv) parentName then
+      match ← trySynthInstance parentTy with
+      | .none => pure ()
+      | r     => return r
+    if (← read).useInhabited then
+      let u ← getLevel parentTy
+      let cls := Expr.app (Expr.const ``Inhabited [u]) parentTy
+      match ← trySynthInstance cls with
+      | .none      => pure ()
+      | .undef     => return .undef
+      | .some inst => return .some <| mkApp2 (Expr.const ``Inhabited.default [u]) parentTy inst
+    return .none
+
   while !worklist.isEmpty do
     let (parentName, parentFields) :: worklist' := worklist | unreachable!
     worklist := worklist'
+    let env ← getEnv
     let parentFields := if parentFields.isEmpty then getStructureFieldsFlattened env parentName (includeSubobjectFields := false) else parentFields
     -- We only try synthesizing if the parent contains one of the remaining fields
     -- and if every parent field is an allowed field.
@@ -1145,7 +1189,7 @@ private partial def addParentInstanceFields : StructInstM Unit := do
         trace[Elab.struct] "could not calculate type for parent `{.ofConstName parentName}`"
         deferred := (parentName, parentFields) :: deferred
       | some (parentTy, _) =>
-        match ← trySynthInstance parentTy with
+        match ← trySynthParent parentName parentTy with
         | .none => trace[Elab.struct] "failed to synthesize instance for parent {parentTy}"
         | .undef =>
           trace[Elab.struct] "instance synthesis stuck for parent {parentTy}"
@@ -1199,17 +1243,19 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
   let fields ← addSourceFields structName s.sources.explicit fields
   trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
   let ellipsis := s.sources.implicit.isSome
+  let useInhabited := s.sources.useInhabited
   let (val, _) ← main
     |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
              -- See the note in `ElabAppArgs.processExplicitArg`
              -- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
              -- so we do not specifically check for it to disable defaults.
              -- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
-             useDefaults := !(← readThe Term.Context).inPattern
+             useDefaults := !(← readThe Term.Context).inPattern || useInhabited
              -- Similarly, for patterns we disable using parent instances to fill in fields
-             useParentInstanceFields := !(← readThe Term.Context).inPattern
+             useParentInstanceFields := !(← readThe Term.Context).inPattern || useInhabited
              -- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
              unsynthesizedAsMVars := ellipsis
+             useInhabited := useInhabited
      }
     |>.run { type := ctorFnType }
   return val
@@ -1333,6 +1379,15 @@ where
       trace[Elab.struct] "result:{indentExpr r}"
       return r
 
+@[builtin_term_elab structInstDefault] def elabStructInstDefault : TermElab := fun stx expectedType? => do
+  let sourcesView : SourcesView := { explicit := #[], implicit := none, useInhabited := true }
+  let (structName, structType?) ← getStructName expectedType? sourcesView
+  withTraceNode `Elab.struct (fun _ => return m!"elaborating default value for `{structName}`") do
+    let struct : StructInstView := { ref := stx, fields := #[], sources := sourcesView }
+    let r ← withSynthesize (postpone := .yes) <| elabStructInstView struct structName structType?
+    trace[Elab.struct] "result:{indentExpr r}"
+    return r
+
 builtin_initialize
   registerTraceClass `Elab.struct
   registerTraceClass `Elab.struct.modifyOp

src/Lean/Meta/DecLevel.lean

@@ -69,12 +69,16 @@ def decLevel (u : Level) : MetaM Level := do
 
 /-- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
    Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
-   and then decrement 1 to obtain `u`. -/
+   instantiate and normalize it, and then decrement 1 to obtain `u`. -/
 def getDecLevel (type : Expr) : MetaM Level := do
-  decLevel (← getLevel type)
+  let l ← getLevel type
+  let l ← normalizeLevel l
+  decLevel l
 
 def getDecLevel? (type : Expr) : MetaM (Option Level) := do
-  decLevel? (← getLevel type)
+  let l ← getLevel type
+  let l ← normalizeLevel l
+  decLevel? l
 
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.step

src/Lean/Parser/Do.lean

@@ -66,6 +66,14 @@ def notFollowedByRedefinedTermToken :=
       "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
+namespace InternalSyntax
+/--
+Internal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
+uses `()` if possible and gives better error messages.
+-/
+scoped syntax (name := doSkip) "skip" : doElem
+end InternalSyntax
+
 @[builtin_doElem_parser] def doLet      := leading_parser
   "let " >> optional "mut " >> letConfig >> letDecl
 @[builtin_doElem_parser] def doLetElse  := leading_parser withPosition <|

src/Lean/Parser/Term.lean

@@ -354,6 +354,13 @@ def structInstFieldDef := leading_parser
 def structInstFieldEqns := leading_parser
   optional "private" >> matchAlts
 
+/--
+Synthesizes a default value for a structure, making use of `Inhabited` instances for
+missing fields, as well as `Inhabited` instances for parent structures.
+-/
+@[builtin_term_parser] def structInstDefault := leading_parser
+  "struct_inst_default%"
+
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
 def funStrictImplicitBinder :=

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -117,12 +117,13 @@ private partial def isSyntheticTacticCompletion
     (cmdStx   : Syntax)
     : Bool := Id.run do
   let hoverFilePos := fileMap.toPosition hoverPos
-  go hoverFilePos cmdStx 0
+  go hoverFilePos cmdStx 0 none
 where
   go
-      (hoverFilePos : Position)
-      (stx : Syntax)
-      (leadingWs : Nat)
+      (hoverFilePos         : Position)
+      (stx                  : Syntax)
+      (leadingWs            : Nat)
+      (leadingTokenTailPos? : Option String.Pos.Raw)
       : Bool := Id.run do
     match stx.getPos?, stx.getTailPos? with
     | some startPos, some endPos =>
@@ -132,8 +133,9 @@ where
       if ! isCursorInCompletionRange then
         return false
       let mut wsBeforeArg := leadingWs
+      let mut lastArgTailPos? := leadingTokenTailPos?
       for arg in stx.getArgs do
-        if go hoverFilePos arg wsBeforeArg then
+        if go hoverFilePos arg wsBeforeArg lastArgTailPos? then
           return true
         -- We must account for the whitespace before an argument because the syntax nodes we use
         -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
@@ -141,7 +143,12 @@ where
         -- This method of computing whitespace assumes that there are no syntax nodes without tokens
         -- after `by` and before the first proper tactic syntax.
         wsBeforeArg := arg.getTrailingSize
-      return isCompletionInEmptyTacticBlock stx
+        -- Track the tail position of the most recent preceding sibling that has a position so
+        -- that empty tactic blocks (which lack positions) can locate their opening token (e.g.
+        -- the `by` keyword) for indentation checking. The tail position lets us distinguish
+        -- cursors before and after the opener on the opener's line.
+        lastArgTailPos? := arg.getTailPos? <|> lastArgTailPos?
+      return isCompletionInEmptyTacticBlock stx lastArgTailPos?
         || isCompletionAfterSemicolon stx
         || isCompletionOnTacticBlockIndentation hoverFilePos stx
     | _, _ =>
@@ -150,7 +157,7 @@ where
       -- tactic blocks always occur within other syntax with ranges that let us narrow down the
       -- search to the degree that we can be sure that the cursor is indeed in this empty tactic
       -- block.
-      return isCompletionInEmptyTacticBlock stx
+      return isCompletionInEmptyTacticBlock stx leadingTokenTailPos?
 
   isCompletionOnTacticBlockIndentation
       (hoverFilePos : Position)
@@ -190,8 +197,47 @@ where
     else
       none
 
-  isCompletionInEmptyTacticBlock (stx : Syntax) : Bool :=
-    isCursorInProperWhitespace fileMap hoverPos && isEmptyTacticBlock stx
+  isCompletionInEmptyTacticBlock (stx : Syntax) (leadingTokenTailPos? : Option String.Pos.Raw) : Bool := Id.run do
+    if ! isCursorInProperWhitespace fileMap hoverPos then
+      return false
+    if ! isEmptyTacticBlock stx then
+      return false
+    -- Bracketed tactic blocks `{ ... }` are delimited by the braces themselves, so tactics
+    -- inserted in an empty bracketed block can appear at any column between the braces
+    -- (`withoutPosition` disables indentation constraints inside `tacticSeqBracketed`).
+    if stx.getKind == ``Parser.Tactic.tacticSeqBracketed then
+      let some openEndPos := stx[0].getTailPos?
+        | return false
+      let some closeStartPos := stx[2].getPos?
+        | return false
+      return openEndPos.byteIdx <= hoverPos.byteIdx && hoverPos.byteIdx <= closeStartPos.byteIdx
+    return isAtExpectedTacticIndentation leadingTokenTailPos?
+
+  -- After an empty tactic opener like `by`, tactics on a subsequent line must be inserted at an
+  -- increased indentation level (two spaces past the indentation of the line containing the
+  -- opener token). We mirror that here so that tactic completions are not offered in positions
+  -- where a tactic could not actually be inserted. On the same line as the opener, completions
+  -- are allowed only in the trailing whitespace past the opener — cursors earlier on the line
+  -- belong to the surrounding term, not to the tactic block.
+  isAtExpectedTacticIndentation (leadingTokenTailPos? : Option String.Pos.Raw) : Bool := Id.run do
+    let some tokenTailPos := leadingTokenTailPos?
+      | return true
+    let hoverFilePos := fileMap.toPosition hoverPos
+    let tokenTailFilePos := fileMap.toPosition tokenTailPos
+    if hoverFilePos.line == tokenTailFilePos.line then
+      return hoverPos.byteIdx >= tokenTailPos.byteIdx
+    let expectedColumn := countLeadingSpaces (fileMap.lineStart tokenTailFilePos.line) + 2
+    return hoverFilePos.column == expectedColumn
+
+  countLeadingSpaces (pos : String.Pos.Raw) : Nat := Id.run do
+    let mut p := pos
+    let mut n : Nat := 0
+    while ! p.atEnd fileMap.source do
+      if p.get fileMap.source != ' ' then
+        break
+      p := p.next fileMap.source
+      n := n + 1
+    return n
 
   isEmptyTacticBlock (stx : Syntax) : Bool :=
     stx.getKind == ``Parser.Tactic.tacticSeq && isEmpty stx

src/Std/Do/SPred/DerivedLaws.lean

@@ -178,6 +178,48 @@ theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entai
 @[simp] theorem entails_4 {P Q : SPred [σ₁, σ₂, σ₃, σ₄]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄, (P s₁ s₂ s₃ s₄).down → (Q s₁ s₂ s₃ s₄).down) := iff_of_eq rfl
 @[simp] theorem entails_5 {P Q : SPred [σ₁, σ₂, σ₃, σ₄, σ₅]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄ s₅, (P s₁ s₂ s₃ s₄ s₅).down → (Q s₁ s₂ s₃ s₄ s₅).down) := iff_of_eq rfl
 
+/-!
+# `SPred.evalsTo`
+
+Relates a stateful value `SVal σs α` to a pure value `a : α`, lifting equality through the state.
+-/
+
+/-- Relates a stateful value to a pure value, lifting equality through the state layers. -/
+def evalsTo {α : Type u} {σs : List (Type u)} (f : SVal σs α) (a : α) : SPred σs :=
+  match σs with
+  | [] => ⌜a = f⌝
+  | _ :: _ => fun s => evalsTo (f s) a
+
+@[simp, grind =] theorem evalsTo_nil {f : SVal [] α} {a : α} :
+    evalsTo f a = ⌜a = f⌝ := rfl
+
+theorem evalsTo_cons {f : σ → SVal σs α} {a : α} {s : σ} :
+    evalsTo (σs := σ::σs) f a s = evalsTo (f s) a := rfl
+
+@[simp, grind =] theorem evalsTo_1 {f : SVal [σ] α} {a : α} {s : σ} :
+    evalsTo f a s = evalsTo (f s) a := rfl
+
+@[simp, grind =] theorem evalsTo_2 {f : SVal [σ₁, σ₂] α} {a : α} {s₁ : σ₁} {s₂ : σ₂} :
+    evalsTo f a s₁ s₂ = evalsTo (f s₁ s₂) a := rfl
+
+@[simp, grind =] theorem evalsTo_3 {f : SVal [σ₁, σ₂, σ₃] α} {a : α}
+    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} :
+    evalsTo f a s₁ s₂ s₃ = evalsTo (f s₁ s₂ s₃) a := rfl
+
+@[simp, grind =] theorem evalsTo_4 {f : SVal [σ₁, σ₂, σ₃, σ₄] α} {a : α}
+    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} {s₄ : σ₄} :
+    evalsTo f a s₁ s₂ s₃ s₄ = evalsTo (f s₁ s₂ s₃ s₄) a := rfl
+
+@[simp, grind =] theorem evalsTo_5 {f : SVal [σ₁, σ₂, σ₃, σ₄, σ₅] α} {a : α}
+    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} {s₄ : σ₄} {s₅ : σ₅} :
+    evalsTo f a s₁ s₂ s₃ s₄ s₅ = evalsTo (f s₁ s₂ s₃ s₄ s₅) a := rfl
+
+theorem evalsTo_total {P : SPred σs} (f : SVal σs α) :
+    P ⊢ₛ ∃ m, evalsTo f m := by
+  induction σs with
+  | nil => simp
+  | cons _ _ ih => intro s; apply ih
+
 /-! # Tactic support -/
 
 namespace Tactic
@@ -338,3 +380,4 @@ theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ]
     · exact HasFrame.reassoc.mp.trans SPred.and_elim_r
     · intro hp
       exact HasFrame.reassoc.mp.trans (SPred.and_elim_l' (h hp))
+

src/Std/Do/SPred/Laws.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
+import Init.PropLemmas
 
 @[expose] public section
 
@@ -157,3 +158,17 @@ theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t =>
   induction σs
   case nil => rfl
   case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih
+
+/-! # Prop-indexed quantifiers -/
+
+/-- Simplifies an existential over a true proposition. -/
+theorem exists_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∃ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.exists_prop_of_true h
+  | cons σ σs ih => ext; exact ih
+
+/-- Simplifies a universal over a true proposition. -/
+theorem forall_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∀ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.forall_prop_of_true h
+  | cons σ σs ih => ext; exact ih

src/Std/Do/Triple/RepeatSpec.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Std.Do.Triple.SpecLemmas
+import Std.Tactic.Do.Syntax
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+namespace Std.Do
+
+/-!
+# Specification theorem for `Loop`-based `repeat`/`while` loops
+
+This file contains the `@[spec]` theorem for `forIn` over `Lean.Loop`, which enables
+verified reasoning about `repeat`/`while` loops using `mvcgen`.
+-/
+
+set_option mvcgen.warning false
+
+/-- A variant (termination measure) for a `repeat`/`while` loop. -/
+@[spec_invariant_type]
+abbrev RepeatVariant (β : Type u) (ps : PostShape.{u}) := β → SVal ps.args (ULift Nat)
+
+set_option linter.missingDocs false in
+abbrev RepeatVariant.eval {β ps} (variant : RepeatVariant β ps) (b : β) (n : Nat) :=
+  SPred.evalsTo (variant b) ⟨n⟩
+
+/-- An invariant for a `repeat`/`while` loop. -/
+@[spec_invariant_type]
+abbrev RepeatInvariant β ps := PostCond (Bool × β) ps
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+
+private theorem RepeatVariant.eval_total {P : SPred ps.args} (variant : RepeatVariant β ps) (b : β) :
+    P ⊢ₛ ∃ m, RepeatVariant.eval variant b m := by
+  mintro _
+  mhave h2 := SPred.evalsTo_total (variant b)
+  mcases h2 with ⟨m, h2⟩
+  mexists m.down
+
+private theorem RepeatVariant.add_eval {P Q : SPred ps.args} (variant : RepeatVariant β ps) (b : β)
+    (h : spred(∃ m, RepeatVariant.eval variant b m ∧ P) ⊢ₛ Q) : P ⊢ₛ Q := by
+  apply SPred.entails.trans _ h
+  mintro _
+  mhave h2 := RepeatVariant.eval_total variant b
+  mcases h2 with ⟨m, h2⟩
+  mexists m
+  mconstructor <;> massumption
+
+end
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+variable [Monad m] [Lean.Order.MonadTail m] [WPMonad m ps]
+
+@[spec]
+theorem Spec.forIn_loop
+    {l : _root_.Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)}
+    (measure : RepeatVariant β ps)
+    (inv : RepeatInvariant β ps)
+    (step : ∀ b mb,
+      Triple (f () b)
+        spred(RepeatVariant.eval measure b mb ∧ inv.1 (false, b))
+        (fun r => match r with
+          | .yield b' => spred(∃ mb', RepeatVariant.eval measure b' mb' ∧ ⌜mb' < mb⌝ ∧ inv.1 (false, b'))
+          | .done b' => inv.1 (true, b'), inv.2)) :
+    Triple (forIn l init f) spred(inv.1 (false, init)) (fun b => inv.1 (true, b), inv.2) := by
+  haveI : Nonempty β := ⟨init⟩
+  simp only [forIn]
+  apply RepeatVariant.add_eval measure init
+  apply SPred.exists_elim
+  intro minit
+  induction minit using Nat.strongRecOn generalizing init with
+  | _ minit ih =>
+  rw [_root_.Lean.Loop.forIn_eq]
+  mvcgen [step, ih] with
+  | vc2 =>
+    mrename_i h
+    mcases h with ⟨mb', ⟨hmeasure, ⌜hmb'⌝, h⟩⟩
+    mspec Triple.of_entails_wp (ih mb' hmb')
+
+end
+
+end Std.Do

src/Std/Do/Triple/SpecLemmas.lean

@@ -10,6 +10,7 @@ public import Std.Do.Triple.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Range.Polymorphic
 public import Init.Data.Slice.Array
+public import Init.While
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.

src/Std/Internal/Http/Protocol/H1/Parser.lean

@@ -260,7 +260,7 @@ and returns the `RequestTarget` together with the raw major/minor version number
 Both `parseRequestLine` and `parseRequestLineRawVersion` call this after consuming
 the method token, keeping URI validation and version parsing in one place.
 -/
-private def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
+def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
   let rawUri ← parseURI limits <* sp
   let uri ← match (Std.Http.URI.Parser.parseRequestTarget <* eof).run rawUri with
   | .ok res => pure res
@@ -446,7 +446,7 @@ Returns `true` if `name` (compared case-insensitively) is a field that MUST NOT
 trailer sections per RFC 9112 §6.5. Forbidden fields are those required for message framing
 (`content-length`, `transfer-encoding`), routing (`host`), or connection management (`connection`).
 -/
-private def isForbiddenTrailerField (name : String) : Bool :=
+def isForbiddenTrailerField (name : String) : Bool :=
   let n := name.toLower
   n == "content-length" || n == "transfer-encoding" || n == "host" ||
   n == "connection" || n == "expect" || n == "te" ||

src/Std/Tactic/Do.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Tactic.Do.ProofMode
 public import Std.Tactic.Do.Syntax
+public import Std.Do.Triple.RepeatSpec
 
 @[expose] public section
 

src/runtime/CMakeLists.txt

@@ -39,7 +39,7 @@ if(USE_MIMALLOC)
   # Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir
   include_directories(${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/include)
   # make all symbols visible, always build with optimizations as otherwise Lean becomes too slow
-  set(MIMALLOC_FLAGS "-DMI_SHARED_LIB -DMI_SHARED_LIB_EXPORT -O3 -DNDEBUG -DMI_WIN_NOREDIRECT -Wno-unused-function")
+  set(MIMALLOC_FLAGS "-DMI_SHARED_LIB -DMI_SHARED_LIB_EXPORT -O3 -DNDEBUG -DMI_WIN_NOREDIRECT -DMI_SECURE=${LEAN_MI_SECURE} -Wno-unused-function")
   if(CMAKE_CXX_COMPILER_ID MATCHES "AppleClang|Clang")
     string(APPEND MIMALLOC_FLAGS " -Wno-deprecated")
   endif()

src/stdlib.make.in

@@ -54,7 +54,7 @@ ifeq "${USE_LAKE}" "ON"
 
 # build in parallel
 Init:
-	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)
+	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml ${LEAN_EXTRA_LAKE_OPTS} $(LAKE_EXTRA_ARGS)
 
 Std Lean Lake Leanc LeanChecker LeanIR: Init