From 6e54c08bccd26221f2452b201eb1724758025adb Mon Sep 17 00:00:00 2001
From: Willem Vanhulle <willemvanhulle@protonmail.com>
Date: Sat, 28 Feb 2026 11:22:29 +0100
Subject: [PATCH 1/3] feat: add Source pretty-printer and named-arg block
 formatter

---
 src/Init/Data/Format/Basic.lean       |  28 ++++--
 src/Lean/Data/Format.lean             |   2 +-
 src/Lean/Parser/Extra.lean            |   4 +-
 src/Lean/Parser/Term.lean             |  31 +++++++
 src/Lean/PrettyPrinter/Formatter.lean |  12 ++-
 src/Lean/PrettyPrinter/Source.lean    | 124 ++++++++++++++++++++++++++
 tests/lean/run/ppMultilineStr.lean    |  67 ++++++++++++++
 tests/lean/run/ppNamedArgFormat.lean  |  52 +++++++++++
 tests/lean/run/ppSource.lean          | 101 +++++++++++++++++++++
 9 files changed, 404 insertions(+), 17 deletions(-)
 create mode 100644 src/Lean/PrettyPrinter/Source.lean
 create mode 100644 tests/lean/run/ppMultilineStr.lean
 create mode 100644 tests/lean/run/ppNamedArgFormat.lean
 create mode 100644 tests/lean/run/ppSource.lean

diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean
index e0dbb5fa8be5..7de56d7c0bb9 100644
--- a/src/Init/Data/Format/Basic.lean
+++ b/src/Init/Data/Format/Basic.lean
@@ -57,10 +57,16 @@ inductive Format where
   | nil                 : Format
   /--
   A position where a newline may be inserted if the current group does not fit within the allotted
-  column width.
+  column width. When the surrounding group is flattened, `line` becomes a space.
   -/
   | line                : Format
   /--
+  An unconditional newline that indents to the current level.
+  Unlike `line`, `hardLine` always produces a newline and prevents the surrounding group
+  from being flattened.
+  -/
+  | hardLine            : Format
+  /--
   `align` tells the formatter to pad with spaces to the current indentation level, or else add a
   newline if we are already at or past the indent.
 
@@ -80,7 +86,8 @@ inductive Format where
   /--
   A node containing a plain string.
 
-  If the string contains newlines, the formatter emits them and then indents to the current level.
+  If the string contains newlines, the formatter emits them at column 0.
+  Use `Format.line` or `Format.nest` to control indentation of line breaks.
   -/
   | text                : String → Format
   /--
@@ -112,6 +119,7 @@ namespace Format
 def isEmpty : Format → Bool
   | nil          => true
   | line         => false
+  | hardLine     => false
   | align _      => true
   | text msg     => msg == ""
   | nest _ f     => f.isEmpty
@@ -162,16 +170,17 @@ private structure SpaceResult where
 private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
   | nil,          _,       _, _ => {}
   | line,         flatten, _, _ => if flatten then { space := 1 } else { foundLine := true }
+  | hardLine,     flatten, _, _ => { foundLine := true, foundFlattenedHardLine := flatten }
   | align force,  flatten, m, w =>
     if flatten && !force then {}
     else if w < m then
       { space := (m - w).toNat }
     else
       { foundLine := true }
-  | text s,       flatten, _, _ =>
+  | text s,       _, _, _ =>
     let p := String.Internal.posOf s '\n'
     let off := String.Internal.offsetOfPos s p
-    { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, space := off }
+    { foundLine := p != s.rawEndPos, space := off }
   | append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m)
   | nest n f,     flatten, m, w => spaceUptoLine f flatten (m - n) w
   | group f _,    _,       m, w => spaceUptoLine f true m w
