fix: test and select gate test

This PR globally enables `warning.simp.varHead` (added in #13325) and
silences the warning in `Lake.Util.Family.Mathlib` adaptations were
already merged as part of adaptations for #13325. This is a separate PR
from #13325 due to warning appearing when re-bootstrapping, so we needed
`stage0` update before enabling this option.

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/While.lean

@@ -35,21 +35,23 @@ instance [Monad m] : ForIn m Loop Unit where
 syntax "repeat " doSeq : doElem
 
 macro_rules
-  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
+  | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)
 
 syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
 
 macro_rules
-  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h:ident : $cond then $seq else break)
+  | `(doElem| while%$tk $h : $cond do $seq) =>
+    `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
 
 syntax "while " termBeforeDo " do " doSeq : doElem
 
 macro_rules
-  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
+  | `(doElem| while%$tk $cond do $seq) => `(doElem| repeat%$tk if $cond then $seq else break)
 
 syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
 
 macro_rules
-  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
+  | `(doElem| repeat%$tk $seq until $cond) =>
+    `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
 
 end Lean

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -90,6 +90,22 @@ partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (Cod
         | break
       if !(w == z && targetId == x) then
         break
+      if mask[i]!.isSome then
+        /-
+        Suppose we encounter a situation like
+        ```
+        let x.1 := proj[0] y
+        inc x.1
+        let x.2 := proj[0] y
+        inc x.2
+        ```
+        The `inc x.2` will already have been removed. If we don't perform this check we will also
+        remove `inc x.1` and have effectively removed two refcounts while only one was legal.
+        -/
+        keep := keep.push d
+        keep := keep.push d'
+        ds := ds.pop.pop
+        continue
       /-
       Found
       ```

src/Lean/Elab/BuiltinDo/Basic.lean

@@ -21,7 +21,8 @@ def elabDoIdDecl (x : Ident) (xType? : Option Term) (rhs : TSyntax `doElem) (k :
   let xType ← Term.elabType (xType?.getD (mkHole x))
   let lctx ← getLCtx
   let ctx ← read
-  elabDoElem rhs <| .mk (kind := kind) x.getId xType do
+  let ref ← getRef -- store the surrounding reference for error messages in `k`
+  elabDoElem rhs <| .mk (kind := kind) x.getId xType do withRef ref do
     withLCtxKeepingMutVarDefs lctx ctx x.getId do
       Term.addLocalVarInfo x (← getFVarFromUserName x.getId)
       k

src/Lean/Elab/BuiltinDo/For.lean

@@ -23,7 +23,7 @@ open Lean.Meta
   | `(doFor| for $[$_ : ]? $_:ident in $_ do $_) =>
     -- This is the target form of the expander, handled by `elabDoFor` below.
     Macro.throwUnsupported
-  | `(doFor| for $decls:doForDecl,* do $body) =>
+  | `(doFor| for%$tk $decls:doForDecl,* do $body) =>
     let decls := decls.getElems
     let `(doForDecl| $[$h? : ]? $pattern in $xs) := decls[0]! | Macro.throwUnsupported
     let mut doElems := #[]
@@ -74,12 +74,13 @@ open Lean.Meta
           | some ($y, s') =>
             $s:ident := s'
             do $body)
-    doElems := doElems.push (← `(doSeqItem| for $[$h? : ]? $x:ident in $xs do $body))
+    doElems := doElems.push (← `(doSeqItem| for%$tk $[$h? : ]? $x:ident in $xs do $body))
     `(doElem| do $doElems*)
   | _ => Macro.throwUnsupported
 
 @[builtin_doElem_elab Lean.Parser.Term.doFor] def elabDoFor : DoElab := fun stx dec => do
-  let `(doFor| for $[$h? : ]? $x:ident in $xs do $body) := stx | throwUnsupportedSyntax
+  let `(doFor| for%$tk $[$h? : ]? $x:ident in $xs do $body) := stx | throwUnsupportedSyntax
+  let dec ← dec.ensureUnitAt tk
   checkMutVarsForShadowing #[x]
   let uα ← mkFreshLevelMVar
   let uρ ← mkFreshLevelMVar
@@ -124,9 +125,6 @@ open Lean.Meta
       defs := defs.push (mkConst ``Unit.unit)
     return defs
 
-  unless ← isDefEq dec.resultType (← mkPUnit) do
-    logError m!"Type mismatch. `for` loops have result type {← mkPUnit}, but the rest of the `do` sequence expected {dec.resultType}."
-
   let (preS, σ) ← mkProdMkN (← useLoopMutVars none) mi.u
 
   let (app, p?) ← match h? with
@@ -153,6 +151,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/BuiltinDo/If.lean

@@ -17,6 +17,7 @@ namespace Lean.Elab.Do
 open Lean.Parser.Term
 open Lean.Meta
 
+open InternalSyntax in
 /--
 If the given syntax is a `doIf`, return an equivalent `doIf` that has an `else` but no `else if`s or
 `if let`s.
@@ -25,8 +26,8 @@ If the given syntax is a `doIf`, return an equivalent `doIf` that has an `else`
   match stx with
   | `(doElem|if $_:doIfProp then $_ else $_) =>
     Macro.throwUnsupported
-  | `(doElem|if $cond:doIfCond then $t $[else if $conds:doIfCond then $ts]* $[else $e?]?) => do
-    let mut e : Syntax ← e?.getDM `(doSeq|pure PUnit.unit)
+  | `(doElem|if%$tk $cond:doIfCond then $t $[else if%$tks $conds:doIfCond then $ts]* $[else $e?]?) => do
+    let mut e : Syntax ← e?.getDM `(doSeq| skip%$tk)
     let mut eIsSeq := true
     for (cond, t) in Array.zip (conds.reverse.push cond) (ts.reverse.push t) do
       e ← if eIsSeq then pure e else `(doSeq|$(⟨e⟩):doElem)

src/Lean/Elab/BuiltinDo/Let.lean

@@ -88,17 +88,18 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
     throwError "`+generalize` is not supported in `do` blocks"
 
 partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
-    (dec : DoElemCont) : DoElabM Expr := do
+    (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   checkLetConfigInDo config
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
+  let dec ← dec.ensureUnitAt tk
   -- Some decl preprocessing on the patterns and expected types:
   let decl ← pushTypeIntoReassignment letOrReassign decl
   let mγ ← mkMonadicType (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
     let declNew ← `(letDecl| $(⟨← liftMacroM <| Term.expandLetEqnsDecl decl⟩):letIdDecl)
-    return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew dec
+    return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew tk dec
   | `(letDecl| $pattern:term $[: $xType?]? := $rhs) =>
     let rhs ← match xType? with | some xType => `(($rhs : $xType)) | none => pure rhs
     let contElab : DoElabM Expr := elabWithReassignments letOrReassign vars dec.continueWithUnit
@@ -162,10 +163,11 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
             mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   | _ => throwUnsupportedSyntax
 
-def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (dec : DoElemCont) : DoElabM Expr := do
+def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   match stx with
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
     letOrReassign.checkMutVars #[x]
+    let dec ← dec.ensureUnitAt tk
     -- For plain variable reassignment, we know the expected type of the reassigned variable and
     -- propagate it eagerly via type ascription if the user hasn't provided one themselves:
     let xType? ← match letOrReassign, xType? with
@@ -177,6 +179,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
+    let dec ← dec.ensureUnitAt tk
     elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
   | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
     let rest? := rest?.join
@@ -205,17 +208,18 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   Term.mkLetConfig letConfigStx initConfig
 
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
-  let `(doLet| let $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
+  let `(doLet| let%$tk $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut config mutTk?
-  elabDoLetOrReassign config (.let mutTk?) decl dec
+  elabDoLetOrReassign config (.let mutTk?) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
-  let `(doHave| have $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
+  let `(doHave| have%$tk $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← Term.mkLetConfig config { nondep := true }
-  elabDoLetOrReassign config .have decl dec
+  elabDoLetOrReassign config .have decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetRec] def elabDoLetRec : DoElab := fun stx dec => do
-  let `(doLetRec| let rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
+  let `(doLetRec| let%$tk rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
+  let dec ← dec.ensureUnitAt tk
   let vars ← getLetRecDeclsVars decls
   let mγ ← mkMonadicType (← read).doBlockResultType
   doElabToSyntax m!"let rec body of group {vars}" dec.continueWithUnit fun body => do
@@ -227,13 +231,13 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 @[builtin_doElem_elab Lean.Parser.Term.doReassign] def elabDoReassign : DoElab := fun stx dec => do
   -- def doReassign := letIdDeclNoBinders <|> letPatDecl
   match stx with
-  | `(doReassign| $x:ident $[: $xType?]? := $rhs) =>
+  | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} .reassign decl dec
+    elabDoLetOrReassign {} .reassign decl tk dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} .reassign decl dec
+    elabDoLetOrReassign {} .reassign decl decl dec
   | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
@@ -255,17 +259,17 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
     elabDoElem (← `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetArrow] def elabDoLetArrow : DoElab := fun stx dec => do
-  let `(doLetArrow| let $[mut%$mutTk?]? $cfg:letConfig $decl) := stx | throwUnsupportedSyntax
+  let `(doLetArrow| let%$tk $[mut%$mutTk?]? $cfg:letConfig $decl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut cfg mutTk?
   checkLetConfigInDo config
   if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
     throwErrorAt cfg "configuration options are not supported with `←`"
-  elabDoArrow (.let mutTk?) decl dec
+  elabDoArrow (.let mutTk?) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
   match stx with
   | `(doReassignArrow| $decl:doIdDecl) =>
-    elabDoArrow .reassign decl dec
+    elabDoArrow .reassign decl decl dec
   | `(doReassignArrow| $decl:doPatDecl) =>
-    elabDoArrow .reassign decl dec
+    elabDoArrow .reassign decl decl dec
   | _ => throwUnsupportedSyntax

src/Lean/Elab/BuiltinDo/Misc.lean

@@ -16,6 +16,12 @@ namespace Lean.Elab.Do
 open Lean.Parser.Term
 open Lean.Meta
 
+open InternalSyntax in
+@[builtin_doElem_elab Lean.Parser.Term.InternalSyntax.doSkip] def elabDoSkip : DoElab := fun stx dec => do
+  let `(doSkip| skip%$tk) := stx | throwUnsupportedSyntax
+  let dec ← dec.ensureUnitAt tk
+  dec.continueWithUnit
+
 @[builtin_doElem_elab Lean.Parser.Term.doExpr] def elabDoExpr : DoElab := fun stx dec => do
   let `(doExpr| $e:term) := stx | throwUnsupportedSyntax
   let mα ← mkMonadicType dec.resultType
@@ -26,24 +32,28 @@ open Lean.Meta
   let `(doNested| do $doSeq) := stx | throwUnsupportedSyntax
   elabDoSeq ⟨doSeq.raw⟩ dec
 
+open InternalSyntax in
 @[builtin_doElem_elab Lean.Parser.Term.doUnless] def elabDoUnless : DoElab := fun stx dec => do
-  let `(doUnless| unless $cond do $body) := stx | throwUnsupportedSyntax
-  elabDoElem (← `(doElem| if $cond then pure PUnit.unit else $body)) dec
+  let `(doUnless| unless%$tk $cond do $body) := stx | throwUnsupportedSyntax
+  elabDoElem (← `(doElem| if $cond then skip%$tk else $body)) dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doDbgTrace] def elabDoDbgTrace : DoElab := fun stx dec => do
-  let `(doDbgTrace| dbg_trace $msg:term) := stx | throwUnsupportedSyntax
+  let `(doDbgTrace| dbg_trace%$tk $msg:term) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "dbg_trace body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(dbg_trace $msg; $body)) mγ
 
 @[builtin_doElem_elab Lean.Parser.Term.doAssert] def elabDoAssert : DoElab := fun stx dec => do
-  let `(doAssert| assert! $cond) := stx | throwUnsupportedSyntax
+  let `(doAssert| assert!%$tk $cond) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "assert! body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(assert! $cond; $body)) mγ
 
 @[builtin_doElem_elab Lean.Parser.Term.doDebugAssert] def elabDoDebugAssert : DoElab := fun stx dec => do
-  let `(doDebugAssert| debug_assert! $cond) := stx | throwUnsupportedSyntax
+  let `(doDebugAssert| debug_assert!%$tk $cond) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "debug_assert! body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(debug_assert! $cond; $body)) mγ

src/Lean/Elab/Deriving/Basic.lean

@@ -220,7 +220,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
+            let isMeta := (← read).isMetaSection || isMarkedMeta (← getEnv) declName
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 wrapInstance result.instVal result.instType
@@ -255,11 +255,12 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             logInfoAt cmdRef m!"Try this: {newText}"
         throwError "failed to derive instance because it depends on \
           `{.ofConstName noncompRef}`, which is noncomputable"
+    let isMeta := (← read).isMetaSection || isMarkedMeta (← getEnv) declName
     if isNoncomputable || (← read).isNoncomputableSection then
       addDecl <| Declaration.defnDecl decl
       modifyEnv (addNoncomputable · instName)
     else
-      addAndCompile <| Declaration.defnDecl decl
+      addAndCompile (Declaration.defnDecl decl) (markMeta := isMeta)
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
   -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
   -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command

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

@@ -374,16 +374,63 @@ def withLCtxKeepingMutVarDefs (oldLCtx : LocalContext) (oldCtx : Context) (resul
     mutVarDefs := oldMutVarDefs
   }) k
 
+def mkMonadicResultTypeMismatchError (contType : Expr) (elementType : Expr) : MessageData :=
+  m!"Type mismatch. The `do` element has monadic result type{indentExpr elementType}\n\
+    but the rest of the `do` block has monadic result type{indentExpr contType}"
+
+/--
+Given a continuation `dec`, a reference `ref`, and an element result type `elementType`, returns a
+continuation derived from `dec` with result type `elementType`.
+If `dec` already has result type `elementType`, simply returns `dec`.
+Otherwise, an error is logged and a new continuation is returned that calls `dec` with `sorry` as a
+result. The error is reported at `ref`.
+-/
+def DoElemCont.ensureHasTypeAt (dec : DoElemCont) (ref : Syntax) (elementType : Expr) : DoElabM DoElemCont := do
+  if ← isDefEqGuarded dec.resultType elementType then
+    return dec
+  let errMessage := mkMonadicResultTypeMismatchError dec.resultType elementType
+  unless (← readThe Term.Context).errToSorry do
+    throwErrorAt ref errMessage
+  logErrorAt ref errMessage
+  return {
+    resultName := ← mkFreshUserName `__r
+    resultType := elementType
+    k := do
+      mapLetDecl dec.resultName dec.resultType (← mkSorry dec.resultType true)
+          (nondep := true) (kind := .implDetail) fun _ => dec.k
+    kind := dec.kind
+  }
+
+/--
+Given a continuation `dec` and a reference `ref`, returns a continuation derived from `dec` with result type `PUnit`.
+If `dec` already has result type `PUnit`, simply returns `dec`. Otherwise, an error is logged and a
+new continuation is returned that calls `dec` with `sorry` as a result. The error is reported at `ref`.
+-/
+def DoElemCont.ensureUnitAt (dec : DoElemCont) (ref : Syntax) : DoElabM DoElemCont := do
+  dec.ensureHasTypeAt ref (← mkPUnit)
+
+/--
+Given a continuation `dec`, returns a continuation derived from `dec` with result type `PUnit`.
+If `dec` already has result type `PUnit`, simply returns `dec`. Otherwise, an error is logged and a
+new continuation is returned that calls `dec` with `sorry` as a result.
+-/
+def DoElemCont.ensureUnit (dec : DoElemCont) : DoElabM DoElemCont := do
+  dec.ensureUnitAt (← getRef)
+
 /--
 Return `$e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k)`, cancelling
 the bind if `$(← dec.k)` is `pure $dec.resultName` or `e` is some `pure` computation.
 -/
 def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr := do
+  -- let eResultTy ← mkFreshResultType
+  -- let e ← Term.ensureHasType (← mkMonadicType eResultTy) e
+  -- let dec ← dec.ensureHasType eResultTy
   let x := dec.resultName
-  let eResultTy := dec.resultType
   let k := dec.k
+  let eResultTy := dec.resultType
   -- 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 +458,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
@@ -421,9 +467,8 @@ Return `let $k.resultName : PUnit := PUnit.unit; $(← k.k)`, ensuring that the
 is `PUnit` and then immediately zeta-reduce the `let`.
 -/
 def DoElemCont.continueWithUnit (dec : DoElemCont) : DoElabM Expr := do
-  let unit ← mkPUnitUnit
-  discard <| Term.ensureHasType dec.resultType unit
-  mapLetDeclZeta dec.resultName (← mkPUnit) unit (nondep := true) (kind := .ofBinderName dec.resultName) fun _ =>
+  let dec ← dec.ensureUnit
+  mapLetDeclZeta dec.resultName (← mkPUnit) (← mkPUnitUnit) (nondep := true) (kind := .ofBinderName dec.resultName) fun _ =>
     dec.k
 
 /-- Elaborate the `DoElemCont` with the `deadCode` flag set to `deadSyntactically` to emit warnings. -/
@@ -545,7 +590,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.
@@ -601,6 +649,7 @@ def enterFinally (resultType : Expr) (k : DoElabM Expr) : DoElabM Expr := do
 /-- Extracts `MonadInfo` and monadic result type `α` from the expected type of a `do` block `m α`. -/
 private partial def extractMonadInfo (expectedType? : Option Expr) : Term.TermElabM (MonadInfo × Expr) := do
   let some expectedType := expectedType? | mkUnknownMonadResult
+  let expectedType ← instantiateMVars expectedType
   let extractStep? (type : Expr) : Term.TermElabM (Option (MonadInfo × Expr)) := do
     let .app m resultType := type.consumeMData | return none
     unless ← isType resultType do return none

src/Lean/Elab/Do/InferControlInfo.lean

@@ -79,6 +79,7 @@ builtin_initialize controlInfoElemAttribute : KeyedDeclsAttribute ControlInfoHan
 
 namespace InferControlInfo
 
+open InternalSyntax in
 mutual
 
 partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
@@ -152,6 +153,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     let finInfo ← ofOptionSeq finSeq?
     return info.sequence finInfo
   -- Misc
+  | `(doElem| skip) => return .pure
   | `(doElem| dbg_trace $_) => return .pure
   | `(doElem| assert! $_) => return .pure
   | `(doElem| debug_assert! $_) => return .pure

src/Lean/Elab/Do/Legacy.lean

@@ -1815,6 +1815,13 @@ mutual
               return mkTerminalAction term
             else
               return mkSeq term (← doSeqToCode doElems)
+          else if k == ``Parser.Term.InternalSyntax.doSkip then
+            -- In the legacy elaborator, `skip` is treated as `pure PUnit.unit`.
+            let term ← withRef doElem `(pure PUnit.unit)
+            if doElems.isEmpty then
+              return mkTerminalAction term
+            else
+              return mkSeq term (← doSeqToCode doElems)
           else
             throwError "unexpected do-element of kind {doElem.getKind}:\n{doElem}"
 end

src/Lean/Elab/Idbg.lean

@@ -364,8 +364,9 @@ def elabIdbgTerm : TermElab := fun stx expectedType? => do
 
 @[builtin_doElem_elab Lean.Parser.Term.doIdbg]
 def elabDoIdbg : DoElab := fun stx dec => do
-  let `(Lean.Parser.Term.doIdbg| idbg $e) := stx | throwUnsupportedSyntax
+  let `(Lean.Parser.Term.doIdbg| idbg%$tk $e) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "idbg body" dec.continueWithUnit fun body => do
     elabIdbgCore (e := e) (body := body) (ref := stx) mγ
 

src/Lean/Elab/Inductive.lean

@@ -73,6 +73,8 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
         throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
       checkValidCtorModifier ctorModifiers
       let ctorName := ctor.getIdAt 3
+      if ctorName.hasMacroScopes && isCoinductive then
+        throwError "Coinductive predicates are not allowed inside of macro scopes"
       let ctorName := declName ++ ctorName
       let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
       let (binders, type?) := expandOptDeclSig ctor[4]

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/Meta/Tactic/Simp/SimpTheorems.lean

@@ -51,7 +51,7 @@ register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
 }
 
 register_builtin_option warning.simp.varHead : Bool := {
-  defValue := false
+  defValue := true
   descr := "If true, warns when the head symbol of the left-hand side of a `@[simp]` theorem \
     is a variable. Such lemmas are tried on every simp step, which can be slow."
 }

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/Internal/Async/Select.lean

@@ -132,6 +132,8 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
   let gen := mkStdGen seed
   let selectables := shuffleIt selectables gen
 
+  let gate ← IO.Promise.new
+
   for selectable in selectables do
     if let some val ← selectable.selector.tryFn then
       let result ← selectable.cont val
@@ -141,11 +143,14 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
   let promise ← IO.Promise.new
 
   for selectable in selectables do
+    if ← finished.get then
+      break
+
     let waiterPromise ← IO.Promise.new
     let waiter := Waiter.mk finished waiterPromise
     selectable.selector.registerFn waiter
 
-    discard <| IO.bindTask (t := waiterPromise.result?) fun res? => do
+    discard <| IO.bindTask (t := waiterPromise.result?) (sync := true) fun res? => do
       match res? with
       | none =>
         /-
@@ -157,18 +162,20 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
         let async : Async _ :=
           try
             let res ← IO.ofExcept res
+            discard <| await gate.result?
 
             for selectable in selectables do
               selectable.selector.unregisterFn
 
-            let contRes ← selectable.cont res
-            promise.resolve (.ok contRes)
+            promise.resolve (.ok (← selectable.cont res))
           catch e =>
             promise.resolve (.error e)
 
         async.toBaseIO
 
-  Async.ofPromise (pure promise)
+  gate.resolve ()
+  let result ← Async.ofPromise (pure promise)
+  return result
 
 /--
 Performs fair and data-loss free non-blocking multiplexing on the `Selectable`s in `selectables`.
@@ -224,6 +231,8 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
         let derivedWaiter := Waiter.mk waiter.finished waiterPromise
         selectable.selector.registerFn derivedWaiter
 
+        let barrier ← IO.Promise.new
+
         discard <| IO.bindTask (t := waiterPromise.result?) fun res? => do
           match res? with
           | none => return (Task.pure (.ok ()))
@@ -231,6 +240,7 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
             let async : Async _ := do
               let mainPromise := waiter.promise
 
+              await barrier
               for selectable in selectables do
                 selectable.selector.unregisterFn
 

src/Std/Internal/Http.lean

@@ -6,5 +6,189 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Protocol.H1
+public import Std.Internal.Http.Server
+public import Std.Internal.Http.Test.Helpers
+
+public section
+
+/-!
+# HTTP Library
+
+A low-level HTTP/1.1 server implementation for Lean. This library provides a pure,
+sans-I/O protocol implementation that can be used with the `Async` library or with
+custom connection handlers.
+
+## Overview
+
+This module provides a complete HTTP/1.1 server implementation with support for:
+
+- Request/response handling with directional streaming bodies
+- Keep-alive connections
+- Chunked transfer encoding
+- Header validation and management
+- Configurable timeouts and limits
+
+**Sans I/O Architecture**: The core protocol logic doesn't perform any actual I/O itself -
+it just defines how data should be processed. This separation allows the protocol implementation
+to remain pure and testable, while different transports (TCP sockets, mock clients) handle
+the actual reading and writing of bytes.
+
+## Quick Start
+
+The main entry point is `Server.serve`, which starts an HTTP/1.1 server. Implement the
+`Server.Handler` type class to define how the server handles requests, errors, and
+`Expect: 100-continue` headers:
+
+```lean
+import Std.Internal.Http
+
+open Std Internal IO Async
+open Std Http Server
+
+structure MyHandler
+
+instance : Handler MyHandler where
+  onRequest _ req := do
+    Response.ok |>.text "Hello, World!"
+
+def main : IO Unit := Async.block do
+  let addr : Net.SocketAddress := .v4 ⟨.ofParts 127 0 0 1, 8080⟩
+  let server ← Server.serve addr MyHandler.mk
+  server.waitShutdown
+```
+
+## Working with Requests
+
+Incoming requests are represented by `Request Body.Stream`, which bundles the request
+line, parsed headers, and a lazily-consumed body. Headers are available immediately,
+while the body can be streamed or collected on demand, allowing handlers to process both
+small and large payloads efficiently.
+
+### Reading Headers
+
+```lean
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+  -- Access request method and URI
+  let method := req.head.method      -- Method.get, Method.post, etc.
+  let uri := req.head.uri            -- RequestTarget
+
+  -- Read a specific header
+  if let some contentType := req.head.headers.get? (.mk "content-type") then
+    IO.println s!"Content-Type: {contentType}"
+
+  Response.ok |>.text "OK"
+```
+
+### URI Query Semantics
+
+`RequestTarget.query` is parsed using form-style key/value conventions (`k=v&...`), and `+` is decoded as a
+space in query components. If you need RFC 3986 opaque query handling, use the raw request target string
+(`toString req.head.uri`) and parse it with custom logic.
+
+### Reading the Request Body
+
+The request body is exposed as `Body.Stream`, which can be consumed incrementally or
+collected into memory. The `readAll` method reads the entire body, with an optional size
+limit to protect against unbounded payloads.
+
+```lean
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+  -- Collect entire body as a String
+  let bodyStr : String ← req.body.readAll
+
+  -- Or with a maximum size limit
+  let bodyStr : String ← req.body.readAll (maximumSize := some 1024)
+
+  Response.ok |>.text s!"Received: {bodyStr}"
+```
+
+## Building Responses
+
+Responses are constructed using a builder API that starts from a status code and adds
+headers and a body. Common helpers exist for text, HTML, JSON, and binary responses, while
+still allowing full control over status codes and header values.
+
+Response builders produce `Async (Response Body.Stream)`.
+
+```lean
+-- Text response
+Response.ok |>.text "Hello!"
+
+-- HTML response
+Response.ok |>.html "<h1>Hello!</h1>"
+
+-- JSON response
+Response.ok |>.json "{\"key\": \"value\"}"
+
+-- Binary response
+Response.ok |>.bytes someByteArray
+
+-- Custom status
+Response.new |>.status .created |>.text "Resource created"
+
+-- With custom headers
+Response.ok
+  |>.header! "X-Custom-Header" "value"
+  |>.header! "Cache-Control" "no-cache"
+  |>.text "Response with headers"
+```
+
+### Streaming Responses
+
+For large responses or server-sent events, use streaming:
+
+```lean
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+  Response.ok
+    |>.header! "Content-Type" "text/plain"
+    |>.stream fun stream => do
+      for i in [0:10] do
+        stream.send { data := s!"chunk {i}\n".toUTF8 }
+        Async.sleep 1000
+      stream.close
+```
+
+## Server Configuration
+
+Configure server behavior with `Config`:
+
+```lean
+def config : Config := {
+  maxRequests := 10000000,
+  lingeringTimeout := 5000,
+}
+
+let server ← Server.serve addr MyHandler.mk config
+```
+
+## Handler Type Class
+
+Implement `Server.Handler` to define how the server processes events. The class has three
+methods, all with default implementations:
+
+- `onRequest` — called for each incoming request; returns a response inside `ContextAsync`
+- `onFailure` — called when an error occurs while processing a request
+- `onContinue` — called when a request includes an `Expect: 100-continue` header; return
+  `true` to accept the body or `false` to reject it
+
+```lean
+structure MyHandler where
+  greeting : String
+
+instance : Handler MyHandler where
+  onRequest self req := do
+    Response.ok |>.text self.greeting
+
+  onFailure self err := do
+    IO.eprintln s!"Error: {err}"
+```
+
+The handler methods operate in the following monads:
+
+- `onRequest` uses `ContextAsync` — an asynchronous monad (`ReaderT CancellationContext Async`) that provides:
+  - Full access to `Async` operations (spawning tasks, sleeping, concurrent I/O)
+  - A `CancellationContext` tied to the client connection — when the client disconnects, the
+    context is cancelled, allowing your handler to detect this and stop work early
+- `onFailure` uses `Async`
+- `onContinue` uses `Async`
+-/

src/Std/Internal/Http/Data/Body/Any.lean

@@ -48,6 +48,12 @@ structure Any where
   -/
   recvSelector : Selector (Option Chunk)
 
+  /--
+  Non-blocking receive attempt. Returns `none` if no chunk is immediately available,
+  `some (some chunk)` when a chunk is ready, or `some none` at end-of-stream.
+  -/
+  tryRecv : Async (Option (Option Chunk))
+
   /--
   Returns the declared size.
   -/
@@ -67,6 +73,7 @@ def ofBody [Http.Body α] (body : α) : Any where
   close := Http.Body.close body
   isClosed := Http.Body.isClosed body
   recvSelector := Http.Body.recvSelector body
+  tryRecv := Http.Body.tryRecv body
   getKnownSize := Http.Body.getKnownSize body
   setKnownSize := Http.Body.setKnownSize body
 
@@ -77,6 +84,7 @@ instance : Http.Body Any where
   close := Any.close
   isClosed := Any.isClosed
   recvSelector := Any.recvSelector
+  tryRecv := Any.tryRecv
   getKnownSize := Any.getKnownSize
   setKnownSize := Any.setKnownSize
 

src/Std/Internal/Http/Data/Body/Basic.lean

@@ -50,6 +50,12 @@ class Body (α : Type) where
   -/
   recvSelector : α → Selector (Option Chunk)
 
+  /--
+  Non-blocking receive attempt. Returns `none` if no chunk is immediately available,
+  `some (some chunk)` when a chunk is ready, or `some none` at end-of-stream.
+  -/
+  tryRecv (body : α) : Async (Option (Option Chunk))
+
   /--
   Gets the declared size of the body.
   -/

src/Std/Internal/Http/Data/Body/Empty.lean

@@ -52,6 +52,13 @@ Empty bodies are always closed for reading.
 def isClosed (_ : Empty) : Async Bool :=
   pure true
 
+/--
+Non-blocking receive. Empty bodies are always at EOF.
+-/
+@[inline]
+def tryRecv (_ : Empty) : Async (Option (Option Chunk)) :=
+  pure (some none)
+
 /--
 Selector that immediately resolves with end-of-stream for an empty body.
 -/
@@ -72,6 +79,7 @@ instance : Http.Body Empty where
   close := Empty.close
   isClosed := Empty.isClosed
   recvSelector := Empty.recvSelector
+  tryRecv := Empty.tryRecv
   getKnownSize _ := pure (some <| .fixed 0)
   setKnownSize _ _ := pure ()
 

src/Std/Internal/Http/Data/Body/Full.lean

@@ -100,6 +100,14 @@ def getKnownSize (full : Full) : Async (Option Body.Length) :=
     | none => pure (some (.fixed 0))
     | some data => pure (some (.fixed data.size))
 
+/--
+Non-blocking receive. `Full` bodies are always in-memory, so data is always
+immediately available. Returns `some chunk` on first call, `some none` (EOF)
+once consumed or closed.
+-/
+def tryRecv (full : Full) : Async (Option (Option Chunk)) := do
+  return some (← full.state.atomically takeChunk)
+
 /--
 Selector that immediately resolves to the remaining chunk (or EOF).
 -/
@@ -128,6 +136,7 @@ instance : Http.Body Full where
   close := Full.close
   isClosed := Full.isClosed
   recvSelector := Full.recvSelector
+  tryRecv := Full.tryRecv
   getKnownSize := Full.getKnownSize
   setKnownSize _ _ := pure ()
 

src/Std/Internal/Http/Data/Body/Stream.lean

@@ -227,6 +227,19 @@ def tryRecv (stream : Stream) : Async (Option Chunk) :=
     Channel.pruneFinishedWaiters
     Channel.tryRecv'
 
+/--
+Non-blocking receive for the `Body` typeclass. Returns `none` when no producer is
+waiting and the channel is still open, `some (some chunk)` when data is ready,
+or `some none` at end-of-stream (channel closed with no pending producer).
+-/
+def tryRecvBody (stream : Stream) : Async (Option (Option Chunk)) :=
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    if ← Channel.recvReady' then
+      return some (← Channel.tryRecv')
+    else
+      return none
+
 private def recv' (stream : Stream) : BaseIO (AsyncTask (Option Chunk)) := do
   stream.state.atomically do
     Channel.pruneFinishedWaiters
@@ -598,6 +611,7 @@ instance : Http.Body Stream where
   close := Stream.close
   isClosed := Stream.isClosed
   recvSelector := Stream.recvSelector
+  tryRecv := Stream.tryRecvBody
   getKnownSize := Stream.getKnownSize
   setKnownSize := Stream.setKnownSize
 

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/Internal/Http/Server.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async
+public import Std.Internal.Async.TCP
+public import Std.Sync.CancellationToken
+public import Std.Sync.Semaphore
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
+public import Std.Internal.Http.Server.Connection
+
+public section
+
+/-!
+# HTTP Server
+
+This module defines a simple, asynchronous HTTP/1.1 server implementation.
+
+It provides the `Std.Http.Server` structure, which encapsulates all server state, and functions for
+starting, managing, and gracefully shutting down the server.
+
+The server runs entirely using `Async` and uses a shared `CancellationContext` to signal shutdowns.
+Each active client connection is tracked, and the server automatically resolves its shutdown
+promise once all connections have closed.
+-/
+
+namespace Std.Http
+open Std.Internal.IO.Async TCP
+
+set_option linter.all true
+
+/--
+The `Server` structure holds all state required to manage the lifecycle of an HTTP server, including
+connection tracking and shutdown coordination.
+-/
+structure Server where
+
+  /--
+  The context used for shutting down all connections and the server.
+  -/
+  context : Std.CancellationContext
+
+  /--
+  Active HTTP connections
+  -/
+  activeConnections : Std.Mutex Nat
+
+  /--
+  Semaphore used to enforce the maximum number of simultaneous active connections.
+  `none` means no connection limit.
+  -/
+  connectionLimit : Option Std.Semaphore
+
+  /--
+  Indicates when the server has successfully shut down.
+  -/
+  shutdownPromise : Std.Channel Unit
+
+  /--
+  Configuration of the server
+  -/
+  config : Std.Http.Config
+
+namespace Server
+
+/--
+Create a new `Server` structure with an optional configuration.
+-/
+def new (config : Std.Http.Config := {}) : IO Server := do
+  let context ← Std.CancellationContext.new
+  let activeConnections ← Std.Mutex.new 0
+  let connectionLimit ←
+    if config.maxConnections = 0 then
+      pure none
+    else
+      some <$> Std.Semaphore.new config.maxConnections
+  let shutdownPromise ← Std.Channel.new
+
+  return { context, activeConnections, connectionLimit, shutdownPromise, config }
+
+/--
+Triggers cancellation of all requests and the accept loop in the server. This function should be used
+in conjunction with `waitShutdown` to properly coordinate the shutdown sequence.
+-/
+@[inline]
+def shutdown (s : Server) : Async Unit :=
+  s.context.cancel .shutdown
+
+/--
+Waits for the server to shut down. Blocks until another task or async operation calls the `shutdown` function.
+-/
+@[inline]
+def waitShutdown (s : Server) : Async Unit := do
+  Async.ofAsyncTask ((← s.shutdownPromise.recv).map Except.ok)
+
+/--
+Returns a `Selector` that waits for the server to shut down.
+-/
+@[inline]
+def waitShutdownSelector (s : Server) : Selector Unit :=
+  s.shutdownPromise.recvSelector
+
+/--
+Triggers cancellation of all requests and the accept loop, then waits for the server to fully shut down.
+This is a convenience function combining `shutdown` and then `waitShutdown`.
+-/
+@[inline]
+def shutdownAndWait (s : Server) : Async Unit := do
+  s.context.cancel .shutdown
+  s.waitShutdown
+
+@[inline]
+private def frameCancellation (s : Server) (releaseConnectionPermit : Bool := false)
+    (action : ContextAsync α) : ContextAsync α := do
+  s.activeConnections.atomically (modify (· + 1))
+  try
+    action
+  finally
+    if releaseConnectionPermit then
+      if let some limit := s.connectionLimit then
+        limit.release
+
+    s.activeConnections.atomically do
+      modify (· - 1)
+
+      if (← get) = 0 ∧ (← s.context.isCancelled) then
+        discard <| s.shutdownPromise.send ()
+
+/--
+Start a new HTTP/1.1 server on the given socket address. This function uses `Async` to handle tasks
+and TCP connections, and returns a `Server` structure that can be used to cancel the server.
+-/
+def serve {σ : Type} [Handler σ]
+    (addr : Net.SocketAddress)
+    (handler : σ)
+    (config : Config := {}) (backlog : UInt32 := 1024) : Async Server := do
+
+  let httpServer ← Server.new config
+
+  let server ← Socket.Server.mk
+  server.bind addr
+  server.listen backlog
+  server.noDelay
+
+  let runServer := do
+    frameCancellation httpServer (action := do
+      while true do
+        let permitAcquired ←
+          if let some limit := httpServer.connectionLimit then
+            let permit ← limit.acquire
+            await permit
+            pure true
+          else
+            pure false
+
+        let result ← Selectable.one #[
+          .case (server.acceptSelector) (fun x => pure <| some x),
+          .case (← ContextAsync.doneSelector) (fun _ => pure none)
+        ]
+
+        match result with
+        | some client =>
+          let extensions ← do
+            match (← EIO.toBaseIO client.getPeerName) with
+            | .ok addr => pure <| Extensions.empty.insert (Server.RemoteAddr.mk addr)
+            | .error _ => pure Extensions.empty
+
+          ContextAsync.background
+            (frameCancellation httpServer (releaseConnectionPermit := permitAcquired)
+              (action := do
+                serveConnection client handler config extensions))
+        | none =>
+          if permitAcquired then
+            if let some limit := httpServer.connectionLimit then
+              limit.release
+          break
+    )
+
+  background (runServer httpServer.context)
+
+  return httpServer
+
+end Std.Http.Server

src/Std/Internal/Http/Server/Config.lean

@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Time
+public import Std.Internal.Http.Protocol.H1
+
+public section
+
+/-!
+# Config
+
+This module exposes the `Config`, a structure that describes timeout, request and headers
+configuration of an HTTP Server.
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/--
+Connection limits configuration with validation.
+-/
+structure Config where
+  /--
+  Maximum number of simultaneous active connections (default: 1024).
+  Setting this to `0` disables the limit entirely: the server will accept any number of
+  concurrent connections and no semaphore-based cap is enforced. Use with care — an
+  unconstrained server may exhaust file descriptors or memory under adversarial load.
+  -/
+  maxConnections : Nat := 1024
+
+  /--
+  Maximum number of requests per connection.
+  -/
+  maxRequests : Nat := 100
+
+  /--
+  Maximum number of headers allowed per request.
+  -/
+  maxHeaders : Nat := 50
+
+  /--
+  Maximum aggregate byte size of all header field lines in a single message
+  (name + value bytes plus 4 bytes per line for `: ` and `\r\n`). Default: 64 KiB.
+  -/
+  maxHeaderBytes : Nat := 65536
+
+  /--
+  Timeout (in milliseconds) for receiving additional data while a request is actively being
+  processed (e.g. reading the request body). Applies after the request headers have been parsed
+  and replaces the keep-alive timeout for the duration of the request.
+  -/
+  lingeringTimeout : Time.Millisecond.Offset := 10000
+
+  /--
+  Timeout for keep-alive connections
+  -/
+  keepAliveTimeout : { x : Time.Millisecond.Offset // x > 0 } :=  ⟨12000, by decide⟩
+
+  /--
+  Maximum time (in milliseconds) allowed to receive the complete request headers after the first
+  byte of a new request arrives. This prevents Slowloris-style attacks where a client sends bytes
+  at a slow rate to hold a connection slot open without completing a request. Once a request starts,
+  each individual read must complete within this window. Default: 5 seconds.
+  -/
+  headerTimeout : Time.Millisecond.Offset := 5000
+
+  /--
+  Whether to enable keep-alive connections by default.
+  -/
+  enableKeepAlive : Bool := true
+
+  /--
+  The maximum size that the connection can receive in a single recv call.
+  -/
+  maximumRecvSize : Nat := 8192
+
+  /--
+  Default buffer size for the connection
+  -/
+  defaultPayloadBytes : Nat := 8192
+
+  /--
+  Whether to automatically generate the `Date` header in responses.
+  -/
+  generateDate : Bool := true
+
+  /--
+  The `Server` header value injected into outgoing responses.
+  `none` suppresses the header entirely.
+  -/
+  serverName : Option Header.Value := some (.mk "LeanHTTP/1.1")
+
+  /--
+  Maximum length of request URI (default: 8192 bytes)
+  -/
+  maxUriLength : Nat := 8192
+
+  /--
+  Maximum number of bytes consumed while parsing request start-lines (default: 8192 bytes).
+  -/
+  maxStartLineLength : Nat := 8192
+
+  /--
+  Maximum length of header field name (default: 256 bytes)
+  -/
+  maxHeaderNameLength : Nat := 256
+
+  /--
+  Maximum length of header field value (default: 8192 bytes)
+  -/
+  maxHeaderValueLength : Nat := 8192
+
+  /--
+  Maximum number of spaces in delimiter sequences (default: 16)
+  -/
+  maxSpaceSequence : Nat := 16
+
+  /--
+  Maximum number of leading empty lines (bare CRLF) to skip before a request-line
+  (RFC 9112 §2.2 robustness). Default: 8.
+  -/
+  maxLeadingEmptyLines : Nat := 8
+
+  /--
+  Maximum length of chunk extension name (default: 256 bytes)
+  -/
+  maxChunkExtNameLength : Nat := 256
+
+  /--
+  Maximum length of chunk extension value (default: 256 bytes)
+  -/
+  maxChunkExtValueLength : Nat := 256
+
+  /--
+  Maximum number of bytes consumed while parsing one chunk-size line with extensions (default: 8192 bytes).
+  -/
+  maxChunkLineLength : Nat := 8192
+
+  /--
+  Maximum allowed chunk payload size in bytes (default: 8 MiB).
+  -/
+  maxChunkSize : Nat := 8 * 1024 * 1024
+
+  /--
+  Maximum allowed total body size per request in bytes (default: 64 MiB).
+  -/
+  maxBodySize : Nat := 64 * 1024 * 1024
+
+  /--
+  Maximum length of reason phrase (default: 512 bytes)
+  -/
+  maxReasonPhraseLength : Nat := 512
+
+  /--
+  Maximum number of trailer headers (default: 20)
+  -/
+  maxTrailerHeaders : Nat := 20
+
+  /--
+  Maximum number of extensions on a single chunk-size line (default: 16).
+  -/
+  maxChunkExtensions : Nat := 16
+
+namespace Config
+
+/--
+Converts to HTTP/1.1 config.
+-/
+def toH1Config (config : Config) : Protocol.H1.Config where
+  maxMessages := config.maxRequests
+  maxHeaders := config.maxHeaders
+  maxHeaderBytes := config.maxHeaderBytes
+  enableKeepAlive := config.enableKeepAlive
+  agentName := config.serverName
+  maxUriLength := config.maxUriLength
+  maxStartLineLength := config.maxStartLineLength
+  maxHeaderNameLength := config.maxHeaderNameLength
+  maxHeaderValueLength := config.maxHeaderValueLength
+  maxSpaceSequence := config.maxSpaceSequence
+  maxLeadingEmptyLines := config.maxLeadingEmptyLines
+  maxChunkExtensions := config.maxChunkExtensions
+  maxChunkExtNameLength := config.maxChunkExtNameLength
+  maxChunkExtValueLength := config.maxChunkExtValueLength
+  maxChunkLineLength := config.maxChunkLineLength
+  maxChunkSize := config.maxChunkSize
+  maxBodySize := config.maxBodySize
+  maxReasonPhraseLength := config.maxReasonPhraseLength
+  maxTrailerHeaders := config.maxTrailerHeaders
+
+end Std.Http.Config

src/Std/Internal/Http/Server/Connection.lean

@@ -0,0 +1,561 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async.TCP
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Transport
+public import Std.Internal.Http.Protocol.H1
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
+
+public section
+
+namespace Std
+namespace Http
+namespace Server
+
+open Std Internal IO Async TCP Protocol
+open Time
+
+/-!
+# Connection
+
+This module defines `Server.Connection`, a structure used to handle a single HTTP connection with
+possibly multiple requests.
+-/
+
+set_option linter.all true
+
+/--
+Represents the remote address of a client connection.
+-/
+structure RemoteAddr where
+  /--
+  The socket address of the remote client.
+  -/
+  addr : Net.SocketAddress
+deriving TypeName
+
+instance : ToString RemoteAddr where
+  toString addr := toString addr.addr
+
+/--
+A single HTTP connection.
+-/
+structure Connection (α : Type) where
+  /--
+  The client connection.
+  -/
+  socket : α
+
+  /--
+  The processing machine for HTTP/1.1.
+  -/
+  machine : H1.Machine .receiving
+
+  /--
+  Extensions to attach to each request (e.g., remote address).
+  -/
+  extensions : Extensions := .empty
+
+namespace Connection
+
+/--
+Events produced by the async select loop in `receiveWithTimeout`.
+Each variant corresponds to one possible outcome of waiting for I/O.
+-/
+private inductive Recv (β : Type)
+  | bytes (x : Option ByteArray)
+  | responseBody (x : Option Chunk)
+  | bodyInterest (x : Bool)
+  | response (x : (Except Error (Response β)))
+  | timeout
+  | shutdown
+  | close
+
+/--
+The set of I/O sources to wait on during a single poll iteration.
+Each `Option` field is `none` when that source is not currently active.
+-/
+private structure PollSources (α β : Type) where
+  socket : Option α
+  expect : Option Nat
+  response : Option (Std.Channel (Except Error (Response β)))
+  responseBody : Option β
+  requestBody : Option Body.Stream
+  timeout : Millisecond.Offset
+  keepAliveTimeout : Option Millisecond.Offset
+  headerTimeout : Option Timestamp
+  connectionContext : CancellationContext
+
+/--
+Waits for the next I/O event across all active sources described by `sources`.
+Computes the socket recv size from `config`, then races all active selectables.
+Calls `Handler.onFailure` and returns `.close` on transport errors.
+-/
+private def pollNextEvent
+    {σ β : Type} [Transport α] [Handler σ] [Body β]
+    (config : Config) (handler : σ) (sources : PollSources α β)
+    : Async (Recv β) := do
+  let expectedBytes := sources.expect
+    |>.getD config.defaultPayloadBytes
+    |>.min config.maximumRecvSize
+    |>.toUInt64
+
+  let mut selectables : Array (Selectable (Recv β)) := #[
+    .case sources.connectionContext.doneSelector (fun _ => do
+      let reason ← sources.connectionContext.getCancellationReason
+      match reason with
+      | some .deadline => pure .timeout
+      | _ => pure .shutdown)
+  ]
+
+  if let some socket := sources.socket then
+    selectables := selectables.push (.case (Transport.recvSelector socket expectedBytes) (Recv.bytes · |> pure))
+
+
+    if sources.keepAliveTimeout.isNone then
+      if let some timeout := sources.headerTimeout then
+        selectables := selectables.push (.case (← Selector.sleep (timeout - (← Timestamp.now)).toMilliseconds) (fun _ => pure .timeout))
+      else
+        selectables := selectables.push (.case (← Selector.sleep sources.timeout) (fun _ => pure .timeout))
+
+  if let some responseBody := sources.responseBody then
+    selectables := selectables.push (.case (Body.recvSelector responseBody) (Recv.responseBody · |> pure))
+
+  if let some requestBody := sources.requestBody then
+    selectables := selectables.push (.case (requestBody.interestSelector) (Recv.bodyInterest · |> pure))
+
+  if let some response := sources.response then
+    selectables := selectables.push (.case response.recvSelector (Recv.response · |> pure))
+
+  try Selectable.one selectables
+  catch e =>
+    Handler.onFailure handler e
+    pure .close
+
+/--
+Handles the `Expect: 100-continue` protocol for a pending request head.
+Races between the handler's decision (`Handler.onContinue`), the connection being
+cancelled, and a lingering timeout. Returns the updated machine and whether
+`pendingHead` should be cleared (i.e. when the request is rejected).
+-/
+private def handleContinueEvent
+    {σ : Type} [Handler σ]
+    (handler : σ) (machine : H1.Machine .receiving) (head : Request.Head)
+    (config : Config) (connectionContext : CancellationContext)
+    : Async (H1.Machine .receiving × Bool) := do
+
+  let continueChannel : Std.Channel Bool ← Std.Channel.new
+  let continueTask ← Handler.onContinue handler head |>.asTask
+
+  BaseIO.chainTask continueTask fun
+    | .ok v => discard <| continueChannel.send v
+    | .error _ => discard <| continueChannel.send false
+
+  let canContinue ← Selectable.one #[
+    .case continueChannel.recvSelector pure,
+    .case connectionContext.doneSelector (fun _ => pure false),
+    .case (← Selector.sleep config.lingeringTimeout) (fun _ => pure false)
+  ]
+
+  let status := if canContinue then Status.«continue» else Status.expectationFailed
+  return (machine.canContinue status, !canContinue)
+
+/--
+Injects a `Date` header into a response head if `Config.generateDate` is set
+and the response does not already include one.
+-/
+private def prepareResponseHead (config : Config) (head : Response.Head) : Async Response.Head := do
+  if config.generateDate ∧ ¬head.headers.contains Header.Name.date then
+    let now ← Std.Time.DateTime.now (tz := .UTC)
+    return { head with headers := head.headers.insert Header.Name.date (Header.Value.ofString! now.toRFC822String) }
+  else
+    return head
+
+/--
+Applies a successful handler response to the machine.
+Optionally injects a `Date` header, records the known body size, and sends the
+response head. Returns the updated machine and the body stream to drain, or `none`
+when the body should be omitted (e.g., for HEAD requests).
+-/
+private def applyResponse
+    {β : Type} [Body β]
+    (config : Config) (machine : H1.Machine .receiving) (res : Response β)
+    : Async (H1.Machine .receiving × Option β) := do
+  let size ← Body.getKnownSize res.body
+  let machineSized :=
+    if let some knownSize := size then machine.setKnownSize knownSize
+    else machine
+  let responseHead ← prepareResponseHead config res.line
+  let machineWithHead := machineSized.send responseHead
+  if machineWithHead.writer.omitBody then
+    if ¬(← Body.isClosed res.body) then
+      Body.close res.body
+    return (machineWithHead, none)
+  else
+    return (machineWithHead, some res.body)
+
+/--
+All mutable state carried through the connection processing loop.
+Bundled into a struct so it can be passed to and returned from helper functions.
+-/
+private structure ConnectionState (β : Type) where
+  machine : H1.Machine .receiving
+  requestStream : Body.Stream
+  keepAliveTimeout : Option Millisecond.Offset
+  currentTimeout : Millisecond.Offset
+  headerTimeout : Option Timestamp
+  response : Std.Channel (Except Error (Response β))
+  respStream : Option β
+  requiresData : Bool
+  expectData : Option Nat
+  handlerDispatched : Bool
+  pendingHead : Option Request.Head
+
+/--
+Processes all H1 events from a single machine step, updating the connection state.
+Handles keep-alive resets, body-size tracking, `Expect: 100-continue`, and parse errors.
+Returns the updated state; stops early on `.failed`.
+-/
+private def processH1Events
+    {σ β : Type} [Handler σ] [Body β]
+    (handler : σ) (config : Config) (connectionContext : CancellationContext)
+    (events : Array (H1.Event .receiving))
+    (state : ConnectionState β)
+    : Async (ConnectionState β) := do
+
+  let mut st := state
+
+  for event in events do
+    match event with
+    | .needMoreData expect =>
+      st := { st with requiresData := true, expectData := expect }
+
+    | .needAnswer => pure ()
+
+    | .endHeaders head =>
+
+      -- Sets the pending head and removes the KeepAlive or Header timeout.
+      st := { st with
+        currentTimeout := config.lingeringTimeout
+        keepAliveTimeout := none
+        headerTimeout := none
+        pendingHead := some head
+      }
+
+      if let some length := head.getSize true then
+        -- Sets the size of the body that is going out of the connection.
+        Body.setKnownSize st.requestStream (some length)
+
+    | .«continue» =>
+      if let some head := st.pendingHead then
+        let (newMachine, clearPending) ← handleContinueEvent handler st.machine head config connectionContext
+        st := { st with machine := newMachine }
+        if clearPending then
+          st := { st with pendingHead := none }
+
+    | .next =>
+      -- Reset all per-request state for the next pipelined request.
+      if ¬(← Body.isClosed st.requestStream) then
+        Body.close st.requestStream
+
+      if let some res := st.respStream then
+        if ¬(← Body.isClosed res) then
+          Body.close res
+
+      let newStream ← Body.mkStream
+
+      st := { st with
+        requestStream := newStream
+        response := ← Std.Channel.new
+        respStream := none
+        keepAliveTimeout := some config.keepAliveTimeout.val
+        currentTimeout := config.keepAliveTimeout.val
+        headerTimeout := none
+        handlerDispatched := false
+      }
+
+    | .failed err =>
+      Handler.onFailure handler (toString err)
+
+      if ¬(← Body.isClosed st.requestStream) then
+        Body.close st.requestStream
+
+      st := { st with requiresData := false, pendingHead := none }
+      break
+
+    | .closeBody =>
+      if ¬(← Body.isClosed st.requestStream) then
+        Body.close st.requestStream
+
+    | .close => pure ()
+
+  return st
+
+/--
+Dispatches a pending request head to the handler if one is waiting.
+Spawns the handler as an async task and routes its result back through `state.response`.
+Returns the updated state with `pendingHead` cleared and `handlerDispatched` set.
+-/
+private def dispatchPendingRequest
+    {σ : Type} [Handler σ]
+    (handler : σ) (extensions : Extensions) (connectionContext : CancellationContext)
+    (state : ConnectionState (Handler.ResponseBody σ))
+    : Async (ConnectionState (Handler.ResponseBody σ)) := do
+  if let some line := state.pendingHead then
+
+    let task ← Handler.onRequest handler { line, body := state.requestStream, extensions } connectionContext
+      |>.asTask
+
+    BaseIO.chainTask task (discard ∘ state.response.send)
+    return { state with pendingHead := none, handlerDispatched := true }
+  else
+    return state
+
+/--
+Eagerly drains body chunks that are immediately available via `Body.tryRecv`,
+without going through the `Selectable.one` scheduler.
+
+For fully-buffered bodies (e.g. `Body.Full`) whose selector always resolves
+immediately, this eliminates two extra `Selectable.one` round-trips per response
+(one for the data chunk, one for EOF). Streaming bodies return `none` from
+`tryRecv` on the first miss and fall back to the normal poll loop unchanged.
+-/
+private def tryDrainBody [Body β]
+    (machine : H1.Machine .receiving) (body : β)
+    : Async (H1.Machine .receiving × Option β) := do
+  let mut m := machine
+  let mut result : Option β := some body
+  let mut cont := true
+  while cont do
+    match ← Body.tryRecv body with
+    | none =>
+      cont := false
+    | some (some chunk) =>
+      m := m.sendData #[chunk]
+    | some none =>
+      m := m.userClosedBody
+      if !(← Body.isClosed body) then Body.close body
+      result := none
+      cont := false
+  return (m, result)
+
+/--
+Processes a single async I/O event and updates the connection state.
+Returns the updated state and `true` if the connection should be closed immediately.
+-/
+private def handleRecvEvent
+    {σ β : Type} [Handler σ] [Body β]
+    (handler : σ) (config : Config)
+    (event : Recv β) (state : ConnectionState β)
+    : Async (ConnectionState β × Bool) := do
+
+  match event with
+  | .bytes (some bs) =>
+
+    let mut st := state
+
+    -- After the first byte after idle we switch from keep-alive timeout to per-request header timeout.
+    if st.keepAliveTimeout.isSome then
+      st := { st with
+        keepAliveTimeout := none
+        headerTimeout := some <| (← Timestamp.now) + config.headerTimeout
+      }
+
+    return ({ st with machine := st.machine.feed bs }, false)
+
+  | .bytes none =>
+    return ({ state with machine := state.machine.noMoreInput }, false)
+
+  | .responseBody (some chunk) =>
+    return ({ state with machine := state.machine.sendData #[chunk] }, false)
+
+  | .responseBody none =>
+    if let some res := state.respStream then
+      if ¬(← Body.isClosed res) then Body.close res
+    return ({ state with machine := state.machine.userClosedBody, respStream := none }, false)
+
+  | .bodyInterest interested =>
+    if interested then
+      let (newMachine, pulledChunk) := state.machine.pullBody
+      let mut st := { state with machine := newMachine }
+
+      if let some pulled := pulledChunk then
+        try st.requestStream.send pulled.chunk pulled.incomplete
+        catch e => Handler.onFailure handler e
+        if pulled.final then
+          if ¬(← Body.isClosed st.requestStream) then
+            Body.close st.requestStream
+
+      return (st, false)
+    else
+      return (state, false)
+
+  | .close => return (state, true)
+
+  | .timeout =>
+    Handler.onFailure handler "request header timeout"
+    return ({ state with machine := state.machine.closeWithError .requestTimeout, handlerDispatched := false }, false)
+
+  | .shutdown =>
+    return ({ state with machine := state.machine.closeWithError .serviceUnavailable, handlerDispatched := false }, false)
+
+  | .response (.error err) =>
+    Handler.onFailure handler err
+    return ({ state with machine := state.machine.closeWithError .internalServerError, handlerDispatched := false }, false)
+
+  | .response (.ok res) =>
+    if state.machine.failed then
+      if ¬(← Body.isClosed res.body) then Body.close res.body
+      return ({ state with handlerDispatched := false }, false)
+    else
+      let (newMachine, newRespStream) ← applyResponse config state.machine res
+
+      -- Drains all available chunks.
+      let (drainedMachine, drainedRespStream) ←
+        match newRespStream with
+        | none => pure (newMachine, none)
+        | some body => tryDrainBody newMachine body
+
+      return ({ state with machine := drainedMachine, handlerDispatched := false, respStream := drainedRespStream }, false)
+
+/--
+Computes the active `PollSources` for the current connection state.
+Determines which IO sources need attention and whether to include the socket.
+-/
+private def buildPollSources
+    {α β : Type} [Transport α]
+    (socket : α) (connectionContext : CancellationContext) (state : ConnectionState β)
+    : Async (PollSources α β) := do
+  let requestBodyOpen ←
+    if state.machine.canPullBody then pure !(← Body.isClosed state.requestStream)
+    else pure false
+
+  let requestBodyInterested ←
+    if state.machine.canPullBody ∧ requestBodyOpen then state.requestStream.hasInterest
+    else pure false
+
+  let requestBody ←
+    if state.machine.canPullBodyNow ∧ requestBodyOpen then pure (some state.requestStream)
+    else pure none
+
+  -- Include the socket only when there is more to do than waiting for the handler alone.
+  let pollSocket :=
+    state.requiresData ∨ !state.handlerDispatched ∨ state.respStream.isSome ∨
+    state.machine.writer.sentMessage ∨ (state.machine.canPullBody ∧ requestBodyInterested)
+
+  return {
+    socket := if pollSocket then some socket else none
+    expect := state.expectData
+    response := if state.handlerDispatched then some state.response else none
+    responseBody := state.respStream
+    requestBody := requestBody
+    timeout := state.currentTimeout
+    keepAliveTimeout := state.keepAliveTimeout
+    headerTimeout := state.headerTimeout
+    connectionContext := connectionContext
+  }
+
+/--
+Runs the main request/response processing loop for a single connection.
+Drives the HTTP/1.1 state machine through four phases each iteration:
+send buffered output, process H1 events, dispatch pending requests, poll for I/O.
+-/
+private def handle
+    {σ : Type} [Transport α] [h : Handler σ]
+    (connection : Connection α)
+    (config : Config)
+    (connectionContext : CancellationContext)
+    (handler : σ) : Async Unit := do
+
+  let _ : Body (Handler.ResponseBody σ) := Handler.responseBodyInstance
+
+  let socket := connection.socket
+  let initStream ← Body.mkStream
+
+  let mut state : ConnectionState (Handler.ResponseBody σ) := {
+    machine := connection.machine
+    requestStream := initStream
+    keepAliveTimeout := some config.keepAliveTimeout.val
+    currentTimeout := config.keepAliveTimeout.val
+    headerTimeout := none
+    response := ← Std.Channel.new
+    respStream := none
+    requiresData := false
+    expectData := none
+    handlerDispatched := false
+    pendingHead := none
+  }
+
+  while ¬state.machine.halted do
+
+    -- Phase 1: advance the state machine and flush any output.
+    let (newMachine, step) := state.machine.step
+    state := { state with machine := newMachine }
+
+    if step.output.size > 0 then
+      try Transport.sendAll socket step.output.data
+      catch e =>
+        Handler.onFailure handler e
+        break
+
+    -- Phase 2: process all events emitted by this step.
+    state ← processH1Events handler config connectionContext step.events state
+
+    -- Phase 3: dispatch any newly parsed request to the handler.
+    state ← dispatchPendingRequest handler connection.extensions connectionContext state
+
+    -- Phase 4: wait for the next IO event when any source needs attention.
+    if state.requiresData ∨ state.handlerDispatched ∨ state.respStream.isSome ∨ state.machine.canPullBody then
+      state := { state with requiresData := false }
+      let sources ← buildPollSources socket connectionContext state
+      let event ← pollNextEvent config handler sources
+      let (newState, shouldClose) ← handleRecvEvent handler config event state
+      state := newState
+      if shouldClose then break
+
+  -- Clean up: close all open streams and the socket.
+  if ¬(← Body.isClosed state.requestStream) then
+    Body.close state.requestStream
+
+  if let some res := state.respStream then
+    if ¬(← Body.isClosed res) then Body.close res
+
+  Transport.close socket
+
+end Connection
+
+/--
+Handles request/response processing for a single connection using an `Async` handler.
+The library-level entry point for running a server is `Server.serve`.
+This function can be used with a `TCP.Socket` or any other type that implements
+`Transport` to build custom server loops.
+
+# Example
+
+```lean
+-- Create a TCP socket server instance
+let server ← Socket.Server.mk
+server.bind addr
+server.listen backlog
+
+-- Enter an infinite loop to handle incoming client connections
+while true do
+  let client ← server.accept
+  background (serveConnection client handler config)
+```
+-/
+def serveConnection
+    {σ : Type} [Transport t] [Handler σ]
+    (client : t) (handler : σ)
+    (config : Config) (extensions : Extensions := .empty) : ContextAsync Unit := do
+  (Connection.mk client { config := config.toH1Config } extensions)
+  |>.handle config (← ContextAsync.getContext) handler
+
+end Std.Http.Server

src/Std/Internal/Http/Server/Handler.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async
+public import Std.Internal.Http.Data
+public import Std.Internal.Async.ContextAsync
+
+public section
+
+namespace Std.Http.Server
+
+open Std.Internal.IO.Async
+
+set_option linter.all true
+
+/--
+A type class for handling HTTP server requests. Implement this class to define how the server
+responds to incoming requests, failures, and `Expect: 100-continue` headers.
+-/
+class Handler (σ : Type) where
+  /--
+  Concrete body type produced by `onRequest`.
+  Defaults to `Body.Any`, but handlers may override it with any reader/writer-compatible body.
+  -/
+  ResponseBody : Type := Body.Any
+
+  /--
+  Body instance required by the connection loop for receiving response chunks.
+  -/
+  [responseBodyInstance : Body ResponseBody]
+
+  /--
+  Called for each incoming HTTP request.
+  -/
+  onRequest (self : σ) (request : Request Body.Stream) : ContextAsync (Response ResponseBody)
+
+  /--
+  Called when an I/O or transport error occurs while processing a request (e.g. broken socket,
+  handler exception). This is a **notification only**: the connection will close regardless of
+  the handler's response. Use this for logging and metrics. The default implementation does nothing.
+  -/
+  onFailure (self : σ) (error : IO.Error) : Async Unit :=
+    pure ()
+
+  /--
+  Called when a request includes an `Expect: 100-continue` header. Return `true` to send a
+  `100 Continue` response and accept the body. If `false` is returned the server sends
+  `417 Expectation Failed`, disables keep-alive, and closes the request body reader.
+  This function is guarded by `Config.lingeringTimeout` and may be cancelled on server shutdown.
+  The default implementation always returns `true`.
+  -/
+  onContinue (self : σ) (request : Request.Head) : Async Bool :=
+    pure true
+
+/--
+A stateless HTTP handler.
+-/
+structure StatelessHandler where
+  /--
+  Function called for each incoming request.
+  -/
+  onRequest : Request Body.Stream → ContextAsync (Response Body.Any)
+
+  /--
+  Function called when an I/O or transport error occurs. The default does nothing.
+  -/
+  onFailure : IO.Error → Async Unit := fun _ => pure ()
+
+  /--
+  Function called when a request includes `Expect: 100-continue`. Return `true` to accept
+  the body or `false` to reject it with `417 Expectation Failed`. The default always accepts.
+  -/
+  onContinue : Request.Head → Async Bool := fun _ => pure true
+
+instance : Handler StatelessHandler where
+  onRequest self request := self.onRequest request
+  onFailure self error := self.onFailure error
+  onContinue self request := self.onContinue request
+
+namespace Handler
+
+/--
+Builds a `StatelessHandler` from a request-handling function.
+-/
+def ofFn
+    (f : Request Body.Stream → ContextAsync (Response Body.Any)) :
+    StatelessHandler :=
+  { onRequest := f }
+
+/--
+Builds a `StatelessHandler` from all three callback functions.
+-/
+def ofFns
+    (onRequest : Request Body.Stream → ContextAsync (Response Body.Any))
+    (onFailure : IO.Error → Async Unit := fun _ => pure ())
+    (onContinue : Request.Head → Async Bool := fun _ => pure true) :
+    StatelessHandler :=
+  { onRequest, onFailure, onContinue }
+
+/--
+Builds a `StatelessHandler` from a request function and a failure callback. Useful for
+attaching error logging to a handler.
+-/
+def withFailure
+    (handler : StatelessHandler)
+    (onFailure : IO.Error → Async Unit) :
+    StatelessHandler :=
+  { handler with onFailure }
+
+/--
+Builds a `StatelessHandler` from a request function and a continue callback
+-/
+def withContinue
+    (handler : StatelessHandler)
+    (onContinue : Request.Head → Async Bool) :
+    StatelessHandler :=
+  { handler with onContinue }
+
+end Handler
+
+end Std.Http.Server

src/Std/Internal/Http/Test/Helpers.lean

@@ -0,0 +1,243 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Server
+public import Std.Internal.Async
+public import Std.Internal.Async.Timer
+import Init.Data.String.Legacy
+
+public section
+
+open Std.Internal.IO Async
+open Std Http
+
+namespace Std.Http.Internal.Test
+
+abbrev TestHandler := Request Body.Stream → ContextAsync (Response Body.Any)
+
+instance : Std.Http.Server.Handler TestHandler where
+  onRequest handler request := handler request
+
+/--
+Default config for server tests. Short lingering timeout, no Date header.
+-/
+def defaultConfig : Config :=
+  { lingeringTimeout := 1000, generateDate := false }
+
+private def sendRaw
+    (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+    (handler : TestHandler) (config : Config) : IO ByteArray :=
+  Async.block do
+    client.send raw
+    Std.Http.Server.serveConnection server handler config |>.run
+    let res ← client.recv?
+    pure (res.getD .empty)
+
+private def sendClose
+    (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+    (handler : TestHandler) (config : Config) : IO ByteArray :=
+  Async.block do
+    client.send raw
+    client.getSendChan.close
+    Std.Http.Server.serveConnection server handler config |>.run
+    let res ← client.recv?
+    pure (res.getD .empty)
+
+-- Timeout wrapper
+
+private def withTimeout {α : Type} (name : String) (ms : Nat) (action : IO α) : IO α := do
+  let task ← IO.asTask action
+  let ticks := (ms + 9) / 10
+  let rec loop : Nat → IO α
+    | 0 => do IO.cancel task; throw <| IO.userError s!"'{name}' timed out after {ms}ms"
+    | n + 1 => do
+      if (← IO.getTaskState task) == .finished then
+        match ← IO.wait task with
+        | .ok x => pure x
+        | .error e => throw e
+      else IO.sleep 10; loop n
+  loop ticks
+
+-- Test grouping
+
+/--
+Run `tests` and wrap any failure message with the group name.
+Use as `#eval runGroup "Topic" do ...`.
+-/
+def runGroup (name : String) (tests : IO Unit) : IO Unit :=
+  try tests
+  catch e => throw (IO.userError s!"[{name}]\n{e}")
+
+-- Per-test runners
+
+/--
+Create a fresh mock connection, send `raw`, and run assertions.
+-/
+def check
+    (name : String)
+    (raw : String)
+    (handler : TestHandler)
+    (expect : ByteArray → IO Unit)
+    (config : Config := defaultConfig) : IO Unit := do
+  let (client, server) ← Mock.new
+  let response ← sendRaw client server raw.toUTF8 handler config
+  try expect response
+  catch e => throw (IO.userError s!"[{name}] {e}")
+
+/--
+Like `check` but closes the client channel before running the server.
+Use for tests involving truncated input or silent-close (EOF-triggered behavior).
+-/
+def checkClose
+    (name : String)
+    (raw : String)
+    (handler : TestHandler)
+    (expect : ByteArray → IO Unit)
+    (config : Config := defaultConfig) : IO Unit := do
+  let (client, server) ← Mock.new
+  let response ← sendClose client server raw.toUTF8 handler config
+  try expect response
+  catch e => throw (IO.userError s!"[{name}] {e}")
+
+/--
+Like `check` wrapped in a wall-clock timeout.
+Required when the test involves streaming, async timers, or keep-alive behavior.
+-/
+def checkTimed
+    (name : String)
+    (ms : Nat := 2000)
+    (raw : String)
+    (handler : TestHandler)
+    (expect : ByteArray → IO Unit)
+    (config : Config := defaultConfig) : IO Unit :=
+  withTimeout name ms <| check name raw handler expect config
+
+-- Assertion helpers
+
+/--
+Assert the response starts with `prefix_` (e.g. `"HTTP/1.1 200"`).
+-/
+def assertStatus (response : ByteArray) (prefix_ : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  unless text.startsWith prefix_ do
+    throw <| IO.userError s!"expected status {prefix_.quote}, got:\n{text.quote}"
+
+/--
+Assert the response is byte-for-byte equal to `expected`.
+Use sparingly — prefer `assertStatus` + `assertContains` for 200 responses.
+-/
+def assertExact (response : ByteArray) (expected : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  unless text == expected do
+    throw <| IO.userError s!"expected:\n{expected.quote}\ngot:\n{text.quote}"
+
+/--
+Assert `needle` appears anywhere in the response.
+-/
+def assertContains (response : ByteArray) (needle : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  unless text.contains needle do
+    throw <| IO.userError s!"expected to contain {needle.quote}, got:\n{text.quote}"
+
+/--
+Assert `needle` does NOT appear in the response.
+-/
+def assertAbsent (response : ByteArray) (needle : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  if text.contains needle then
+    throw <| IO.userError s!"expected NOT to contain {needle.quote}, got:\n{text.quote}"
+
+/--
+Assert the response contains exactly `n` occurrences of `"HTTP/1.1 "`.
+-/
+def assertResponseCount (response : ByteArray) (n : Nat) : IO Unit := do
+  let text := String.fromUTF8! response
+  let got := (text.splitOn "HTTP/1.1 ").length - 1
+  unless got == n do
+    throw <| IO.userError s!"expected {n} HTTP/1.1 responses, got {got}:\n{text.quote}"
+
+-- Common fixed response strings
+
+def r400 : String :=
+  "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r408 : String :=
+  "HTTP/1.1 408 Request Timeout\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r413 : String :=
+  "HTTP/1.1 413 Content Too Large\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r417 : String :=
+  "HTTP/1.1 417 Expectation Failed\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r431 : String :=
+  "HTTP/1.1 431 Request Header Fields Too Large\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r505 : String :=
+  "HTTP/1.1 505 HTTP Version Not Supported\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+-- Standard handlers
+
+/--
+Always respond 200 "ok" without reading the request body.
+-/
+def okHandler : TestHandler := fun _ => Response.ok |>.text "ok"
+
+/--
+Read the full request body and echo it back as text/plain.
+-/
+def echoHandler : TestHandler := fun req => do
+  Response.ok |>.text (← req.body.readAll)
+
+/--
+Respond 200 with the request URI as the body.
+-/
+def uriHandler : TestHandler := fun req =>
+  Response.ok |>.text (toString req.line.uri)
+
+-- Request builder helpers
+
+/--
+Minimal GET request. `extra` is appended as raw header lines (each ending with `\x0d\n`)
+before the blank line.
+-/
+def mkGet (path : String := "/") (extra : String := "") : String :=
+  s!"GET {path} HTTP/1.1\x0d\nHost: example.com\x0d\n{extra}\x0d\n"
+
+/--
+GET with `Connection: close`.
+-/
+def mkGetClose (path : String := "/") : String :=
+  mkGet path "Connection: close\x0d\n"
+
+/--
+POST with a fixed Content-Length body. `extra` is appended before the blank line.
+-/
+def mkPost (path : String) (body : String) (extra : String := "") : String :=
+  s!"POST {path} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {body.toUTF8.size}\x0d\n{extra}\x0d\n{body}"
+
+/--
+POST with Transfer-Encoding: chunked. `chunkedBody` is the pre-formatted body
+(use `chunk` + `chunkEnd` to build it).
+-/
+def mkChunked (path : String) (chunkedBody : String) (extra : String := "") : String :=
+  s!"POST {path} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n{extra}\x0d\n{chunkedBody}"
+
+/--
+Format a single chunk: `<hex-size>\x0d\n<data>\x0d\n`.
+-/
+def chunk (data : String) : String :=
+  let hexSize := Nat.toDigits 16 data.toUTF8.size |> String.ofList
+  s!"{hexSize}\x0d\n{data}\x0d\n"
+
+/--
+The terminal zero-chunk that ends a chunked body.
+-/
+def chunkEnd : String := "0\x0d\n\x0d\n"
+
+end Std.Http.Internal.Test

src/Std/Internal/Http/Transport.lean

@@ -0,0 +1,249 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Protocol.H1
+
+public section
+
+/-!
+# Transport
+
+This module exposes a `Transport` type class that is used to represent different transport mechanisms
+that can be used with an HTTP connection.
+-/
+
+namespace Std.Http
+open Std Internal IO Async TCP
+
+set_option linter.all true
+
+/--
+Generic HTTP interface that abstracts over different transport mechanisms.
+-/
+class Transport (α : Type) where
+  /--
+  Receive data from the client connection, up to the expected size.
+  Returns None if the connection is closed or no data is available.
+  -/
+  recv : α → UInt64 → Async (Option ByteArray)
+
+  /--
+  Send all data through the client connection.
+  -/
+  sendAll : α → Array ByteArray → Async Unit
+
+  /--
+  Get a selector for receiving data asynchronously.
+  -/
+  recvSelector : α → UInt64 → Selector (Option ByteArray)
+
+  /--
+  Close the transport connection.
+  The default implementation is a no-op; override this for transports that require explicit teardown.
+  For `Socket.Client`, the runtime closes the file descriptor when the object is finalized.
+  -/
+  close : α → IO Unit := fun _ => pure ()
+
+instance : Transport Socket.Client where
+  recv client expect := client.recv? expect
+  sendAll client data := client.sendAll data
+  recvSelector client expect := client.recvSelector expect
+
+open Internal.IO.Async in
+
+/--
+Shared state for a bidirectional mock connection.
+-/
+private structure Mock.SharedState where
+  /--
+  Client to server direction.
+  -/
+  clientToServer : Std.CloseableChannel ByteArray
+
+  /--
+  Server to client direction.
+  -/
+  serverToClient : Std.CloseableChannel ByteArray
+
+/--
+Mock client endpoint for testing.
+-/
+structure Mock.Client where
+  private shared : Mock.SharedState
+
+/--
+Mock server endpoint for testing.
+-/
+structure Mock.Server where
+  private shared : Mock.SharedState
+
+namespace Mock
+
+/--
+Creates a mock server and client that are connected to each other and share the
+same underlying state, enabling bidirectional communication.
+-/
+def new : BaseIO (Mock.Client × Mock.Server) := do
+  let first ← Std.CloseableChannel.new
+  let second ← Std.CloseableChannel.new
+
+  return (⟨⟨first, second⟩⟩, ⟨⟨first, second⟩⟩)
+
+/--
+Receives data from a channel, joining all available data up to the expected size. First does a
+blocking recv, then greedily consumes available data with tryRecv until `expect` bytes are reached.
+-/
+def recvJoined (recvChan : Std.CloseableChannel ByteArray) (expect : Option UInt64) : Async (Option ByteArray) := do
+  match ← await (← recvChan.recv) with
+  | none => return none
+  | some first =>
+    let mut result := first
+    repeat
+      if let some expect := expect then
+        if result.size.toUInt64 ≥ expect then break
+
+      match ← recvChan.tryRecv with
+      | none => break
+      | some chunk => result := result ++ chunk
+    return some result
+
+/--
+Sends a single ByteArray through a channel.
+-/
+def send (sendChan : Std.CloseableChannel ByteArray) (data : ByteArray) : Async Unit := do
+  Async.ofAsyncTask ((← sendChan.send data) |>.map (Except.mapError (IO.userError ∘ toString)))
+
+/--
+Sends ByteArrays through a channel.
+-/
+def sendAll (sendChan : Std.CloseableChannel ByteArray) (data : Array ByteArray) : Async Unit := do
+  for chunk in data do
+    send sendChan chunk
+
+/--
+Creates a selector for receiving from a channel.
+-/
+def recvSelector (recvChan : Std.CloseableChannel ByteArray) : Selector (Option ByteArray) :=
+  recvChan.recvSelector
+
+end Mock
+
+namespace Mock.Client
+
+/--
+Gets the receive channel for a client (server to client direction).
+-/
+def getRecvChan (client : Mock.Client) : Std.CloseableChannel ByteArray :=
+  client.shared.serverToClient
+
+/--
+Gets the send channel for a client (client to server direction).
+-/
+def getSendChan (client : Mock.Client) : Std.CloseableChannel ByteArray :=
+  client.shared.clientToServer
+
+/--
+Sends a single ByteArray.
+-/
+def send (client : Mock.Client) (data : ByteArray) : Async Unit :=
+  Mock.send (getSendChan client) data
+
+/--
+Receives data, joining all available chunks.
+-/
+def recv? (client : Mock.Client) (expect : Option UInt64 := none) : Async (Option ByteArray) :=
+  Mock.recvJoined (getRecvChan client) expect
+
+/--
+Tries to receive data without blocking, joining all immediately available chunks.
+Returns `none` if no data is available.
+-/
+def tryRecv? (client : Mock.Client) (_expect : UInt64 := 0) : BaseIO (Option ByteArray) := do
+  match ← (getRecvChan client).tryRecv with
+  | none => return none
+  | some first =>
+    let mut result := first
+    repeat
+      match ← (getRecvChan client).tryRecv with
+      | none => break
+      | some chunk => result := result ++ chunk
+    return some result
+
+/--
+Closes the mock server and client.
+-/
+def close (client : Mock.Client) : IO Unit := do
+  if !(← client.shared.clientToServer.isClosed) then client.shared.clientToServer.close
+  if !(← client.shared.serverToClient.isClosed) then client.shared.serverToClient.close
+
+end Mock.Client
+
+namespace Mock.Server
+
+/--
+Gets the receive channel for a server (client to server direction).
+-/
+def getRecvChan (server : Mock.Server) : Std.CloseableChannel ByteArray :=
+  server.shared.clientToServer
+
+/--
+Gets the send channel for a server (server to client direction).
+-/
+def getSendChan (server : Mock.Server) : Std.CloseableChannel ByteArray :=
+  server.shared.serverToClient
+
+/--
+Sends a single ByteArray.
+-/
+def send (server : Mock.Server) (data : ByteArray) : Async Unit :=
+  Mock.send (getSendChan server) data
+
+/--
+Receives data, joining all available chunks.
+-/
+def recv? (server : Mock.Server) (expect : Option UInt64 := none) : Async (Option ByteArray) :=
+  Mock.recvJoined (getRecvChan server) expect
+
+/--
+Tries to receive data without blocking, joining all immediately available chunks. Returns `none` if no
+data is available.
+-/
+def tryRecv? (server : Mock.Server) (_expect : UInt64 := 0) : BaseIO (Option ByteArray) := do
+  match ← (getRecvChan server).tryRecv with
+  | none => return none
+  | some first =>
+    let mut result := first
+    repeat
+      match ← (getRecvChan server).tryRecv with
+      | none => break
+      | some chunk => result := result ++ chunk
+    return some result
+
+/--
+Closes the mock server and client.
+-/
+def close (server : Mock.Server) : IO Unit := do
+  if !(← server.shared.clientToServer.isClosed) then server.shared.clientToServer.close
+  if !(← server.shared.serverToClient.isClosed) then server.shared.serverToClient.close
+
+
+end Mock.Server
+
+instance : Transport Mock.Client where
+  recv client expect := Mock.recvJoined (Mock.Client.getRecvChan client) (some expect)
+  sendAll client data := Mock.sendAll (Mock.Client.getSendChan client) data
+  recvSelector client _ := Mock.recvSelector (Mock.Client.getRecvChan client)
+  close client := client.close
+
+instance : Transport Mock.Server where
+  recv server expect := Mock.recvJoined (Mock.Server.getRecvChan server) (some expect)
+  sendAll server data := Mock.sendAll (Mock.Server.getSendChan server) data
+  recvSelector server _ := Mock.recvSelector (Mock.Server.getRecvChan server)
+  close server := server.close
+
+end Std.Http

src/Std/Net/Addr.lean

@@ -124,6 +124,9 @@ end IPv4Addr
 
 namespace SocketAddressV4
 
+instance : ToString SocketAddressV4 where
+  toString sa := toString sa.addr ++ ":" ++ toString sa.port
+
 instance : Coe SocketAddressV4 SocketAddress where
   coe addr := .v4 addr
 
@@ -161,6 +164,9 @@ end IPv6Addr
 
 namespace SocketAddressV6
 
+instance : ToString SocketAddressV6 where
+  toString sa := "[" ++ toString sa.addr ++ "]:" ++ toString sa.port
+
 instance : Coe SocketAddressV6 SocketAddress where
   coe addr := .v6 addr
 
@@ -186,6 +192,11 @@ end IPAddr
 
 namespace SocketAddress
 
+instance : ToString SocketAddress where
+  toString
+    | .v4 sa => toString sa
+    | .v6 sa => toString sa
+
 /--
 Obtain the `AddressFamily` associated with a `SocketAddress`.
 -/

src/Std/Sync.lean

@@ -11,6 +11,7 @@ public import Std.Sync.Channel
 public import Std.Sync.Mutex
 public import Std.Sync.RecursiveMutex
 public import Std.Sync.Barrier
+public import Std.Sync.Semaphore
 public import Std.Sync.SharedMutex
 public import Std.Sync.Notify
 public import Std.Sync.Broadcast

src/Std/Sync/Semaphore.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Init.Data.Queue
+public import Init.System.Promise
+public import Std.Sync.Mutex
+
+public section
+
+namespace Std
+
+private structure SemaphoreState where
+  permits : Nat
+  waiters : Std.Queue (IO.Promise Unit) := ∅
+deriving Nonempty
+
+/--
+Counting semaphore.
+
+`Semaphore.acquire` returns a promise that is resolved once a permit is available.
+If a permit is currently available, the returned promise is already resolved.
+`Semaphore.release` either resolves one waiting promise or increments the available permits.
+-/
+structure Semaphore where private mk ::
+  private lock : Mutex SemaphoreState
+
+/--
+Creates a resolved promise.
+-/
+private def mkResolvedPromise [Nonempty α] (a : α) : BaseIO (IO.Promise α) := do
+  let promise ← IO.Promise.new
+  promise.resolve a
+  return promise
+
+/--
+Creates a new semaphore with `permits` initially available permits.
+-/
+def Semaphore.new (permits : Nat) : BaseIO Semaphore := do
+  return { lock := ← Mutex.new { permits } }
+
+/--
+Requests one permit.
+Returns a promise that resolves once the permit is acquired.
+-/
+def Semaphore.acquire (sem : Semaphore) : BaseIO (IO.Promise Unit) := do
+  sem.lock.atomically do
+    let st ← get
+    if st.permits > 0 then
+      set { st with permits := st.permits - 1 }
+      mkResolvedPromise ()
+    else
+      let promise ← IO.Promise.new
+      set { st with waiters := st.waiters.enqueue promise }
+      return promise
+
+/--
+Tries to acquire a permit without blocking. Returns `true` on success.
+-/
+def Semaphore.tryAcquire (sem : Semaphore) : BaseIO Bool := do
+  sem.lock.atomically do
+    let st ← get
+    if st.permits > 0 then
+      set { st with permits := st.permits - 1 }
+      return true
+    else
+      return false
+
+/--
+Releases one permit and resolves one waiting acquirer, if any.
+-/
+def Semaphore.release (sem : Semaphore) : BaseIO Unit := do
+  let waiter? ← sem.lock.atomically do
+    let st ← get
+    match st.waiters.dequeue? with
+    | some (waiter, waiters) =>
+      set { st with waiters }
+      return some waiter
+    | none =>
+      set { st with permits := st.permits + 1 }
+      return none
+  if let some waiter := waiter? then
+    waiter.resolve ()
+
+/--
+Returns the number of currently available permits.
+-/
+def Semaphore.availablePermits (sem : Semaphore) : BaseIO Nat :=
+  sem.lock.atomically do
+    return (← get).permits
+
+end Std

src/lake/Lake/Util/Family.lean

@@ -154,6 +154,7 @@ public class FamilyOut {α : Type u} {β : Type v} (f : α → β) (a : α) (b :
 -- Simplifies proofs involving open type families.
 -- Scoped to avoid slowing down `simp` in downstream projects (the discrimination
 -- tree key is `_`, so it would be attempted on every goal).
+set_option warning.simp.varHead false in
 attribute [scoped simp] FamilyOut.fam_eq
 
 public instance [FamilyDef f a b] : FamilyOut f a b where

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/runtime/io.cpp

@@ -752,6 +752,7 @@ extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezo
     u_strToUTF8(dst_name, sizeof(dst_name), &dst_name_len, tzID, tzIDLength, &status);
 
     if (U_FAILURE(status)) {
+        ucal_close(cal);
         return lean_io_result_mk_error(lean_mk_io_error_invalid_argument(EINVAL, mk_string("failed to convert DST name to UTF-8")));
     }
 
@@ -1397,7 +1398,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path() {
     memset(dest, 0, PATH_MAX);
     pid_t pid = getpid();
     snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
-    if (readlink(path, dest, PATH_MAX) == -1) {
+    if (readlink(path, dest, PATH_MAX - 1) == -1) {
         return io_result_mk_error("failed to locate application");
     } else {
         return io_result_mk_ok(mk_string(dest));

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