chore: add safety notes to release command

This PR adds two safety notes to the Claude Code release command:
- Mathlib bump branches live on `mathlib4-nightly-testing`, not the main `mathlib4` repo
- Never force-update remote refs without explicit user confirmation

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

.claude/CLAUDE.md

@@ -7,6 +7,11 @@ To build Lean you should use `make -j$(nproc) -C build/release`.
 The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
 Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
 
+To rebuild individual modules without a full build, use Lake directly:
+```
+cd src && lake build Init.Prelude
+```
+
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -56,6 +61,11 @@ make -C build/release/stage2 clean-stdlib
 ```
 must be run manually before building.
 
+To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
+```
+cd build/release/stage2 && lake build Init.Prelude
+```
+
 ## New features
 
 When asked to implement new features:

.claude/commands/release.md

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

src/CMakeLists.txt

@@ -614,6 +614,38 @@ else()
       OUTPUT_VARIABLE GIT_SHA1
       OUTPUT_STRIP_TRAILING_WHITESPACE
     )
+    # Fallback for jj workspaces where git cannot find .git directly.
+    # Use `jj git root` to find the backing git repo, then `jj log` to
+    # resolve the current workspace's commit (git HEAD points to the root
+    # workspace, not the current one).
+    if("${GIT_SHA1}" STREQUAL "")
+      find_program(JJ_EXECUTABLE jj)
+      if(JJ_EXECUTABLE)
+        execute_process(
+          COMMAND "${JJ_EXECUTABLE}" git root
+          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+          OUTPUT_VARIABLE _jj_git_dir
+          OUTPUT_STRIP_TRAILING_WHITESPACE
+          ERROR_QUIET
+          RESULT_VARIABLE _jj_git_root_result
+        )
+        execute_process(
+          COMMAND "${JJ_EXECUTABLE}" log -r @ --no-graph -T "commit_id"
+          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+          OUTPUT_VARIABLE _jj_commit
+          OUTPUT_STRIP_TRAILING_WHITESPACE
+          ERROR_QUIET
+          RESULT_VARIABLE _jj_rev_result
+        )
+        if(_jj_git_root_result EQUAL 0 AND _jj_rev_result EQUAL 0)
+          execute_process(
+            COMMAND git --git-dir "${_jj_git_dir}" ls-tree "${_jj_commit}" stage0 --object-only
+            OUTPUT_VARIABLE GIT_SHA1
+            OUTPUT_STRIP_TRAILING_WHITESPACE
+          )
+        endif()
+      endif()
+    endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
     # Now that we've prepared the information for the next stage, we can forget that we will use
     # Lake in the future as we won't use it in this stage
@@ -797,7 +829,14 @@ if(LLVM AND STAGE GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(STDLIBS Init Std Lean Leanc LeanIR)
+set(
+  STDLIBS
+  Init
+  Std
+  Lean
+  Leanc
+  LeanIR
+)
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   list(APPEND STDLIBS Lake LeanChecker)
 endif()
@@ -905,10 +944,7 @@ if(PREV_STAGE)
 endif()
 
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-  add_custom_target(leanir ALL
-    DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir
-    VERBATIM)
+  add_custom_target(leanir ALL DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir VERBATIM)
 endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution

src/Init/Grind/Util.lean

@@ -30,13 +30,13 @@ simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
 ```
 using `eq_self`.
 -/
-def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
+@[expose] def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
 
 /--
 Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
 from beta reduction during preprocessing. See `ProveEq.lean` for details.
 -/
-def abstractFn {α : Sort u} (a : α) : α := a
+@[expose] def abstractFn {α : Sort u} (a : α) : α := a
 
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b

src/Init/Notation.lean

@@ -624,6 +624,23 @@ existing code. It may be removed in a future version of the library.
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr
 
+/--
+The attribute `@[deprecated_arg old new]` marks a named parameter as deprecated.
+
+When a caller uses the old name with a replacement available, a deprecation warning is emitted
+and the argument is silently forwarded to the new parameter. When no replacement is provided,
+the parameter is treated as removed and using it produces an error.
+
+* `@[deprecated_arg old new (since := "2026-03-18")]` marks `old` as a deprecated alias for `new`.
+* `@[deprecated_arg old new "use foo instead" (since := "2026-03-18")]` adds a custom message.
+* `@[deprecated_arg old (since := "2026-03-18")]` marks `old` as a removed parameter (no replacement).
+* `@[deprecated_arg old "no longer needed" (since := "2026-03-18")]` removed with a custom message.
+
+A warning is emitted if `(since := "...")` is omitted.
+-/
+syntax (name := deprecated_arg) "deprecated_arg" ppSpace ident (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
+
 /--
 The attribute `@[suggest_for ..]` on a declaration suggests likely ways in which
 someone might **incorrectly** refer to a definition.

src/Lean/Compiler/LCNF/CoalesceRC.lean

@@ -21,7 +21,7 @@ Within a basic block, it is always safe to:
   until the later inc) and thus doing all relevant `inc` in the beginning doesn't change
   semantics.
 - Move all decrements on a variable to the last `dec` location (summing the counts). Because the
-  value is guaranteed to stay alive until at least the last `dec` anyway so a similiar argument to
+  value is guaranteed to stay alive until at least the last `dec` anyway so a similar argument to
   `inc` holds.
 
 Crucially this pass must be placed after `expandResetReuse` as that one relies on `inc`s still being

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -69,8 +69,8 @@ open ImpureType
 abbrev Mask := Array (Option FVarId)
 
 /--
-Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`.
-Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed.
+Try to erase `inc` instructions on projections of `targetId` occurring in the tail of `ds`.
+Return the updated `ds` and mask containing the `FVarId`s whose `inc` was removed.
 -/
 partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) :
     CompilerM (Array (CodeDecl .impure) × Mask) := do

src/Lean/Elab.lean

@@ -39,6 +39,7 @@ public import Lean.Elab.Extra
 public import Lean.Elab.GenInjective
 public import Lean.Elab.BuiltinTerm
 public import Lean.Elab.Arg
+public import Lean.Elab.DeprecatedArg
 public import Lean.Elab.PatternVar
 public import Lean.Elab.ElabRules
 public import Lean.Elab.Macro

src/Lean/Elab/App.lean

@@ -11,6 +11,7 @@ public import Lean.Elab.Binders
 public import Lean.Elab.RecAppSyntax
 public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
+import Lean.Elab.DeprecatedArg
 import Init.Omega
 
 public section
@@ -88,6 +89,38 @@ def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM U
 private def findBinderName? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg :=
   namedArgs.find? fun namedArg => namedArg.name == binderName
 
+/--
+If the function being applied is a constant, search `namedArgs` for an argument whose name is
+a deprecated alias of `binderName`. When `linter.deprecated.arg` is enabled (the default),
+returns `some namedArg` after emitting a deprecation warning with a code action hint. When the
+option is disabled, returns `none` (the old name falls through to the normal "invalid argument"
+error). The returned `namedArg` retains its original (old) name.
+-/
+private def findDeprecatedBinderName? (namedArgs : List NamedArg) (f : Expr) (binderName : Name) :
+    TermElabM (Option NamedArg) := do
+  unless linter.deprecated.arg.get <| ← getOptions do return .none
+  unless f.getAppFn.isConst do return none
+  let declName := f.getAppFn.constName!
+  let env ← getEnv
+  for namedArg in namedArgs do
+    if let some entry := findDeprecatedArg? env declName namedArg.name then
+      if entry.newArg? == some binderName then
+        let msg := formatDeprecatedArgMsg entry
+        let span? := namedArg.ref[1]
+        let hint ←
+          if span?.getHeadInfo matches .original .. then
+            MessageData.hint "Rename this argument:" #[{
+              suggestion := .string entry.newArg?.get!.toString
+              span?
+              toCodeActionTitle? := some fun s =>
+                s!"Rename argument `{entry.oldArg}` to `{s}`"
+            }]
+          else
+            pure .nil
+        logWarningAt namedArg.ref <| .tagged ``deprecatedArgExt msg ++ hint
+        return some namedArg
+  return none
+
 /-- Erase entry for `binderName` from `namedArgs`. -/
 def eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) : List NamedArg :=
   namedArgs.filter (·.name != binderName)
@@ -238,6 +271,23 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
     else
       for namedArg in s.namedArgs do
         let f := s.f.getAppFn
+        if f.isConst then
+          let env ← getEnv
+          if linter.deprecated.arg.get (← getOptions) then
+            if let some entry := findDeprecatedArg? env f.constName! namedArg.name then
+              if entry.newArg?.isNone then
+                let msg := formatDeprecatedArgMsg entry
+                let hint ←
+                  if namedArg.ref.getHeadInfo matches .original .. then
+                    MessageData.hint "Delete this argument:" #[{
+                      suggestion := .string ""
+                      span? := namedArg.ref
+                      toCodeActionTitle? := some fun _ =>
+                        s!"Delete deprecated argument `{entry.oldArg}`"
+                    }]
+                  else
+                    pure .nil
+                throwErrorAt namedArg.ref (msg ++ hint)
         let validNames ← getFoundNamedArgs
         let fnName? := if f.isConst then some f.constName! else none
         throwInvalidNamedArg namedArg fnName? validNames
@@ -756,13 +806,16 @@ mutual
       let binderName := fType.bindingName!
       let binfo := fType.bindingInfo!
       let s ← get
-      match findBinderName? s.namedArgs binderName with
+      let namedArg? ← match findBinderName? s.namedArgs binderName with
+        | some namedArg => pure (some namedArg)
+        | none => findDeprecatedBinderName? s.namedArgs s.f binderName
+      match namedArg? with
       | some namedArg =>
         propagateExpectedType namedArg.val
-        eraseNamedArg binderName
+        eraseNamedArg namedArg.name
         elabAndAddNewArg binderName namedArg.val
         main
-      | none          =>
+      | none =>
         unless binderName.hasMacroScopes do
           pushFoundNamedArg binderName
         match binfo with

src/Lean/Elab/BuiltinDo/If.lean

@@ -63,6 +63,6 @@ where
     doElabToSyntax "else branch of if with condition {cond}" (elabDiteBranch false) fun else_ => do
     let mγ ← mkMonadicType (← read).doBlockResultType
     match h with
-    | `(_%$tk) => Term.elabTermEnsuringType (← `(if $(⟨tk⟩):hole : $cond then $then_ else $else_)) mγ
+    | `(_%$tk) => Term.elabTermEnsuringType (← `(if _%$tk : $cond then $then_ else $else_)) mγ
     | `($h:ident) => Term.elabTermEnsuringType (← `(if $h:ident : $cond then $then_ else $else_)) mγ
     | _ => throwUnsupportedSyntax

src/Lean/Elab/Coinductive.lean

@@ -43,7 +43,7 @@ builtin_initialize
 
   Upon such rewrite, the code for adding flat inductives does not diverge much from the usual
   way its done for inductive declarations, but we omit applying attributes/modifiers and
-  we do not set the syntax references to track those declarations (as this is auxillary piece of
+  we do not set the syntax references to track those declarations (as this is auxiliary piece of
   data hidden from the user).
 
   Then, upon adding such flat inductives for each definition in the mutual block to the environment,
@@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
         | throwError "expected to be quantifier"
       let motiveMVar ← mkFreshExprMVar type
       /-
-        We intro all the indices and the occurence of the coinductive predicate
+        We intro all the indices and the occurrence of the coinductive predicate
       -/
       let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1)
       subgoal.withContext do
@@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
           -/
           let originalCasesOn := mkAppN originalCasesOn indices
           /-
-            The next argument is the occurence of the coinductive predicate.
+            The next argument is the occurrence of the coinductive predicate.
             The original `casesOn` of the flat inductive mentions it in
             unrolled form, so we need to rewrite it.
           -/
@@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T
   let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
   /-
     We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
-    form of the associated flat inductives and applying paramaters, as well as recursive calls
+    form of the associated flat inductives and applying parameters, as well as recursive calls
     (with their parameters passed).
   -/
   let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do

src/Lean/Elab/DeprecatedArg.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.EnvExtension
+public import Lean.Message
+import Lean.Elab.Term
+
+public section
+
+namespace Lean.Elab
+open Meta
+
+register_builtin_option linter.deprecated.arg : Bool := {
+  defValue := true
+  descr := "if true, generate deprecation warnings and errors for deprecated parameters"
+}
+
+/-- Entry mapping an old parameter name to a new (or no) parameter for a given declaration. -/
+structure DeprecatedArgEntry where
+  declName : Name
+  oldArg : Name
+  newArg? : Option Name := none
+  text? : Option String := none
+  since? : Option String := none
+  deriving Inhabited
+
+/-- State: `declName → (oldArg → entry)` -/
+abbrev DeprecatedArgState := NameMap (NameMap DeprecatedArgEntry)
+
+private def addDeprecatedArgEntry (s : DeprecatedArgState) (e : DeprecatedArgEntry) : DeprecatedArgState :=
+  let inner := (s.find? e.declName).getD {} |>.insert e.oldArg e
+  s.insert e.declName inner
+
+builtin_initialize deprecatedArgExt :
+    SimplePersistentEnvExtension DeprecatedArgEntry DeprecatedArgState ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := addDeprecatedArgEntry
+    addImportedFn := mkStateFromImportedEntries addDeprecatedArgEntry {}
+  }
+
+/-- Look up a deprecated argument mapping for `(declName, argName)`. -/
+def findDeprecatedArg? (env : Environment) (declName : Name) (argName : Name) :
+    Option DeprecatedArgEntry :=
+  (deprecatedArgExt.getState env |>.find? declName) >>= (·.find? argName)
+
+/-- Format the deprecation warning message for a deprecated argument. -/
+def formatDeprecatedArgMsg (entry : DeprecatedArgEntry) : MessageData :=
+  let base := match entry.newArg? with
+  | some newArg =>
+    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated, \
+      use `{newArg}` instead"
+  | none =>
+    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated"
+  match entry.text? with
+  | some text => base ++ m!": {text}"
+  | none => base
+
+builtin_initialize registerBuiltinAttribute {
+  name := `deprecated_arg
+  descr := "mark a parameter as deprecated"
+  add := fun declName stx _kind => do
+    let `(attr| deprecated_arg $oldId $[$newId?]? $[$text?]? $[(since := $since?)]?) := stx
+      | throwError "Invalid `[deprecated_arg]` attribute syntax"
+    let oldArg := oldId.getId
+    let newArg? := newId?.map TSyntax.getId
+    let text? := text?.map TSyntax.getString |>.filter (!·.isEmpty)
+    let since? := since?.map TSyntax.getString
+    let info ← getConstInfo declName
+    let paramNames ← MetaM.run' do
+      forallTelescopeReducing info.type fun xs _ =>
+        xs.mapM fun x => return (← x.fvarId!.getDecl).userName
+    if let some newArg := newArg? then
+      -- We have a replacement provided
+      unless Array.any paramNames (· == newArg) do
+        throwError "`{newArg}` is not a parameter of `{declName}`"
+      if Array.any paramNames (· == oldArg) then
+        throwError "`{oldArg}` is still a parameter of `{declName}`; \
+          rename it to `{newArg}` before adding `@[deprecated_arg]`"
+    else
+      -- We do not have a replacement provided
+      if Array.any paramNames (· == oldArg) then
+        throwError "`{oldArg}` is still a parameter of `{declName}`; \
+          remove it before adding `@[deprecated_arg]`"
+    if since?.isNone then
+      logWarning "`[deprecated_arg]` attribute should specify the date or library version \
+        at which the deprecation was introduced, using `(since := \"...\")`"
+    modifyEnv fun env => deprecatedArgExt.addEntry env {
+      declName, oldArg, newArg?, text?, since?
+    }
+}
+
+end Lean.Elab

src/Lean/Elab/DocString.lean

@@ -85,6 +85,10 @@ structure State where
   -/
   lctx : LocalContext
   /--
+  The local instances.
+
+  The `MonadLift TermElabM DocM` instance runs the lifted action with these instances, so elaboration
+  commands that mutate this state cause it to take effect in subsequent commands.
   -/
   localInstances : LocalInstances
   /--

src/Lean/LibrarySuggestions/Basic.lean

@@ -91,10 +91,10 @@ end FoldRelevantConstantsImpl
 @[implemented_by FoldRelevantConstantsImpl.foldUnsafe]
 public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n)
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n)
 
 end Lean.Expr

src/Lean/Linter/MissingDocs.lean

@@ -112,15 +112,37 @@ builtin_initialize
 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
   logLint linter.missingDocs stx m!"missing doc string for {msg}"
 
+def lintEmpty (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  logLint linter.missingDocs stx m!"empty doc string for {msg}"
+
 def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {stx.getId}"
 
+def lintEmptyNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lintEmpty stx s!"{msg} {stx.getId}"
+
 def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+def lintEmptyField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lintEmpty stx s!"{msg} {parent.getId}.{stx.getId}"
+
 def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+private def isEmptyDocString (docOpt : Syntax) : CommandElabM Bool := do
+  if docOpt.isNone then return false
+  let docStx : TSyntax `Lean.Parser.Command.docComment := ⟨docOpt[0]⟩
+  -- Verso doc comments with interpolated content cannot be extracted as plain text,
+  -- but they are clearly not empty.
+  if let .node _ `Lean.Parser.Command.versoCommentBody _ := docStx.raw[1] then
+    if !docStx.raw[1][0].isAtom then return false
+  let text ← getDocStringText docStx
+  return text.trimAscii.isEmpty
+
+def isMissingDoc (docOpt : Syntax) : CommandElabM Bool := do
+  return docOpt.isNone || (← isEmptyDocString docOpt)
+
 def hasInheritDoc (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.simple &&
@@ -130,38 +152,68 @@ def hasTacticAlt (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.tactic_alt
 
-def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
+def declModifiersDocStatus (mods : Syntax) : CommandElabM (Option Bool) := do
   let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
     mods[2][0].getKind == ``Command.public else
     mods[2][0].getKind != ``Command.private
-  return isPublic && mods[0].isNone && !hasInheritDoc mods[1]
+  if !isPublic || hasInheritDoc mods[1] then return none
+  if mods[0].isNone then return some false
+  if (← isEmptyDocString mods[0]) then return some true
+  return none
 
-def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
-  if k == ``«abbrev» then lintNamed id "public abbrev"
-  else if k == ``definition then lintNamed id "public def"
-  else if k == ``«opaque» then lintNamed id "public opaque"
-  else if k == ``«axiom» then lintNamed id "public axiom"
-  else if k == ``«inductive» then lintNamed id "public inductive"
-  else if k == ``classInductive then lintNamed id "public inductive"
-  else if k == ``«structure» then lintNamed id "public structure"
+def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
+  return (← declModifiersDocStatus mods).isSome
+
+private def lintDocStatus (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  if isEmpty then lintEmpty stx msg else lint stx msg
+
+private def lintDocStatusNamed (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  if isEmpty then lintEmptyNamed stx msg else lintNamed stx msg
+
+private def lintDocStatusField (isEmpty : Bool) (parent stx : Syntax) (msg : String) :
+    CommandElabM Unit :=
+  if isEmpty then lintEmptyField parent stx msg else lintField parent stx msg
+
+def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) (isEmpty : Bool := false) :
+    CommandElabM Unit := do
+  if k == ``«abbrev» then lintDocStatusNamed isEmpty id "public abbrev"
+  else if k == ``definition then lintDocStatusNamed isEmpty id "public def"
+  else if k == ``«opaque» then lintDocStatusNamed isEmpty id "public opaque"
+  else if k == ``«axiom» then lintDocStatusNamed isEmpty id "public axiom"
+  else if k == ``«inductive» then lintDocStatusNamed isEmpty id "public inductive"
+  else if k == ``classInductive then lintDocStatusNamed isEmpty id "public inductive"
+  else if k == ``«structure» then lintDocStatusNamed isEmpty id "public structure"
+
+private def docOptStatus (docOpt attrs : Syntax) (checkTacticAlt := false) :
+    CommandElabM (Option Bool) := do
+  if hasInheritDoc attrs then return none
+  if checkTacticAlt && hasTacticAlt attrs then return none
+  if docOpt.isNone then return some false
+  if (← isEmptyDocString docOpt) then return some true
+  return none
 
 @[builtin_missing_docs_handler declaration]
 def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``Command.private then return -- not private
   let k := rest.getKind
-  if (← declModifiersPubNoDoc head) then -- no doc string
-    lintDeclHead k rest[1][0]
+  if let some isEmpty ← declModifiersDocStatus head then
+    lintDeclHead k rest[1][0] isEmpty
   if k == ``«inductive» || k == ``classInductive then
     for stx in rest[4].getArgs do
       let head := stx[2]
-      if stx[0].isNone && (← declModifiersPubNoDoc head) then
-        lintField rest[1][0] stx[3] "public constructor"
+      -- Constructor has two doc comment positions: the leading one before `|` (stx[0])
+      -- and the one inside declModifiers (head[0]). If either is non-empty, skip.
+      let leadingEmpty ← isEmptyDocString stx[0]
+      if !stx[0].isNone && !leadingEmpty then
+        pure () -- constructor has a non-empty leading doc comment
+      else if let some modsEmpty ← declModifiersDocStatus head then
+        lintDocStatusField (leadingEmpty || modsEmpty) rest[1][0] stx[3] "public constructor"
     unless rest[5].isNone do
       for stx in rest[5][0][1].getArgs do
         let head := stx[0]
-        if (← declModifiersPubNoDoc head) then -- no doc string
-          lintField rest[1][0] stx[1] "computed field"
+        if let some isEmpty ← declModifiersDocStatus head then
+          lintDocStatusField isEmpty rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
     unless rest[4][2].isNone do
       let redecls : Std.HashSet String.Pos.Raw :=
@@ -173,45 +225,52 @@ def checkDecl : SimpleHandler := fun stx => do
               else s
             else s
       let parent := rest[1][0]
-      let lint1 stx := do
+      let lint1 isEmpty stx := do
         if let some range := stx.getRange? then
           if redecls.contains range.start then return
-        lintField parent stx "public field"
+        lintDocStatusField isEmpty parent stx "public field"
       for stx in rest[4][2][0].getArgs do
         let head := stx[0]
-        if (← declModifiersPubNoDoc head) then
+        if let some isEmpty ← declModifiersDocStatus head then
           if stx.getKind == ``structSimpleBinder then
-            lint1 stx[1]
+            lint1 isEmpty stx[1]
           else
             for stx in stx[2].getArgs do
-              lint1 stx
+              lint1 isEmpty stx
 
 @[builtin_missing_docs_handler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
-  if !stx[2].isNone && (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[2][0] "initializer"
+  if !stx[2].isNone then
+    if let some isEmpty ← declModifiersDocStatus stx[0] then
+      lintDocStatusNamed isEmpty stx[2][0] "initializer"
 
 @[builtin_missing_docs_handler «notation»]
 def checkNotation : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
-    if stx[5].isNone then lint stx[3] "notation"
-    else lintNamed stx[5][0][3] "notation"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "notation"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "notation"
 
 @[builtin_missing_docs_handler «mixfix»]
 def checkMixfix : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
-    if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal
-    else lintNamed stx[5][0][3] stx[3][0].getAtomVal
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] stx[3][0].getAtomVal
+      else lintDocStatusNamed isEmpty stx[5][0][3] stx[3][0].getAtomVal
 
 @[builtin_missing_docs_handler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "syntax"
-    else lintNamed stx[5][0][3] "syntax"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "syntax"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "syntax"
 
 def mkSimpleHandler (name : String) (declNameStxIdx := 2) : SimpleHandler := fun stx => do
-  if stx[0].isNone then
-    lintNamed stx[declNameStxIdx] name
+  if (← isMissingDoc stx[0]) then
+    if (← isEmptyDocString stx[0]) then
+      lintEmptyNamed stx[declNameStxIdx] name
+    else
+      lintNamed stx[declNameStxIdx] name
 
 @[builtin_missing_docs_handler syntaxAbbrev]
 def checkSyntaxAbbrev : SimpleHandler := mkSimpleHandler "syntax"
@@ -221,20 +280,22 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtin_missing_docs_handler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "macro"
-    else lintNamed stx[5][0][3] "macro"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "macro"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "macro"
 
 @[builtin_missing_docs_handler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "elab"
-    else lintNamed stx[5][0][3] "elab"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "elab"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "elab"
 
 @[builtin_missing_docs_handler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
-  if (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[3] "class abbrev"
+  if let some isEmpty ← declModifiersDocStatus stx[0] then
+    lintDocStatusNamed isEmpty stx[3] "class abbrev"
 
 @[builtin_missing_docs_handler Parser.Tactic.declareSimpLikeTactic]
 def checkSimpLike : SimpleHandler := mkSimpleHandler "simp-like tactic"
@@ -244,8 +305,8 @@ def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler (declNameStxId
 
 @[builtin_missing_docs_handler Option.registerOption]
 def checkRegisterOption : SimpleHandler := fun stx => do
-  if (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[2] "option"
+  if let some isEmpty ← declModifiersDocStatus stx[0] then
+    lintDocStatusNamed isEmpty stx[2] "option"
 
 @[builtin_missing_docs_handler registerSimpAttr]
 def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -99,7 +99,7 @@ where
       if (← withReducibleAndInstances <| isDefEq x val) then
         return true
       else
-        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
+        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsynthesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
         return false
     | _ =>
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"

src/Lean/Server/FileWorker/SemanticHighlighting.lean

@@ -46,7 +46,7 @@ structure LeanSemanticToken where
   stx  : Syntax
   /-- Type of the semantic token. -/
   type : SemanticTokenType
-  /-- In case of overlap, higher-priority tokens will take precendence -/
+  /-- In case of overlap, higher-priority tokens will take precedence -/
   priority : Nat := 5
 
 /-- Semantic token information with absolute LSP positions. -/
@@ -57,7 +57,7 @@ structure AbsoluteLspSemanticToken where
   tailPos : Lsp.Position
   /-- Start position of the semantic token. -/
   type    : SemanticTokenType
-  /-- In case of overlap, higher-priority tokens will take precendence -/
+  /-- In case of overlap, higher-priority tokens will take precedence -/
   priority : Nat := 5
   deriving BEq, Hashable, FromJson, ToJson
 

src/Lean/Server/Logging.lean

@@ -90,11 +90,11 @@ where
     messageMethod? msg <|> (do pending.get? (← messageId? msg))
 
 local instance : ToJson Std.Time.ZonedDateTime where
-  toJson dt := Std.Time.Formats.iso8601.format dt
+  toJson dt := dt.toISO8601String
 
 local instance : FromJson Std.Time.ZonedDateTime where
   fromJson?
-    | .str s => Std.Time.Formats.iso8601.parse s
+    | .str s => Std.Time.ZonedDateTime.fromISO8601String s
     | _ => throw "Expected string when converting JSON to Std.Time.ZonedDateTime"
 
 structure LogEntry where

src/Std/Internal/Http/Data.lean

@@ -14,6 +14,7 @@ public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Chunk
 public import Std.Internal.Http.Data.Headers
 public import Std.Internal.Http.Data.URI
+public import Std.Internal.Http.Data.Body
 
 /-!
 # HTTP Data Types

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

@@ -0,0 +1,24 @@
+/-
+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.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Length
+public import Std.Internal.Http.Data.Body.Any
+public import Std.Internal.Http.Data.Body.Stream
+public import Std.Internal.Http.Data.Body.Empty
+public import Std.Internal.Http.Data.Body.Full
+
+public section
+
+/-!
+# Body
+
+This module re-exports all HTTP body types: `Body.Empty`, `Body.Full`, `Body.Stream`,
+`Body.Any`, and `Body.Length`, along with the `Http.Body` typeclass and conversion
+utilities (`ToByteArray`, `FromByteArray`).
+-/

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

@@ -0,0 +1,83 @@
+/-
+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.Data.Body.Basic
+
+public section
+
+/-!
+# Body.Any
+
+A type-erased body backed by closures. Implements `Http.Body` and can be constructed from any
+type that also implements `Http.Body`. Used as the default handler response body type.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+A type-erased body handle. Operations are stored as closures, making it open to any body type
+that implements `Http.Body`.
+-/
+structure Any where
+
+  /--
+  Receives the next body chunk. Returns `none` at end-of-stream.
+  -/
+  recv : Async (Option Chunk)
+
+  /--
+  Closes the body stream.
+  -/
+  close : Async Unit
+
+  /--
+  Returns `true` when the body stream is closed.
+  -/
+  isClosed : Async Bool
+
+  /--
+  Selector that resolves when a chunk is available or EOF is reached.
+  -/
+  recvSelector : Selector (Option Chunk)
+
+  /--
+  Returns the declared size.
+  -/
+  getKnownSize : Async (Option Body.Length)
+
+  /--
+  Sets the size of the body.
+  -/
+  setKnownSize : Option Body.Length → Async Unit
+namespace Any
+
+/--
+Erases a body of any `Http.Body` instance into a `Body.Any`.
+-/
+def ofBody [Http.Body α] (body : α) : Any where
+  recv := Http.Body.recv body
+  close := Http.Body.close body
+  isClosed := Http.Body.isClosed body
+  recvSelector := Http.Body.recvSelector body
+  getKnownSize := Http.Body.getKnownSize body
+  setKnownSize := Http.Body.setKnownSize body
+
+end Any
+
+instance : Http.Body Any where
+  recv := Any.recv
+  close := Any.close
+  isClosed := Any.isClosed
+  recvSelector := Any.recvSelector
+  getKnownSize := Any.getKnownSize
+  setKnownSize := Any.setKnownSize
+
+end Std.Http.Body

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

@@ -0,0 +1,102 @@
+/-
+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.ContextAsync
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.Body.Length
+
+public section
+
+/-!
+# Body.Basic
+
+This module defines the `Body` typeclass for HTTP body streams, and shared conversion types
+`ToByteArray` and `FromByteArray` used for encoding and decoding body content.
+-/
+
+namespace Std.Http
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+Typeclass for values that can be read as HTTP body streams.
+-/
+class Body (α : Type) where
+  /--
+  Receives the next body chunk. Returns `none` at end-of-stream.
+  -/
+  recv : α → Async (Option Chunk)
+
+  /--
+  Closes the body stream.
+  -/
+  close : α → Async Unit
+
+  /--
+  Returns `true` when the body stream is closed.
+  -/
+  isClosed : α → Async Bool
+
+  /--
+  Selector that resolves when a chunk is available or EOF is reached.
+  -/
+  recvSelector : α → Selector (Option Chunk)
+
+  /--
+  Gets the declared size of the body.
+  -/
+  getKnownSize : α → Async (Option Body.Length)
+
+  /--
+  Sets the declared size of a body.
+  -/
+  setKnownSize : α → Option Body.Length → Async Unit
+end Std.Http
+
+namespace Std.Http.Body
+
+/--
+Typeclass for types that can be converted to a `ByteArray`.
+-/
+class ToByteArray (α : Type) where
+
+  /--
+  Transforms into a `ByteArray`.
+  -/
+  toByteArray : α → ByteArray
+
+instance : ToByteArray ByteArray where
+  toByteArray := id
+
+instance : ToByteArray String where
+  toByteArray := String.toUTF8
+
+/--
+Typeclass for types that can be decoded from a `ByteArray`. The conversion may fail with an error
+message if the bytes are not valid for the target type.
+-/
+class FromByteArray (α : Type) where
+
+  /--
+  Attempts to decode a `ByteArray` into the target type, returning an error message on failure.
+  -/
+  fromByteArray : ByteArray → Except String α
+
+instance : FromByteArray ByteArray where
+  fromByteArray := .ok
+
+instance : FromByteArray String where
+  fromByteArray bs :=
+    match String.fromUTF8? bs with
+    | some s => .ok s
+    | none => .error "invalid UTF-8 encoding"
+
+end Std.Http.Body

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

@@ -0,0 +1,116 @@
+/-
+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.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Any
+
+public section
+
+/-!
+# Body.Empty
+
+Represents an always-empty, already-closed body handle.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+An empty body handle.
+-/
+structure Empty where
+deriving Inhabited, BEq
+
+namespace Empty
+
+/--
+Receives from an empty body, always returning end-of-stream.
+-/
+@[inline]
+def recv (_ : Empty) : Async (Option Chunk) :=
+  pure none
+
+/--
+Closes an empty body (no-op).
+-/
+@[inline]
+def close (_ : Empty) : Async Unit :=
+  pure ()
+
+/--
+Empty bodies are always closed for reading.
+-/
+@[inline]
+def isClosed (_ : Empty) : Async Bool :=
+  pure true
+
+/--
+Selector that immediately resolves with end-of-stream for an empty body.
+-/
+@[inline]
+def recvSelector (_ : Empty) : Selector (Option Chunk) where
+  tryFn := pure (some none)
+  registerFn waiter := do
+    let lose := pure ()
+    let win promise := do
+      promise.resolve (.ok none)
+    waiter.race lose win
+  unregisterFn := pure ()
+
+end Empty
+
+instance : Http.Body Empty where
+  recv := Empty.recv
+  close := Empty.close
+  isClosed := Empty.isClosed
+  recvSelector := Empty.recvSelector
+  getKnownSize _ := pure (some <| .fixed 0)
+  setKnownSize _ _ := pure ()
+
+
+instance : Coe Empty Any := ⟨Any.ofBody⟩
+
+instance : Coe (Response Empty) (Response Any) where
+  coe f := { f with }
+
+instance : Coe (ContextAsync (Response Empty)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+instance : Coe (Async (Response Empty)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+end Body
+
+namespace Request.Builder
+open Internal.IO.Async
+
+/--
+Builds a request with no body.
+-/
+def empty (builder : Builder) : Async (Request Body.Empty) :=
+  pure <| builder.body {}
+
+end Request.Builder
+
+namespace Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response with no body.
+-/
+def empty (builder : Builder) : Async (Response Body.Empty) :=
+  pure <| builder.body {}
+
+end Response.Builder

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

@@ -0,0 +1,232 @@
+/-
+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.Sync
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Any
+public import Init.Data.ByteArray
+
+public section
+
+/-!
+# Body.Full
+
+A body backed by a fixed `ByteArray` held in a `Mutex`.
+
+The byte array is consumed at most once: the first call to `recv` atomically takes the data
+and returns it as a single chunk; subsequent calls return `none` (end-of-stream).
+Closing the body discards any unconsumed data.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+A body backed by a fixed, mutex-protected `ByteArray`.
+
+The data is consumed on the first read. Once consumed (or explicitly closed), the body
+behaves as a closed, empty channel.
+-/
+structure Full where
+  private mk ::
+  private state : Mutex (Option ByteArray)
+deriving Nonempty
+
+namespace Full
+
+private def takeChunk : AtomicT (Option ByteArray) Async (Option Chunk) := do
+  match ← get with
+  | none =>
+    pure none
+  | some data =>
+    set (none : Option ByteArray)
+    if data.isEmpty then
+      pure none
+    else
+      pure (some (Chunk.ofByteArray data))
+
+/--
+Creates a `Full` body from a `ByteArray`.
+-/
+def ofByteArray (data : ByteArray) : Async Full := do
+  let state ← Mutex.new (some data)
+  return { state }
+
+/--
+Creates a `Full` body from a `String`.
+-/
+def ofString (data : String) : Async Full := do
+  let state ← Mutex.new (some data.toUTF8)
+  return { state }
+
+/--
+Receives the body data. Returns the full byte array on the first call as a single chunk,
+then `none` on all subsequent calls.
+-/
+def recv (full : Full) : Async (Option Chunk) :=
+  full.state.atomically do
+    takeChunk
+
+/--
+Closes the body, discarding any unconsumed data.
+-/
+def close (full : Full) : Async Unit :=
+  full.state.atomically do
+    set (none : Option ByteArray)
+
+/--
+Returns `true` when the data has been consumed or the body has been closed.
+-/
+def isClosed (full : Full) : Async Bool :=
+  full.state.atomically do
+    return (← get).isNone
+
+/--
+Returns the known size of the remaining data.
+Returns `some (.fixed n)` with the current byte count, or `some (.fixed 0)` if the body has
+already been consumed or closed.
+-/
+def getKnownSize (full : Full) : Async (Option Body.Length) :=
+  full.state.atomically do
+    match ← get with
+    | none => pure (some (.fixed 0))
+    | some data => pure (some (.fixed data.size))
+
+/--
+Selector that immediately resolves to the remaining chunk (or EOF).
+-/
+def recvSelector (full : Full) : Selector (Option Chunk) where
+  tryFn := do
+    let chunk ← full.state.atomically do
+      takeChunk
+    pure (some chunk)
+
+  registerFn waiter := do
+    full.state.atomically do
+      let lose := pure ()
+
+      let win promise := do
+        let chunk ← takeChunk
+        promise.resolve (.ok chunk)
+
+      waiter.race lose win
+
+  unregisterFn := pure ()
+
+end Full
+
+instance : Http.Body Full where
+  recv := Full.recv
+  close := Full.close
+  isClosed := Full.isClosed
+  recvSelector := Full.recvSelector
+  getKnownSize := Full.getKnownSize
+  setKnownSize _ _ := pure ()
+
+instance : Coe Full Any := ⟨Any.ofBody⟩
+
+instance : Coe (Response Full) (Response Any) where
+  coe f := { f with }
+
+instance : Coe (ContextAsync (Response Full)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+instance : Coe (Async (Response Full)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+end Body
+
+namespace Request.Builder
+
+open Internal.IO.Async
+
+/--
+Builds a request body from raw bytes without setting any headers.
+Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
+-/
+def fromBytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) := do
+  return builder.body (← Body.Full.ofByteArray content)
+
+/--
+Builds a request with a binary body.
+Sets `Content-Type: application/octet-stream`.
+Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
+-/
+def bytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
+
+/--
+Builds a request with a text body.
+Sets `Content-Type: text/plain; charset=utf-8`.
+-/
+def text (builder : Builder) (content : String) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
+
+/--
+Builds a request with a JSON body.
+Sets `Content-Type: application/json`.
+-/
+def json (builder : Builder) (content : String) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
+
+/--
+Builds a request with an HTML body.
+Sets `Content-Type: text/html; charset=utf-8`.
+-/
+def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
+
+end Request.Builder
+
+namespace Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response body from raw bytes without setting any headers.
+Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
+-/
+def fromBytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) := do
+  return builder.body (← Body.Full.ofByteArray content)
+
+/--
+Builds a response with a binary body.
+Sets `Content-Type: application/octet-stream`.
+Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
+-/
+def bytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
+
+/--
+Builds a response with a text body.
+Sets `Content-Type: text/plain; charset=utf-8`.
+-/
+def text (builder : Builder) (content : String) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
+
+/--
+Builds a response with a JSON body.
+Sets `Content-Type: application/json`.
+-/
+def json (builder : Builder) (content : String) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
+
+/--
+Builds a response with an HTML body.
+Sets `Content-Type: text/html; charset=utf-8`.
+-/
+def html (builder : Builder) (content : String) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
+
+end Response.Builder

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

@@ -0,0 +1,60 @@
+/-
+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 Init.Data.Repr
+
+public section
+
+/-!
+# Body.Length
+
+This module defines the `Length` type, that represents the Content-Length or Transfer-Encoding
+of an HTTP request or response.
+-/
+
+namespace Std.Http.Body
+
+set_option linter.all true
+
+/--
+Size of the body of a response or request.
+-/
+inductive Length
+  /--
+  Indicates that the HTTP message body uses **chunked transfer encoding**.
+  -/
+  | chunked
+
+  /--
+  Indicates that the HTTP message body has a **fixed, known length**, as specified by the
+  `Content-Length` header.
+  -/
+  | fixed (n : Nat)
+deriving Repr, BEq
+
+namespace Length
+
+/--
+Checks if the `Length` is chunked.
+-/
+@[inline]
+def isChunked : Length → Bool
+  | .chunked => true
+  | _ => false
+
+/--
+Checks if the `Length` is a fixed size.
+-/
+@[inline]
+def isFixed : Length → Bool
+  | .fixed _ => true
+  | _ => false
+
+end Length
+
+end Std.Http.Body

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

@@ -0,0 +1,650 @@
+/-
+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.Sync
+public import Std.Internal.Async
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Any
+public import Init.Data.ByteArray
+
+public section
+
+/-!
+# Body.Stream
+
+This module defines a zero-buffer rendezvous body channel (`Body.Stream`) that supports
+both sending and receiving chunks.
+
+There is no queue and no capacity. A send waits for a receiver and a receive waits for a sender.
+At most one blocked producer and one blocked consumer are supported.
+-/
+
+namespace Std.Http
+
+namespace Body
+
+open Std Internal IO Async
+
+set_option linter.all true
+
+namespace Channel
+
+open Internal.IO.Async in
+private inductive Consumer where
+  | normal (promise : IO.Promise (Option Chunk))
+  | select (finished : Waiter (Option Chunk))
+
+private def Consumer.resolve (c : Consumer) (x : Option Chunk) : BaseIO Bool := do
+  match c with
+  | .normal promise =>
+    promise.resolve x
+    return true
+  | .select waiter =>
+    let lose := return false
+    let win promise := do
+      promise.resolve (.ok x)
+      return true
+    waiter.race lose win
+
+private structure Producer where
+  chunk : Chunk
+
+  /--
+  Resolved with `true` when consumed by a receiver, `false` when the channel closes.
+  -/
+  done : IO.Promise Bool
+
+open Internal.IO.Async in
+private def resolveInterestWaiter (waiter : Waiter Bool) (x : Bool) : BaseIO Bool := do
+  let lose := return false
+  let win promise := do
+    promise.resolve (.ok x)
+    return true
+  waiter.race lose win
+
+private structure State where
+  /--
+  A single blocked producer waiting for a receiver.
+  -/
+  pendingProducer : Option Producer
+
+  /--
+  A single blocked consumer waiting for a producer.
+  -/
+  pendingConsumer : Option Consumer
+
+  /--
+  A waiter for `Stream.interestSelector`.
+  -/
+  interestWaiter : Option (Internal.IO.Async.Waiter Bool)
+
+  /--
+  Whether the channel is closed.
+  -/
+  closed : Bool
+
+  /--
+  Known size of the stream if available.
+  -/
+  knownSize : Option Body.Length
+
+  /--
+  Buffered partial chunk data accumulated from `Stream.send ... (incomplete := true)`.
+  These partial pieces are collapsed and emitted as a single chunk on the next complete send.
+  -/
+  pendingIncompleteChunk : Option Chunk := none
+deriving Nonempty
+
+end Channel
+
+/--
+A zero-buffer rendezvous body channel that supports both sending and receiving chunks.
+-/
+structure Stream where
+  private mk ::
+  private state : Mutex Channel.State
+deriving Nonempty, TypeName
+
+/--
+Creates a rendezvous body stream.
+-/
+def mkStream : Async Stream := do
+  let state ← Mutex.new {
+    pendingProducer := none
+    pendingConsumer := none
+    interestWaiter := none
+    closed := false
+    knownSize := none
+  }
+  return { state }
+
+namespace Channel
+
+private def decreaseKnownSize (knownSize : Option Body.Length) (chunk : Chunk) : Option Body.Length :=
+  match knownSize with
+  | some (.fixed res) => some (Body.Length.fixed (res - chunk.data.size))
+  | _ => knownSize
+
+private def pruneFinishedWaiters [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
+    AtomicT State m Unit := do
+  let st ← get
+
+  let pendingConsumer ←
+    match st.pendingConsumer with
+    | some (.select waiter) =>
+      if ← waiter.checkFinished then
+        pure none
+      else
+        pure st.pendingConsumer
+    | _ =>
+      pure st.pendingConsumer
+
+  let interestWaiter ←
+    match st.interestWaiter with
+    | some waiter =>
+      if ← waiter.checkFinished then
+        pure none
+      else
+        pure st.interestWaiter
+    | none =>
+      pure none
+
+  set { st with pendingConsumer, interestWaiter }
+
+private def signalInterest [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
+    AtomicT State m Unit := do
+  let st ← get
+  if let some waiter := st.interestWaiter then
+    discard <| resolveInterestWaiter waiter true
+    set { st with interestWaiter := none }
+
+private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
+    AtomicT State m Bool := do
+  let st ← get
+  return st.pendingProducer.isSome || st.closed
+
+private def hasInterest' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
+    AtomicT State m Bool := do
+  let st ← get
+  return st.pendingConsumer.isSome
+
+private def tryRecv' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
+    AtomicT State m (Option Chunk) := do
+  let st ← get
+  if let some producer := st.pendingProducer then
+    set {
+      st with
+      pendingProducer := none
+      knownSize := decreaseKnownSize st.knownSize producer.chunk
+    }
+    discard <| producer.done.resolve true
+    return some producer.chunk
+  else
+    return none
+
+private def close' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
+    AtomicT State m Unit := do
+  let st ← get
+  if st.closed then
+    return ()
+
+  if let some consumer := st.pendingConsumer then
+    discard <| consumer.resolve none
+
+  if let some waiter := st.interestWaiter then
+    discard <| resolveInterestWaiter waiter false
+
+  if let some producer := st.pendingProducer then
+    discard <| producer.done.resolve false
+
+  set {
+    st with
+    pendingProducer := none
+    pendingConsumer := none
+    interestWaiter := none
+    pendingIncompleteChunk := none
+    closed := true
+  }
+
+end Channel
+
+namespace Stream
+
+/--
+Attempts to receive a chunk from the channel without blocking.
+Returns `some chunk` only when a producer is already waiting.
+-/
+def tryRecv (stream : Stream) : Async (Option Chunk) :=
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    Channel.tryRecv'
+
+private def recv' (stream : Stream) : BaseIO (AsyncTask (Option Chunk)) := do
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+
+    if let some chunk ← Channel.tryRecv' then
+      return AsyncTask.pure (some chunk)
+
+    let st ← get
+    if st.closed then
+      return AsyncTask.pure none
+
+    if st.pendingConsumer.isSome then
+      return Task.pure (.error (IO.Error.userError "only one blocked consumer is allowed"))
+
+    let promise ← IO.Promise.new
+    set { st with pendingConsumer := some (.normal promise) }
+    Channel.signalInterest
+    return promise.result?.map (sync := true) fun
+      | none => .error (IO.Error.userError "the promise linked to the consumer was dropped")
+      | some res => .ok res
+
+/--
+Receives a chunk from the channel. Blocks until a producer sends one.
+Returns `none` if the channel is closed and no producer is waiting.
+-/
+def recv (stream : Stream) : Async (Option Chunk) := do
+  Async.ofAsyncTask (← recv' stream)
+
+/--
+Closes the channel.
+-/
+def close (stream : Stream) : Async Unit :=
+  stream.state.atomically do
+    Channel.close'
+
+/--
+Checks whether the channel is closed.
+-/
+@[always_inline, inline]
+def isClosed (stream : Stream) : Async Bool :=
+  stream.state.atomically do
+    return (← get).closed
+
+/--
+Gets the known size if available.
+-/
+@[always_inline, inline]
+def getKnownSize (stream : Stream) : Async (Option Body.Length) :=
+  stream.state.atomically do
+    return (← get).knownSize
+
+/--
+Sets known size metadata.
+-/
+@[always_inline, inline]
+def setKnownSize (stream : Stream) (size : Option Body.Length) : Async Unit :=
+  stream.state.atomically do
+    modify fun st => { st with knownSize := size }
+
+open Internal.IO.Async in
+
+/--
+Creates a selector that resolves when a producer is waiting (or the channel closes).
+-/
+def recvSelector (stream : Stream) : Selector (Option Chunk) where
+  tryFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      if ← Channel.recvReady' then
+        return some (← Channel.tryRecv')
+      else
+        return none
+
+  registerFn waiter := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      if ← Channel.recvReady' then
+        let lose := return ()
+        let win promise := do
+          promise.resolve (.ok (← Channel.tryRecv'))
+        waiter.race lose win
+      else
+        let st ← get
+        if st.pendingConsumer.isSome then
+          throw (.userError "only one blocked consumer is allowed")
+
+        set { st with pendingConsumer := some (.select waiter) }
+        Channel.signalInterest
+
+  unregisterFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+
+/--
+Iterates over chunks until the channel closes.
+-/
+@[inline]
+protected partial def forIn
+    {β : Type} (stream : Stream) (acc : β)
+    (step : Chunk → β → Async (ForInStep β)) : Async β := do
+
+  let rec @[specialize] loop (stream : Stream) (acc : β) : Async β := do
+    if let some chunk ← stream.recv then
+      match ← step chunk acc with
+      | .done res => return res
+      | .yield res => loop stream res
+    else
+      return acc
+
+  loop stream acc
+
+/--
+Context-aware iteration over chunks until the channel closes.
+-/
+@[inline]
+protected partial def forIn'
+    {β : Type} (stream : Stream) (acc : β)
+    (step : Chunk → β → ContextAsync (ForInStep β)) : ContextAsync β := do
+
+  let rec @[specialize] loop (stream : Stream) (acc : β) : ContextAsync β := do
+    let data ← Selectable.one #[
+      .case stream.recvSelector pure,
+      .case (← ContextAsync.doneSelector) (fun _ => pure none),
+    ]
+
+    if let some chunk := data then
+      match ← step chunk acc with
+      | .done res => return res
+      | .yield res => loop stream res
+    else
+      return acc
+
+  loop stream acc
+
+/--
+Abstracts over how the next chunk is received, allowing `readAll` to work in both `Async`
+(no cancellation) and `ContextAsync` (races with cancellation via `doneSelector`).
+-/
+class NextChunk (m : Type → Type) where
+  /--
+  Receives the next chunk, stopping at EOF or (in `ContextAsync`) when the context is cancelled.
+  -/
+  nextChunk : Stream → m (Option Chunk)
+
+instance : NextChunk Async where
+  nextChunk := Stream.recv
+
+instance : NextChunk ContextAsync where
+  nextChunk stream := do
+    Selectable.one #[
+      .case stream.recvSelector pure,
+      .case (← ContextAsync.doneSelector) (fun _ => pure none),
+    ]
+
+/--
+Reads all remaining chunks and decodes them into `α`.
+
+Works in both `Async` (reads until EOF, no cancellation) and `ContextAsync` (also stops if the
+context is cancelled).
+-/
+partial def readAll
+    [FromByteArray α]
+    [Monad m] [MonadExceptOf IO.Error m] [NextChunk m]
+    (stream : Stream)
+    (maximumSize : Option UInt64 := none) :
+    m α := do
+
+  let rec loop (result : ByteArray) : m ByteArray := do
+    match ← NextChunk.nextChunk stream with
+    | none => return result
+    | some chunk =>
+      let result := result ++ chunk.data
+      if let some max := maximumSize then
+        if result.size.toUInt64 > max then
+          throw (.userError s!"body exceeded maximum size of {max} bytes")
+      loop result
+
+  let result ← loop ByteArray.empty
+
+  match FromByteArray.fromByteArray result with
+  | .ok a => return a
+  | .error msg => throw (.userError msg)
+
+private def collapseForSend
+    (stream : Stream)
+    (chunk : Chunk)
+    (incomplete : Bool) : BaseIO (Except IO.Error (Option Chunk)) := do
+
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    let st ← get
+
+    if st.closed then
+      return .error (.userError "channel closed")
+
+    let merged := match st.pendingIncompleteChunk with
+      | some pending =>
+        {
+          data := pending.data ++ chunk.data
+          extensions := if pending.extensions.isEmpty then chunk.extensions else pending.extensions
+        }
+      | none => chunk
+
+    if incomplete then
+      set { st with pendingIncompleteChunk := some merged }
+      return .ok none
+    else
+      set { st with pendingIncompleteChunk := none }
+      return .ok (some merged)
+
+/--
+Sends a chunk, retrying if a select-mode consumer races and loses. If no consumer is ready,
+installs the chunk as a pending producer and awaits acknowledgement from the receiver.
+-/
+private partial def send' (stream : Stream) (chunk : Chunk) : Async Unit := do
+  let done ← IO.Promise.new
+  let result : Except IO.Error (Option Bool) ← stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    let st ← get
+
+    if st.closed then
+      return .error (IO.Error.userError "channel closed")
+
+    if let some consumer := st.pendingConsumer then
+      let success ← consumer.resolve (some chunk)
+
+      if success then
+        set {
+          st with
+          pendingConsumer := none
+          knownSize := Channel.decreaseKnownSize st.knownSize chunk
+        }
+        return .ok (some true)
+      else
+        set { st with pendingConsumer := none }
+        return .ok (some false)
+    else if st.pendingProducer.isSome then
+      return .error (IO.Error.userError "only one blocked producer is allowed")
+    else
+      set { st with pendingProducer := some { chunk, done } }
+      return .ok none
+
+  match result with
+  | .error err =>
+    throw err
+  | .ok (some true) =>
+    return ()
+  | .ok (some false) =>
+    -- The select-mode consumer raced and lost; recurse to allocate a fresh `done` promise.
+    send' stream chunk
+  | .ok none =>
+    match ← await done.result? with
+    | some true => return ()
+    | _ => throw (IO.Error.userError "channel closed")
+
+/--
+Sends a chunk.
+
+If `incomplete := true`, the chunk is buffered and collapsed with subsequent chunks, and is not
+delivered to the receiver yet.
+If `incomplete := false`, any buffered incomplete pieces are collapsed with this chunk and the
+single merged chunk is sent.
+-/
+def send (stream : Stream) (chunk : Chunk) (incomplete : Bool := false) : Async Unit := do
+  match (← collapseForSend stream chunk incomplete) with
+  | .error err => throw err
+  | .ok none => pure ()
+  | .ok (some toSend) =>
+    if toSend.data.isEmpty ∧ toSend.extensions.isEmpty then
+      return ()
+
+    send' stream toSend
+
+/--
+Returns `true` when a consumer is currently blocked waiting for data.
+-/
+def hasInterest (stream : Stream) : Async Bool :=
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    Channel.hasInterest'
+
+open Internal.IO.Async in
+/--
+Creates a selector that resolves when consumer interest is present.
+Returns `true` when a consumer is waiting, `false` when the channel closes first.
+-/
+def interestSelector (stream : Stream) : Selector Bool where
+  tryFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      let st ← get
+      if st.pendingConsumer.isSome then
+        return some true
+      else if st.closed then
+        return some false
+      else
+        return none
+
+  registerFn waiter := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      let st ← get
+
+      if st.pendingConsumer.isSome then
+        let lose := return ()
+        let win promise := do
+          promise.resolve (.ok true)
+        waiter.race lose win
+      else if st.closed then
+        let lose := return ()
+        let win promise := do
+          promise.resolve (.ok false)
+        waiter.race lose win
+      else if st.interestWaiter.isSome then
+        throw (.userError "only one blocked interest selector is allowed")
+      else
+        set { st with interestWaiter := some waiter }
+
+  unregisterFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+
+end Stream
+
+/--
+Creates a body from a producer function.
+Returns the stream immediately and runs `gen` in a detached task.
+The channel is always closed when `gen` returns or throws.
+Errors from `gen` are not rethrown here; consumers observe end-of-stream via `recv = none`.
+-/
+def stream (gen : Stream → Async Unit) : Async Stream := do
+  let s ← mkStream
+  background <| do
+    try
+      gen s
+    finally
+      s.close
+  return s
+
+/--
+Creates a body from a fixed byte array.
+-/
+def fromBytes (content : ByteArray) : Async Stream := do
+  stream fun s => do
+    s.setKnownSize (some (.fixed content.size))
+    if content.size > 0 then
+      s.send (Chunk.ofByteArray content)
+
+/--
+Creates an empty `Stream` body channel (already closed, no data).
+
+Prefer `Body.Empty` when you need a concrete zero-cost type. Use this when the calling
+context requires a `Stream` specifically.
+-/
+def empty : Async Stream := do
+  let s ← mkStream
+  s.setKnownSize (some (.fixed 0))
+  s.close
+  return s
+
+instance : ForIn Async Stream Chunk where
+  forIn := Stream.forIn
+
+instance : ForIn ContextAsync Stream Chunk where
+  forIn := Stream.forIn'
+
+instance : Http.Body Stream where
+  recv := Stream.recv
+  close := Stream.close
+  isClosed := Stream.isClosed
+  recvSelector := Stream.recvSelector
+  getKnownSize := Stream.getKnownSize
+  setKnownSize := Stream.setKnownSize
+
+instance : Coe Stream Any := ⟨Any.ofBody⟩
+
+instance : Coe (Response Stream) (Response Any) where
+  coe f := { f with }
+
+instance : Coe (ContextAsync (Response Stream)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+instance : Coe (Async (Response Stream)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+end Body
+
+namespace Request.Builder
+
+open Internal.IO.Async
+
+/--
+Builds a request with a streaming body generator.
+-/
+def stream
+    (builder : Builder)
+    (gen : Body.Stream → Async Unit) :
+    Async (Request Body.Stream) := do
+  let s ← Body.stream gen
+  return Request.Builder.body builder s
+
+end Request.Builder
+
+namespace Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response with a streaming body generator.
+-/
+def stream
+    (builder : Builder)
+    (gen : Body.Stream → Async Unit) :
+    Async (Response Body.Stream) := do
+  let s ← Body.stream gen
+  return Response.Builder.body builder s
+
+end Response.Builder

src/Std/Internal/Http/Data/Request.lean

@@ -124,12 +124,6 @@ def new : Builder := { }
 
 namespace Builder
 
-/--
-Creates a new HTTP request builder with the default head
-(method: GET, version: HTTP/1.1, target: `*`).
--/
-def empty : Builder := { }
-
 /--
 Sets the HTTP method for the request being built.
 -/

src/Std/Internal/Http/Data/Response.lean

@@ -111,7 +111,7 @@ namespace Builder
 /--
 Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
 -/
-def empty : Builder := { }
+def new : Builder := { }
 
 /--
 Sets the HTTP status code for the response being built.
@@ -173,66 +173,66 @@ end Builder
 Creates a new HTTP Response builder with the 200 status code.
 -/
 def ok : Builder :=
-  .empty |>.status .ok
+  .new |>.status .ok
 
 /--
 Creates a new HTTP Response builder with the provided status.
 -/
 def withStatus (status : Status) : Builder :=
-  .empty |>.status status
+  .new |>.status status
 
 /--
 Creates a new HTTP Response builder with the 404 status code.
 -/
 def notFound : Builder :=
-  .empty |>.status .notFound
+  .new |>.status .notFound
 
 /--
 Creates a new HTTP Response builder with the 500 status code.
 -/
 def internalServerError : Builder :=
-  .empty |>.status .internalServerError
+  .new |>.status .internalServerError
 
 /--
 Creates a new HTTP Response builder with the 400 status code.
 -/
 def badRequest : Builder :=
-  .empty |>.status .badRequest
+  .new |>.status .badRequest
 
 /--
 Creates a new HTTP Response builder with the 201 status code.
 -/
 def created : Builder :=
-  .empty |>.status .created
+  .new |>.status .created
 
 /--
 Creates a new HTTP Response builder with the 202 status code.
 -/
 def accepted : Builder :=
-  .empty |>.status .accepted
+  .new |>.status .accepted
 
 /--
 Creates a new HTTP Response builder with the 401 status code.
 -/
 def unauthorized : Builder :=
-  .empty |>.status .unauthorized
+  .new |>.status .unauthorized
 
 /--
 Creates a new HTTP Response builder with the 403 status code.
 -/
 def forbidden : Builder :=
-  .empty |>.status .forbidden
+  .new |>.status .forbidden
 
 /--
 Creates a new HTTP Response builder with the 409 status code.
 -/
 def conflict : Builder :=
-  .empty |>.status .conflict
+  .new |>.status .conflict
 
 /--
 Creates a new HTTP Response builder with the 503 status code.
 -/
 def serviceUnavailable : Builder :=
-  .empty |>.status .serviceUnavailable
+  .new |>.status .serviceUnavailable
 
 end Response

src/Std/Internal/Http/Data/URI.lean

@@ -94,4 +94,3 @@ def parseOrRoot (s : String) : Std.Http.URI.Path :=
   parse? s |>.getD { segments := #[], absolute := true }
 
 end Std.Http.URI.Path
-

src/Std/Time.lean

@@ -17,7 +17,8 @@ public import Std.Time.Zoned.Database
 
 public section
 
-namespace Std.Time
+namespace Std
+namespace Time
 
 /-!
 # Time
@@ -129,30 +130,23 @@ Represents spans of time and the difference between two points in time.
 # Formats
 
 Format strings are used to convert between `String` representations and date/time types, like `yyyy-MM-dd'T'HH:mm:ss.sssZ`.
-The table below shows the available format specifiers. Repeating a pattern character may change the
-text style, minimum width, or offset/fraction form, depending on the field.
+The table below shows the available format specifiers. Some specifiers can be repeated to control truncation or offsets.
+When a character is repeated `n` times, it usually truncates the value to `n` characters.
 
-The current Lean implementation follows Java's pattern language where practical, but it is not fully
-locale-sensitive. Text forms currently use English data, and localized weekday/week-of-month fields use
-the library's fixed Monday-first interpretation.
-
-For numeric fields that accept both one- and two-letter forms, the single-letter form parses a
-non-padded number and the two-letter form parses a zero-padded width of two.
+The `number` type format specifiers, such as `h` and `K`, are parsed based on the number of repetitions.
+If the repetition count is one, the format allows values ranging from 1 up to the maximum capacity of
+the respective data type.
 
 The supported formats include:
-- `G`: Represents the era, such as BCE (Before Common Era) or CE (Common Era).
-  - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "CE").
-  - `GGGG` (full): Displays the era in a full format (e.g., "Common Era").
-  - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "C").
+- `G`: Represents the era, such as AD (Anno Domini) or BC (Before Christ).
+  - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "AD").
+  - `GGGG` (full): Displays the era in a full format (e.g., "Anno Domini").
+  - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "A").
 - `y`: Represents the year of the era.
   - `y`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678").
   - `yy`: Displays the year in a two-digit format, showing the last two digits (e.g., "04" for 2004).
   - `yyyy`: Displays the year in a four-digit format (e.g., "2004").
   - `yyyy+`: Extended format for years with more than four digits.
-- `Y`: Represents the week-based year (ISO-like behavior around year boundaries).
-  - `Y`, `YYY`, `YYYY`: Displays the week-based year (e.g., "2017").
-  - `YY`: Displays the last two digits of the week-based year (e.g., "17").
-  - `YYYYY+`: Extended format for week-based years with more than four digits.
 - `u`: Represents the year.
   - `u`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678").
   - `uu`: Two-digit year format, showing the last two digits (e.g., "04" for 2004).
@@ -164,94 +158,69 @@ The supported formats include:
   - `MMM`: Displays the abbreviated month name (e.g., "Jul").
   - `MMMM`: Displays the full month name (e.g., "July").
   - `MMMMM`: Displays the month in a narrow form (e.g., "J" for July).
-- `L`: Represents the standalone month of the year.
-  - Supports the same widths as `M`; in the current English data it formats the same values.
 - `d`: Represents the day of the month.
 - `Q`: Represents the quarter of the year.
   - `Q`, `QQ`: Displays the quarter as a number (e.g., "3", "03").
   - `QQQ` (short): Displays the quarter as an abbreviated text (e.g., "Q3").
   - `QQQQ` (full): Displays the full quarter text (e.g., "3rd quarter").
   - `QQQQQ` (narrow): Displays the quarter as a short number (e.g., "3").
-- `q`: Represents the standalone quarter of the year.
-  - Supports the same widths as `Q`; in the current English data it formats the same values.
 - `w`: Represents the week of the week-based year, each week starts on Monday (e.g., "27").
-- `W`: Represents the week of the month using the library's fixed Monday-first week model (e.g., "2").
+- `W`: Represents the week of the month, each week starts on Monday (e.g., "4").
 - `E`: Represents the day of the week as text.
   - `E`, `EE`, `EEE`: Displays the abbreviated weekday name (e.g., "Tue").
   - `EEEE`: Displays the full day name (e.g., "Tuesday").
   - `EEEEE`: Displays the narrow day name (e.g., "T" for Tuesday).
-  - `EEEEEE`: Displays the short two-letter weekday name (e.g., "Tu").
 - `e`: Represents the weekday as number or text.
   - `e`, `ee`: Displays the weekday as a number, starting from 1 (Monday) to 7 (Sunday).
   - `eee`, `eeee`, `eeeee`: Displays the weekday as text (same format as `E`).
-  - `eeeeee`: Displays the short two-letter weekday name (e.g., "Tu").
-- `c`: Standalone weekday.
-  - `c`: Displays the numeric weekday using the same Monday-to-Sunday numbering as `e`.
-  - `ccc`, `cccc`, `ccccc`: Display standalone text (same values as `e` in the current English data).
-  - `cccccc`: Displays the short two-letter weekday name (e.g., "Tu").
-- `F`: Represents the occurrence of the weekday within the month (e.g., the 2nd Sunday formats as `2`).
+- `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3").
 - `a`: Represents the AM or PM designation of the day.
-  - `a`, `aa`, `aaa`: Displays AM/PM (e.g., "PM").
-  - `aaaa`: Displays the full form (e.g., "ante meridiem", "post meridiem").
-  - `aaaaa`: Displays the narrow form (e.g., "a", "p").
-- `b`: Represents the day period, extending AM/PM with noon and midnight (TR35 §4, supported in Java 16+). The `B` symbol (flexible day periods) is not supported.
-  - `b`, `bb`, `bbb`: Displays a short form (e.g., "AM", "PM", "noon", "midnight").
-  - `bbbb`: Displays a full form (e.g., "ante meridiem", "post meridiem", "noon", "midnight"); unlike `a`, the AM/PM spellings are lowercase here.
-  - `bbbbb`: Displays a narrow form (e.g., "a", "p", "n", "mi").
+  - `a`, `aa`, `aaa`: Displays AM or PM in a concise format (e.g., "PM").
+  - `aaaa`: Displays the full AM/PM designation (e.g., "Post Meridium").
 - `h`: Represents the hour of the AM/PM clock (1-12) (e.g., "12").
-  - `h`, `hh` are supported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `K`: Represents the hour of the AM/PM clock (0-11) (e.g., "0").
-  - `K`, `KK` are supported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `k`: Represents the hour of the day in a 1-24 format (e.g., "24").
-  - `k`, `kk` are supported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `H`: Represents the hour of the day in a 0-23 format (e.g., "0").
-  - `H`, `HH` are supported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `m`: Represents the minute of the hour (e.g., "30").
-  - `m`, `mm` are supported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `s`: Represents the second of the minute (e.g., "55").
-  - `s`, `ss` are supported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `S`: Represents a fraction of a second, typically displayed as a decimal number (e.g., "978" for milliseconds).
-  - One or more repetitions of the character truncates to the specified number of most-significant digits; it does not round.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `A`: Represents the millisecond of the day (e.g., "1234").
-  - One or more repetitions of the character indicates zero-padding to the specified number of characters (no truncation is applied).
-- `n`: Represents the nanosecond of the second (e.g., "987654321"). This is a Lean/Java extension, not a TR35 field.
-  - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated.
-- `N`: Represents the nanosecond of the day (e.g., "1234000000"). This is a Lean/Java extension, not a TR35 field.
-  - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated.
-- `V`: Time zone ID.
-  - `VV`: Displays the zone identifier/name.
-  - Other counts are unsupported, matching Java.
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `n`: Represents the nanosecond of the second (e.g., "987654321").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `N`: Represents the nanosecond of the day (e.g., "1234000000").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `VV`: Represents the time zone ID, which could be a city-based zone (e.g., "America/Los_Angeles"), a UTC marker (`"Z"`), or a specific offset (e.g., "-08:30").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `z`: Represents the time zone name.
-  - `z`, `zz`, `zzz`: Shows a short zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "UTC", otherwise the abbreviation (e.g., "PST").
-  - `zzzz`: Displays the full zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "Coordinated Universal Time", otherwise the full zone name (e.g., "Pacific Standard Time").
-- `v`: Generic time zone name.
-  - `v`: In the current Lean timezone data this displays the stored abbreviation; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "UTC".
-  - `vvvv`: In the current Lean timezone data this displays the stored zone name/ID; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "Coordinated Universal Time".
+  - `z`, `zz`, `zzz`: Shows an abbreviated time zone name (e.g., "PST" for Pacific Standard Time).
+  - `zzzz`: Displays the full time zone name (e.g., "Pacific Standard Time").
 - `O`: Represents the localized zone offset in the format "GMT" followed by the time difference from UTC.
-  - `O`: Displays the GMT offset in a short format (e.g., "GMT+8"), or "GMT" for UTC.
-  - `OOOO`: Displays the full GMT offset with padded hour and minutes (e.g., "GMT+08:00"), or "GMT" for UTC.
+  - `O`: Displays the GMT offset in a simple format (e.g., "GMT+8").
+  - `OOOO`: Displays the full GMT offset, including hours and minutes (e.g., "GMT+08:00").
 - `X`: Represents the zone offset. It uses 'Z' for UTC and can represent any offset (positive or negative).
-  - `X`: Displays hour and optional minute offset (e.g., "-08", "-0830", or "Z").
+  - `X`: Displays the hour offset (e.g., "-08").
   - `XX`: Displays the hour and minute offset without a colon (e.g., "-0830").
   - `XXX`: Displays the hour and minute offset with a colon (e.g., "-08:30").
-  - `XXXX`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "-0830", "-083045").
-  - `XXXXX`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "-08:30", "-08:30:45").
-- `x`: Represents the zone offset. Similar to `X`, but never displays `'Z'` for UTC.
-  - `x`: Displays hour and optional minute offset (e.g., "+00", "+0530").
+  - `XXXX`: Displays the hour, minute, and second offset without a colon (e.g., "-083045").
+  - `XXXXX`: Displays the hour, minute, and second offset with a colon (e.g., "-08:30:45").
+- `x`: Represents the zone offset. Similar to X, but does not display 'Z' for UTC and focuses only on positive offsets.
+  - `x`: Displays the hour offset (e.g., "+08").
   - `xx`: Displays the hour and minute offset without a colon (e.g., "+0830").
   - `xxx`: Displays the hour and minute offset with a colon (e.g., "+08:30").
-  - `xxxx`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "+0830", "+083045").
-  - `xxxxx`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "+08:30", "+08:30:45").
-- `Z`: Represents the zone offset in RFC/CLDR `Z` forms.
-  - `Z`, `ZZ`, `ZZZ`: Displays hour and minute offset without colon, with optional seconds (e.g., "+0800", "+083045").
-  - `ZZZZ`: Displays localized GMT form (e.g., "GMT+08:00").
-  - `ZZZZZ`: Displays hour and minute offset with a colon and optional seconds, and uses `"Z"` for UTC (e.g., "Z", "+08:30", "+08:30:45").
-# Runtime Parsing
-
-- `ZonedDateTime.parse` parses common zoned date-time formats with explicit offsets, but does not resolve timezone identifiers like `[Europe/Paris]`.
-- `ZonedDateTime.parseIO` resolves identifier-based inputs via the default timezone database.
-- `ZonedDateTime.fromLeanDateTimeWithIdentifierString` is pure and does not perform timezone database resolution.
-- `ZonedDateTime.fromLeanDateTimeWithIdentifierStringIO` resolves identifiers using the default timezone database.
+  - `xxxx`: Displays the hour, minute, and second offset without a colon (e.g., "+083045").
+  - `xxxxx`: Displays the hour, minute, and second offset with a colon (e.g., "+08:30:45").
+- `Z`: Always includes an hour and minute offset and may use 'Z' for UTC, providing clear differentiation between UTC and other time zones.
+  - `Z`: Displays the hour and minute offset without a colon (e.g., "+0800").
+  - `ZZ`: Displays "GMT" followed by the time offset (e.g., "GMT+08:00" or "Z").
+  - `ZZZ`: Displays the full hour, minute, and second offset with a colon (e.g., "+08:30:45" or "Z").
 
 # Macros
 
@@ -265,10 +234,8 @@ The `.sssssssss` can be omitted in most cases.
 - **`offset("+HH:mm")`**: Represents a timezone offset in the format `+HH:mm`, where `+` or `-` indicates the direction from UTC.
 - **`timezone("NAME/ID ZZZ")`**: Specifies a timezone using a region-based name or ID, along with its associated offset.
 - **`datespec("FORMAT")`**: Defines a compile-time date format based on the provided string.
-- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZZZ")`**: Represents a `ZonedDateTime` with a fixed timezone and optional nanosecond precision.
+- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZ")`**: Represents a `ZonedDateTime` with a fixed timezone and optional nanosecond precision.
 - **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss[IDENTIFIER]")`**: Defines an `IO ZonedDateTime`, where the timezone identifier is dynamically retrieved from the default timezone database.
 - **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss, timezone")`**: Represents an `IO ZonedDateTime`, using a specified `timezone` term and allowing optional nanoseconds.
 
 -/
-
-end Std.Time

src/Std/Time/Date/PlainDate.lean

@@ -355,28 +355,6 @@ def weekOfYear (date : PlainDate) : Week.Ordinal :=
     let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
     w
 
-/--
-Returns the week-based year for a given `PlainDate`.
--/
-def weekBasedYear (date : PlainDate) : Year.Offset :=
-  let year := date.year
-  let doy  := date.dayOfYear
-  let dow  := date.weekday.toOrdinal.sub 1
-
-  if doy.val ≤ 3 then
-    if doy.val - dow.val < -2 then
-      year - 1
-    else
-      year
-  else if doy.val ≥ 363 then
-    let leap := if date.inLeapYear then 1 else 0
-    if (doy.val - 363 - leap) - dow.val ≥ 0 then
-      year + 1
-    else
-      year
-  else
-    year
-
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays
 

src/Std/Time/DateTime/PlainDateTime.lean

@@ -502,11 +502,6 @@ def weekOfMonth (date : PlainDateTime) : Bounded.LE 1 5 :=
   date.date.weekOfMonth
 
 /--
-Returns the week-based year for a given `PlainDateTime`.
--/
-def weekBasedYear (date : PlainDateTime) : Year.Offset :=
-  date.date.weekBasedYear
-/--
 Determines the week of the month for the given `PlainDateTime`. The week of the month is calculated based
 on the day of the month and the weekday. Each week starts on Monday because the entire library is
 based on the Gregorian Calendar.

src/Std/Time/Format.lean

@@ -23,207 +23,144 @@ set_option linter.all true
 The ISO 8601 format, used for representing date and time in a standardized
 format. The format follows the pattern `uuuu-MM-dd'T'HH:mm:ssXXX`.
 -/
-def iso8601 : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssXXX")
+def iso8601 : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssXXX")
+
 
 /--
 The americanDate format, which follows the pattern `MM-dd-uuuu`.
 -/
-def americanDate : Format Awareness.any := datespec("MM-dd-uuuu")
+def americanDate : GenericFormat .any := datespec("MM-dd-uuuu")
 
 /--
 The europeanDate format, which follows the pattern `dd-MM-uuuu`.
 -/
-def europeanDate : Format Awareness.any := datespec("dd-MM-uuuu")
+def europeanDate : GenericFormat .any := datespec("dd-MM-uuuu")
 
 /--
-The time12Hour format, which follows the pattern `hh:mm:ss a` for representing time
+The time12Hour format, which follows the pattern `hh:mm:ss aa` for representing time
 in a 12-hour clock format with an upper case AM/PM marker.
 -/
-def time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
+def time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
 
 /--
 The Time24Hour format, which follows the pattern `HH:mm:ss` for representing time
 in a 24-hour clock format.
 -/
-def time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def time24Hour : GenericFormat .any := datespec("HH:mm:ss")
 
 /--
 The DateTimeZone24Hour format, which follows the pattern `uuuu-MM-dd:HH:mm:ss.SSSSSSSSS` for
 representing date, time, and time zone.
 -/
-def dateTime24Hour : Format (.only .GMT) := datespec("uuuu-MM-dd:HH:mm:ss.SSSSSSSSS")
+def dateTime24Hour : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd:HH:mm:ss.SSSSSSSSS")
 
 /--
 The DateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ`
 for representing date, time, and time zone.
 -/
-def dateTimeWithZone : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ")
+def dateTimeWithZone : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ")
 
 /--
 The leanTime24Hour format, which follows the pattern `HH:mm:ss.SSSSSSSSS` for representing time
 in a 24-hour clock format. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanTime24Hour : Format Awareness.any := datespec("HH:mm:ss.SSSSSSSSS")
+def leanTime24Hour : GenericFormat .any := datespec("HH:mm:ss.SSSSSSSSS")
 
 /--
 The leanTime24HourNoNanos format, which follows the pattern `HH:mm:ss` for representing time
 in a 24-hour clock format. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanTime24HourNoNanos : Format Awareness.any := datespec("HH:mm:ss")
+def leanTime24HourNoNanos : GenericFormat .any := datespec("HH:mm:ss")
 
 /--
 The leanDateTime24Hour format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS` for
 representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTime24Hour : Format (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS")
+def leanDateTime24Hour : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS")
 
 /--
 The leanDateTime24HourNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss` for
 representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTime24HourNoNanos : Format (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss")
+def leanDateTime24HourNoNanos : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss")
 
 /--
 The leanDateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithZone : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ")
+def leanDateTimeWithZone : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ")
 
 /--
 The leanDateTimeWithZoneNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ssZZZZZ`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithZoneNoNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ")
+def leanDateTimeWithZoneNoNanos : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ")
 
 /--
 The leanDateTimeWithIdentifier format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss[z]`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithIdentifier : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss'['VV']'")
+def leanDateTimeWithIdentifier : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss'['zzzz']'")
 
 /--
 The leanDateTimeWithIdentifierAndNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'[z]'`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithIdentifierAndNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'['VV']'")
-
-/--
-The leanDateTimeWithZoneAndName format, which follows the pattern
-`uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ'['VV']'` for representing date, time, timezone offset,
-and timezone identifier. This is the canonical Lean format used in `repr` for named timezones.
--/
-def leanDateTimeWithZoneAndName : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ'['VV']'")
-
-/--
-The leanDateTimeWithZoneAndNameNoNanos format, which follows the pattern
-`uuuu-MM-dd'T'HH:mm:ssZZZZZ'['zzzz']'` for representing date, time, timezone offset, and timezone
-identifier without nanoseconds.
--/
-def leanDateTimeWithZoneAndNameNoNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ'['VV']'")
+def leanDateTimeWithIdentifierAndNanos : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'['zzzz']'")
 
 /--
 The Lean Date format, which follows the pattern `uuuu-MM-dd`. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDate : Format Awareness.any := datespec("uuuu-MM-dd")
+def leanDate : GenericFormat .any := datespec("uuuu-MM-dd")
 
 /--
 The SQLDate format, which follows the pattern `uuuu-MM-dd` and is commonly used
 in SQL databases to represent dates.
 -/
-def sqlDate : Format Awareness.any := datespec("uuuu-MM-dd")
+def sqlDate : GenericFormat .any := datespec("uuuu-MM-dd")
 
 /--
 The LongDateFormat, which follows the pattern `EEEE, MMMM d, uuuu HH:mm:ss` for
 representing a full date and time with the day of the week and month name.
 -/
-def longDateFormat : Format (.only .GMT) := datespec("EEEE, MMMM d, uuuu HH:mm:ss")
+def longDateFormat : GenericFormat (.only .GMT) := datespec("EEEE, MMMM d, uuuu HH:mm:ss")
 
 /--
 The AscTime format, which follows the pattern `EEE MMM d HH:mm:ss uuuu`. This format
 is often used in older systems for logging and time-stamping events.
 -/
-def ascTime : Format (.only .GMT) := datespec("EEE MMM d HH:mm:ss uuuu")
+def ascTime : GenericFormat (.only .GMT) := datespec("EEE MMM d HH:mm:ss uuuu")
 
 /--
 The RFC822 format, which follows the pattern `eee, dd MMM uuuu HH:mm:ss ZZZ`.
 This format is used in email headers and HTTP headers.
 -/
-def rfc822 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def rfc822 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
 
 /--
-The RFC850 format, which follows the pattern `eee, dd-MMM-yy HH:mm:ss ZZZ`.
+The RFC850 format, which follows the pattern `eee, dd-MMM-YY HH:mm:ss ZZZ`.
 This format is an older standard for representing date and time in headers.
 -/
-def rfc850 : Format Awareness.any := datespec("eee, dd-MMM-yy HH:mm:ss ZZZ")
-
-/--
-A `MultiFormat` that parses `leanDateTimeWithZone` with or without nanoseconds.
--/
-def leanDateTimeWithZoneAlt : MultiFormat Awareness.any :=
-  .new #[leanDateTimeWithZone, leanDateTimeWithZoneNoNanos]
-
-/--
-A `MultiFormat` that parses `leanDateTimeWithZoneAndName` with or without nanoseconds.
--/
-def leanDateTimeWithZoneAndNameAlt : MultiFormat Awareness.any :=
-  .new #[leanDateTimeWithZoneAndName, leanDateTimeWithZoneAndNameNoNanos]
-
-/--
-A `MultiFormat` that parses `leanDateTime24Hour` with or without nanoseconds.
--/
-def leanDateTime24HourAlt : MultiFormat (.only .GMT) :=
-  .new #[leanDateTime24Hour, leanDateTime24HourNoNanos]
-
-/--
-A `MultiFormat` that parses `leanTime24Hour` with or without nanoseconds.
--/
-def leanTime24HourAlt : MultiFormat Awareness.any :=
-  .new #[leanTime24Hour, leanTime24HourNoNanos]
-
-/--
-A `MultiFormat` that parses `leanDateTimeWithIdentifier` with or without nanoseconds.
--/
-def leanDateTimeWithIdentifierAlt : MultiFormat Awareness.any :=
-  .new #[leanDateTimeWithIdentifier, leanDateTimeWithIdentifierAndNanos]
+def rfc850 : GenericFormat .any := datespec("eee, dd-MM-uuuu HH:mm:ss ZZZ")
 
 end Formats
 
-namespace Format
-
-/--
-Parses the input string, resolving any timezone identifier via the default timezone database.
-For formats with a timezone identifier specifier but no offset specifier (e.g.
-`uuuu-MM-dd'T'HH:mm:ss'['zzzz']'`), this performs a tzdb lookup to find the correct UTC offset.
-For all other formats this behaves identically to `parse`.
--/
-def parseIO (format : Format Awareness.any) (input : String) : IO ZonedDateTime := do
-  if format.hasIdentifierSpecifier && !format.hasOffsetSpecifier then
-    match format.parseUnchecked input with
-    | .error err => throw <| IO.userError err
-    | .ok zdt =>
-      let rules ← Database.defaultGetZoneRules zdt.timezone.name
-      pure <| ZonedDateTime.ofPlainDateTime zdt.toPlainDateTime rules
-  else
-    IO.ofExcept (format.parse input)
-
-end Format
-
 namespace TimeZone
 
 /--
 Parses a string into a `TimeZone` object. The input string must be in the format `"VV ZZZZZ"`.
 -/
 def fromTimeZone (input : String) : Except String TimeZone := do
-  let spec : Format Awareness.any := datespec("VV ZZZZZ")
+  let spec : GenericFormat .any := datespec("VV ZZZZZ")
   spec.parseBuilder (fun id off => some (TimeZone.mk off id (off.toIsoString true) false)) input
 
 namespace Offset
@@ -232,7 +169,7 @@ namespace Offset
 Parses a string representing an offset into an `Offset` object. The input string must follow the `"xxx"` format.
 -/
 def fromOffset (input : String) : Except String Offset := do
-  let spec : Format Awareness.any := datespec("xxx")
+  let spec : GenericFormat .any := datespec("xxx")
   spec.parseBuilder some input
 
 end Offset
@@ -244,44 +181,76 @@ namespace PlainDate
 Formats a `PlainDate` using a specific format.
 -/
 def format (date : PlainDate) (format : String) : String :=
-  let format : Except String (Format Awareness.any) := Format.spec format
+  let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
     let res := res.formatGeneric fun
       | .G _ => some date.era
       | .y _ => some date.year
-      | .Y _ => some date.weekBasedYear
       | .u _ => some date.year
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
-      | .Q _ | .q _ => some date.quarter
+      | .Qorq _ => some date.quarter
       | .w _ => some date.weekOfYear
-      | .W _ => some date.weekOfMonth
-      | .M _ | .L _ => some date.month
+      | .W _ => some date.alignedWeekOfMonth
+      | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
-      | .e _ | .c _ => some date.weekday
+      | .eorc _ => some date.weekday
       | .F _ => some date.weekOfMonth
       | _ => none
     match res with
     | some res => res
     | none => "invalid time"
 
+/--
+Parses a date string in the American format (`MM-dd-uuuu`) and returns a `PlainDate`.
+-/
+def fromAmericanDateString (input : String) : Except String PlainDate := do
+  Formats.americanDate.parseBuilder (fun m d y => PlainDate.ofYearMonthDay? y m d) input
+
+/--
+Converts a date in the American format (`MM-dd-uuuu`) into a `String`.
+-/
+def toAmericanDateString (input : PlainDate) : String :=
+  Formats.americanDate.formatBuilder input.month input.day input.year
+
+/--
+Parses a date string in the SQL format (`uuuu-MM-dd`) and returns a `PlainDate`.
+-/
+def fromSQLDateString (input : String) : Except String PlainDate := do
+  Formats.sqlDate.parseBuilder PlainDate.ofYearMonthDay? input
+
+/--
+Converts a date in the SQL format (`uuuu-MM-dd`) into a `String`.
+-/
+def toSQLDateString (input : PlainDate) : String :=
+  Formats.sqlDate.formatBuilder input.year input.month input.day
+
+/--
+Parses a date string in the Lean format (`uuuu-MM-dd`) and returns a `PlainDate`.
+-/
+def fromLeanDateString (input : String) : Except String PlainDate := do
+  Formats.leanDate.parseBuilder PlainDate.ofYearMonthDay? input
+
+/--
+Converts a date in the Lean format (`uuuu-MM-dd`) into a `String`.
+-/
+def toLeanDateString (input : PlainDate) : String :=
+  Formats.leanDate.formatBuilder input.year input.month input.day
+
 /--
 Parses a `String` in the `AmericanDate` or `SQLDate` format and returns a `PlainDate`.
 -/
 def parse (input : String) : Except String PlainDate :=
-  Formats.americanDate.parseBuilder (fun m d y => PlainDate.ofYearMonthDay? y m d) input
-  <|> Formats.sqlDate.parseBuilder PlainDate.ofYearMonthDay? input
-
-def leanDateString (d : PlainDate) : String :=
-  Formats.leanDate.formatBuilder d.year d.month d.day
+  fromAmericanDateString input
+  <|> fromSQLDateString input
 
 instance : ToString PlainDate where
-  toString := leanDateString
+  toString := toLeanDateString
 
 instance : Repr PlainDate where
-  reprPrec d := Repr.addAppParen ("date(\"" ++ leanDateString d ++ "\")")
+  reprPrec data := Repr.addAppParen ("date(\"" ++ toLeanDateString data ++ "\")")
 
 end PlainDate
 
@@ -291,7 +260,7 @@ namespace PlainTime
 Formats a `PlainTime` using a specific format.
 -/
 def format (time : PlainTime) (format : String) : String :=
-  let format : Except String (Format Awareness.any) := Format.spec format
+  let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
@@ -302,16 +271,6 @@ def format (time : PlainTime) (format : String) : String :=
       | .n _ => some time.nanosecond
       | .s _ => some time.second
       | .a _ => some (HourMarker.ofOrdinal time.hour)
-      | .b _ =>
-        let h := time.hour.val
-        let m := time.minute.val
-        let s := time.second.val
-        let n := time.nanosecond.val
-        some <|
-          if h = 12 ∧ m = 0 ∧ s = 0 ∧ n = 0 then .noon
-          else if h = 0 ∧ m = 0 ∧ s = 0 ∧ n = 0 then .midnight
-          else if h < 12 then .am
-          else .pm
       | .h _ => some time.hour.toRelative
       | .K _ => some (time.hour.emod 12 (by decide))
       | .S _ => some time.nanosecond
@@ -323,24 +282,58 @@ def format (time : PlainTime) (format : String) : String :=
     | none => "invalid time"
 
 /--
-Parses a `String` in the `Time12Hour`, `Time24Hour`, or lean time (with optional nanoseconds) format
-and returns a `PlainTime`.
+Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`.
+-/
+def fromTime24Hour (input : String) : Except String PlainTime :=
+  Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
+
+/--
+Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
+-/
+def toTime24Hour (input : PlainTime) : String :=
+  Formats.time24Hour.formatBuilder input.hour input.minute input.second
+
+/--
+Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`.
+-/
+def fromLeanTime24Hour (input : String) : Except String PlainTime :=
+  Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
+  <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| PlainTime.ofHourMinuteSecondsNano h m s 0) input
+
+/--
+Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`).
+-/
+def toLeanTime24Hour (input : PlainTime) : String :=
+  Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond
+
+/--
+Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`.
+-/
+def fromTime12Hour (input : String) : Except String PlainTime := do
+  let builder h m s a : Option PlainTime := do
+    let value ← Internal.Bounded.ofInt? h.val
+    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s
+
+  Formats.time12Hour.parseBuilder builder input
+
+/--
+Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`).
+-/
+def toTime12Hour (input : PlainTime) : String :=
+  Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute input.second (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am)
+
+/--
+Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`.
 -/
 def parse (input : String) : Except String PlainTime :=
-  Formats.time12Hour.parseBuilder (fun h m s a => do
-    let value ← Internal.Bounded.ofInt? h.val
-    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s) input
-  <|> Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
-  <|> Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
-
-def leanTimeString (t : PlainTime) : String :=
-  Formats.leanTime24Hour.formatBuilder t.hour t.minute t.second t.nanosecond
+  fromTime12Hour input
+  <|> fromTime24Hour input
 
 instance : ToString PlainTime where
-  toString := leanTimeString
+  toString := toLeanTime24Hour
 
 instance : Repr PlainTime where
-  reprPrec data := Repr.addAppParen ("time(\"" ++ leanTimeString data ++ "\")")
+  reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")")
 
 end PlainTime
 
@@ -350,60 +343,99 @@ namespace ZonedDateTime
 Formats a `ZonedDateTime` using a specific format.
 -/
 def format (data: ZonedDateTime) (format : String) : String :=
-  let format : Except String (Format Awareness.any) := Format.spec format
+  let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
-  | .ok res => res.format data
+  | .ok res => res.format data.toDateTime
 
 /--
-Parses a `String` in common zoned date-time formats and returns a `ZonedDateTime`.
-This parser does not resolve timezone identifiers like `[Europe/Paris]`; use `parseIO` for that.
+Parses a `String` in the `ISO8601` format and returns a `ZonedDateTime`.
 -/
--- Wraps Format.parse to fix type unification (Awareness.any.type vs ZonedDateTime).
-private def parseFormat (fmt : Format Awareness.any) (input : String) : Except String ZonedDateTime :=
-  fmt.parse input
+def fromISO8601String (input : String) : Except String ZonedDateTime :=
+  Formats.iso8601.parse input
 
+/--
+Formats a `ZonedDateTime` value into an ISO8601 string.
+-/
+def toISO8601String (date : ZonedDateTime) : String :=
+  Formats.iso8601.format date.toDateTime
+
+/--
+Parses a `String` in the rfc822 format and returns a `ZonedDateTime`.
+-/
+def fromRFC822String (input : String) : Except String ZonedDateTime :=
+  Formats.rfc822.parse input
+
+/--
+Formats a `ZonedDateTime` value into an RFC822 format string.
+-/
+def toRFC822String (date : ZonedDateTime) : String :=
+  Formats.rfc822.format date.toDateTime
+
+/--
+Parses a `String` in the rfc850 format and returns a `ZonedDateTime`.
+-/
+def fromRFC850String (input : String) : Except String ZonedDateTime :=
+  Formats.rfc850.parse input
+
+/--
+Formats a `ZonedDateTime` value into an RFC850 format string.
+-/
+def toRFC850String (date : ZonedDateTime) : String :=
+  Formats.rfc850.format date.toDateTime
+
+/--
+Parses a `String` in the dateTimeWithZone format and returns a `ZonedDateTime` object in the GMT time zone.
+-/
+def fromDateTimeWithZoneString (input : String) : Except String ZonedDateTime :=
+  Formats.dateTimeWithZone.parse input
+
+/--
+Formats a `ZonedDateTime` value into a simple date time with timezone string.
+-/
+def toDateTimeWithZoneString (pdt : ZonedDateTime) : String :=
+  Formats.dateTimeWithZone.format pdt.toDateTime
+
+/--
+Parses a `String` in the lean date time format with timezone format and returns a `ZonedDateTime` object.
+-/
+def fromLeanDateTimeWithZoneString (input : String) : Except String ZonedDateTime :=
+  Formats.leanDateTimeWithZone.parse input
+  <|> Formats.leanDateTimeWithZoneNoNanos.parse input
+
+/--
+Parses a `String` in the lean date time format with identifier and returns a `ZonedDateTime` object.
+-/
+def fromLeanDateTimeWithIdentifierString (input : String) : Except String ZonedDateTime :=
+  Formats.leanDateTimeWithIdentifier.parse input
+  <|> Formats.leanDateTimeWithIdentifierAndNanos.parse input
+
+/--
+Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation.
+-/
+def toLeanDateTimeWithZoneString (zdt : ZonedDateTime) : String :=
+  Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset
+/--
+Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier.
+-/
+def toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : String :=
+  Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.timezone.name
+
+/--
+Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `ZonedDateTime`.
+-/
 def parse (input : String) : Except String ZonedDateTime :=
-  parseFormat Formats.iso8601 input
-  <|> parseFormat Formats.rfc822 input
-  <|> parseFormat Formats.rfc850 input
-  <|> parseFormat Formats.leanDateTimeWithZone input
-  <|> parseFormat Formats.leanDateTimeWithZoneNoNanos input
-  <|> parseFormat Formats.leanDateTimeWithZoneAndName input
-  <|> parseFormat Formats.leanDateTimeWithZoneAndNameNoNanos input
-  <|> parseFormat Formats.dateTimeWithZone input
-  <|> parseFormat Formats.leanDateTimeWithIdentifier input
-  <|> parseFormat Formats.leanDateTimeWithIdentifierAndNanos input
-
-/--
-Parses a `String` in common zoned date-time formats.
-If the input uses a timezone identifier (for example, `[Europe/Paris]`), it resolves it using the default timezone database.
--/
-def parseIO (input : String) : IO ZonedDateTime := do
-  match parse input with
-  | .ok zdt => pure zdt
-  | .error err =>
-    let identParse : Except String ZonedDateTime :=
-      Formats.leanDateTimeWithIdentifier.parseUnchecked input
-      <|> Formats.leanDateTimeWithIdentifierAndNanos.parseUnchecked input
-    match identParse with
-    | .ok zdt =>
-      let rules ← Database.defaultGetZoneRules zdt.timezone.name
-      pure <| ZonedDateTime.ofPlainDateTime zdt.toPlainDateTime rules
-    | .error _ => throw <| IO.userError err
+  fromISO8601String input
+  <|> fromRFC822String input
+  <|> fromRFC850String input
+  <|> fromDateTimeWithZoneString input
+  <|> fromLeanDateTimeWithIdentifierString input
 
 instance : ToString ZonedDateTime where
-  toString data := Formats.leanDateTimeWithIdentifierAndNanos.format data
+  toString := toLeanDateTimeWithIdentifierString
 
 instance : Repr ZonedDateTime where
-  reprPrec data :=
-    let name := data.timezone.name
-    let str :=
-      if name == data.timezone.offset.toIsoString true then
-        Formats.leanDateTimeWithZone.format data
-      else
-        Formats.leanDateTimeWithZoneAndName.format data
-    Repr.addAppParen ("zoned(\"" ++ str ++ "\")")
+  reprPrec data := Repr.addAppParen ("zoned(\"" ++ toLeanDateTimeWithZoneString data ++ "\")")
 
 end ZonedDateTime
 
@@ -413,31 +445,22 @@ namespace PlainDateTime
 Formats a `PlainDateTime` using a specific format.
 -/
 def format (date : PlainDateTime) (format : String) : String :=
-  let format : Except String (Format Awareness.any) := Format.spec format
+  let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
     let res := res.formatGeneric fun
       | .G _ => some date.era
       | .y _ => some date.year
-      | .Y _ =>
-        let week := date.weekOfYear
-        some <|
-          if date.month.val = 1 ∧ week.val ≥ 52 then
-            date.year - 1
-          else if date.month.val = 12 ∧ week.val = 1 then
-            date.year + 1
-          else
-            date.year
       | .u _ => some date.year
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
-      | .Q _ | .q _ => some date.quarter
+      | .Qorq _ => some date.quarter
       | .w _ => some date.weekOfYear
-      | .W _ => some date.weekOfMonth
-      | .M _ | .L _ => some date.month
+      | .W _ => some date.alignedWeekOfMonth
+      | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
-      | .e _ | .c _ => some date.weekday
+      | .eorc _ => some date.weekday
       | .F _ => some date.weekOfMonth
       | .H _ => some date.hour
       | .k _ => some date.hour.shiftTo1BasedHour
@@ -456,22 +479,71 @@ def format (date : PlainDateTime) (format : String) : String :=
     | none => "invalid time"
 
 /--
-Parses a `String` in the `AscTime`, `LongDate`, `DateTime`, or `LeanDateTime` format and returns a `PlainDateTime`.
+Parses a `String` in the `AscTime` format and returns a `PlainDateTime` object in the GMT time zone.
+-/
+def fromAscTimeString (input : String) : Except String PlainDateTime :=
+  Formats.ascTime.parse input
+  |>.map DateTime.toPlainDateTime
+
+/--
+Formats a `PlainDateTime` value into an AscTime format string.
+-/
+def toAscTimeString (pdt : PlainDateTime) : String :=
+  Formats.ascTime.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC)
+
+/--
+Parses a `String` in the `LongDateFormat` and returns a `PlainDateTime` object in the GMT time zone.
+-/
+def fromLongDateFormatString (input : String) : Except String PlainDateTime :=
+  Formats.longDateFormat.parse input
+  |>.map DateTime.toPlainDateTime
+
+/--
+Formats a `PlainDateTime` value into a LongDateFormat string.
+-/
+def toLongDateFormatString (pdt : PlainDateTime) : String :=
+  Formats.longDateFormat.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC)
+
+/--
+Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
+-/
+def fromDateTimeString (input : String) : Except String PlainDateTime :=
+  Formats.dateTime24Hour.parse input
+  |>.map DateTime.toPlainDateTime
+
+/--
+Formats a `PlainDateTime` value into a `DateTime` format string.
+-/
+def toDateTimeString (pdt : PlainDateTime) : String :=
+  Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
+
+/--
+Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
+-/
+def fromLeanDateTimeString (input : String) : Except String PlainDateTime :=
+  (Formats.leanDateTime24Hour.parse input <|> Formats.leanDateTime24HourNoNanos.parse input)
+  |>.map DateTime.toPlainDateTime
+
+/--
+Formats a `PlainDateTime` value into a `DateTime` format string.
+-/
+def toLeanDateTimeString (pdt : PlainDateTime) : String :=
+  Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
+
+/--
+Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`.
 -/
 def parse (date : String) : Except String PlainDateTime :=
-  (Formats.ascTime.parse date).map DateTime.toPlainDateTime
-  <|> (Formats.longDateFormat.parse date).map DateTime.toPlainDateTime
-  <|> (Formats.dateTime24Hour.parse date).map DateTime.toPlainDateTime
-  <|> (Formats.leanDateTime24HourAlt.parse date).map DateTime.toPlainDateTime
-
-def leanPlainDateTimeString (date : PlainDateTime) : String :=
-  Formats.leanDateTime24Hour.formatBuilder date.year date.month date.day date.hour date.minute date.time.second date.nanosecond
+  fromAscTimeString date
+  <|> fromLongDateFormatString date
+  <|> fromDateTimeString date
+  <|> fromLeanDateTimeString date
 
 instance : ToString PlainDateTime where
-  toString := leanPlainDateTimeString
+  toString := toLeanDateTimeString
 
 instance : Repr PlainDateTime where
-  reprPrec data := Repr.addAppParen ("datetime(\"" ++ leanPlainDateTimeString data ++ "\")")
+  reprPrec data := Repr.addAppParen ("datetime(\"" ++ toLeanDateTimeString data ++ "\")")
 
 end PlainDateTime
 
@@ -481,22 +553,76 @@ namespace DateTime
 Formats a `DateTime` using a specific format.
 -/
 def format (data: DateTime tz) (format : String) : String :=
-  let format : Except String (Format Awareness.any) := Format.spec format
+  let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res => res.format data
 
+/--
+Parses a `String` in the `AscTime` format and returns a `DateTime` object in the GMT time zone.
+-/
+def fromAscTimeString (input : String) : Except String (DateTime .GMT) :=
+  Formats.ascTime.parse input
+
+/--
+Formats a `DateTime` value into an AscTime format string.
+-/
+def toAscTimeString (datetime : DateTime .GMT) : String :=
+  Formats.ascTime.format datetime
+
+/--
+Parses a `String` in the `LongDateFormat` and returns a `DateTime` object in the GMT time zone.
+-/
+def fromLongDateFormatString (input : String) : Except String (DateTime .GMT) :=
+  Formats.longDateFormat.parse input
+
+/--
+Formats a `DateTime` value into a LongDateFormat string.
+-/
+def toLongDateFormatString (datetime : DateTime .GMT) : String :=
+  Formats.longDateFormat.format datetime
+
+/--
+Formats a `DateTime` value into an ISO8601 string.
+-/
+def toISO8601String (date : DateTime tz) : String :=
+  Formats.iso8601.format date
+
+/--
+Formats a `DateTime` value into an RFC822 format string.
+-/
+def toRFC822String (date : DateTime tz) : String :=
+  Formats.rfc822.format date
+
+/--
+Formats a `DateTime` value into an RFC850 format string.
+-/
+def toRFC850String (date : DateTime tz) : String :=
+  Formats.rfc850.format date
+
+/--
+Formats a `DateTime` value into a `DateTimeWithZone` format string.
+-/
+def toDateTimeWithZoneString (pdt : DateTime tz) : String :=
+  Formats.dateTimeWithZone.format pdt
+
+/--
+Formats a `DateTime` value into a `DateTimeWithZone` format string that can be parsed by `date%`.
+-/
+def toLeanDateTimeWithZoneString (pdt : DateTime tz) : String :=
+  Formats.leanDateTimeWithZone.format pdt
+
 /--
 Parses a `String` in the `AscTime` or `LongDate` format and returns a `DateTime`.
 -/
 def parse (date : String) : Except String (DateTime .GMT) :=
-  Formats.ascTime.parse date
-  <|> Formats.longDateFormat.parse date
+  fromAscTimeString date
+  <|> fromLongDateFormatString date
 
 instance : Repr (DateTime tz) where
-  reprPrec data := Repr.addAppParen (Formats.leanDateTimeWithZone.format data)
+  reprPrec data := Repr.addAppParen (toLeanDateTimeWithZoneString data)
 
 instance : ToString (DateTime tz) where
-  toString data := Formats.leanDateTimeWithZone.format data
+  toString := toLeanDateTimeWithZoneString
 
 end DateTime

src/Std/Time/Notation.lean

@@ -21,7 +21,6 @@ private meta def convertText : Text → MacroM (TSyntax `term)
   | .short  => `(Std.Time.Text.short)
   | .full   => `(Std.Time.Text.full)
   | .narrow => `(Std.Time.Text.narrow)
-  | .twoLetterShort => `(Std.Time.Text.twoLetterShort)
 
 private meta def convertNumber : Number → MacroM (TSyntax `term)
   | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding))
@@ -59,40 +58,26 @@ private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term)
 private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
-  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
-  | .M p =>
+  | .MorL p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.M (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.M (.inr $(← convertText txt)))
-  | .L p =>
-    match p with
-    | .inl num => do `(Std.Time.Modifier.L (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.L (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.MorL (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.MorL (.inr $(← convertText txt)))
   | .d p => do `(Std.Time.Modifier.d $(← convertNumber p))
-  | .Q p =>
+  | .Qorq p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.Q (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.Q (.inr $(← convertText txt)))
-  | .q p =>
-    match p with
-    | .inl num => do `(Std.Time.Modifier.q (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.q (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.Qorq (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.Qorq (.inr $(← convertText txt)))
   | .w p => do `(Std.Time.Modifier.w $(← convertNumber p))
   | .W p => do `(Std.Time.Modifier.W $(← convertNumber p))
   | .E p => do `(Std.Time.Modifier.E $(← convertText p))
-  | .e p =>
+  | .eorc p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.e (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.e (.inr $(← convertText txt)))
-  | .c p =>
-    match p with
-    | .inl num => do `(Std.Time.Modifier.c (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.c (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.eorc (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.eorc (.inr $(← convertText txt)))
   | .F p => do `(Std.Time.Modifier.F $(← convertNumber p))
   | .a p => do `(Std.Time.Modifier.a $(← convertText p))
-  | .b p => do `(Std.Time.Modifier.b $(← convertText p))
   | .h p => do `(Std.Time.Modifier.h $(← convertNumber p))
   | .K p => do `(Std.Time.Modifier.K $(← convertNumber p))
   | .k p => do `(Std.Time.Modifier.k $(← convertNumber p))
@@ -103,9 +88,8 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .A p => do `(Std.Time.Modifier.A $(← convertNumber p))
   | .n p => do `(Std.Time.Modifier.n $(← convertNumber p))
   | .N p => do `(Std.Time.Modifier.N $(← convertNumber p))
-  | .V p => do `(Std.Time.Modifier.V $(← convertNumber p))
+  | .V => `(Std.Time.Modifier.V)
   | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p))
-  | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p))
   | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p))
   | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p))
   | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p))
@@ -223,40 +207,33 @@ syntax "timezone(" str ")" : term
 
 macro_rules
   | `(zoned( $date:str )) => do
-      let s := date.getString
-      match (Formats.leanDateTimeWithZoneAlt.parse s : Except String ZonedDateTime) with
+      match ZonedDateTime.fromLeanDateTimeWithZoneString date.getString with
       | .ok res => do return ← convertZonedDateTime res
       | .error _ =>
-        match (Formats.leanDateTimeWithZoneAndNameAlt.parse s : Except String ZonedDateTime) with
-        | .ok res => do return ← convertZonedDateTime res
-        | .error _ =>
-          let identParse : Except String ZonedDateTime :=
-            Formats.leanDateTimeWithIdentifier.parseUnchecked s
-            <|> Formats.leanDateTimeWithIdentifierAndNanos.parseUnchecked s
-          match identParse with
-          | .ok res => do return ← convertZonedDateTime res (identifier := true)
-          | .error res => Macro.throwErrorAt date s!"error: {res}"
+        match ZonedDateTime.fromLeanDateTimeWithIdentifierString date.getString with
+        | .ok res => do return ← convertZonedDateTime res (identifier := true)
+        | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(zoned( $date:str, $timezone )) => do
-      match (Formats.leanDateTime24HourAlt.parse date.getString).map DateTime.toPlainDateTime with
+      match PlainDateTime.fromLeanDateTimeString date.getString with
       | .ok res => do
         let plain ← convertPlainDateTime res
         `(Std.Time.ZonedDateTime.ofPlainDateTime $plain $timezone)
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(datetime( $date:str )) => do
-      match (Formats.leanDateTime24HourAlt.parse date.getString).map DateTime.toPlainDateTime with
+      match PlainDateTime.fromLeanDateTimeString date.getString with
       | .ok res => do
         return ← convertPlainDateTime res
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(date( $date:str )) => do
-      match PlainDate.parse date.getString with
+      match PlainDate.fromSQLDateString date.getString with
       | .ok res => return ← convertPlainDate res
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(time( $time:str )) => do
-      match PlainTime.parse time.getString with
+      match PlainTime.fromLeanTime24Hour time.getString with
       | .ok res => return ← convertPlainTime res
       | .error res => Macro.throwErrorAt time s!"error: {res}"
 

src/Std/Time/Notation/Spec.lean

@@ -19,7 +19,6 @@ private meta def convertText : Text → MacroM (TSyntax `term)
   | .short => `(Std.Time.Text.short)
   | .full => `(Std.Time.Text.full)
   | .narrow => `(Std.Time.Text.narrow)
-  | .twoLetterShort => `(Std.Time.Text.twoLetterShort)
 
 private meta def convertNumber : Number → MacroM (TSyntax `term)
   | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding))
@@ -57,40 +56,26 @@ private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term)
 private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
-  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
-  | .M p =>
+  | .MorL p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.M (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.M (.inr $(← convertText txt)))
-  | .L p =>
-    match p with
-    | .inl num => do `(Std.Time.Modifier.L (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.L (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.MorL (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.MorL (.inr $(← convertText txt)))
   | .d p => do `(Std.Time.Modifier.d $(← convertNumber p))
-  | .Q p =>
+  | .Qorq p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.Q (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.Q (.inr $(← convertText txt)))
-  | .q p =>
-    match p with
-    | .inl num => do `(Std.Time.Modifier.q (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.q (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.Qorq (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.Qorq (.inr $(← convertText txt)))
   | .w p => do `(Std.Time.Modifier.w $(← convertNumber p))
   | .W p => do `(Std.Time.Modifier.W $(← convertNumber p))
   | .E p => do `(Std.Time.Modifier.E $(← convertText p))
-  | .e p =>
+  | .eorc p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.e (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.e (.inr $(← convertText txt)))
-  | .c p =>
-    match p with
-    | .inl num => do `(Std.Time.Modifier.c (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.c (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.eorc (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.eorc (.inr $(← convertText txt)))
   | .F p => do `(Std.Time.Modifier.F $(← convertNumber p))
   | .a p => do `(Std.Time.Modifier.a $(← convertText p))
-  | .b p => do `(Std.Time.Modifier.b $(← convertText p))
   | .h p => do `(Std.Time.Modifier.h $(← convertNumber p))
   | .K p => do `(Std.Time.Modifier.K $(← convertNumber p))
   | .k p => do `(Std.Time.Modifier.k $(← convertNumber p))
@@ -101,9 +86,8 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .A p => do `(Std.Time.Modifier.A $(← convertNumber p))
   | .n p => do `(Std.Time.Modifier.n $(← convertNumber p))
   | .N p => do `(Std.Time.Modifier.N $(← convertNumber p))
-  | .V p => do `(Std.Time.Modifier.V $(← convertNumber p))
+  | .V => `(Std.Time.Modifier.V)
   | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p))
-  | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p))
   | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p))
   | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p))
   | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p))
@@ -125,7 +109,7 @@ syntax "datespec(" str "," term ")" : term
 
 private meta def formatStringToFormat (fmt : TSyntax `str) (config : Option (TSyntax `term)) : MacroM (TSyntax `term) := do
   let input := fmt.getString
-  let format : Except String (Format .any) := Format.spec input
+  let format : Except String (GenericFormat .any) := GenericFormat.spec input
   match format with
   | .ok res =>
     let alts ← res.string.mapM convertFormatPart

src/Std/Time/Zoned/DateTime.lean

@@ -410,17 +410,9 @@ def weekday (dt : DateTime tz) : Weekday :=
 /--
 Determines the era of the given `DateTime` based on its year.
 -/
-@[inline]
 def era (date : DateTime tz) : Year.Era :=
   date.year.era
 
-/--
-Returns the week-based year for a given `DateTime`.
--/
-@[inline]
-def weekBasedYear (date : DateTime tz) : Year.Offset :=
-  date.date.get.weekBasedYear
-
 /--
 Sets the `DateTime` to the specified `desiredWeekday`.
 -/

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -15,7 +15,8 @@ public section
 namespace Std
 namespace Time
 
-set_option linter.all true
+-- TODO (@kim-em): re-enable this once there is a mechanism to exclude `linter.indexVariables`.
+-- set_option linter.all true
 
 /--
 Represents a date and time with timezone information.
@@ -152,13 +153,6 @@ Getter for the `Year` inside of a `ZonedDateTime`
 def year (zdt : ZonedDateTime) : Year.Offset :=
   zdt.date.get.year
 
-/--
-Returns the week-based year for a given `ZonedDateTime`.
--/
-@[inline]
-def weekBasedYear (zdt : ZonedDateTime) : Year.Offset :=
-  zdt.date.get.weekBasedYear
-
 /--
 Getter for the `Month` inside of a `ZonedDateTime`
 -/

src/lake/Lake/CLI/Help.lean

@@ -386,7 +386,7 @@ OPTIONS:
   --force-download                redownload existing files
 
 Downloads build outputs for packages in the workspace from a remote cache
-service. The cache service used can be specifed via the `--service` option.
+service. The cache service used can be specified via the `--service` option.
 Otherwise, Lake will the system default, or, if none is configured, Reservoir.
 See `lake cache services` for more information on how to configure services.
 
@@ -429,7 +429,7 @@ USAGE:
 
 Uploads the input-to-output mappings contained in the specified file along
 with the corresponding output artifacts to a remote cache. The cache service
-used via be specified via `--service` option. If not specifed, Lake will used
+used can be specified via the `--service` option. If not specified, Lake will use
 the system default, or error if none is configured. See the help page of
 `lake cache services` for more information on how to configure services.
 

src/lake/Lake/CLI/Main.lean

@@ -446,7 +446,7 @@ protected def get : CliM PUnit := do
           logWarning endpointDeprecation
           if opts.mappingsOnly then
             error "`--mappings-only` requires services to be configured
-              via the Lake system configuration (not enviroment variables)"
+              via the Lake system configuration (not environment variables)"
           return .downloadService artifactEndpoint revisionEndpoint ws.lakeEnv.cacheService?
         | none, none =>
             return ws.defaultCacheService

src/lake/Lake/Config/Cache.lean

@@ -765,12 +765,13 @@ where
       \n  remote URL: {info.url}"
     match cfg.kind with
     | .get =>
-      if let .ok size := out.getAs Nat "size_download" then
-        if size > 0 then
-          if let .ok contentType := out.getAs String "content_type" then
-            if contentType != artifactContentType then
-              if let .ok resp ← IO.FS.readFile info.path |>.toBaseIO then
-                msg := s!"{msg}\nunexpected response:\n{resp}"
+      unless code? matches .ok 404 do -- ignore response bodies on 404s
+        if let .ok size := out.getAs Nat "size_download" then
+          if size > 0 then
+            if let .ok contentType := out.getAs String "content_type" then
+              if contentType != artifactContentType then
+                if let .ok resp ← IO.FS.readFile info.path |>.toBaseIO then
+                  msg := s!"{msg}\nunexpected response:\n{resp}"
       removeFileIfExists info.path
     | .put =>
       if let .ok size := out.getAs Nat "size_download" then
@@ -787,7 +788,7 @@ private def transferArtifacts
     match cfg.kind with
     | .get =>
       cfg.infos.forM fun info => do
-        h.putStrLn s!"url = {info.url}"
+        h.putStrLn s!"url = {info.url.quote}"
         h.putStrLn s!"-o {info.path.toString.quote}"
       h.flush
       return #[
@@ -798,7 +799,7 @@ private def transferArtifacts
     | .put =>
       cfg.infos.forM fun info => do
         h.putStrLn s!"-T {info.path.toString.quote}"
-        h.putStrLn s!"url = {info.url}"
+        h.putStrLn s!"url = {info.url.quote}"
       h.flush
       return #[
         "-Z", "-X", "PUT", "-L",
@@ -827,6 +828,13 @@ private def transferArtifacts
   if s.didError then
     failure
 
+private def reservoirArtifactsUrl (service : CacheService) (scope : CacheServiceScope) : String :=
+  let endpoint :=
+    match scope.impl with
+    | .repo scope => appendScope s!"{service.impl.apiEndpoint}/repositories" scope
+    | .str scope => appendScope s!"{service.impl.apiEndpoint}/packages" scope
+  s!"{endpoint}/artifacts"
+
 public def downloadArtifacts
    (descrs : Array ArtifactDescr) (cache : Cache)
    (service : CacheService) (scope : CacheServiceScope) (force := false)
@@ -844,8 +852,68 @@ public def downloadArtifacts
     return s.push {url, path, descr}
   if infos.isEmpty then
     return
+  let infos ← id do
+    if service.isReservoir then
+      -- Artifact cloud storage URLs are fetched in a single request
+      -- to avoid hammering the Reservoir web host
+      fetchUrls (service.reservoirArtifactsUrl scope) infos
+    else return infos
   IO.FS.createDirAll cache.artifactDir
   transferArtifacts {scope, infos, kind := .get}
+where
+  fetchUrls url infos := IO.FS.withTempFile fun h path => do
+    let body := Json.arr <| infos.map (toJson ·.descr.hash)
+    h.putStr body.compress
+    h.flush
+    let args := #[
+        "-X", "POST", "-L", "-d", s!"@{path}",
+        "--retry", "3", -- intermittent network errors can occur
+        "-s", "-w", "%{stderr}%{json}\n",
+        "-H", "Content-Type: application/json",
+      ]
+    let args := Reservoir.lakeHeaders.foldl (· ++ #["-H", ·]) args
+    let spawnArgs := {
+      cmd := "curl", args := args.push url
+      stdout := .piped, stderr := .piped
+    }
+    logVerbose (mkCmdLog spawnArgs)
+    let {stdout, stderr, exitCode} ← IO.Process.output spawnArgs
+    match Json.parse stdout >>= fromJson? with
+    | .ok (resp :  ReservoirResp (Array String)) =>
+      match resp with
+      | .data urls =>
+        if h : infos.size = urls.size then
+          let s := infos.size.fold (init := infos.toVector) fun i hi s =>
+            s.set i {s[i] with url := urls[i]'(h ▸ hi)}
+          return s.toArray
+        else
+          error s!"failed to fetch artifact URLs\
+          \n  POST {url}\
+          \nIncorrect number of results: expected {infos.size}, got {urls.size}"
+      | .error status message =>
+        error s!"failed to fetch artifact URLs (status code: {status})\
+          \n  POST {url}\
+          \nReservoir error: {message}"
+    | .error _ =>
+      match Json.parse stderr >>= fromJson? with
+      | .ok (out : JsonObject) =>
+        let mut msg := "failed to fetch artifact URLs"
+        if let .ok code := out.getAs Nat "http_code" then
+          msg := s!"{msg} (status code: {code})"
+        msg := s!"{msg}\n  POST {url}"
+        if let .ok errMsg := out.getAs String "errormsg" then
+          msg := s!"{msg}\n  Transfer error: {errMsg}"
+        unless stdout.isEmpty do
+          msg := s!"{msg}\nstdout:\n{stdout.trimAsciiEnd}"
+        logError msg
+        logVerbose s!"curl JSON:\n{stderr.trimAsciiEnd}"
+      | .error e =>
+        logError s!"failed to fetch artifact URLs\
+          \n  POST {url}
+          \nInvalid curl JSON: {e}; received: {stderr.trimAscii}"
+        unless stdout.isEmpty do
+          logWarning s!"curl produced unexpected output:\n{stdout.trimAsciiEnd}"
+      error s!"curl exited with code {exitCode}"
 
 @[deprecated "Deprecated without replacement." (since := "2026-02-27")]
 public def downloadOutputArtifacts

src/lake/Lake/Reservoir.lean

@@ -103,24 +103,6 @@ public instance : FromJson RegistryPkg := ⟨RegistryPkg.fromJson?⟩
 
 end RegistryPkg
 
-/-- A Reservoir API response object. -/
-public inductive ReservoirResp (α : Type u)
-| data (a : α)
-| error (status : Nat) (message : String)
-
-public protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String (ReservoirResp α) := do
-  let obj ← JsonObject.fromJson? val
-  if let some (err : JsonObject) ← obj.get? "error" then
-    let status ← err.get "status"
-    let message ← err.get "message"
-    return .error status message
-  else if let some (val : Json) ← obj.get? "data" then
-    .data <$> fromJson? val
-  else
-    .data <$> fromJson? val
-
-public instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩
-
 public def Reservoir.pkgApiUrl (lakeEnv : Lake.Env) (owner pkg : String) :=
    s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
 

src/lake/Lake/Util/Reservoir.lean

@@ -6,8 +6,9 @@ Authors: Mac Malone
 module
 
 prelude
-public import Init.Prelude
-import Init.Data.Array.Basic
+public import Lake.Util.JsonObject
+
+open Lean
 
 namespace Lake
 
@@ -15,3 +16,23 @@ public def Reservoir.lakeHeaders : Array String := #[
   "X-Reservoir-Api-Version:1.0.0",
   "X-Lake-Registry-Api-Version:0.1.0"
 ]
+
+/-- A Reservoir API response object. -/
+public inductive ReservoirResp (α : Type u)
+| data (a : α)
+| error (status : Nat) (message : String)
+
+public protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String (ReservoirResp α) := do
+  if let .ok obj := JsonObject.fromJson? val then
+    if let some (err : JsonObject) ← obj.get? "error" then
+      let status ← err.get "status"
+      let message ← err.get "message"
+      return .error status message
+    else if let some (val : Json) ← obj.get? "data" then
+      .data <$> fromJson? val
+    else
+      .data <$> fromJson? val
+  else
+    .data <$> fromJson? val
+
+public instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩

tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean

@@ -6,6 +6,7 @@ open Lean Meta Elab Tactic Sym Std Do SpecAttr
 namespace GetThrowSet
 
 set_option mvcgen.warning false
+set_option backward.do.legacy false -- exercises asymmetric bind depth from new do elaborator
 
 abbrev M := ExceptT String <| StateM Nat
 

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -876,11 +876,10 @@ meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
 meta def work (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
   let goal := { goal with mvarId }
-  let mut worklist := Std.Queue.empty.enqueue goal
+  let mut worklist := #[goal]
   repeat do
-    let some (goal, worklist') := worklist.dequeue? | break
-    let mut goal := goal
-    worklist := worklist'
+    let mut some goal := worklist.back? | break
+    worklist := worklist.pop
     let res ← solve goal.mvarId
     match res with
     | .noEntailment .. | .noProgramFoundInTarget .. =>
@@ -896,7 +895,7 @@ meta def work (goal : Grind.Goal) : VCGenM Unit := do
       -- to share E-graph context before forking.
       if subgoals.length > 1 then
         goal ← (← read).preTac.processHypotheses goal
-      worklist := worklist.enqueueAll (subgoals.map ({ goal with mvarId := · }))
+      worklist := worklist ++ (subgoals |>.map ({ goal with mvarId := · }) |>.reverse)
 
 public structure Result where
   invariants : Array MVarId

tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean

@@ -15,5 +15,7 @@ set_option maxHeartbeats 100000000
 
 -- Benchmark `mvcgen' with grind`: grind integrated into VCGen loop for incremental
 -- context internalization. This avoids O(n) re-internalization per VC.
-#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail)
+-- `simplifying_assumptions [Nat.add_assoc]` here speeds up grind and kernel checking by a factor
+-- of 2 because long chains `s + 1 + ... + 1` are collapsed into `s + n`.
+#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' simplifying_assumptions [Nat.add_assoc] with grind) `(tactic| fail)
   [50, 100, 150]

tests/elab/async_http_body.lean

@@ -0,0 +1,725 @@
+import Std.Internal.Http.Data.Body
+
+open Std.Internal.IO Async
+open Std.Http
+open Std.Http.Body
+
+/-! ## Stream tests -/
+
+-- Test send and recv on stream
+
+def channelSendRecv : Async Unit := do
+  let stream ← Body.mkStream
+  let chunk := Chunk.ofByteArray "hello".toUTF8
+
+  let sendTask ← async (t := AsyncTask) <| stream.send chunk
+  let result ← stream.recv
+
+  assert! result.isSome
+  assert! result.get!.data == "hello".toUTF8
+  await sendTask
+
+#eval channelSendRecv.block
+
+
+-- Test tryRecv on empty stream returns none
+
+def channelTryRecvEmpty : Async Unit := do
+  let stream ← Body.mkStream
+  let result ← stream.tryRecv
+  assert! result.isNone
+
+#eval channelTryRecvEmpty.block
+
+-- Test tryRecv consumes a waiting producer
+
+def channelTryRecvWithPendingSend : Async Unit := do
+  let stream ← Body.mkStream
+
+  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "data".toUTF8)
+  let mut result := none
+  let mut fuel := 100
+  while result.isNone && fuel > 0 do
+    result ← stream.tryRecv
+    if result.isNone then
+      let _ ← Selectable.one #[
+        .case (← Selector.sleep 1) pure
+      ]
+    fuel := fuel - 1
+
+  assert! result.isSome
+  assert! result.get!.data == "data".toUTF8
+  await sendTask
+
+#eval channelTryRecvWithPendingSend.block
+
+-- Test close sets closed flag
+
+def channelClose : Async Unit := do
+  let stream ← Body.mkStream
+  assert! !(← stream.isClosed)
+  stream.close
+  assert! (← stream.isClosed)
+
+#eval channelClose.block
+
+-- Test recv on closed stream returns none
+
+def channelRecvAfterClose : Async Unit := do
+  let stream ← Body.mkStream
+  stream.close
+  let result ← stream.recv
+  assert! result.isNone
+
+#eval channelRecvAfterClose.block
+
+-- Test for-in iteration collects chunks until close
+
+def channelForIn : Async Unit := do
+  let stream ← Body.mkStream
+
+  let producer ← async (t := AsyncTask) <| do
+    stream.send (Chunk.ofByteArray "a".toUTF8)
+    stream.send (Chunk.ofByteArray "b".toUTF8)
+    stream.close
+
+  let mut acc : ByteArray := .empty
+  for chunk in stream do
+    acc := acc ++ chunk.data
+
+  assert! acc == "ab".toUTF8
+  await producer
+
+#eval channelForIn.block
+
+-- Test chunk extensions are preserved
+
+def channelExtensions : Async Unit := do
+  let stream ← Body.mkStream
+  let chunk := { data := "hello".toUTF8, extensions := #[(.mk "key", some (Chunk.ExtensionValue.ofString! "value"))] : Chunk }
+
+  let sendTask ← async (t := AsyncTask) <| stream.send chunk
+  let result ← stream.recv
+
+  assert! result.isSome
+  assert! result.get!.extensions.size == 1
+  assert! result.get!.extensions[0]! == (Chunk.ExtensionName.mk "key", some <| .ofString! "value")
+  await sendTask
+
+#eval channelExtensions.block
+
+-- Test known size metadata
+
+def channelKnownSize : Async Unit := do
+  let stream ← Body.mkStream
+  stream.setKnownSize (some (.fixed 100))
+  let size ← stream.getKnownSize
+  assert! size == some (.fixed 100)
+
+#eval channelKnownSize.block
+
+-- Test known size decreases when a chunk is consumed
+
+def channelKnownSizeDecreases : Async Unit := do
+  let stream ← Body.mkStream
+  stream.setKnownSize (some (.fixed 5))
+
+  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "hello".toUTF8)
+  let _ ← stream.recv
+  await sendTask
+
+  let size ← stream.getKnownSize
+  assert! size == some (.fixed 0)
+
+#eval channelKnownSizeDecreases.block
+
+-- Test only one blocked producer is allowed
+
+def channelSingleProducerRule : Async Unit := do
+  let stream ← Body.mkStream
+  let send1 ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "one".toUTF8)
+
+  -- Yield so `send1` can occupy the single pending-producer slot.
+  let _ ← Selectable.one #[
+    .case (← Selector.sleep 5) pure
+  ]
+
+  let send2Failed ←
+    try
+      stream.send (Chunk.ofByteArray "two".toUTF8)
+      pure false
+    catch _ =>
+      pure true
+  assert! send2Failed
+
+  let first ← stream.recv
+  assert! first.isSome
+  assert! first.get!.data == "one".toUTF8
+
+  await send1
+
+#eval channelSingleProducerRule.block
+
+-- Test only one blocked consumer is allowed
+
+def channelSingleConsumerRule : Async Unit := do
+  let stream ← Body.mkStream
+
+  let recv1 ← async (t := AsyncTask) <| stream.recv
+
+  let hasInterest ← Selectable.one #[
+    .case stream.interestSelector pure
+  ]
+  assert! hasInterest
+
+  let recv2Failed ←
+    try
+      let _ ← stream.recv
+      pure false
+    catch _ =>
+      pure true
+
+  assert! recv2Failed
+
+  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "ok".toUTF8)
+  let r1 ← await recv1
+
+  assert! r1.isSome
+  assert! r1.get!.data == "ok".toUTF8
+  await sendTask
+
+#eval channelSingleConsumerRule.block
+
+-- Test hasInterest reflects blocked receiver state
+
+def channelHasInterest : Async Unit := do
+  let stream ← Body.mkStream
+  assert! !(← stream.hasInterest)
+
+  let recvTask ← async (t := AsyncTask) <| stream.recv
+
+  let hasInterest ← Selectable.one #[
+    .case stream.interestSelector pure
+  ]
+  assert! hasInterest
+  assert! (← stream.hasInterest)
+
+  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "x".toUTF8)
+  let _ ← await recvTask
+  await sendTask
+
+  assert! !(← stream.hasInterest)
+
+#eval channelHasInterest.block
+
+-- Test interestSelector resolves false when stream closes first
+
+def channelInterestSelectorClose : Async Unit := do
+  let stream ← Body.mkStream
+
+  let waitInterest ← async (t := AsyncTask) <|
+    Selectable.one #[
+      .case stream.interestSelector pure
+    ]
+
+  stream.close
+  let interested ← await waitInterest
+  assert! interested == false
+
+#eval channelInterestSelectorClose.block
+
+-- Test incomplete sends are buffered and merged into one chunk on the final send
+
+def channelIncompleteChunks : Async Unit := do
+  let stream ← Body.mkStream
+
+  let sendTask ← async (t := AsyncTask) <| do
+    stream.send (Chunk.ofByteArray "hel".toUTF8) (incomplete := true)
+    stream.send (Chunk.ofByteArray "lo".toUTF8)
+
+  let result ← stream.recv
+
+  assert! result.isSome
+  assert! result.get!.data == "hello".toUTF8
+  await sendTask
+
+#eval channelIncompleteChunks.block
+
+-- Test sending to a closed stream raises an error
+
+def channelSendAfterClose : Async Unit := do
+  let stream ← Body.mkStream
+  stream.close
+
+  let failed ←
+    try
+      stream.send (Chunk.ofByteArray "test".toUTF8)
+      pure false
+    catch _ =>
+      pure true
+  assert! failed
+
+#eval channelSendAfterClose.block
+
+-- Test Body.stream runs producer and returns the stream handle
+
+def channelStreamHelper : Async Unit := do
+  let stream ← Body.stream fun s => do
+    s.send (Chunk.ofByteArray "hello".toUTF8)
+
+  let result ← stream.recv
+  assert! result.isSome
+  assert! result.get!.data == "hello".toUTF8
+
+  let eof ← stream.recv
+  assert! eof.isNone
+
+#eval channelStreamHelper.block
+
+-- Test Body.empty creates an already-closed Stream
+
+def channelEmptyHelper : Async Unit := do
+  let stream ← Body.empty
+  assert! (← stream.isClosed)
+
+  let result ← stream.recv
+  assert! result.isNone
+
+#eval channelEmptyHelper.block
+
+-- Test Stream.readAll concatenates all chunks
+
+def channelReadAll : Async Unit := do
+  let stream ← Body.mkStream
+
+  let sendTask ← async (t := AsyncTask) <| do
+    stream.send (Chunk.ofByteArray "foo".toUTF8)
+    stream.send (Chunk.ofByteArray "bar".toUTF8)
+    stream.close
+
+  let result : ByteArray ← stream.readAll
+  assert! result == "foobar".toUTF8
+  await sendTask
+
+#eval channelReadAll.block
+
+-- Test Stream.readAll enforces a maximum size limit
+
+def channelReadAllMaxSize : Async Unit := do
+  let stream ← Body.mkStream
+
+  let sendTask ← async (t := AsyncTask) <| do
+    stream.send (Chunk.ofByteArray "abcdefgh".toUTF8)
+    stream.close
+
+  let failed ←
+    try
+      let _ : ByteArray ← stream.readAll (maximumSize := some 4)
+      pure false
+    catch _ =>
+      pure true
+  assert! failed
+  await sendTask
+
+#eval channelReadAllMaxSize.block
+
+-- Test Stream.getKnownSize reflects the value set via setKnownSize
+
+def channelKnownSizeRoundtrip : Async Unit := do
+  let stream ← Body.mkStream
+  stream.setKnownSize (some (.fixed 42))
+
+  let size ← stream.getKnownSize
+  assert! size == some (.fixed 42)
+
+#eval channelKnownSizeRoundtrip.block
+
+/-! ## Full tests -/
+
+-- Test Full.recv returns content once then EOF
+
+def fullRecvConsumesOnce : Async Unit := do
+  let full ← Body.Full.ofString "hello"
+  let first ← full.recv
+  let second ← full.recv
+
+  assert! first.isSome
+  assert! first.get!.data == "hello".toUTF8
+  assert! second.isNone
+
+#eval fullRecvConsumesOnce.block
+
+-- Test Full known-size metadata tracks consumption
+
+def fullKnownSizeLifecycle : Async Unit := do
+  let data := ByteArray.mk #[0x01, 0x02, 0x03, 0x04]
+  let full ← Body.Full.ofByteArray data
+
+  assert! (← full.getKnownSize) == some (.fixed 4)
+  let chunk ← full.recv
+  assert! chunk.isSome
+  assert! chunk.get!.data == data
+  assert! (← full.getKnownSize) == some (.fixed 0)
+
+#eval fullKnownSizeLifecycle.block
+
+-- Test Full.close discards remaining content
+
+def fullClose : Async Unit := do
+  let full ← Body.Full.ofString "bye"
+  assert! !(← full.isClosed)
+  full.close
+  assert! (← full.isClosed)
+  assert! (← full.recv).isNone
+
+#eval fullClose.block
+
+-- Test Full from an empty ByteArray returns none on the first recv
+
+def fullEmptyBytes : Async Unit := do
+  let full ← Body.Full.ofByteArray ByteArray.empty
+  let result ← full.recv
+  assert! result.isNone
+
+#eval fullEmptyBytes.block
+
+-- Test Full.recvSelector resolves immediately with the stored chunk
+
+def fullRecvSelectorResolves : Async Unit := do
+  let full ← Body.Full.ofString "world"
+  let result ← Selectable.one #[
+    .case full.recvSelector pure
+  ]
+  assert! result.isSome
+  assert! result.get!.data == "world".toUTF8
+
+#eval fullRecvSelectorResolves.block
+
+-- Test Full.getKnownSize returns 0 after close
+
+def fullKnownSizeAfterClose : Async Unit := do
+  let full ← Body.Full.ofString "data"
+  assert! (← full.getKnownSize) == some (.fixed 4)
+  full.close
+  assert! (← full.getKnownSize) == some (.fixed 0)
+
+#eval fullKnownSizeAfterClose.block
+
+-- Test Full.tryRecv succeeds once and returns none thereafter
+
+def fullTryRecvIdempotent : Async Unit := do
+  let full ← Body.Full.ofString "once"
+  let first ← full.recv
+  let second ← full.recv
+  assert! first.isSome
+  assert! first.get!.data == "once".toUTF8
+  assert! second.isNone
+
+#eval fullTryRecvIdempotent.block
+
+/-! ## Empty tests -/
+
+-- Test Empty.recv always returns none
+
+def emptyBodyRecv : Async Unit := do
+  let body : Body.Empty := {}
+  let result ← body.recv
+  assert! result.isNone
+
+#eval emptyBodyRecv.block
+
+-- Test Empty.isClosed is always true
+
+def emptyBodyIsClosed : Async Unit := do
+  let body : Body.Empty := {}
+  assert! (← body.isClosed)
+
+#eval emptyBodyIsClosed.block
+
+-- Test Empty.close is a no-op: still closed and recv still returns none
+
+def emptyBodyClose : Async Unit := do
+  let body : Body.Empty := {}
+  body.close
+  assert! (← body.isClosed)
+  let result ← body.recv
+  assert! result.isNone
+
+#eval emptyBodyClose.block
+
+-- Test Empty.recvSelector resolves immediately with none
+
+def emptyBodyRecvSelector : Async Unit := do
+  let body : Body.Empty := {}
+  let result ← Selectable.one #[
+    .case body.recvSelector pure
+  ]
+  assert! result.isNone
+
+#eval emptyBodyRecvSelector.block
+
+/-! ## Any tests -/
+
+-- Test Any wrapping a Full body forwards recv correctly
+
+def anyFromFull : Async Unit := do
+  let full ← Body.Full.ofString "hello"
+  let any : Body.Any := full
+  let result ← any.recv
+  assert! result.isSome
+  assert! result.get!.data == "hello".toUTF8
+
+#eval anyFromFull.block
+
+-- Test Any wrapping an Empty body returns none and reports closed
+
+def anyFromEmpty : Async Unit := do
+  let empty : Body.Empty := {}
+  let any : Body.Any := empty
+  let result ← any.recv
+  assert! result.isNone
+  assert! (← any.isClosed)
+
+#eval anyFromEmpty.block
+
+-- Test Any.close closes the underlying body
+
+def anyCloseForwards : Async Unit := do
+  let full ← Body.Full.ofString "test"
+  let any : Body.Any := full
+  any.close
+  assert! (← any.isClosed)
+  let result ← any.recv
+  assert! result.isNone
+
+#eval anyCloseForwards.block
+
+-- Test Any.recvSelector resolves immediately for a Full body
+
+def anyRecvSelectorFromFull : Async Unit := do
+  let full ← Body.Full.ofString "sel"
+  let any : Body.Any := full
+  let result ← Selectable.one #[
+    .case any.recvSelector pure
+  ]
+  assert! result.isSome
+  assert! result.get!.data == "sel".toUTF8
+
+#eval anyRecvSelectorFromFull.block
+
+/-! ## Request.Builder body tests -/
+
+private def recvBuiltBody (body : Body.Full) : Async (Option Chunk) :=
+  body.recv
+
+-- Test Request.Builder.text sets correct headers
+
+def requestBuilderText : Async Unit := do
+  let req ← Request.post (.originForm! "/api")
+    |>.text "Hello, World!"
+
+  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
+  assert! req.line.headers.get? Header.Name.contentLength == none
+
+  let body ← recvBuiltBody req.body
+  assert! body.isSome
+  assert! body.get!.data == "Hello, World!".toUTF8
+
+#eval requestBuilderText.block
+
+-- Test Request.Builder.json sets correct headers
+
+def requestBuilderJson : Async Unit := do
+  let req ← Request.post (.originForm! "/api")
+    |>.json "{\"key\": \"value\"}"
+
+  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
+  assert! req.line.headers.get? Header.Name.contentLength == none
+  let body ← recvBuiltBody req.body
+  assert! body.isSome
+  assert! body.get!.data == "{\"key\": \"value\"}".toUTF8
+
+#eval requestBuilderJson.block
+
+-- Test Request.Builder.fromBytes sets body
+
+def requestBuilderFromBytes : Async Unit := do
+  let data := ByteArray.mk #[0x01, 0x02, 0x03]
+  let req ← Request.post (.originForm! "/api")
+    |>.fromBytes data
+
+  assert! req.line.headers.get? Header.Name.contentLength == none
+  let body ← recvBuiltBody req.body
+  assert! body.isSome
+  assert! body.get!.data == data
+
+#eval requestBuilderFromBytes.block
+
+-- Test Request.Builder.noBody creates empty body
+
+def requestBuilderNoBody : Async Unit := do
+  let req ← Request.get (.originForm! "/api")
+    |>.empty
+
+  assert! req.body == {}
+
+#eval requestBuilderNoBody.block
+
+-- Test Request.Builder.bytes sets application/octet-stream content type
+
+def requestBuilderBytes : Async Unit := do
+  let data := ByteArray.mk #[0xde, 0xad, 0xbe, 0xef]
+  let req ← Request.post (.originForm! "/api")
+    |>.bytes data
+
+  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/octet-stream")
+  let body ← recvBuiltBody req.body
+  assert! body.isSome
+  assert! body.get!.data == data
+
+#eval requestBuilderBytes.block
+
+-- Test Request.Builder.html sets text/html content type
+
+def requestBuilderHtml : Async Unit := do
+  let req ← Request.post (.originForm! "/api")
+    |>.html "<h1>Hello</h1>"
+
+  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/html; charset=utf-8")
+  let body ← recvBuiltBody req.body
+  assert! body.isSome
+  assert! body.get!.data == "<h1>Hello</h1>".toUTF8
+
+#eval requestBuilderHtml.block
+
+-- Test Request.Builder.stream creates a streaming body
+
+def requestBuilderStream : Async Unit := do
+  let req ← Request.post (.originForm! "/api")
+    |>.stream fun s => do
+      s.send (Chunk.ofByteArray "streamed".toUTF8)
+
+  let result ← req.body.recv
+  assert! result.isSome
+  assert! result.get!.data == "streamed".toUTF8
+
+#eval requestBuilderStream.block
+
+-- Test Request.Builder.noBody body is always closed and returns none
+
+def requestBuilderNoBodyAlwaysClosed : Async Unit := do
+  let req ← Request.get (.originForm! "/api")
+    |>.empty
+
+  assert! (← req.body.isClosed)
+  let result ← req.body.recv
+  assert! result.isNone
+
+#eval requestBuilderNoBodyAlwaysClosed.block
+
+/-! ## Response.Builder body tests -/
+
+-- Test Response.Builder.text sets correct headers
+
+def responseBuilderText : Async Unit := do
+  let res ← Response.ok
+    |>.text "Hello, World!"
+
+  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
+  assert! res.line.headers.get? Header.Name.contentLength == none
+
+  let body ← recvBuiltBody res.body
+  assert! body.isSome
+  assert! body.get!.data == "Hello, World!".toUTF8
+
+#eval responseBuilderText.block
+
+-- Test Response.Builder.json sets correct headers
+
+def responseBuilderJson : Async Unit := do
+  let res ← Response.ok
+    |>.json "{\"status\": \"ok\"}"
+
+  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
+  assert! res.line.headers.get? Header.Name.contentLength == none
+  let body ← recvBuiltBody res.body
+  assert! body.isSome
+  assert! body.get!.data == "{\"status\": \"ok\"}".toUTF8
+
+#eval responseBuilderJson.block
+
+-- Test Response.Builder.fromBytes sets body
+
+def responseBuilderFromBytes : Async Unit := do
+  let data := ByteArray.mk #[0xaa, 0xbb]
+  let res ← Response.ok
+    |>.fromBytes data
+
+  assert! res.line.headers.get? Header.Name.contentLength == none
+  let body ← recvBuiltBody res.body
+  assert! body.isSome
+  assert! body.get!.data == data
+
+#eval responseBuilderFromBytes.block
+
+-- Test Response.Builder.noBody creates empty body
+
+def responseBuilderNoBody : Async Unit := do
+  let res ← Response.ok
+    |>.empty
+
+  assert! res.body == {}
+
+#eval responseBuilderNoBody.block
+
+-- Test Response.Builder.bytes sets application/octet-stream content type
+
+def responseBuilderBytes : Async Unit := do
+  let data := ByteArray.mk #[0xca, 0xfe]
+  let res ← Response.ok
+    |>.bytes data
+
+  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/octet-stream")
+  let body ← recvBuiltBody res.body
+  assert! body.isSome
+  assert! body.get!.data == data
+
+#eval responseBuilderBytes.block
+
+-- Test Response.Builder.html sets text/html content type
+
+def responseBuilderHtml : Async Unit := do
+  let res ← Response.ok
+    |>.html "<p>OK</p>"
+
+  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/html; charset=utf-8")
+  let body ← recvBuiltBody res.body
+  assert! body.isSome
+  assert! body.get!.data == "<p>OK</p>".toUTF8
+
+#eval responseBuilderHtml.block
+
+-- Test Response.Builder.stream creates a streaming body
+
+def responseBuilderStream : Async Unit := do
+  let res ← Response.ok
+    |>.stream fun s => do
+      s.send (Chunk.ofByteArray "streamed".toUTF8)
+
+  let result ← res.body.recv
+  assert! result.isSome
+  assert! result.get!.data == "streamed".toUTF8
+
+#eval responseBuilderStream.block
+
+-- Test Response.Builder.noBody body is always closed and returns none
+
+def responseBuilderNoBodyAlwaysClosed : Async Unit := do
+  let res ← Response.ok
+    |>.empty
+
+  assert! (← res.body.isClosed)
+  let result ← res.body.recv
+  assert! result.isNone
+
+#eval responseBuilderNoBodyAlwaysClosed.block

tests/elab/dateTimeOrd.lean

@@ -45,4 +45,4 @@ example : Std.LawfulBEqOrd (DateTime TimeZone.GMT) := inferInstance
    "Sat Jan 01 02:01:01 2025",
    "Sat Jan 02 01:01:01 2025",
    "Sat Feb 01 01:01:01 2025",
-   "Sat Jan 01 01:01:01 2026"].map (DateTime.parse · |>.toOption.get!)
+   "Sat Jan 01 01:01:01 2026"].map (DateTime.fromAscTimeString . |>.toOption.get!)

tests/elab/deprecated_arg.lean

@@ -0,0 +1,330 @@
+/-
+Tests for the `deprecated_arg` attribute.
+-/
+
+-- `newArg` is not a parameter of the declaration
+/--
+error: `new` is not a parameter of `f1`
+-/
+#guard_msgs in
+@[deprecated_arg old new]
+def f1 (x : Nat) : Nat := x
+
+-- `oldArg` is still a parameter of the declaration (rename not applied)
+/--
+error: `old` is still a parameter of `f2`; rename it to `new` before adding `@[deprecated_arg]`
+-/
+#guard_msgs in
+@[deprecated_arg old new]
+def f2 (old new : Nat) : Nat := old + new
+
+-- Neither name is a parameter — reports that `newArg` is not a parameter
+/--
+error: `baz` is not a parameter of `f3`
+-/
+#guard_msgs in
+@[deprecated_arg bar baz]
+def f3 (x : Nat) : Nat := x
+
+-- Valid usage without `since`: warns about missing `since`
+/--
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+-/
+#guard_msgs in
+@[deprecated_arg old new]
+def f4 (new : Nat) : Nat := new
+
+-- Valid usage with `since`: no warning
+#guard_msgs in
+@[deprecated_arg old new (since := "2026-03-18")]
+def f5 (new : Nat) : Nat := new
+
+-- Multiple renames without `since`: warns twice
+/--
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+---
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+-/
+#guard_msgs in
+@[deprecated_arg old1 new1, deprecated_arg old2 new2]
+def f6 (new1 new2 : Nat) : Nat := new1 + new2
+
+/-! ## Functional tests: warning + correct elaboration -/
+
+-- Old name produces warning with code action hint and elaborates correctly
+/--
+warning: parameter `old` of `f4` has been deprecated, use `new` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲
+---
+info: f4 42 : Nat
+-/
+#guard_msgs in
+#check f4 (old := 42)
+
+-- New name produces no warning
+/--
+info: f4 42 : Nat
+-/
+#guard_msgs in
+#check f4 (new := 42)
+
+-- Positional arguments are unaffected
+/--
+info: f4 42 : Nat
+-/
+#guard_msgs in
+#check f4 42
+
+-- `since` field does not appear in warning message (consistent with `@[deprecated]`)
+/--
+warning: parameter `old` of `f5` has been deprecated, use `new` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲
+---
+info: f5 42 : Nat
+-/
+#guard_msgs in
+#check f5 (old := 42)
+
+-- Multiple renames: both warnings emitted with code action hints
+/--
+warning: parameter `old1` of `f6` has been deprecated, use `new1` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲1
+---
+warning: parameter `old2` of `f6` has been deprecated, use `new2` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲2
+---
+info: f6 1 2 : Nat
+-/
+#guard_msgs in
+#check f6 (old1 := 1) (old2 := 2)
+
+-- Multiple renames: new names produce no warnings
+/--
+info: f6 1 2 : Nat
+-/
+#guard_msgs in
+#check f6 (new1 := 1) (new2 := 2)
+
+-- Mixed: one old name, one new name
+/--
+warning: parameter `old1` of `f6` has been deprecated, use `new1` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲1
+---
+info: f6 1 2 : Nat
+-/
+#guard_msgs in
+#check f6 (old1 := 1) (new2 := 2)
+
+/-! ## Disabling the linter rejects old names -/
+
+-- When `linter.deprecated.arg` is false, old names produce a clean error
+/--
+error: Invalid argument name `old` for function `f4`
+
+Hint: Perhaps you meant one of the following parameter names:
+  • `new`: o̵l̵d̵n̲e̲w̲
+-/
+#guard_msgs in
+set_option linter.deprecated.arg false in
+#check f4 (old := 42)
+
+-- New name still works when linter is disabled
+/--
+info: f4 42 : Nat
+-/
+#guard_msgs in
+set_option linter.deprecated.arg false in
+#check f4 (new := 42)
+
+/-! ## Removed (no replacement) deprecated arguments -/
+
+-- `oldArg` is still a parameter of the declaration
+/--
+error: `removed` is still a parameter of `r1`; remove it before adding `@[deprecated_arg]`
+-/
+#guard_msgs in
+@[deprecated_arg removed]
+def r1 (removed : Nat) : Nat := removed
+
+-- Valid removed arg without `since`: warns about missing `since`
+/--
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+-/
+#guard_msgs in
+@[deprecated_arg removed]
+def r2 (x : Nat) : Nat := x
+
+-- Valid removed arg with `since`: no warning
+#guard_msgs in
+@[deprecated_arg removed (since := "2026-03-23")]
+def r3 (x : Nat) : Nat := x
+
+-- Using a removed arg produces an error with delete hint
+/--
+error: parameter `removed` of `r2` has been deprecated
+
+Hint: Delete this argument:
+  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
+-/
+#guard_msgs in
+#check r2 (removed := 42)
+
+-- Using a removed arg with `since` produces an error with delete hint
+/--
+error: parameter `removed` of `r3` has been deprecated
+
+Hint: Delete this argument:
+  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
+-/
+#guard_msgs in
+#check r3 (removed := 42)
+
+-- Normal args still work alongside removed deprecated args
+/--
+info: r2 42 : Nat
+-/
+#guard_msgs in
+#check r2 (x := 42)
+
+-- Positional args work fine
+/--
+info: r3 42 : Nat
+-/
+#guard_msgs in
+#check r3 42
+
+-- Removed arg: when linter is disabled, falls through to normal "invalid arg" error
+/--
+error: Invalid argument name `removed` for function `r2`
+
+Hint: Perhaps you meant one of the following parameter names:
+  • `x`: r̵e̵m̵o̵v̵e̵d̵x̲
+-/
+#guard_msgs in
+set_option linter.deprecated.arg false in
+#check r2 (removed := 42)
+
+-- Mix of renamed and removed on same declaration
+/--
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+---
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+-/
+#guard_msgs in
+@[deprecated_arg old new, deprecated_arg removed]
+def r4 (new : Nat) : Nat := new
+
+-- Renamed arg still warns
+/--
+warning: parameter `old` of `r4` has been deprecated, use `new` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲
+---
+info: r4 42 : Nat
+-/
+#guard_msgs in
+#check r4 (old := 42)
+
+-- Removed arg errors
+/--
+error: parameter `removed` of `r4` has been deprecated
+
+Hint: Delete this argument:
+  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
+-/
+#guard_msgs in
+#check r4 (removed := 42)
+
+@[deprecated_arg arg (since := "26.03.26")]
+def r5 (x : Nat) : Nat := x
+
+/--
+error: parameter `arg` of `r5` has been deprecated
+
+Hint: Delete this argument:
+  (̵a̵r̵g̵ ̵:̵=̵ ̵6̵)̵
+-/
+#guard_msgs in
+#check r5 3 (arg := 6)
+
+/--
+error: Invalid argument name `arg` for function `r5`
+
+Hint: Perhaps you meant one of the following parameter names:
+  • `x`: a̵r̵g̵x̲
+-/
+#guard_msgs in
+set_option linter.deprecated.arg false in
+#check r5 3 (arg := 6)
+
+/-! ## Custom deprecation messages -/
+
+-- Renamed arg with custom message
+#guard_msgs in
+@[deprecated_arg old new "this parameter was split into two" (since := "2026-03-26")]
+def m1 (new : Nat) : Nat := new
+
+-- Using renamed arg with message shows the message in the warning
+/--
+warning: parameter `old` of `m1` has been deprecated, use `new` instead: this parameter was split into two
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲
+---
+info: m1 42 : Nat
+-/
+#guard_msgs in
+#check m1 (old := 42)
+
+-- Removed arg with custom message
+#guard_msgs in
+@[deprecated_arg gone "no longer needed" (since := "2026-03-26")]
+def m2 (x : Nat) : Nat := x
+
+-- Using removed arg with message shows the message in the error
+/--
+error: parameter `gone` of `m2` has been deprecated: no longer needed
+
+Hint: Delete this argument:
+  (̵g̵o̵n̵e̵ ̵:̵=̵ ̵4̵2̵)̵
+-/
+#guard_msgs in
+#check m2 (gone := 42)
+
+-- Without custom message, behavior unchanged
+/--
+error: parameter `removed` of `r3` has been deprecated
+
+Hint: Delete this argument:
+  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
+-/
+#guard_msgs in
+#check r3 (removed := 42)
+
+-- Removed arg with text but no `since`: warns about missing `since`
+/--
+warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
+-/
+#guard_msgs in
+@[deprecated_arg dropped "use positional args"]
+def m3 (x : Nat) : Nat := x
+
+/--
+error: parameter `dropped` of `m3` has been deprecated: use positional args
+
+Hint: Delete this argument:
+  (̵d̵r̵o̵p̵p̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
+-/
+#guard_msgs in
+#check m3 (dropped := 42)

tests/elab/doDepIfAnon.lean

@@ -0,0 +1,14 @@
+-- Test that anonymous `if _ : cond then ...` works in do blocks (new do elaborator)
+set_option backward.do.legacy false
+def testDepIfAnon (n : Nat) : IO Unit := do
+  if _ : n > 0 then
+    IO.println "positive"
+  else
+    IO.println "zero"
+
+-- Test the named variant too
+def testDepIfNamed (n : Nat) : IO Unit := do
+  if h : n > 0 then
+    IO.println s!"positive: {n} > 0"
+  else
+    IO.println "zero"

tests/elab/grind_13167.lean

@@ -0,0 +1,6 @@
+module
+
+-- https://github.com/leanprover/lean4/issues/13167
+theorem Option.bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
+    pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h)) := by
+  grind [cases Option, pmap]

tests/elab/linterCoe.lean

@@ -27,7 +27,7 @@ Note: This linter can be disabled with `set_option linter.deprecatedCoercions fa
 #guard_msgs in
 def h (foo : X) : Y := foo
 
-/-- -/
+/-- A docstring to make `missingDocs` linter happy-/
 notation a " +' " b => a + b
 
 @[deprecated "" (since := "")]

tests/elab/linterMissingDocs.lean

@@ -105,3 +105,37 @@ def handleMyCmd : SimpleHandler := fun
 my_command y
 
 my_command z
+
+-- Test: empty doc strings should be treated as missing
+/---/
+def emptyDoc1 (x : Nat) := x
+
+/--
+-/
+def emptyDoc2 (x : Nat) := x
+
+/--   -/
+def emptyDoc3 (x : Nat) := x
+
+-- Test: empty doc strings on other declaration kinds
+/---/
+inductive EmptyInd where
+  /---/ | emptyCtorDoc
+  | noCtorDoc
+
+/---/
+notation:20 "empty_nota" x y => Nat.add x y
+
+/---/
+macro "empty_macro" : term => `(my_elab)
+
+/---/
+elab "empty_elab" : term => return Lean.mkConst ``false
+
+-- Test: @[inherit_doc] suppresses even with empty doc
+@[inherit_doc hasDoc]
+def inheritedDoc (x : Nat) := x
+
+-- Test: Verso doc comments with interpolated content are not empty
+/-- See {name}`hasDoc` for details. -/
+def versoDoc (x : Nat) := x

tests/elab/linterMissingDocs.lean.out.expected

@@ -109,3 +109,30 @@ Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:107:11-107:12: warning: missing doc string for my_command z
 
 Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:111:4-111:13: warning: empty doc string for public def emptyDoc1
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:115:4-115:13: warning: empty doc string for public def emptyDoc2
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:118:4-118:13: warning: empty doc string for public def emptyDoc3
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:122:10-122:18: warning: empty doc string for public inductive EmptyInd
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:123:10-123:22: warning: empty doc string for public constructor EmptyInd.emptyCtorDoc
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:124:4-124:13: warning: missing doc string for public constructor EmptyInd.noCtorDoc
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:127:0-127:8: warning: empty doc string for notation
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:130:0-130:5: warning: empty doc string for macro
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:133:0-133:4: warning: empty doc string for elab
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`

tests/elab/timeAPI.lean

@@ -629,9 +629,9 @@ Std.Time.Weekday.friday
   println! repr date.weekOfYear
   println! repr date.weekOfMonth
 
-  println! (date.format "MM-dd-uuuu")
-  println! (date.format "uuuu-MM-dd")
-  println! (date.format "uuuu-MM-dd")
+  println! date.toAmericanDateString
+  println! date.toLeanDateString
+  println! date.toSQLDateString
 
   println! date.toDaysSinceUNIXEpoch
   println! date.toTimestampAssumingUTC

tests/elab/timeCanonFormats.lean

@@ -8,7 +8,7 @@ def date₁ := zoned("2014-06-16T03:03:03-03:00")
 info: "Monday, June 16, 2014 06:03:03"
 -/
 #guard_msgs in
-#eval Formats.longDateFormat.format date₁
+#eval Formats.longDateFormat.format date₁.toDateTime
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -134,7 +134,7 @@ info: "Mon, 16 Jun 2014 03:03:03 -0300"
 #eval Formats.rfc822.format date₂
 
 /--
-info: "Mon, 16-Jun-14 03:03:03 -0300"
+info: "Mon, 16-06-2014 03:03:03 -0300"
 -/
 #guard_msgs in
 #eval Formats.rfc850.format date₂

tests/elab/timeFieldSymbols.lean

@@ -1,833 +0,0 @@
-import Std.Time
-open Std.Time
-
--- Reference date: Sunday, July 14, 2002 23:13:12.324354679 UTC+09:00 (Q3, week 28, day 195)
-def td := zoned("2002-07-14T23:13:12.324354679+09:00")
-
--- Same date/time at UTC (for UTC timezone name tests)
-def tdUTC := zoned("2002-07-14T23:13:12.324354679+00:00")
-
--- AM hour (09:13:12 for AM/PM tests)
-def tdAM := zoned("2002-07-14T09:13:12.000000000+09:00")
-
--- Exact noon and midnight (for day-period tests)
-def tdNoon := zoned("2002-07-14T12:00:00.000000000+09:00")
-def tdMidnight := zoned("2002-07-14T00:00:00.000000000+09:00")
-def tdWeekMonth := zoned("2002-08-05T23:13:12.324354679+09:00")
-
--- Named timezone (for z/V name tests)
-def tokyoTZ : TimeZone := { offset := { second := 32400 }, name := "Asia/Tokyo", abbreviation := "JST", isDST := false }
-
-def tdNamed := ZonedDateTime.ofPlainDateTime td.toPlainDateTime (TimeZone.ZoneRules.ofTimeZone tokyoTZ)
-
--- Week-based year boundary: Dec 31, 2018 is in ISO week 1 of 2019
-def tdWeekBound := ZonedDateTime.ofPlainDateTime datetime("2018-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
-
--- Additional week-based year boundary cases
--- Jan 1, 2017 (Sunday) → ISO week 52 of 2016
-def tdWeekBound2 := ZonedDateTime.ofPlainDateTime datetime("2017-01-01T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
--- Jan 2, 2017 (Monday) → ISO week 1 of 2017
-def tdWeekBound3 := ZonedDateTime.ofPlainDateTime datetime("2017-01-02T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
--- Dec 31, 2019 (Tuesday) → ISO week 1 of 2020
-def tdWeekBound4 := ZonedDateTime.ofPlainDateTime datetime("2019-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
--- Jan 1, 2021 (Friday) → ISO week 53 of 2020
-def tdWeekBound5 := ZonedDateTime.ofPlainDateTime datetime("2021-01-01T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
--- Jan 4, 2021 (Monday) → ISO week 1 of 2021
-def tdWeekBound6 := ZonedDateTime.ofPlainDateTime datetime("2021-01-04T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
-
--- Jan 1 (day 1) for D zero-padding tests
-def tdJan1 := zoned("2002-01-01T12:00:00.000000000+09:00")
-
--- Exact noon/midnight with sub-second nanos (b bug fix verification)
-def tdNoonNano     := zoned("2002-07-14T12:00:00.000000001+09:00")
-def tdMidnightNano := zoned("2002-07-14T00:00:00.000000001+09:00")
-
--- Small fractional-second values (S truncation fix verification)
--- 10ms = 10_000_000 ns  →  "010..." not "100..."
-def tdTenMs  := zoned("2002-07-14T23:13:12.010000000+09:00")
--- 1ms = 1_000_000 ns   →  "001..."
-def tdOneMs  := zoned("2002-07-14T23:13:12.001000000+09:00")
--- 1ns = 1 ns           →  "000000001"
-def tdOneNs  := zoned("2002-07-14T23:13:12.000000001+09:00")
-
--- PlainTime values for b-on-PlainTime tests
-def ptNoon         := time("12:00:00.000000000")
-def ptMidnight     := time("00:00:00.000000000")
-def ptAM           := time("09:13:12.000000000")
-def ptPM           := time("23:13:12.000000000")
-def ptNoonNano     := time("12:00:00.000000001")
-def ptMidnightNano := time("00:00:00.000000001")
-
--- Aligned week-of-month edge cases: Aug 1/4/5/11/12 2002
-def tdAug1  := zoned("2002-08-01T12:00:00.000000000+09:00")  -- Thu, W=1
-def tdAug4  := zoned("2002-08-04T12:00:00.000000000+09:00")  -- Sun, W=1
-def tdAug12 := zoned("2002-08-12T12:00:00.000000000+09:00")  -- Mon, W=3
-
--- ─────────────────────────────────────────────────────────────────────────────
--- G  Era
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "AD AD AD Anno Domini A"
--/
-#guard_msgs in
-#eval td.format "G GG GGG GGGG GGGGG"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- y  Year of era
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "2002 02 2002 02002 000002002"
--/
-#guard_msgs in
-#eval td.format "y yy yyyy yyyyy yyyyyyyyy"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- Y  Week-based year
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "2002 02 2002 02002 000002002"
--/
-#guard_msgs in
-#eval td.format "Y YY YYYY YYYYY YYYYYYYYY"
-
--- Boundary: Dec 31, 2018 belongs to ISO week 1 of 2019
-/--
-info: "2019 19 2019"
--/
-#guard_msgs in
-#eval tdWeekBound.format "Y YY YYYY"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- u  Extended year (signed, no era flip)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "2002 02 2002 02002 000002002"
--/
-#guard_msgs in
-#eval td.format "u uu uuuu uuuuu uuuuuuuuu"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- Q / q  Quarter (Q = formatting, q = standalone — same output here)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "3 03 Q3 3rd quarter 3"
--/
-#guard_msgs in
-#eval td.format "Q QQ QQQ QQQQ QQQQQ"
-
-/--
-info: "3 03 Q3 3rd quarter 3"
--/
-#guard_msgs in
-#eval td.format "q qq qqq qqqq qqqqq"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- M / L  Month (M = formatting, L = standalone — same output here)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "7 07 Jul July J"
--/
-#guard_msgs in
-#eval td.format "M MM MMM MMMM MMMMM"
-
-/--
-info: "7 07 Jul July J"
--/
-#guard_msgs in
-#eval td.format "L LL LLL LLLL LLLLL"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- w  Week of week-based year
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "28 28"
--/
-#guard_msgs in
-#eval td.format "w ww"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- W  Week of month (Monday-first)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "2"
--/
-#guard_msgs in
-#eval td.format "W"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- d  Day of month
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "14 14"
--/
-#guard_msgs in
-#eval td.format "d dd"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- D  Day of year
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "195 195 195"
--/
-#guard_msgs in
-#eval td.format "D DD DDD"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- F  Day-of-week-in-month / occurrence within the month
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "2"
--/
-#guard_msgs in
-#eval td.format "F"
-
-/--
-info: "1 1"
--/
-#guard_msgs in
-#eval tdWeekMonth.format "W F"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- E  Day of week (text only)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "Sun Sun Sun Sunday S"
--/
-#guard_msgs in
-#eval td.format "E EE EEE EEEE EEEEE"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- e  Localized day of week (count 1-2 = numeric ordinal, 3-5 = text)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "7 07 Sun Sunday S"
--/
-#guard_msgs in
-#eval td.format "e ee eee eeee eeeee"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- c  Standalone day of week (count 1 = numeric, 3-5 = text)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "7 Sun Sunday S"
--/
-#guard_msgs in
-#eval td.format "c ccc cccc ccccc"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- a  AM/PM marker (counts 1-3 = short, 4 = full, 5 = narrow)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "PM"
--/
-#guard_msgs in
-#eval td.format "a"
-
-/--
-info: "AM"
--/
-#guard_msgs in
-#eval tdAM.format "a"
-
-/--
-info: "PM PM PM PM p"
--/
-#guard_msgs in
-#eval td.format "a aa aaa aaaa aaaaa"
-
-/--
-info: "AM AM AM AM a"
--/
-#guard_msgs in
-#eval tdAM.format "a aa aaa aaaa aaaaa"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- b  Day period (counts 1-3 = short, 4 = full, 5 = narrow)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "PM PM PM PM p"
--/
-#guard_msgs in
-#eval td.format "b bb bbb bbbb bbbbb"
-
-/--
-info: "AM AM AM AM a"
--/
-#guard_msgs in
-#eval tdAM.format "b bb bbb bbbb bbbbb"
-
-/--
-info: "noon noon noon noon n"
--/
-#guard_msgs in
-#eval tdNoon.format "b bb bbb bbbb bbbbb"
-
-/--
-info: "midnight midnight midnight midnight mi"
--/
-#guard_msgs in
-#eval tdMidnight.format "b bb bbb bbbb bbbbb"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- H  Hour of day (0-23)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "23 23"
--/
-#guard_msgs in
-#eval td.format "H HH"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- h  Clock hour of AM/PM (1-12)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "11 11"
--/
-#guard_msgs in
-#eval td.format "h hh"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- K  Hour of AM/PM (0-11)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "11 11"
--/
-#guard_msgs in
-#eval td.format "K KK"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- k  Clock hour of day (1-24)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "23 23"
--/
-#guard_msgs in
-#eval td.format "k kk"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- m  Minute
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "13 13"
--/
-#guard_msgs in
-#eval td.format "m mm"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- s  Second
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "12 12"
--/
-#guard_msgs in
-#eval td.format "s ss"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- S  Fractional seconds (truncated from nanoseconds)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "3 32 324 3243 324354679"
--/
-#guard_msgs in
-#eval td.format "S SS SSS SSSS SSSSSSSSS"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- A  Milliseconds since midnight
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "83592324 83592324 83592324 83592324 083592324"
--/
-#guard_msgs in
-#eval td.format "A AA AAA AAAA AAAAAAAAA"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- n  Nanosecond (Lean/Java extension; minimum width, no truncation)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "324354679 324354679 324354679 324354679 324354679"
--/
-#guard_msgs in
-#eval td.format "n nn nnn nnnn nnnnnnnnn"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- N  Nanoseconds since midnight (Lean/Java extension; minimum width, no truncation)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "83592324354679 83592324354679 83592324354679 83592324354679 83592324354679"
--/
-#guard_msgs in
-#eval td.format "N NN NNN NNNN NNNNNNNNN"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- z  Time zone name (short = abbreviation/id, full = long name)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "+09:00 +09:00 +09:00 +09:00"
--/
-#guard_msgs in
-#eval td.format "z zz zzz zzzz"
-
-/--
-info: "UTC UTC UTC Coordinated Universal Time"
--/
-#guard_msgs in
-#eval tdUTC.format "z zz zzz zzzz"
-
-/--
-info: "JST JST JST Asia/Tokyo"
--/
-#guard_msgs in
-#eval tdNamed.format "z zz zzz zzzz"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- Z  Zone offset
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "+0900 +0900 +0900 GMT+09:00 +09:00"
--/
-#guard_msgs in
-#eval td.format "Z ZZ ZZZ ZZZZ ZZZZZ"
-
-/--
-info: "+0000 +0000 +0000 GMT Z"
--/
-#guard_msgs in
-#eval tdUTC.format "Z ZZ ZZZ ZZZZ ZZZZZ"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- O  Localized GMT offset
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "GMT+9 GMT+09:00"
--/
-#guard_msgs in
-#eval td.format "O OOOO"
-
-/--
-info: "GMT GMT"
--/
-#guard_msgs in
-#eval tdUTC.format "O OOOO"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- V  Zone ID (`VV` only; other widths rejected to match Java)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "+09:00"
--/
-#guard_msgs in
-#eval td.format "VV"
-
--- UTC offset-only zone: raw "+00:00", not normalized to "UTC"
-/--
-info: "+00:00"
--/
-#guard_msgs in
-#eval tdUTC.format "VV"
-
-/--
-info: "Asia/Tokyo"
--/
-#guard_msgs in
-#eval tdNamed.format "VV"
-
-/--
-info: "error: offset 1: invalid quantity of characters for 'V': must be 2"
--/
-#guard_msgs in
-#eval td.format "V"
-
-/--
-info: "error: offset 3: invalid quantity of characters for 'V': must be 2"
--/
-#guard_msgs in
-#eval td.format "VVV"
-
-/--
-info: "error: offset 4: invalid quantity of characters for 'V': must be 2"
--/
-#guard_msgs in
-#eval td.format "VVVV"
-
-/--
-info: "error: offset 3: invalid quantity of characters for 'd'"
--/
-#guard_msgs in
-#eval td.format "ddd"
-
-/--
-info: "error: offset 3: invalid quantity of characters for 'w'"
--/
-#guard_msgs in
-#eval td.format "www"
-
-/--
-info: "error: offset 2: invalid quantity of characters for 'W'"
--/
-#guard_msgs in
-#eval td.format "WW"
-
-/--
-info: "error: offset 2: invalid quantity of characters for 'F'"
--/
-#guard_msgs in
-#eval td.format "FF"
-
-/--
-info: "Su"
--/
-#guard_msgs in
-#eval td.format "EEEEEE"
-
-/--
-info: "Su"
--/
-#guard_msgs in
-#eval td.format "eeeeee"
-
-/--
-info: "error: offset 2: invalid quantity of characters for 'c'"
--/
-#guard_msgs in
-#eval td.format "cc"
-
-/--
-info: "Su"
--/
-#guard_msgs in
-#eval td.format "cccccc"
-
-/--
-info: "error: offset 6: invalid quantity of characters for 'a'"
--/
-#guard_msgs in
-#eval td.format "aaaaaa"
-
-/--
-info: "error: offset 3: invalid quantity of characters for 'H'"
--/
-#guard_msgs in
-#eval td.format "HHH"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- v  Generic timezone name (no DST distinction; short = abbreviation, full = name)
--- ─────────────────────────────────────────────────────────────────────────────
-
--- offset-only zone: short = raw offset, full = raw offset (same as z)
-/--
-info: "+09:00 +09:00"
--/
-#guard_msgs in
-#eval td.format "v vvvv"
-
--- UTC offset-only: normalized to "UTC"/"Coordinated Universal Time" (same as z)
-/--
-info: "UTC Coordinated Universal Time"
--/
-#guard_msgs in
-#eval tdUTC.format "v vvvv"
-
--- named zone: short = abbreviation, full = IANA name
-/--
-info: "JST Asia/Tokyo"
--/
-#guard_msgs in
-#eval tdNamed.format "v vvvv"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- X  ISO 8601 offset (uses Z for UTC)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "+09 +0900 +09:00 +0900 +09:00"
--/
-#guard_msgs in
-#eval td.format "X XX XXX XXXX XXXXX"
-
-/--
-info: "Z Z Z Z Z"
--/
-#guard_msgs in
-#eval tdUTC.format "X XX XXX XXXX XXXXX"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- x  ISO 8601 offset (no Z for UTC)
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "+09 +0900 +09:00 +0900 +09:00"
--/
-#guard_msgs in
-#eval td.format "x xx xxx xxxx xxxxx"
-
-/--
-info: "+00 +0000 +00:00 +0000 +00:00"
--/
-#guard_msgs in
-#eval tdUTC.format "x xx xxx xxxx xxxxx"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- Y  Week-based year: extended boundary cases
--- ─────────────────────────────────────────────────────────────────────────────
-
--- Jan 1, 2017 is Sunday → belongs to ISO week 52 of 2016
-/--
-info: "2016 16 2016"
--/
-#guard_msgs in
-#eval tdWeekBound2.format "Y YY YYYY"
-
--- Jan 2, 2017 is Monday → first day of ISO week 1 of 2017
-/--
-info: "2017 17 2017"
--/
-#guard_msgs in
-#eval tdWeekBound3.format "Y YY YYYY"
-
--- Dec 31, 2019 is Tuesday → belongs to ISO week 1 of 2020
-/--
-info: "2020 20 2020"
--/
-#guard_msgs in
-#eval tdWeekBound4.format "Y YY YYYY"
-
--- Jan 1, 2021 is Friday → belongs to ISO week 53 of 2020
-/--
-info: "2020 20 2020"
--/
-#guard_msgs in
-#eval tdWeekBound5.format "Y YY YYYY"
-
--- Jan 4, 2021 is Monday → first day of ISO week 1 of 2021
-/--
-info: "2021 21 2021"
--/
-#guard_msgs in
-#eval tdWeekBound6.format "Y YY YYYY"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- w  Week of year paired with Y: check they agree at boundaries
--- ─────────────────────────────────────────────────────────────────────────────
-
--- Jan 1, 2017 → Y=2016 w=52
-/--
-info: "2016 52"
--/
-#guard_msgs in
-#eval tdWeekBound2.format "Y w"
-
--- Jan 2, 2017 → Y=2017 w=1
-/--
-info: "2017 1"
--/
-#guard_msgs in
-#eval tdWeekBound3.format "Y w"
-
--- Dec 31, 2019 → Y=2020 w=1
-/--
-info: "2020 1"
--/
-#guard_msgs in
-#eval tdWeekBound4.format "Y w"
-
--- Jan 1, 2021 → Y=2020 w=53
-/--
-info: "2020 53"
--/
-#guard_msgs in
-#eval tdWeekBound5.format "Y w"
-
--- Jan 4, 2021 → Y=2021 w=1
-/--
-info: "2021 1"
--/
-#guard_msgs in
-#eval tdWeekBound6.format "Y w"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- D  Day of year: zero-padding with count 1/2/3 for day 1
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "1 01 001"
--/
-#guard_msgs in
-#eval tdJan1.format "D DD DDD"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- W  Aligned week-of-month: Java ALIGNED_WEEK_OF_MONTH = (dayOfMonth-1)/7+1
--- ─────────────────────────────────────────────────────────────────────────────
-
--- Aug 1 (Thu): (1-1)/7+1 = 1 → W=1
-/--
-info: "1"
--/
-#guard_msgs in
-#eval tdAug1.format "W"
-
--- Aug 4 (Sun): (4-1)/7+1 = 1 → W=1
-/--
-info: "1"
--/
-#guard_msgs in
-#eval tdAug4.format "W"
-
--- Aug 5 (Mon): (5-1)/7+1 = 1 → W=1
-/--
-info: "1"
--/
-#guard_msgs in
-#eval tdWeekMonth.format "W"
-
--- Aug 12 (Mon): (12-1)/7+1 = 2 → W=2
-/--
-info: "2"
--/
-#guard_msgs in
-#eval tdAug12.format "W"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- h / K / k  Hour edge cases: midnight (H=0) and noon (H=12)
--- ─────────────────────────────────────────────────────────────────────────────
-
--- midnight: H=0, h=12, K=0, k=24
-/--
-info: "0 12 0 24"
--/
-#guard_msgs in
-#eval tdMidnight.format "H h K k"
-
--- noon: H=12, h=12, K=0, k=12
-/--
-info: "12 12 0 12"
--/
-#guard_msgs in
-#eval tdNoon.format "H h K k"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- S  Fractional seconds: truncation for values < 10^8 nanoseconds
--- ─────────────────────────────────────────────────────────────────────────────
-
--- 10ms = 10_000_000 ns → left-pad to 9 → "010000000"
-/--
-info: "0 01 010 0100 010000000"
--/
-#guard_msgs in
-#eval tdTenMs.format "S SS SSS SSSS SSSSSSSSS"
-
--- 1ms = 1_000_000 ns → "001000000"
-/--
-info: "0 00 001 0010 001000000"
--/
-#guard_msgs in
-#eval tdOneMs.format "S SS SSS SSSS SSSSSSSSS"
-
--- 1ns → "000000001"
-/--
-info: "0 00 000 0000 000000001"
--/
-#guard_msgs in
-#eval tdOneNs.format "S SS SSS SSSS SSSSSSSSS"
-
--- zero nanoseconds → "000000000"
-/--
-info: "0 00 000 0000 000000000"
--/
-#guard_msgs in
-#eval tdNoon.format "S SS SSS SSSS SSSSSSSSS"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- b  Day period: nanoseconds prevent noon/midnight classification
--- ─────────────────────────────────────────────────────────────────────────────
-
--- 12:00:00.000000001 → PM, not noon (non-zero nanosecond)
-/--
-info: "PM"
--/
-#guard_msgs in
-#eval tdNoonNano.format "b"
-
--- 00:00:00.000000001 → AM, not midnight
-/--
-info: "AM"
--/
-#guard_msgs in
-#eval tdMidnightNano.format "b"
-
--- exact noon and midnight still work
-/--
-info: "noon midnight"
--/
-#guard_msgs in
-#eval s!"{tdNoon.format "b"} {tdMidnight.format "b"}"
-
--- ─────────────────────────────────────────────────────────────────────────────
--- b  Day period on PlainTime
--- ─────────────────────────────────────────────────────────────────────────────
-
-/--
-info: "noon"
--/
-#guard_msgs in
-#eval ptNoon.format "b"
-
-/--
-info: "midnight"
--/
-#guard_msgs in
-#eval ptMidnight.format "b"
-
-/--
-info: "AM"
--/
-#guard_msgs in
-#eval ptAM.format "b"
-
-/--
-info: "PM"
--/
-#guard_msgs in
-#eval ptPM.format "b"
-
--- non-zero nano at noon/midnight → falls back to AM/PM
-/--
-info: "PM"
--/
-#guard_msgs in
-#eval ptNoonNano.format "b"
-
-/--
-info: "AM"
--/
-#guard_msgs in
-#eval ptMidnightNano.format "b"

tests/elab/timeFormats.lean

@@ -1,17 +1,17 @@
 import Std.Time
 open Std.Time
 
-def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
-def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
-def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : Format Awareness.any := datespec("MMMM D, uuuu h:mm a")
-def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
-def Time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
-def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
-def EraDate : Format Awareness.any := datespec("MM D, uuuu G")
-def DateSmall : Format Awareness.any := datespec("uu-MM-dd")
+def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
+def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
+def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : GenericFormat .any := datespec("MMMM D, uuuu h:mm aa")
+def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
+def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
+def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
+def EraDate : GenericFormat .any := datespec("MM D, uuuu G")
+def DateSmall : GenericFormat .any := datespec("uu-MM-dd")
 
 -- Dates
 
@@ -27,7 +27,7 @@ def time₂ := time("03:11:01")
 info: "Monday, June 16, 2014 03:03:03 -0300"
 -/
 #guard_msgs in
-#eval FullDayTimeZone.format date₁
+#eval FullDayTimeZone.format date₁.toDateTime
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -197,13 +197,13 @@ info: "03:11:01 AM"
 info: "2024-08-15T14:03:47-03:00"
 -/
 #guard_msgs in
-#eval Formats.iso8601.format dateBR₁
+#eval dateBR₁.toISO8601String
 
 /--
 info: "2024-08-15T14:03:47Z"
 -/
 #guard_msgs in
-#eval Formats.iso8601.format dateUTC₁
+#eval dateUTC₁.toISO8601String
 
 /--
 info: "06/16/2014"
@@ -297,7 +297,7 @@ def tz : TimeZone := { offset := { second := -3600 }, name := "America/Sao_Paulo
 def zoned₆ := ZonedDateTime.ofPlainDateTime (zoned₄.toPlainDateTime) (TimeZone.ZoneRules.ofTimeZone tz)
 
 /--
-info: "AD AD AD Anno Domini A"
+info: "CE CE CE Common Era C"
 -/
 #guard_msgs in
 #eval zoned₄.format "G GG GGG GGGG GGGGG"
@@ -321,10 +321,10 @@ info: "195 195 195"
 #eval zoned₄.format "D DD DDD"
 
 /--
-info: "14 14"
+info: "14 14 014 0014 00014"
 -/
 #guard_msgs in
-#eval zoned₄.format "d dd"
+#eval zoned₄.format "d dd ddd dddd ddddd"
 
 /--
 info: "7 07 Jul July J"
@@ -339,16 +339,16 @@ info: "3 03 3rd quarter 3"
 #eval zoned₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28"
+info: "28 28 028 0028"
 -/
 #guard_msgs in
-#eval zoned₄.format "w ww"
+#eval zoned₄.format "w ww www wwww"
 
 /--
-info: "2"
+info: "2 02 002 0002"
 -/
 #guard_msgs in
-#eval zoned₄.format "W"
+#eval zoned₄.format "W WW WWW WWWW"
 
 /--
 info: "Sun Sun Sun Sunday S"
@@ -363,46 +363,46 @@ info: "7 07 Sun Sunday S"
 #eval zoned₄.format "e ee eee eeee eeeee"
 
 /--
-info: "2"
+info: "2 02 002 0002"
 -/
 #guard_msgs in
-#eval zoned₄.format "F"
+#eval zoned₄.format "F FF FFF FFFF"
 
 /--
-info: "11 11"
+info: "11 11 011 0011 0011"
 -/
 #guard_msgs in
-#eval zoned₄.format "h hh"
+#eval zoned₄.format "h hh hhh hhhh hhhh"
 
 /--
-info: "11 11"
+info: "11 11 011 0011 000011"
 -/
 #guard_msgs in
-#eval zoned₄.format "K KK"
+#eval zoned₄.format "K KK KKK KKKK KKKKKK"
 
 /--
-info: "23 23"
+info: "23 23 023 0023 000023"
 -/
 #guard_msgs in
-#eval zoned₄.format "k kk"
+#eval zoned₄.format "k kk kkk kkkk kkkkkk"
 
 /--
-info: "23 23"
+info: "23 23 023 0023 00023"
 -/
 #guard_msgs in
-#eval zoned₄.format "H HH"
+#eval zoned₄.format "H HH HHH HHHH HHHHH"
 
 /--
-info: "13 13"
+info: "13 13 013 0013 00013"
 -/
 #guard_msgs in
-#eval zoned₄.format "m mm"
+#eval zoned₄.format "m mm mmm mmmm mmmmm"
 
 /--
-info: "12 12"
+info: "12 12 012 0012 00012"
 -/
 #guard_msgs in
-#eval zoned₄.format "s ss"
+#eval zoned₄.format "s ss sss ssss sssss"
 
 
 /--
@@ -441,7 +441,7 @@ info: "+09:00 +09:00 +09:00 +09:00"
 #eval zoned₄.format "z zz zzzz zzzz"
 
 /--
-info: "UTC UTC Coordinated Universal Time Coordinated Universal Time"
+info: "+00:00 +00:00 +00:00 +00:00"
 -/
 #guard_msgs in
 #eval zoned₅.format "z zz zzzz zzzz"
@@ -483,7 +483,7 @@ info: "+0900 +0900 +0900 GMT+09:00 +09:00"
 #eval zoned₄.format "Z ZZ ZZZ ZZZZ ZZZZZ"
 
 /--
-info: "AD AD AD Anno Domini A"
+info: "CE CE CE Common Era C"
 -/
 #guard_msgs in
 #eval datetime₄.format "G GG GGG GGGG GGGGG"
@@ -513,10 +513,10 @@ info: "7 07 Jul J"
 #eval datetime₄.format "M MM MMM MMMMM"
 
 /--
-info: "14 14"
+info: "14 14 014 0014 00014"
 -/
 #guard_msgs in
-#eval datetime₄.format "d dd"
+#eval datetime₄.format "d dd ddd dddd ddddd"
 
 /--
 info: "7 07 Jul July J"
@@ -525,9 +525,9 @@ info: "7 07 Jul July J"
 #eval datetime₄.format "M MM MMM MMMM MMMMM"
 
 /--
-info: "14 14"
+info: "14 14 0014 0014"
 -/#guard_msgs in
-#eval datetime₄.format "d dd"
+#eval datetime₄.format "d dd dddd dddd"
 
 /--
 info: "3 03 3rd quarter 3"
@@ -536,16 +536,16 @@ info: "3 03 3rd quarter 3"
 #eval datetime₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28"
+info: "28 28 028 0028"
 -/
 #guard_msgs in
-#eval datetime₄.format "w ww"
+#eval datetime₄.format "w ww www wwww"
 
 /--
-info: "2"
+info: "2 02 002 0002"
 -/
 #guard_msgs in
-#eval datetime₄.format "W"
+#eval datetime₄.format "W WW WWW WWWW"
 
 /--
 info: "Sun Sun Sun Sunday S"
@@ -560,46 +560,46 @@ info: "7 07 Sun Sunday S"
 #eval datetime₄.format "e ee eee eeee eeeee"
 
 /--
-info: "2"
+info: "2 02 002 0002"
 -/
 #guard_msgs in
-#eval datetime₄.format "F"
+#eval datetime₄.format "F FF FFF FFFF"
 
 /--
-info: "11 11"
+info: "11 11 011 0011 0011"
 -/
 #guard_msgs in
-#eval datetime₄.format "h hh"
+#eval datetime₄.format "h hh hhh hhhh hhhh"
 
 /--
-info: "11 11"
+info: "11 11 011 0011 000011"
 -/
 #guard_msgs in
-#eval datetime₄.format "K KK"
+#eval datetime₄.format "K KK KKK KKKK KKKKKK"
 
 /--
-info: "23 23"
+info: "23 23 023 0023 000023"
 -/
 #guard_msgs in
-#eval datetime₄.format "k kk"
+#eval datetime₄.format "k kk kkk kkkk kkkkkk"
 
 /--
-info: "23 23"
+info: "23 23 023 0023 00023"
 -/
 #guard_msgs in
-#eval datetime₄.format "H HH"
+#eval datetime₄.format "H HH HHH HHHH HHHHH"
 
 /--
-info: "13 13"
+info: "13 13 013 0013 00013"
 -/
 #guard_msgs in
-#eval datetime₄.format "m mm"
+#eval datetime₄.format "m mm mmm mmmm mmmmm"
 
 /--
-info: "12 12"
+info: "12 12 012 0012 00012"
 -/
 #guard_msgs in
-#eval datetime₄.format "s ss"
+#eval datetime₄.format "s ss sss ssss sssss"
 
 
 /--
@@ -632,40 +632,41 @@ info: "83592324354679 83592324354679 83592324354679 83592324354679 8359232435467
 #eval datetime₄.format "N NN NNN NNNN NNNNNNNNN"
 
 /--
-info: "11 11"
+info: "11 11 011 0011 0011"
 -/
 #guard_msgs in
-#eval time₄.format "h hh"
+#eval time₄.format "h hh hhh hhhh hhhh"
 
 /--
-info: "11 11"
+info: "11 11 011 0011 000011"
 -/
 #guard_msgs in
-#eval time₄.format "K KK"
+#eval time₄.format "K KK KKK KKKK KKKKKK"
 
 /--
-info: "23 23"
+info: "23 23 023 0023 000023"
+
 -/
 #guard_msgs in
-#eval time₄.format "k kk"
+#eval time₄.format "k kk kkk kkkk kkkkkk"
 
 /--
-info: "23 23"
+info: "23 23 023 0023 00023"
 -/
 #guard_msgs in
-#eval time₄.format "H HH"
+#eval time₄.format "H HH HHH HHHH HHHHH"
 
 /--
-info: "13 13"
+info: "13 13 013 0013 00013"
 -/
 #guard_msgs in
-#eval time₄.format "m mm"
+#eval time₄.format "m mm mmm mmmm mmmmm"
 
 /--
-info: "12 12"
+info: "12 12 012 0012 00012"
 -/
 #guard_msgs in
-#eval time₄.format "s ss"
+#eval time₄.format "s ss sss ssss sssss"
 
 
 /--
@@ -698,7 +699,7 @@ info: "83592324354679 83592324354679 83592324354679 83592324354679 8359232435467
 #eval time₄.format "N NN NNN NNNN NNNNNNNNN"
 
 /--
-info: "AD AD AD Anno Domini A"
+info: "CE CE CE Common Era C"
 -/
 #guard_msgs in
 #eval date₄.format "G GG GGG GGGG GGGGG"
@@ -728,10 +729,10 @@ info: "7 07 Jul J"
 #eval date₄.format "M MM MMM MMMMM"
 
 /--
-info: "14 14"
+info: "14 14 014 0014 00014"
 -/
 #guard_msgs in
-#eval date₄.format "d dd"
+#eval date₄.format "d dd ddd dddd ddddd"
 
 /--
 info: "7 07 Jul July J"
@@ -740,9 +741,9 @@ info: "7 07 Jul July J"
 #eval date₄.format "M MM MMM MMMM MMMMM"
 
 /--
-info: "14 14"
+info: "14 14 0014 0014"
 -/#guard_msgs in
-#eval date₄.format "d dd"
+#eval date₄.format "d dd dddd dddd"
 
 /--
 info: "3 03 3rd quarter 3"
@@ -751,16 +752,16 @@ info: "3 03 3rd quarter 3"
 #eval date₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28"
+info: "28 28 028 0028"
 -/
 #guard_msgs in
-#eval date₄.format "w ww"
+#eval date₄.format "w ww www wwww"
 
 /--
-info: "2"
+info: "2 02 002 0002"
 -/
 #guard_msgs in
-#eval date₄.format "W"
+#eval date₄.format "W WW WWW WWWW"
 
 /--
 info: "Sun Sun Sun Sunday S"
@@ -775,19 +776,19 @@ info: "7 07 Sun Sunday S"
 #eval date₄.format "e ee eee eeee eeeee"
 
 /--
-info: "2"
+info: "2 02 002 0002"
 -/
 #guard_msgs in
-#eval date₄.format "F"
+#eval date₄.format "F FF FFF FFFF"
 
 /--
-info: "-2000 2001 BC"
+info: "-2000 2001 BCE"
 -/
 #guard_msgs in
 #eval datetime₅.format "uuuu yyyy G"
 
 /--
-info: "2002 2002 AD"
+info: "2002 2002 CE"
 -/
 #guard_msgs in
 #eval datetime₄.format "uuuu yyyy G"
@@ -824,7 +825,7 @@ info: ("19343232432-01-04T01:04:03.000000000",
 #guard_msgs in
 #eval
   let r := PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 3 0)
-  let s := r.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS"
+  let s := r.toLeanDateTimeString
   let r := PlainDateTime.parse s
   (s, r, datetime("1932-01-02T05:04:03.000000000"))
 
@@ -839,7 +840,7 @@ def tuple6Mk (a : f) (b : g) (c : h) (d : i) (e : j) (k : z) := some (a, b, c, d
 Parsing Length Tests
 -/
 
-def uFormat : Format Awareness.any := datespec("u uu uuuu uuuuu")
+def uFormat : GenericFormat .any := datespec("u uu uuuu uuuuu")
 
 #eval do assert! (uFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk)
 #eval do assert! (uFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk)
@@ -854,7 +855,7 @@ def uFormat : Format Awareness.any := datespec("u uu uuuu uuuuu")
 #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk)
 #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk)
 
-def yFormat : Format Awareness.any := datespec("y yy yyyy yyyyy")
+def yFormat : GenericFormat .any := datespec("y yy yyyy yyyyy")
 
 #eval do assert! (yFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk)
 #eval do assert! (yFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk)
@@ -869,7 +870,7 @@ def yFormat : Format Awareness.any := datespec("y yy yyyy yyyyy")
 #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk)
 #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk)
 
-def dFormat : Format Awareness.any := datespec("D DD DDD")
+def dFormat : GenericFormat .any := datespec("D DD DDD")
 
 #eval do assert! (dFormat.parseBuilder tuple3Mk "1 12 123" |>.isOk)
 #eval do assert! (dFormat.parseBuilder tuple3Mk "323 12 123" |>.isOk)
@@ -878,23 +879,23 @@ def dFormat : Format Awareness.any := datespec("D DD DDD")
 #eval do assert! (not <| dFormat.parseBuilder tuple3Mk "1 123 123" |>.isOk)
 #eval do assert! (not <| dFormat.parseBuilder tuple3Mk "367 12 123" |>.isOk)
 
-def dayOfMonthFormat : Format Awareness.any := datespec("d dd")
+def dddFormat : GenericFormat .any := datespec("d dd ddd dddd ddddd")
 
-#eval do assert! (dayOfMonthFormat.parseBuilder tuple2Mk "1 12" |>.isOk)
-#eval do assert! (dayOfMonthFormat.parseBuilder tuple2Mk "31 31" |>.isOk)
+#eval do assert! (dddFormat.parseBuilder tuple5Mk "1 12 031 0031 00031" |>.isOk)
+#eval do assert! (dddFormat.parseBuilder tuple5Mk "000031 12 031 0031 00031" |>.isOk)
 
-#eval do assert! (not <| dayOfMonthFormat.parseBuilder tuple2Mk "1 123" |>.isOk)
-#eval do assert! (not <| dayOfMonthFormat.parseBuilder tuple2Mk "32 31" |>.isOk)
+#eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 12 0031 00031" |>.isOk)
+#eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 031 0031 000031" |>.isOk)
 
-def wFormat : Format Awareness.any := datespec("w ww")
+def wFormat : GenericFormat .any := datespec("w ww www wwww")
 
-#eval do assert! (wFormat.parseBuilder tuple2Mk "1 01" |>.isOk)
-#eval do assert! (wFormat.parseBuilder tuple2Mk "2 01" |>.isOk)
+#eval do assert! (wFormat.parseBuilder tuple4Mk "1 01 031 0031" |>.isOk)
+#eval do assert! (wFormat.parseBuilder tuple4Mk "2 01 031 0031" |>.isOk)
 
-#eval do assert! (not <| wFormat.parseBuilder tuple2Mk "2 031" |>.isOk)
-#eval do assert! (not <| wFormat.parseBuilder tuple2Mk "54 01" |>.isOk)
+#eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 00310" |>.isOk)
+#eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 031" |>.isOk)
 
-def qFormat : Format Awareness.any := datespec("q qq")
+def qFormat : GenericFormat .any := datespec("q qq")
 
 #eval do assert! (qFormat.parseBuilder tuple2Mk "1 02" |>.isOk)
 #eval do assert! (qFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -902,14 +903,15 @@ def qFormat : Format Awareness.any := datespec("q qq")
 #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def WFormat : Format Awareness.any := datespec("W")
+def WFormat : GenericFormat .any := datespec("W WW")
 
-#eval do assert! (WFormat.parseBuilder some "1" |>.isOk)
-#eval do assert! (WFormat.parseBuilder some "3" |>.isOk)
+#eval do assert! (WFormat.parseBuilder tuple2Mk "1 06" |>.isOk)
+#eval do assert! (WFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
 
-#eval do assert! (not <| WFormat.parseBuilder some "12" |>.isOk)
+#eval do assert! (not <| WFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
+#eval do assert! (not <| WFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def eFormat : Format Awareness.any := datespec("e ee")
+def eFormat : GenericFormat .any := datespec("e ee")
 
 #eval do assert! (eFormat.parseBuilder tuple2Mk "1 07" |>.isOk)
 #eval do assert! (eFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -917,15 +919,15 @@ def eFormat : Format Awareness.any := datespec("e ee")
 #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def FFormat : Format Awareness.any := datespec("F")
+def FFormat : GenericFormat .any := datespec("F FF")
 
-#eval do assert! (FFormat.parseBuilder some "1" |>.isOk)
-#eval do assert! (FFormat.parseBuilder some "3" |>.isOk)
+#eval do assert! (FFormat.parseBuilder tuple2Mk "1 04" |>.isOk)
+#eval do assert! (FFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
 
-#eval do assert! (not <| FFormat.parseBuilder some "12" |>.isOk)
-#eval do assert! (not <| FFormat.parseBuilder some "6" |>.isOk)
+#eval do assert! (not <| FFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
+#eval do assert! (not <| FFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def hFormat : Format Awareness.any := datespec("h hh")
+def hFormat : GenericFormat .any := datespec("h hh")
 
 #eval do assert! (hFormat.parseBuilder tuple2Mk "1 09" |>.isOk)
 #eval do assert! (hFormat.parseBuilder tuple2Mk "12 12" |>.isOk)
@@ -947,16 +949,16 @@ info: zoned("2002-07-14T14:13:12.000000000+23:59")
 info: Except.error "offset 22: invalid hour offset: 24. Must be between 0 and 23."
 -/
 #guard_msgs in
-#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+24:59"
+#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+24:59"
 
 /--
 info: Except.error "offset 25: invalid minute offset: 60. Must be between 0 and 59."
 -/
 #guard_msgs in
-#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+23:60"
+#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+23:60"
 
 /--
 info: Except.ok (zoned("2002-07-14T14:13:12.000000000Z"))
 -/
 #guard_msgs in
-#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+00:00"
+#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+00:00"

tests/elab/timeIO.lean

@@ -40,9 +40,9 @@ info: 2013-10-19T23:59:59.000000000-03:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Sao_Paulo"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-19T23:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:01") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-19T23:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:00") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:01") zr |>.toLeanDateTimeWithZoneString}"
 
 /-
 Java:
@@ -59,9 +59,9 @@ info: 2019-11-03T01:59:59.000000000-05:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Chicago"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T01:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:59:59") zr |>.toLeanDateTimeWithZoneString}"
 
 /-
 Java:
@@ -78,6 +78,6 @@ info: 2003-10-26T01:59:59.000000000-05:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Monterrey"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.toLeanDateTimeWithZoneString}"

tests/elab/timeLimits.lean

@@ -2,9 +2,9 @@ import Std.Time
 open Std.Time
 
 
-def ISO8601UTCAllow : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
-def ISO8601UTCNot : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
-def ISO8601UTCDef : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
+def ISO8601UTCAllow : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
+def ISO8601UTCNot : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
+def ISO8601UTCDef : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
 
 /--
 info: Except.ok (zoned("2002-07-14T23:14:00.324354679-23:59"))

tests/elab/timeLocalDateTime.lean

@@ -2,8 +2,8 @@ import Std.Time
 import Init
 open Std.Time
 
-def ShortDateTime : Format Awareness.any := datespec("dd/MM/uuuu HH:mm:ss")
-def ShortDate : Format Awareness.any := datespec("dd/MM/uuuu")
+def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss")
+def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu")
 
 def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second
 def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year

tests/elab/timeParse.lean

@@ -1,18 +1,18 @@
 import Std.Time
 open Std.Time
 
-def ISO8601UTC : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
-def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
-def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
-def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : Format Awareness.any := datespec("MMMM dd, uuuu hh:mm a")
-def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
-def Time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
-def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
+def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
+def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
+def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
+def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
+def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
+def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
+def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
 
-def Full12HourWrong : Format Awareness.any := datespec("MM/dd/uuuu hh:mm:ss a XXX")
+def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
 
 -- Dates
 
@@ -30,7 +30,7 @@ info: "2014-06-16T03:03:03.000000100-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := ISO8601UTC.parse! "2014-06-16T03:03:03.000000100-03:00"
-    ISO8601UTC.format t
+    ISO8601UTC.format t.toDateTime
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -41,7 +41,7 @@ info: "2014-06-16T03:03:03.000000000-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := RFC1123.parse! "Mon, 16 Jun 2014 03:03:03 -0300"
-    ISO8601UTC.format t
+    ISO8601UTC.format t.toDateTime
 
 def tm₃ := date₁.toTimestamp
 def date₃ := DateTime.ofTimestamp tm₃ brTZ
@@ -52,7 +52,7 @@ info: "2014-06-16T00:00:00.000000000Z"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := ShortDate.parse! "06/16/2014"
-    ISO8601UTC.format t
+    ISO8601UTC.format t.toDateTime
 
 -- the timestamp is always related to UTC.
 
@@ -73,7 +73,7 @@ info: "2024-08-15T13:28:12.000000000-03:00"
 #guard_msgs in
 #eval
     let t := FullDayTimeZone.parse! "Thursday, August 15, 2024 13:28:12 -0300"
-    ISO8601UTC.format t
+    ISO8601UTC.format t.toDateTime
 
 /--
 info: "2024-08-16T01:28:00.000000000Z"
@@ -81,7 +81,7 @@ info: "2024-08-16T01:28:00.000000000Z"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := LongDateTime.parse! "August 16, 2024 01:28 AM"
-    ISO8601UTC.format t
+    ISO8601UTC.format t.toDateTime
 
 /--
 info: "0000-12-31T22:28:12.000000000+09:00"
@@ -105,7 +105,7 @@ info: "Thu 15 Aug 2024 16:28"
 #guard_msgs in
 #eval
     let t2 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 16:28:12 -0000"
-    CustomDayTime.format t2
+    CustomDayTime.format t2.toDateTime
 
 /--
 info: "2024-08-16T13:28:00.000000000Z"
@@ -113,7 +113,7 @@ info: "2024-08-16T13:28:00.000000000Z"
 #guard_msgs in
 #eval
     let t5 : ZonedDateTime := CustomDayTime.parse! "Thu 16 Aug 2024 13:28"
-    ISO8601UTC.format t5
+    ISO8601UTC.format t5.toDateTime
 
 /--
 info: "2024-08-16T01:28:12.000000000+09:00"
@@ -153,7 +153,7 @@ info: "2024-08-15T14:03:47.000000000-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 -0300"
-    ISO8601UTC.format t
+    ISO8601UTC.format t.toDateTime
 
 /--
 info: "2024-08-15T14:03:47.000000000+09:00"
@@ -161,7 +161,7 @@ info: "2024-08-15T14:03:47.000000000+09:00"
 #guard_msgs in
 #eval
     let t1 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 +0900"
-    ISO8601UTC.format t1
+    ISO8601UTC.format t1.toDateTime
 
 /--
 info: "2014-06-16T03:03:03.000000000-03:00"
@@ -169,7 +169,7 @@ info: "2014-06-16T03:03:03.000000000-03:00"
 #guard_msgs in
 #eval
     let t2 : ZonedDateTime := FullDayTimeZone.parse! "Monday, June 16, 2014 03:03:03 -0300"
-    ISO8601UTC.format t2
+    ISO8601UTC.format t2.toDateTime
 
 /--
 info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
@@ -177,7 +177,7 @@ info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 AM +03:00"
-    (ISO8601UTC.format ·) <$> t2
+    (ISO8601UTC.format ·.toDateTime) <$> t2
 
 /--
 info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
@@ -185,7 +185,7 @@ info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 PM +03:00"
-    (ISO8601UTC.format ·) <$> t2
+    (ISO8601UTC.format ·.toDateTime) <$> t2
 
 /--
 info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
@@ -193,7 +193,7 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 AM +03:00"
-    (ISO8601UTC.format ·) <$> t2
+    (ISO8601UTC.format ·.toDateTime) <$> t2
 
 /--
 info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
@@ -201,4 +201,4 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 PM +03:00"
-    (ISO8601UTC.format ·) <$> t2
+    (ISO8601UTC.format ·.toDateTime) <$> t2

tests/elab/timeSet.lean

@@ -1,18 +1,18 @@
 import Std.Time
 open Std.Time
 
-def ISO8601UTC : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
-def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
-def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
-def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : Format Awareness.any := datespec("MMMM dd, uuuu hh:mm a")
-def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
-def Time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
-def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
+def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
+def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
+def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
+def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
+def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
+def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
+def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
 
-def Full12HourWrong : Format Awareness.any := datespec("MM/dd/uuuu hh:mm:ss a XXX")
+def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
 
 -- Dates
 

tests/elab/timeTzifParse.lean

@@ -98,13 +98,13 @@ info: 0
 #eval code.v1.utLocalIndicators.size
 
 /--
-info: zoned("1969-12-31T21:00:00.000000000-03:00[America/Sao_Paulo]")
+info: zoned("1969-12-31T21:00:00.000000000-03:00")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 0) rules
 
 /--
-info: zoned("2012-12-10T00:35:47.000000000-02:00[America/Sao_Paulo]")
+info: zoned("2012-12-10T00:35:47.000000000-02:00")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 1355106947) rules

tests/elab/versoDocs.lean

@@ -241,7 +241,6 @@ error: Unknown constant `b`
 
 Hint: Insert a fully-qualified name:
   • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲b̲)̲}`b`
-  • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲S̲t̲d̲.̲T̲i̲m̲e̲.̲M̲o̲d̲i̲f̲i̲e̲r̲.̲b̲)̲}`b`
   • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲M̲e̲t̲a̲.̲G̲r̲i̲n̲d̲.̲A̲r̲i̲t̲h̲.̲C̲u̲t̲s̲a̲t̲.̲D̲v̲d̲S̲o̲l̲u̲t̲i̲o̲n̲.̲b̲)̲}`b`
 -/
 #guard_msgs in

tests/elab/versoDocs.lean.out.expected

@@ -5,7 +5,7 @@ Nat.gcd.induction' {P : Nat → Nat → Prop} (m n : Nat) (H0 : ∀ (n : Nat), P
   (H1 : ∀ (m n : Nat), 0 < m → P (n % m) m → P m n) : P m n
 something : Unit
 yetMore' : Unit
-versoDocs.lean:632:43-632:53: warning: Code element could be more specific.
+versoDocs.lean:631:43-631:53: warning: Code element could be more specific.
 
 Hint: Insert a role to document it:
   • {̲l̲e̲a̲n̲}̲`-checked`

tests/pkg/deprecated_arg/DeprecatedArg.lean

@@ -0,0 +1 @@
+import DeprecatedArg.Use

tests/pkg/deprecated_arg/DeprecatedArg/Def.lean

@@ -0,0 +1,5 @@
+@[deprecated_arg arg foo (since := "2026-03-18")]
+def f (foo : Nat) : Nat := foo + 1
+
+@[deprecated_arg old1 new1 (since := "2026-03-18"), deprecated_arg old2 new2 (since := "2026-03-18")]
+def g (new1 new2 : Nat) : Nat := new1 + new2

tests/pkg/deprecated_arg/DeprecatedArg/Use.lean

@@ -0,0 +1,55 @@
+import DeprecatedArg.Def
+
+-- Cross-file: old name produces warning
+/--
+warning: parameter `arg` of `f` has been deprecated, use `foo` instead
+
+Hint: Rename this argument:
+  a̵r̵g̵f̲o̲o̲
+---
+info: f 42 : Nat
+-/
+#guard_msgs in
+#check f (arg := 42)
+
+-- Cross-file: new name produces no warning
+/--
+info: f 42 : Nat
+-/
+#guard_msgs in
+#check f (foo := 42)
+
+-- Cross-file: positional arg produces no warning
+/--
+info: f 42 : Nat
+-/
+#guard_msgs in
+#check f 42
+
+-- Cross-file: multiple renames
+/--
+warning: parameter `old1` of `g` has been deprecated, use `new1` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲1
+---
+warning: parameter `old2` of `g` has been deprecated, use `new2` instead
+
+Hint: Rename this argument:
+  o̵l̵d̵n̲e̲w̲2
+---
+info: g 1 2 : Nat
+-/
+#guard_msgs in
+#check g (old1 := 1) (old2 := 2)
+
+-- Cross-file: disabling the linter rejects old names with a clean error
+/--
+error: Invalid argument name `arg` for function `f`
+
+Hint: Perhaps you meant one of the following parameter names:
+  • `foo`: a̵r̵g̵f̲o̲o̲
+-/
+#guard_msgs in
+set_option linter.deprecated.arg false in
+#check f (arg := 42)

tests/pkg/deprecated_arg/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open Lake DSL
+
+package deprecated_arg
+@[default_target] lean_lib DeprecatedArg

tests/pkg/deprecated_arg/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/deprecated_arg/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

tests/pkg/ver_clash/clean.sh

@@ -1 +1,6 @@
 rm -rf work
+
+# previous clean.sh, without it we would be copying old .git dirs and get a test failure
+rm -rf DiamondExample-*/.git
+rm -rf DiamondExample-*/.lake DiamondExample-*/lake-manifest.json
+rm -f DiamondExample-D/produced.out