@@ -271,14 +280,19 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         be w (gs' is)
       else
         pushOutput (String.Internal.extract s {} p)
-        pushNewline i.indent.toNat
+        pushNewline 0
         let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::is
-        -- after a hard line break, re-evaluate whether to flatten the remaining group
-        -- note that we shouldn't start flattening after a hard break outside a group
         if g.fla == .disallow then
           be w (gs' is)
         else
           pushGroup g.flb is gs w >>= be w
+    | hardLine =>
+      pushNewline i.indent.toNat
+      endTags i.activeTags
+      if g.fla == .disallow then
+        be w (gs' is)
+      else
+        pushGroup g.flb is gs w >>= be w
     | line =>
       match g.flb with
       | FlattenBehavior.allOrNone =>
diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean
index 9bcb44e2ce7c..bc8eabf80e17 100644
--- a/src/Lean/Data/Format.lean
+++ b/src/Lean/Data/Format.lean
@@ -47,7 +47,7 @@ open Std
 export Std
   (Format ToFormat Format.nest Format.nil Format.joinSep Format.line
    Format.sbracket Format.bracket Format.group Format.tag Format.pretty
-   Format.fill Format.paren Format.join Format.align)
+   Format.fill Format.paren Format.join Format.align Format.hardLine)
 export ToFormat (format)
 
 instance : ToFormat Name where
diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean
index c97b763f725e..112ad23fa6d2 100644
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -217,7 +217,7 @@ def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : F
     for i in (List.range stx.getArgs.size).reverse do
       if i % 2 == 0 then p else pSep <|>
         -- If the final separator is a newline, skip it.
-        ((if i == stx.getArgs.size - 1 then pure () else pushWhitespace "\n") *> goLeft)
+        ((if i == stx.getArgs.size - 1 then pure () else pushWhitespace Format.hardLine) *> goLeft)
   -- If there is any newline separator, then we add an `align` at the start
   -- so that `withPosition` will pick up the right column.
   if hasNewlineSep then
@@ -286,7 +286,7 @@ open PrettyPrinter Parser
 
 @[combinator_formatter ppHardSpace, expose] def ppHardSpace.formatter : Formatter := Formatter.pushWhitespace " "
 @[combinator_formatter ppSpace, expose] def ppSpace.formatter : Formatter := Formatter.pushLine
-@[combinator_formatter ppLine, expose] def ppLine.formatter : Formatter := Formatter.pushWhitespace "\n"
+@[combinator_formatter ppLine, expose] def ppLine.formatter : Formatter := Formatter.pushWhitespace Format.hardLine
 @[combinator_formatter ppRealFill, expose] def ppRealFill.formatter (p : Formatter) : Formatter := Formatter.fill p
 @[combinator_formatter ppRealGroup, expose] def ppRealGroup.formatter (p : Formatter) : Formatter := Formatter.group p
 @[combinator_formatter ppIndent, expose] def ppIndent.formatter (p : Formatter) : Formatter := Formatter.indent p
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 4d1645205caa..475a7e702425 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -859,6 +859,37 @@ def argument       :=
 -- argument precedence is `arg` (i.e. does not accept `lead` precedence)
 @[builtin_term_parser] def app := trailing_parser:leadPrec:maxPrec many1 argument
 
+open Lean.PrettyPrinter.Formatter in
+/--
+Custom formatter for function application that uses allOrNone grouping
+when named arguments are present. This formats named arguments in a
+record-like style (all on one line, or each on its own line) rather
+than greedy line-filling.
+-/
+@[builtin_formatter Lean.Parser.Term.app]
+def appFormatter : PrettyPrinter.Formatter := do
+  checkKind ``app
+  let stx ← Syntax.MonadTraverser.getCur
+  let argsNode := stx.getArg 1
+  let hasNamedArg := argsNode.getArgs.any fun arg =>
+    arg.getKind == ``namedArgument
+  let fmtArgs : PrettyPrinter.Formatter := do
+    let stx ← Syntax.MonadTraverser.getCur
+    visitArgs <| stx.getArgs.size.forM fun _ _ => do
+      let cur ← Syntax.MonadTraverser.getCur
+      let k := cur.getKind
+      if k == ``namedArgument || k == ``ellipsis then
+        formatterForKind k
+      else
+        categoryParser.formatter `term
+      checkWsBefore.formatter
+  visitArgs do
+    if hasNamedArg then
+      Lean.PrettyPrinter.Formatter.group fmtArgs
+    else
+      fmtArgs
+    categoryParser.formatter `term
+
 /--
 The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
 More precisely,
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 2067634ee568..8c9afc2474a7 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -371,12 +371,12 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit
       let preNL := Substring.Raw.contains { ss with stopPos := ss'.startPos } '\n'
       let postNL := Substring.Raw.contains { ss with startPos := ss'.stopPos } '\n'
       if postNL then
-        pushWhitespace "\n"
+        pushWhitespace Format.hardLine
       else if !(← get).leadWord.isEmpty then
         pushLine
       push ss'.toString
       if preNL then
-        pushWhitespace "\n"
+        pushWhitespace Format.hardLine
       else
         pushLine
 
@@ -409,11 +409,9 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit
     -- already separated => use `tk` as is
     if st.leadWord == "" then
       push tk.trimAsciiEnd.copy
-    else if tk.endsWith " " then
+    else
       pushLine
       push tk.trimAsciiEnd.copy
-    else
-      push tk -- preserve special whitespace for tokens like ":=\n"
     modify fun st => { st with leadWord := if tk.trimAsciiStart == tk.toSlice then tk else "", leadWordIdent := ident }
 
   if let SourceInfo.original ss _ _ _ := info then
@@ -426,12 +424,12 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit
       -- with the actual token, so dedent
       indent (indent := some (-Std.Format.getIndent (← getOptions))) do
         if postNL then
-          pushWhitespace "\n"
+          pushWhitespace Format.hardLine
         else
           pushLine
         pushWhitespace ss'.toString
         if preNL then
-          pushWhitespace "\n"
+          pushWhitespace Format.hardLine
         else
           -- It is conceivable that the start of comment syntax could be misinterpreted as part of a token,
           -- so add the beginning of it as the leadWord.
diff --git a/src/Lean/PrettyPrinter/Source.lean b/src/Lean/PrettyPrinter/Source.lean
new file mode 100644
index 000000000000..6d1413728d75
--- /dev/null
+++ b/src/Lean/PrettyPrinter/Source.lean
@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Willem Vanhulle
+-/
+module
+
+prelude
+public import Lean.PrettyPrinter
+import Lean.Elab.Import
+import Lean.Elab.Command
+
+namespace Lean.PrettyPrinter
+
+private def isCommentOrBlankLine (line : String) : Bool :=
+  let trimmed := line.trimAsciiStart
+  trimmed.isEmpty || trimmed.startsWith "--"
+
+/-- Strip trailing lines that are pure comments or blank from ppCommand output.
+The formatter's `pushToken` preserves trailing `SourceInfo` comments at incorrect
+indentation (nested under the last expression). The gap extraction re-includes them
+at their correct original indentation.
+Scans backward from the end so only trailing lines are inspected. -/
+public def trimTrailingCommentLines (s : String) : String :=
+  let lines := s.split '\n' |>.toStringList
+  let kept := lines.reverse.dropWhile isCommentOrBlankLine |>.reverse
+  "\n".intercalate kept
+
+/-- Collapse runs of 3+ consecutive newlines down to 2 (at most one blank line).
+Folds over characters, tracking consecutive newline count. -/
+public def collapseBlankLines (s : String) : String :=
+  let (acc, _) := s.foldl (fun (acc, nlCount) c =>
+    if c == '\n' then
+      if nlCount < 2 then (acc.push '\n', nlCount + 1)
+      else (acc, nlCount)
+    else
+      (acc.push c, 0)) ("", 0)
+  acc
+
+/-- Parse all top-level commands from an input context. -/
+private partial def parseCommands (inputCtx : Parser.InputContext) (pmctx : Parser.ParserModuleContext)
+    (parserState : Parser.ModuleParserState) : Array Syntax :=
+  go parserState {} #[]
+where
+  go (mps : Parser.ModuleParserState) (msgs : MessageLog) (acc : Array Syntax) : Array Syntax :=
+    let (stx, mps', msgs') := Parser.parseCommand inputCtx pmctx mps msgs
+    if Parser.isTerminalCommand stx then acc
+    else go mps' msgs' (acc.push stx)
+
+/-- Clean an inter-command gap: collapse excessive blank lines and strip trailing
+non-newline whitespace (original indentation before the next command, which `ppCommand`
+will re-emit at column 0). -/
+public def cleanGap (s : String) : String :=
+  let s := collapseBlankLines s
+  -- Strip trailing spaces/tabs (original indentation) since ppCommand starts at column 0
+  match s.revFind? '\n' with
+  | some pos => String.Pos.Raw.extract s {} (String.Pos.Raw.next s pos.offset)
+  | none     => if s.any (!·.isWhitespace) then s else ""
+
+/-- Extract the inter-command gap from original source and clean it. -/
+private def interCommandGap (contents : String) (prevTailPos : Option String.Pos.Raw)
+    (curStartPos : Option String.Pos.Raw) : String :=
+  match prevTailPos, curStartPos with
+  | some prevEnd, some curStart => cleanGap (String.Pos.Raw.extract contents prevEnd curStart)
+  | none, some curStart       => cleanGap (String.Pos.Raw.extract contents {} curStart)
+  | _, none                     => "\n"
+
+/-- Extract the header text from original source, trimming trailing whitespace. -/
+public def extractHeader (contents : String) (headerStx : Syntax) : String :=
+  let raw := match headerStx.getPos?, headerStx.getTailPos? with
+    | some s, some e => String.Pos.Raw.extract contents s e
+    | _, _           => headerStx.reprint.getD ""
+  raw.trimAsciiEnd.copy
+
+/-- Format the result of `ppCommand`, trimming trailing whitespace and comment lines. -/
+public def cleanCommandOutput (fmtResult : Except Exception Format) (stx : Syntax) : String :=
+  match fmtResult with
+  | .ok fmt  => trimTrailingCommentLines fmt.pretty.trimAsciiEnd.copy
+  | .error _ => trimTrailingCommentLines (stx.reprint.getD "").trimAsciiEnd.copy
+
+/-- Emit a command's original source verbatim, trimming trailing whitespace. -/
+public def verbatimCommand (contents : String) (stx : Syntax) : String :=
+  let raw := match stx.getPos?, stx.getTailPos? with
+    | some s, some e => String.Pos.Raw.extract contents s e
+    | _, _           => stx.reprint.getD ""
+  raw.trimAsciiEnd.copy
+
+/-- Format a sequence of commands. Emits the header verbatim, cleans inter-command gaps,
+and calls `formatCmd` for each command. This is the shared core used by both `ppSource`
+and the LSP formatter. -/
+public def formatCommands [Monad m] (source : String) (headerStx : Syntax)
+    (cmdStxs : Array Syntax) (formatCmd : Syntax → m String) : m String := do
+  let mut result := extractHeader source headerStx
+  let mut prevTailPos := headerStx.getTailPos?
+  for stx in cmdStxs do
+    result := result ++ interCommandGap source prevTailPos stx.getPos?
+    result := result ++ (← formatCmd stx)
+    prevTailPos := stx.getTailPos?
+  if !result.isEmpty && !result.endsWith "\n" then
+    result := result ++ "\n"
+  return result
+
+/-- Pretty-print a Lean source file. Parses the header and commands,
+then pretty-prints each command via `ppCommand`. Only requires parsing,
+not elaboration. Returns the formatted source text. -/
+public def ppSource (contents : String) (fileName : String) (opts : Options := {}) : IO String := do
+  let inputCtx := Parser.mkInputContext contents fileName
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, _) ← Elab.processHeader header opts messages inputCtx (trustLevel := 1024)
+  let pmctx : Parser.ParserModuleContext := { env, options := opts }
+  let cmdStxs := parseCommands inputCtx pmctx parserState
+  let cmdState := Elab.Command.mkState env {} opts
+  let fileMap := FileMap.ofString contents
+  formatCommands contents header.raw cmdStxs fun stx => do
+    let cmdCtx : Elab.Command.Context := {
+      cmdPos := stx.getPos?.getD 0
+      fileName, fileMap
+      snap? := none, cancelTk? := none
+    }
+    let fmtResult ← (Elab.Command.liftCoreM (ppCommand ⟨stx⟩) |>.run cmdCtx |>.run' cmdState).toBaseIO
+    return cleanCommandOutput fmtResult stx
+
+end Lean.PrettyPrinter
diff --git a/tests/lean/run/ppMultilineStr.lean b/tests/lean/run/ppMultilineStr.lean
new file mode 100644
index 000000000000..a9ca4486dd09
--- /dev/null
+++ b/tests/lean/run/ppMultilineStr.lean
@@ -0,0 +1,67 @@
+import Lean
+
+/-! # Multiline string formatting tests
+
+Verify that the formatter preserves newlines inside string literals without
+re-indenting continuation lines. -/
+
+elab "#pp " cmd:command : command => Lean.logInfo cmd
+
+-- Multiline string in a definition
+/--
+info: def greeting :=
+  "Hello
+world"
+-/
+#guard_msgs in
+#pp
+def greeting := "Hello
+world"
+
+-- Interpolated multiline string
+/--
+info: def greeting (name : String) :=
+  s! "Hello
+{name}"
+-/
+#guard_msgs in
+#pp
+def greeting (name : String) := s!"Hello
+{name}"
+
+-- String with multiple newlines
+/--
+info: def lines :=
+  "a
+b
+c"
+-/
+#guard_msgs in
+#pp
+def lines := "a
+b
+c"
+
+-- Multiline string inside a let binding
+/--
+info: def foo :=
+  let s := "Hello
+world"
+  s
+-/
+#guard_msgs in
+#pp
+def foo :=
+  let s := "Hello
+world"
+  s
+
+-- Multiline string in #eval
+/--
+info: #eval "Hello
+world"
+-/
+#guard_msgs in
+#pp
+#eval "Hello
+world"
diff --git a/tests/lean/run/ppNamedArgFormat.lean b/tests/lean/run/ppNamedArgFormat.lean
new file mode 100644
index 000000000000..f6035e10bd7b
--- /dev/null
+++ b/tests/lean/run/ppNamedArgFormat.lean
@@ -0,0 +1,52 @@
+/-!
+# Pretty printer: allOrNone grouping for named arguments in function applications
+
+When a function application contains named arguments, the formatter uses
+allOrNone grouping (either all args on one line, or each on its own line)
+rather than greedy line-filling. This gives a record-like appearance.
+
+Applications with only positional arguments retain the default fill behavior.
+-/
+
+-- Short positional application stays on one line
+/--
+info: Nat.add 1 2 : Nat
+-/
+#guard_msgs in
+#check Nat.add 1 2
+
+-- Positional application that fits stays flat
+set_option pp.fieldNotation false in
+/--
+info: Nat.add (Nat.add 1 2) 3 : Nat
+-/
+#guard_msgs in
+#check Nat.add (Nat.add 1 2) 3
+
+-- Short named-arg application stays on one line
+set_option pp.motives.all true in
+set_option pp.fieldNotation false in
+/--
+info: fun n => Nat.rec (motive := fun x => Nat) 0 (fun k ih => ih + k) n : Nat → Nat
+-/
+#guard_msgs in
+#check fun (n : Nat) => Nat.rec (motive := fun _ => Nat) 0 (fun k ih => ih + k) n
+
+-- Long named-arg application: allOrNone grouping means all args get their own line
+-- since the total doesn't fit in 120 columns
+set_option pp.motives.all true in
+set_option pp.fieldNotation false in
+/--
+info: fun n =>
+  Nat.rec
+    (motive :=
+    fun x =>
+    Nat × Nat × Nat × Nat × Nat)
+    (0, 0, 0, 0, 0)
+    (fun k ih =>
+      (Prod.fst ih + k, Prod.fst (Prod.snd ih), Prod.fst (Prod.snd (Prod.snd ih)),
+        Prod.fst (Prod.snd (Prod.snd (Prod.snd ih))), Prod.snd (Prod.snd (Prod.snd (Prod.snd ih))) + 1))
+    n : Nat → Nat × Nat × Nat × Nat × Nat
+-/
+#guard_msgs in
+#check fun (n : Nat) => Nat.rec (motive := fun _ => Nat × Nat × Nat × Nat × Nat) (0, 0, 0, 0, 0) (fun k ih => (ih.1 + k, ih.2.1, ih.2.2.1, ih.2.2.2.1, ih.2.2.2.2 + 1)) n
diff --git a/tests/lean/run/ppSource.lean b/tests/lean/run/ppSource.lean
new file mode 100644
index 000000000000..6bbc853d197a
--- /dev/null
+++ b/tests/lean/run/ppSource.lean
@@ -0,0 +1,101 @@
+import Lean.PrettyPrinter.Source
+
+open Lean PrettyPrinter in
+/--
+info: def foo :=
+  1
+-/
+#guard_msgs in
+#eval do
+  let input := "def foo:=1\n"
+  let result ← ppSource input "<test>"
+  IO.println result
+
+open Lean PrettyPrinter in
+/--
+info: def foo :=
+  1
+def bar :=
+  2
+-/
+#guard_msgs in
+#eval do
+  let input := "def foo:=1\ndef bar:=2\n"
+  let result ← ppSource input "<test>"
+  IO.println result
+
+-- Test that comments between commands are preserved
+open Lean PrettyPrinter in
+/--
+info: def foo :=
+  1
+
+-- a comment
+def bar :=
+  2
+-/
+#guard_msgs in
+#eval do
+  let input := "def foo := 1\n\n-- a comment\ndef bar := 2\n"
+  let result ← ppSource input "<test>"
+  IO.println result
+
+-- Test that already-formatted input round-trips
+open Lean PrettyPrinter in
+/-- info: true -/
+#guard_msgs in
+#eval do
+  let input := "def foo :=\n  1\n"
+  let result ← ppSource input "<test>"
+  IO.println (result == input)
+
+-- Test blank line collapsing (3+ newlines → 2)
+open Lean PrettyPrinter in
+/--
+info: def foo :=
+  1
+
+def bar :=
+  2
+-/
+#guard_msgs in
+#eval do
+  let input := "def foo := 1\n\n\n\ndef bar := 2\n"
+  let result ← ppSource input "<test>"
+  IO.println result
+
+-- Test that leading whitespace before a top-level command is stripped
+open Lean PrettyPrinter in
+/--
+info: #eval "Hello
+world"
+-/
+#guard_msgs in
+#eval do
+  let input := "   #eval \"Hello\nworld\"\n"
+  let result ← ppSource input "<test>"
+  IO.println result
+
+-- Test that formatting multiline strings is idempotent
+open Lean PrettyPrinter in
+/-- info: true -/
+#guard_msgs in
+#eval do
+  let input := "def greeting := \"Hello\nworld\"\n"
+  let result ← ppSource input "<test>"
+  let result2 ← ppSource result "<test>"
+  IO.println (result == result2)
+
+-- Test leading whitespace stripped across multiple commands
+open Lean PrettyPrinter in
+/--
+info: def foo :=
+  1
+
+#eval "hey"
+-/
+#guard_msgs in
+#eval do
+  let input := "  def foo := 1\n\n  #eval \"hey\"\n"
+  let result ← ppSource input "<test>"
+  IO.println result

From cb38d2cb1a3fe2b3214fc5da33a933f91abaa81b Mon Sep 17 00:00:00 2001
From: Willem Vanhulle <willemvanhulle@protonmail.com>
Date: Sat, 28 Feb 2026 11:22:29 +0100
Subject: [PATCH 2/3] feat: add LSP textDocument/formatting and rangeFormatting

---
 src/Lean/Data/Lsp/Capabilities.lean           |  2 +
 src/Lean/Data/Lsp/LanguageFeatures.lean       | 16 ++++++
 src/Lean/Server/FileSource.lean               |  6 ++
 src/Lean/Server/FileWorker/Formatting.lean    | 57 +++++++++++++++++++
 .../Server/FileWorker/RequestHandling.lean    | 42 ++++++++++++++
 src/Lean/Server/Test/Runner.lean              | 22 +++++++
 src/Lean/Server/Watchdog.lean                 |  2 +
 .../formatting_commands.lean                  |  9 +++
 .../formatting_commands.lean.out.expected     |  6 ++
 .../formatting_comments.lean                  | 11 ++++
 .../formatting_comments.lean.out.expected     |  6 ++
 tests/server_interactive/formatting_do.lean   | 10 ++++
 .../formatting_do.lean.out.expected           |  6 ++
 .../server_interactive/formatting_match.lean  | 13 +++++
 .../formatting_match.lean.out.expected        |  6 ++
 .../server_interactive/formatting_range.lean  |  6 ++
 .../formatting_range.lean.out.expected        |  8 +++
 .../formatting_tactics.lean                   |  8 +++
 .../formatting_tactics.lean.out.expected      |  6 ++
 19 files changed, 242 insertions(+)
 create mode 100644 src/Lean/Server/FileWorker/Formatting.lean
 create mode 100644 tests/server_interactive/formatting_commands.lean
 create mode 100644 tests/server_interactive/formatting_commands.lean.out.expected
 create mode 100644 tests/server_interactive/formatting_comments.lean
 create mode 100644 tests/server_interactive/formatting_comments.lean.out.expected
 create mode 100644 tests/server_interactive/formatting_do.lean
 create mode 100644 tests/server_interactive/formatting_do.lean.out.expected
 create mode 100644 tests/server_interactive/formatting_match.lean
 create mode 100644 tests/server_interactive/formatting_match.lean.out.expected
 create mode 100644 tests/server_interactive/formatting_range.lean
 create mode 100644 tests/server_interactive/formatting_range.lean.out.expected
 create mode 100644 tests/server_interactive/formatting_tactics.lean
 create mode 100644 tests/server_interactive/formatting_tactics.lean.out.expected

diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index 12eec11b4270..fe5d00007f0d 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -136,6 +136,8 @@ structure ServerCapabilities where
   inlayHintProvider?        : Option InlayHintOptions        := none
   signatureHelpProvider?    : Option SignatureHelpOptions    := none
   colorProvider?            : Option DocumentColorOptions    := none
+  documentFormattingProvider : Bool                          := false
+  documentRangeFormattingProvider : Bool                     := false
   experimental?             : Option LeanServerCapabilities  := none
   deriving ToJson, FromJson
 
diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
index 548df6b0e35f..9241fc573a4b 100644
--- a/src/Lean/Data/Lsp/LanguageFeatures.lean
+++ b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -725,5 +725,21 @@ structure ColorInformation where
 structure DocumentColorOptions extends WorkDoneProgressOptions where
   deriving FromJson, ToJson
 
+structure FormattingOptions where
+  tabSize : Nat
+  insertSpaces : Bool
+  deriving FromJson, ToJson
+
+structure DocumentFormattingParams where
+  textDocument : TextDocumentIdentifier
+  options : FormattingOptions
+  deriving FromJson, ToJson
+
+structure DocumentRangeFormattingParams where
+  textDocument : TextDocumentIdentifier
+  range : Range
+  options : FormattingOptions
+  deriving FromJson, ToJson
+
 end Lsp
 end Lean
diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean
index 290830e74d17..7d0a2999815b 100644
--- a/src/Lean/Server/FileSource.lean
+++ b/src/Lean/Server/FileSource.lean
@@ -113,6 +113,12 @@ instance : FileSource SignatureHelpParams where
 instance : FileSource DocumentColorParams where
   fileSource p := fileSource p.textDocument
 
+instance : FileSource DocumentFormattingParams where
+  fileSource? p := fileSource? p.textDocument
+
+instance : FileSource DocumentRangeFormattingParams where
+  fileSource p := fileSource p.textDocument
+
 /--
 Yields the file source of `item` by attempting to obtain `mod : Name` from `item.data?`. \
 Panics if `item.data?` is not present or does not contain a `mod` field and the first element of a
diff --git a/src/Lean/Server/FileWorker/Formatting.lean b/src/Lean/Server/FileWorker/Formatting.lean
new file mode 100644
index 000000000000..66b98e96a33c
--- /dev/null
+++ b/src/Lean/Server/FileWorker/Formatting.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Willem Vanhulle
+-/
+module
+
+prelude
+public import Lean.Server.Requests
+import Lean.PrettyPrinter
+import Lean.PrettyPrinter.Source
+
+public section
+
+namespace Lean.Server.FileWorker.Formatting
+open Lsp
+open Snapshots
+
+/-- Format commands in `[rangeStart, rangeEnd)` byte range. Commands outside the range
+are emitted verbatim from the original source. Returns a full-document `TextEdit`. -/
+def formatCommandRange
+    (doc : EditableDocument) (text : FileMap)
+    (initSnap : Language.Lean.InitialSnapshot)
+    (headerParsed : Language.Lean.HeaderParsedState)
+    (headerSuccess : Language.Lean.HeaderProcessedState)
+    (rangeStart rangeEnd : String.Pos.Raw)
+    : EIO RequestError (Array TextEdit) := do
+  -- Collect all parsed command syntax by walking the CommandParsedSnapshot chain.
+  let mut cmdStxs : Array Syntax := #[]
+  let mut next? := some headerSuccess.firstCmdSnap
+  repeat do
+    match next? with
+    | none => break
+    | some snapshotTask =>
+      let cmdParsed := snapshotTask.get
+      cmdStxs := cmdStxs.push cmdParsed.stx
+      next? := cmdParsed.nextCmdSnap?
+  let headerSnap : Snapshots.Snapshot := {
+    stx := initSnap.stx
+    mpState := headerParsed.parserState
+    cmdState := headerSuccess.cmdState
+  }
+  let result ← PrettyPrinter.formatCommands text.source initSnap.stx cmdStxs fun stx => do
+    let cmdStart := stx.getPos?.getD 0
+    let cmdEnd := stx.getTailPos?.getD 0
+    let overlaps := cmdStart < rangeEnd && cmdEnd > rangeStart
+    if overlaps then
+      let fmtResult ← (headerSnap.runCoreM doc.meta (PrettyPrinter.ppCommand ⟨stx⟩)).toBaseIO
+      return PrettyPrinter.cleanCommandOutput fmtResult stx
+    else
+      return PrettyPrinter.verbatimCommand text.source stx
+  let endPos := text.utf8PosToLspPos text.source.rawEndPos
+  let fullRange : Range := ⟨⟨0, 0⟩, endPos⟩
+  return #[{ range := fullRange, newText := result }]
+
+end Lean.Server.FileWorker.Formatting
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index a51b43e1894f..e49cda006651 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -8,6 +8,7 @@ module
 
 prelude
 public import Lean.Server.FileWorker.ExampleHover
+public import Lean.Server.FileWorker.Formatting
 public import Lean.Server.FileWorker.InlayHints
 public import Lean.Server.FileWorker.SemanticHighlighting
 public import Lean.Server.FileWorker.SignatureHelp
@@ -481,6 +482,37 @@ partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams)
     return doc.reporter.bindCheap (fun _ => doc.cmdSnaps.waitAll)
       |>.mapCheap fun _ => pure WaitForDiagnostics.mk
 
+def handleDocumentFormatting (_ : DocumentFormattingParams)
+    : RequestM (RequestTask (Array TextEdit)) := do
+  let doc ← readDoc
+  let text := doc.meta.text
+  let initSnap := doc.initSnap
+  let some headerParsed := initSnap.result?
+    | return ServerTask.pure (.error (RequestError.internalError "header parsing failed"))
+  let headerProcessedTask := headerParsed.processedSnap.task.asServerTask
+  mapTaskCostly headerProcessedTask fun headerProcessed => do
+    let some headerSuccess := headerProcessed.result?
+      | throw ⟨.internalError, "import processing failed"⟩
+    Formatting.formatCommandRange doc text initSnap headerParsed headerSuccess
+      0 text.source.rawEndPos
+
+/-- Handle `textDocument/rangeFormatting`: format only commands overlapping the given range. -/
+def handleDocumentRangeFormatting (p : DocumentRangeFormattingParams)
+    : RequestM (RequestTask (Array TextEdit)) := do
+  let doc ← readDoc
+  let text := doc.meta.text
+  let initSnap := doc.initSnap
+  let some headerParsed := initSnap.result?
+    | return ServerTask.pure (.error (RequestError.internalError "header parsing failed"))
+  let headerProcessedTask := headerParsed.processedSnap.task.asServerTask
+  mapTaskCostly headerProcessedTask fun headerProcessed => do
+    let some headerSuccess := headerProcessed.result?
+      | throw ⟨.internalError, "import processing failed"⟩
+    let rangeStart := text.lspPosToUtf8Pos p.range.start
+    let rangeEnd := text.lspPosToUtf8Pos p.range.«end»
+    Formatting.formatCommandRange doc text initSnap headerParsed headerSuccess
+      rangeStart rangeEnd
+
 def handleDocumentColor (_ : DocumentColorParams) :
     RequestM (RequestTask (Array ColorInformation)) :=
   -- By default, if no document color provider is registered, VS Code itself provides
@@ -548,6 +580,16 @@ builtin_initialize
     SignatureHelpParams
     (Option SignatureHelp)
     handleSignatureHelp
+  registerLspRequestHandler
+    "textDocument/formatting"
+    DocumentFormattingParams
+    (Array TextEdit)
+    handleDocumentFormatting
+  registerLspRequestHandler
+    "textDocument/rangeFormatting"
+    DocumentRangeFormattingParams
+    (Array TextEdit)
+    handleDocumentRangeFormatting
   registerLspRequestHandler
     "textDocument/documentColor"
     DocumentColorParams
diff --git a/src/Lean/Server/Test/Runner.lean b/src/Lean/Server/Test/Runner.lean
index 51323ba1cb59..4af16889e33a 100644
--- a/src/Lean/Server/Test/Runner.lean
+++ b/src/Lean/Server/Test/Runner.lean
@@ -632,6 +632,26 @@ def processInlayHints : RunnerM Unit := do
   }
   logResponse "textDocument/inlayHint" p
 
+def processFormatting : RunnerM Unit := do
+  let p : DocumentFormattingParams := {
+    textDocument := { uri := (← get).uri }
+    options := { tabSize := 2, insertSpaces := true }
+  }
+  logResponse "textDocument/formatting" p (Array TextEdit)
+
+def processRangeFormatting : RunnerM Unit := do
+  let s ← get
+  let some rangeJson := Json.parse s.params |>.toOption
+    | throw <| IO.userError s!"rangeFormatting: failed to parse range params: {s.params}"
+  let some range := (fromJson? rangeJson : Except String Range) |>.toOption
+    | throw <| IO.userError s!"rangeFormatting: failed to decode Range from: {s.params}"
+  let p : DocumentRangeFormattingParams := {
+    textDocument := { uri := s.uri }
+    range
+    options := { tabSize := 2, insertSpaces := true }
+  }
+  logResponse "textDocument/rangeFormatting" p (Array TextEdit)
+
 def processGenericRequest : RunnerM Unit := do
   let s ← get
   let Except.ok params := Json.parse s.params
@@ -676,6 +696,8 @@ def processDirective (_ws directive : String) (directiveTargetLineNo : Nat)
   | "moduleHierarchyImports" => processModuleHierarchyImports
   | "moduleHierarchyImportedBy" => processModuleHierarchyImportedBy
   | "inlayHints" => processInlayHints
+  | "formatting" => processFormatting
+  | "rangeFormatting" => processRangeFormatting
   | _ => processGenericRequest
 
 def processLine (line : String) : RunnerM Unit := do
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 68ed22f9178c..0f65a35421be 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -1598,6 +1598,8 @@ def mkLeanServerCapabilities : ServerCapabilities := {
     triggerCharacters? := some #[" "]
   }
   colorProvider? := some {}
+  documentFormattingProvider := true
+  documentRangeFormattingProvider := true
   experimental? := some {
     moduleHierarchyProvider? := some {}
     rpcProvider? := some {
diff --git a/tests/server_interactive/formatting_commands.lean b/tests/server_interactive/formatting_commands.lean
new file mode 100644
index 000000000000..a5dfb960ccdc
--- /dev/null
+++ b/tests/server_interactive/formatting_commands.lean
@@ -0,0 +1,9 @@
+structure   Point where
+  x :    Nat
+  y :    Nat
+
+instance :   ToString Point where
+  toString p :=   s!"({p.x}, {p.y})"
+
+def   origin : Point :=  { x := 0,   y := 0 }
+--^ formatting
diff --git a/tests/server_interactive/formatting_commands.lean.out.expected b/tests/server_interactive/formatting_commands.lean.out.expected
new file mode 100644
index 000000000000..c2a602db11a4
--- /dev/null
+++ b/tests/server_interactive/formatting_commands.lean.out.expected
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file:///formatting_commands.lean"},
+ "options": {"tabSize": 2, "insertSpaces": true}}
+[{"range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 9, "character": 0}},
+  "newText":
+  "structure Point where\n  x : Nat\n  y : Nat\n\ninstance : ToString Point where toString p := s! \"({p.x }, {p.y})\"\n\ndef origin : Point :=\n  { x := 0, y := 0 }\n--^ formatting\n"}]
diff --git a/tests/server_interactive/formatting_comments.lean b/tests/server_interactive/formatting_comments.lean
new file mode 100644
index 000000000000..d20c31cd045b
--- /dev/null
+++ b/tests/server_interactive/formatting_comments.lean
@@ -0,0 +1,11 @@
+def   double (n :   Nat) : Nat :=    n * 2
+
+-- Tripling is useful for tests
+
+def triple   (n : Nat) :   Nat := n *   3
+
+/-! ## Combining functions -/
+
+def   six : Nat :=
+  triple   (double 1)
+--^ formatting
diff --git a/tests/server_interactive/formatting_comments.lean.out.expected b/tests/server_interactive/formatting_comments.lean.out.expected
new file mode 100644
index 000000000000..23c71b1b927d
--- /dev/null
+++ b/tests/server_interactive/formatting_comments.lean.out.expected
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file:///formatting_comments.lean"},
+ "options": {"tabSize": 2, "insertSpaces": true}}
+[{"range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 11, "character": 0}},
+  "newText":
+  "def double (n : Nat) : Nat :=\n  n *\n    2\n\n-- Tripling is useful for tests\n\ndef triple (n : Nat) : Nat :=\n  n * 3\n\n/-!## Combining functions -/\n\ndef six : Nat :=\n  triple\n    (double 1)\n--^ formatting\n"}]
diff --git a/tests/server_interactive/formatting_do.lean b/tests/server_interactive/formatting_do.lean
new file mode 100644
index 000000000000..3b402c04b160
--- /dev/null
+++ b/tests/server_interactive/formatting_do.lean
@@ -0,0 +1,10 @@
+def greet   (name : String) : IO   Unit := do
+  let   msg :=  s!"Hello, {name}!"
+  IO.println    msg
+
+def count :   IO Unit := do
+  let mut   s := 0
+  for i in   [0, 1, 2, 3] do
+    s :=   s + i
+  IO.println   s!"{s}"
+--^ formatting
diff --git a/tests/server_interactive/formatting_do.lean.out.expected b/tests/server_interactive/formatting_do.lean.out.expected
new file mode 100644
index 000000000000..6828a6bb66f5
--- /dev/null
+++ b/tests/server_interactive/formatting_do.lean.out.expected
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file:///formatting_do.lean"},
+ "options": {"tabSize": 2, "insertSpaces": true}}
+[{"range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 10, "character": 0}},
+  "newText":
+  "def greet (name : String) : IO Unit := do\n  let msg := s! \"Hello, {name}!\"\n  IO.println msg\n\ndef count : IO Unit := do\n  let mut s := 0\n  for i in [0, 1, 2, 3]do\n    s := s + i\n  IO.println s! \"{s}\"\n--^ formatting\n"}]
diff --git a/tests/server_interactive/formatting_match.lean b/tests/server_interactive/formatting_match.lean
new file mode 100644
index 000000000000..c98e6e888ab1
--- /dev/null
+++ b/tests/server_interactive/formatting_match.lean
@@ -0,0 +1,13 @@
+inductive   Tree where
+  |   leaf : Nat →   Tree
+  | node :   Tree → Tree →   Tree
+
+def Tree.depth :   Tree → Nat
+  |   .leaf _ => 0
+  | .node   l r =>
+    let dl :=   l.depth
+    let dr :=   r.depth
+    match   Nat.ble dl dr with
+    |   true => dr + 1
+    |   false => dl + 1
+--^ formatting
diff --git a/tests/server_interactive/formatting_match.lean.out.expected b/tests/server_interactive/formatting_match.lean.out.expected
new file mode 100644
index 000000000000..be7758934a0a
--- /dev/null
+++ b/tests/server_interactive/formatting_match.lean.out.expected
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file:///formatting_match.lean"},
+ "options": {"tabSize": 2, "insertSpaces": true}}
+[{"range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 13, "character": 0}},
+  "newText":
+  "inductive Tree where\n  | leaf : Nat → Tree\n  | node : Tree → Tree → Tree\n\ndef Tree.depth : Tree → Nat\n  | .leaf _ => 0\n  | .node l r =>\n    let dl := l.depth\n    let dr := r.depth\n    match Nat.ble dl dr with\n    | true => dr + 1\n    | false =>\n      dl +\n        1\n--^ formatting\n"}]
diff --git a/tests/server_interactive/formatting_range.lean b/tests/server_interactive/formatting_range.lean
new file mode 100644
index 000000000000..4a9872078d2a
--- /dev/null
+++ b/tests/server_interactive/formatting_range.lean
@@ -0,0 +1,6 @@
+def   foo : Nat :=    42
+
+def   bar (n :   Nat) : Nat :=   n + 1
+
+def   baz : Nat :=    0
+--^ rangeFormatting: {"start":{"line":2,"character":0},"end":{"line":3,"character":0}}
diff --git a/tests/server_interactive/formatting_range.lean.out.expected b/tests/server_interactive/formatting_range.lean.out.expected
new file mode 100644
index 000000000000..b3c7726e01e5
--- /dev/null
+++ b/tests/server_interactive/formatting_range.lean.out.expected
@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file:///formatting_range.lean"},
+ "range":
+ {"start": {"line": 2, "character": 0}, "end": {"line": 3, "character": 0}},
+ "options": {"tabSize": 2, "insertSpaces": true}}
+[{"range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 6, "character": 0}},
+  "newText":
+  "def   foo : Nat :=    42\n\ndef bar (n : Nat) : Nat :=\n  n + 1\n\ndef   baz : Nat :=    0\n--^ rangeFormatting: {\"start\":{\"line\":2,\"character\":0},\"end\":{\"line\":3,\"character\":0}}\n"}]
diff --git a/tests/server_interactive/formatting_tactics.lean b/tests/server_interactive/formatting_tactics.lean
new file mode 100644
index 000000000000..32333a7a760e
--- /dev/null
+++ b/tests/server_interactive/formatting_tactics.lean
@@ -0,0 +1,8 @@
+theorem and_comm (p q :    Prop) (hp : p)   (hq : q) : q ∧ p := by
+  constructor
+  · exact    hq
+  ·   exact hp
+
+example (n :    Nat) : n + 0   = n := by
+  simp
+--^ formatting
diff --git a/tests/server_interactive/formatting_tactics.lean.out.expected b/tests/server_interactive/formatting_tactics.lean.out.expected
new file mode 100644
index 000000000000..bb1abf1cc598
--- /dev/null
+++ b/tests/server_interactive/formatting_tactics.lean.out.expected
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file:///formatting_tactics.lean"},
+ "options": {"tabSize": 2, "insertSpaces": true}}
+[{"range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 8, "character": 0}},
+  "newText":
+  "theorem and_comm (p q : Prop) (hp : p) (hq : q) : q ∧ p :=\n  by\n  constructor\n  · exact hq\n  · exact hp\n\nexample (n : Nat) : n + 0 = n := by\n  simp\n--^ formatting\n"}]

From 77dd733e32a68264639a4f08da125b20d5468bb0 Mon Sep 17 00:00:00 2001
From: Willem Vanhulle <willemvanhulle@protonmail.com>
Date: Sat, 28 Feb 2026 11:22:29 +0100
Subject: [PATCH 3/3] feat: add lake format CLI command

Adds a 'lake format' subcommand that formats Lean source files in
place using the Source pretty-printer. Wires shell helpers needed
for invoking lake from the worker process.
---
 src/Lean/Shell.lean         | 20 ++++++++++++++++++++
 src/lake/Lake/CLI/Help.lean | 14 ++++++++++++++
 src/lake/Lake/CLI/Main.lean | 22 ++++++++++++++++++++++
 src/util/shell.cpp          |  4 +++-
 4 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean
index 5750411d6de7..49b499619119 100644
--- a/src/Lean/Shell.lean
+++ b/src/Lean/Shell.lean
@@ -8,6 +8,7 @@ module
 prelude
 import Lean.Elab.Frontend
 import Lean.Elab.ParseImportsFast
+import Lean.PrettyPrinter.Source
 import Lean.Server.Watchdog
 import Lean.Server.FileWorker
 import Lean.Compiler.LCNF.EmitC
@@ -150,6 +151,8 @@ def displayHelp (useStderr : Bool) : IO Unit := do
   out.putStrLn    "  -i, --i=iname          create ilean file"
   out.putStrLn    "  -c, --c=fname          name of the C output file"
   out.putStrLn    "  -b, --bc=fname         name of the LLVM bitcode file"
+  out.putStrLn    "      --format           format the input file using the pretty printer"
+  out.putStrLn    "      --format-check    check if input is already formatted; exit 1 if not"
   out.putStrLn    "      --stdin            take input from stdin"
   out.putStrLn    "  -R, --root=dir         set package root directory from which the module name\n"
   out.putStrLn    "                         of the input file is calculated\n"
@@ -247,6 +250,8 @@ structure ShellOptions where
   jsonOutput : Bool := false
   errorOnKinds : Array Name := #[]
   printStats : Bool := false
+  format : Bool := false
+  formatCheck : Bool := false
   run : Bool := false
 
 @[export lean_shell_options_mk]
@@ -387,6 +392,10 @@ def ShellOptions.process (opts : ShellOptions)
     return {opts with onlyDeps := true, depsJson := true}
   | 'J' => -- `--json`
     return {opts with jsonOutput := true}
+  | 'F' => -- `--format`
+    return {opts with format := true}
+  | 'G' => -- `--format-check`
+    return {opts with format := true, formatCheck := true}
   | 'a' => -- `--stats`
     return {opts with printStats := true}
   | 'x' =>  -- `--print-prefix`
@@ -507,6 +516,17 @@ def shellMain (args : List String) (opts : ShellOptions) : IO UInt32 := do
   if opts.onlySrcDeps then
     Elab.printImportSrcs contents fileName
     return 0
+  if opts.format then
+    let formatted ← PrettyPrinter.ppSource contents fileName opts.leanOpts
+    if opts.formatCheck then
+      return if formatted == contents then 0 else 1
+    else if opts.useStdin then
+      IO.print formatted
+    else
+      let tmpFile := fileName ++ ".fmt.tmp"
+      IO.FS.writeFile tmpFile formatted
+      IO.FS.rename tmpFile fileName
+    return 0
   -- Quick and dirty `#lang` support
   ---TODO: make it extensible, and add `lean4md`
   let contents ←
diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index 1822aae4e909..8bac9b16ab15 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -30,6 +30,7 @@ COMMANDS:
   check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
   shake                 minimize imports in source files
+  format <files>...     format Lean source files in place
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           elaborate a Lean file in Lake's context
   update                update dependencies and save them to the manifest
@@ -685,6 +686,18 @@ the workspace's root package's additional Lean arguments and the given args
 (in that order). The `lean` process is executed in Lake's environment like
 `lake env lean` (see `lake help env` for how the environment is set up)."
 
+def helpFormat :=
+"Format Lean source files
+
+USAGE:
+  lake format [OPTIONS] <files>...
+
+OPTIONS:
+  --check    check formatting without modifying; exit 1 if any file would change
+
+Formats files in place using the Lean pretty printer. Imports are built
+so syntax extensions are available. Only requires parsing, not elaboration."
+
 def helpTranslateConfig :=
 "Translate a Lake configuration file into a different language
 
@@ -734,6 +747,7 @@ public def help : (cmd : String) → String
 | "check-lint"          => helpCheckLint
 | "clean"               => helpClean
 | "shake"               => helpShake
+| "format" | "fmt"      => helpFormat
 | "script"              => helpScriptCli
 | "scripts"             => helpScriptList
 | "run"                 => helpScriptRun
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 3efb002aad35..a4f341903e43 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -1114,6 +1114,27 @@ protected def lean : CliM PUnit := do
   let rc ← ws.evalLeanFile leanFile opts.subArgs.toArray (mkBuildConfig opts)
   exit rc
 
+protected def format : CliM PUnit := do
+  -- Parse format-specific options before file args
+  let mut check := false
+  let args ← getArgs
+  match args with
+  | "--check" :: rest => setArgs rest; check := true
+  | _ => pure ()
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let files ← takeArgs
+  if files.isEmpty then
+    throw <| CliError.missingArg "files"
+  let ws ← loadWorkspace (← mkLoadConfig opts)
+  let flag := if check then "--format-check" else "--format"
+  let mut anyFailed := false
+  for file in files do
+    let rc ← ws.evalLeanFile file #[flag] (mkBuildConfig opts)
+    if rc != 0 then
+      anyFailed := true
+  if anyFailed then exit 1
+
 protected def translateConfig : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
@@ -1218,6 +1239,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "check-lint"          => lake.checkLint
 | "clean"               => lake.clean
 | "shake"               => lake.shake
+| "format" | "fmt"      => lake.format
 | "script"              => lake.script
 | "scripts"             => lake.script.list
 | "run"                 => lake.script.run
diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index bcf7eaf74a02..92cad554029c 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -190,6 +190,8 @@ static struct option g_long_options[] = {
     {"setup",        required_argument, 0, 'u'},
     {"error",        required_argument, 0, 'E'},
     {"json",         no_argument,       0, 'J'},
+    {"format",       no_argument,       0, 'F'},
+    {"format-check", no_argument,       0, 'G'},
     {"print-prefix", no_argument,       0, 'x'},
     {"print-libdir", no_argument,       0, 'L'},
 #ifdef LEAN_DEBUG
@@ -199,7 +201,7 @@ static struct option g_long_options[] = {
 };
 
 static char const * g_opt_str =
-    "PdD:o:i:b:c:C:qgvVht:012j:012rR:M:012T:012ap:eE:"
+    "PdD:o:i:b:c:C:qgvVht:012j:012rR:M:012T:012ap:eE:FG"
 #if defined(LEAN_MULTI_THREAD)
     "s:012"
 #endif