From c514b679a9c6272f4df4ce021859c106fa7e8121 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 25 Feb 2025 15:58:43 +0100
Subject: [PATCH 01/12] feat: documentation links and examples

Docstrings are now pre-processed as follows:

 * Output included as part of examples is shown with leading line
 comment indicators in hovers

 * URLs of the form `lean-manual://section/section-id` are rewritten
 to links that point at the corresponding section in the Lean
 reference manual. The reference manual's base URL is configured when
 Lean is built and can be overridden with the `LEAN_MANUAL_ROOT`
 environment variable. This way, releases can point documentation
 links to the correct snapshot, and users can use their own, e.g. for
 offline reading.

Manual URLs in docstrings are validated when the docstring is
added. The presence of a URL starting with `lean-manual://` that is
not a syntactically valid section link causes the docstring to be
rejected. This allows for future extensibility to the set of allowed
links. There is no validation that the linked-to section actually
exists.

A stage0 update will be required to make the documentation site
configurable at build time and for releases.
---
 src/Lean/DocString.lean                       |   4 +-
 src/Lean/DocString/Add.lean                   |  61 +++++
 src/Lean/DocString/Extension.lean             |  18 +-
 src/Lean/DocString/Links.lean                 | 152 ++++++++++++
 src/Lean/Elab/BuiltinCommand.lean             |   2 +-
 src/Lean/Elab/DeclModifiers.lean              |   7 +-
 src/Lean/Elab/Inductive.lean                  |   2 +-
 src/Lean/Elab/InheritDoc.lean                 |   3 +-
 src/Lean/Elab/LetRec.lean                     |   2 +-
 src/Lean/Elab/Structure.lean                  |   3 +-
 .../Server/FileWorker/RequestHandling.lean    |   6 +-
 .../FileWorker/RequestHandling/Hover.lean     | 108 +++++++++
 src/include/lean/lean.h                       |   4 +
 src/version.h.in                              |   2 +
 tests/lean/docstringLinkValidation.lean       |  10 +
 .../docstringLinkValidation.lean.expected.out |   2 +
 .../interactive/docstringLinksExamples.lean   |  95 ++++++++
 .../docstringLinksExamples.lean.expected.out  |  24 ++
 tests/lean/run/3497.lean                      |   2 +-
 tests/lean/run/docstringRewrites.lean         | 228 ++++++++++++++++++
 20 files changed, 718 insertions(+), 17 deletions(-)
 create mode 100644 src/Lean/DocString/Add.lean
 create mode 100644 src/Lean/DocString/Links.lean
 create mode 100644 src/Lean/Server/FileWorker/RequestHandling/Hover.lean
 create mode 100644 tests/lean/docstringLinkValidation.lean
 create mode 100644 tests/lean/docstringLinkValidation.lean.expected.out
 create mode 100644 tests/lean/interactive/docstringLinksExamples.lean
 create mode 100644 tests/lean/interactive/docstringLinksExamples.lean.expected.out
 create mode 100644 tests/lean/run/docstringRewrites.lean

diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean
index 15c0fb12b265..453aaca395a3 100644
--- a/src/Lean/DocString.lean
+++ b/src/Lean/DocString.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.DocString.Extension
+import Lean.DocString.Links
 import Lean.Parser.Tactic.Doc
 import Lean.Parser.Term.Doc
 
@@ -29,4 +30,5 @@ def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true
   let declName := alternativeOfTactic env declName |>.getD declName
   let exts := getTacticExtensionString env declName
   let spellings := getRecommendedSpellingString env declName
-  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts ++ spellings)
+  let str := (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts ++ spellings)
+  str.mapM (rewriteManualLinks ·)
diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean
new file mode 100644
index 000000000000..42131d9e32e1
--- /dev/null
+++ b/src/Lean/DocString/Add.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+prelude
+import Lean.Environment
+import Lean.Exception
+import Lean.Log
+import Lean.DocString.Extension
+import Lean.DocString.Links
+
+set_option linter.missingDocs true
+
+namespace Lean
+
+/--
+Validates all links to the Lean reference manual in `docstring`.
+
+This is intended to be used before saving a docstring that is later subject to rewriting with
+`rewriteManualLinks`.
+-/
+def validateDocComment
+    [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
+    (docstring : TSyntax `Lean.Parser.Command.docComment) :
+    m Unit := do
+  let str := docstring.getDocString
+  let pos? := docstring.raw[1].getHeadInfo? >>= (·.getPos?)
+
+  let (errs, out) ← (rewriteManualLinksCore str : IO _)
+
+  for (⟨start, stop⟩, err) in errs do
+    -- Report errors at their actual location if possible
+    if let some pos := pos? then
+      let urlStx : Syntax := .atom (.synthetic (pos + start) (pos + stop)) (str.extract start stop)
+      logErrorAt urlStx err
+    else
+      logError err
+
+/--
+Adds a docstring to the environment, validating documentation links.
+-/
+def addDocString
+    [Monad m] [MonadError m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
+    (declName : Name) (docComment : TSyntax `Lean.Parser.Command.docComment) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  validateDocComment docComment
+  let docString : String ← getDocStringText docComment
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+
+/--
+Adds a docstring to the environment, validating documentation links.
+-/
+def addDocString'
+    [Monad m] [MonadError m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
+    (declName : Name) (docString? : Option (TSyntax `Lean.Parser.Command.docComment)) : m Unit :=
+  match docString? with
+  | some docString => addDocString declName docString
+  | none => return ()
diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
index fe434c61a940..e0a3abc565e9 100644
--- a/src/Lean/DocString/Extension.lean
+++ b/src/Lean/DocString/Extension.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.DeclarationRange
+import Lean.DocString.Links
 import Lean.MonadEnv
 import Init.Data.String.Extra
 
@@ -18,17 +19,26 @@ namespace Lean
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
 builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
-def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
+/--
+Adds a builtin docstring to the compiler.
+
+Any links to the Lean reference manual are validated, and an IO exception is thrown if invalid links
+are present.
+-/
+def addBuiltinDocString (declName : Name) (docString : String) : IO Unit := do
+  -- In practice, this will not happen, because this code is only called from contexts where the
+  -- links have been pre-validated. The check is in place in case this situation ever changes.
+  validateBuiltinDocString docString
   builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
     throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
   modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+def addDocStringCore' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with
-  | some docString => addDocString declName docString
+  | some docString => addDocStringCore declName docString
   | none => return ()
 
 /--
diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
new file mode 100644
index 000000000000..4eb224547b72
--- /dev/null
+++ b/src/Lean/DocString/Links.lean
@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+prelude
+import Lean.Syntax
+
+set_option linter.missingDocs true
+
+namespace Lean
+
+/- After a stage0 update:
+@[extern "lean_get_manual_root"]
+private opaque getManualRoot : Unit → String
+-/
+private def getManualRoot : Unit → String := fun () => ""
+
+private def fallbackManualRoot := "https://lean-lang.org/doc/reference/latest/"
+
+/--
+Computes the root of the Lean reference manual that should be used for targets.
+
+If the environment variable `LEAN_MANUAL_ROOT` is set, it is used as the root. If not, but a manual
+root is pre-configured for the current Lean executable (typically true for releases), then it is
+used. If neither are true, then `https://lean-lang.org/doc/reference/latest/` is used.
+-/
+def manualRoot : BaseIO String := do
+  let r ←
+    if let some root := (← IO.getEnv "LEAN_MANUAL_ROOT") then
+      pure root
+    else
+      let root := getManualRoot ()
+      if root.isEmpty then
+        pure fallbackManualRoot
+      else
+        pure root
+  return if r.endsWith "/" then r else r ++ "/"
+
+/--
+Rewrites links from the internal Lean manual syntax to the correct URL. This rewriting is an
+overapproximation: any parentheses containing the internal syntax of a Lean manual URL is rewritten.
+
+The internal syntax is the URL scheme `lean-manual` followed by the path `/KIND/MORE...`, where
+`KIND` is a kind of content being linked to. Presently, the only valid kind is `section`, and it
+requires that the remainder of the path consists of one element, which is a section or part identifier.
+
+The correct URL is based on a manual root URL, which is determined by the `LEAN_MANUAL_ROOT`
+environment variable. If this environment variable is not set, a manual root provided when Lean was
+built is used (typically this is the version corresponding to the current release). If no such root
+is available, the latest version of the manual is used.
+-/
+def rewriteManualLinksCore (s : String) : BaseIO (Array (String.Range × String) × String) := do
+  let scheme := "lean-manual://"
+  let mut out := ""
+  let mut errors := #[]
+  let mut iter := s.iter
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+
+    if lookingAt scheme iter.prev then
+        let start := iter.prev.forward scheme.length
+        let mut iter' := start
+        while h' : iter'.hasNext do
+          let c' := iter'.curr' h'
+          iter' := iter'.next' h'
+          if !urlChar c' || iter'.atEnd then
+            match rw (start.extract iter'.prev) with
+            | .error err =>
+              errors := errors.push (⟨iter.prev.i, iter'.prev.i⟩, err)
+              out := out.push c
+              break
+            | .ok path =>
+              out := out ++ (← manualRoot) ++ path
+              out := out.push c'
+              iter := iter'
+              break
+    else
+      out := out.push c
+  pure (errors, out)
+
+where
+  /--
+  Returns `true` if the character is one of those allowed in RFC 3986 sections 2.2 and 2.3. other
+  than '(' or')'.
+  -/
+  urlChar (c : Char) : Bool :=
+    -- unreserved
+    c.isAlphanum || c == '-' || c == '.' || c == '_' || c == '~' ||
+    -- gen-delims
+    c == ':' || c == '/' || c == '?' || c == '#' || c == '[' || c == ']' || c == '@' ||
+    -- sub-delims
+    -- ( and ) are excluded due to Markdown's link syntax
+    c == '!' || c == '$' || c == '&' || c == '\'' || /- c == '(' || c == ')' || -/ c == '*' ||
+    c == '+' || c == ',' || c == ';' || c == '='
+
+  /--
+  Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`.
+  -/
+  lookingAt (goal : String) (iter : String.Iterator) : Bool := Id.run do
+    let mut iter := iter
+    let mut iter' := goal.iter
+    while h : (iter.hasNext ∧ iter'.hasNext) do
+      have ⟨h, h'⟩ := h
+      if iter.curr' h == iter'.curr' h' then
+        iter := iter.next' h
+        iter' := iter'.next' h'
+      else return false
+    return !iter'.hasNext
+
+  rw (path : String) : Except String String := do
+    match path.splitOn "/" with
+    | "section" :: args =>
+      if let [s] := args then
+        if s.isEmpty then
+          throw s!"Empty section ID"
+        return s!"find/?domain=Verso.Genre.Manual.section&name={s}"
+      else
+        throw s!"Expected one item after 'section', but got {args}"
+    | [] | [""] =>
+      throw "Missing documentation type"
+    | other :: _ =>
+      throw s!"Unknown documentation type '{other}'. Expected 'section'."
+
+
+/--
+Rewrites Lean reference manual links in `docstring` to point at the reference manual.
+
+This assumes that all such links have already been validated by `validateDocComment`.
+-/
+def rewriteManualLinks (docString : String) : BaseIO String := do
+  let (errs, str) ← rewriteManualLinksCore docString
+  assert! errs.isEmpty
+  return str
+
+
+/--
+Validates all links to the Lean reference manual in `docstring`, printing an error message if any
+are invalid. Returns `true` if all links are valid.
+
+This is intended to be used before saving a docstring that is later subject to rewriting with
+`rewriteManualLinks`, in contexts where the imports needed to produce better error messages in
+`validateDocComment` are not yet available.
+-/
+def validateBuiltinDocString (docString : String) : IO Unit := do
+  let (errs, _) ← rewriteManualLinksCore docString
+  if !errs.isEmpty then
+    throw <|IO.userError <|
+      s!"Errors in builtin documentation comment:\n" ++
+      String.join (errs.toList.map fun (⟨s, e⟩, msg) => s!" * {repr <| docString.extract s e}:\n    {msg}\n")
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 7734a59ccc38..5e6a940a2aae 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -363,7 +363,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
       addDeclarationRangesFromSyntax declName stx id
-    addDocString declName (← getDocStringText doc)
+    addDocString declName doc
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 043e41885377..c33445aad150 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Lean.Structure
 import Lean.Elab.Attributes
+import Lean.DocString.Add
 
 namespace Lean.Elab
 
@@ -59,7 +60,7 @@ inductive RecKind where
 structure Modifiers where
   /-- Input syntax, used for adjusting declaration range (unless missing) -/
   stx             : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩
-  docString?      : Option String := none
+  docString?      : Option (TSyntax ``Parser.Command.docComment) := none
   visibility      : Visibility := Visibility.regular
   isNoncomputable : Bool := false
   recKind         : RecKind := RecKind.default
@@ -136,9 +137,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
       RecKind.partial
     else
       RecKind.nonrec
-  let docString? ← match docCommentStx.getOptional? with
-    | none   => pure none
-    | some s => pure (some (← getDocStringText ⟨s⟩))
+  let docString? := docCommentStx.getOptional?.map TSyntax.mk
   let visibility ← match visibilityStx.getOptional? with
     | none   => pure Visibility.regular
     | some v =>
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index dc4a91f086b6..d5d2139b3982 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -35,7 +35,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
-      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
+      ctorModifiers := { ctorModifiers with docString? := some ⟨leadingDocComment⟩ }
     if ctorModifiers.isPrivate && modifiers.isPrivate then
       throwError "invalid 'private' constructor in a 'private' inductive datatype"
     if ctorModifiers.isProtected && modifiers.isPrivate then
diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean
index ecc5f316517e..84c855be5a8d 100644
--- a/src/Lean/Elab/InheritDoc.lean
+++ b/src/Lean/Elab/InheritDoc.lean
@@ -25,6 +25,7 @@ builtin_initialize
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
         let some doc ← findSimpleDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
-        addDocString decl doc
+        -- This docstring comes from the environment, so documentation links have already been validated
+        addDocStringCore decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"
   }
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 45b257462956..63dd0114a1b3 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -32,7 +32,7 @@ structure LetRecView where
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
   let mut decls : Array LetRecDeclView := #[]
   for attrDeclStx in letRec[1][0].getSepArgs do
-    let docStr? ← expandOptDocComment? attrDeclStx[0]
+    let docStr? := attrDeclStx[0].getOptional?.map TSyntax.mk
     let attrOptStx := attrDeclStx[1]
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 5461cad822f1..baafbcbb0083 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -564,7 +564,8 @@ where
               let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName
               let fieldDeclName := structDeclName ++ fieldName
               let fieldDeclName ← applyVisibility (← toVisibility fieldInfo) fieldDeclName
-              addDocString' fieldDeclName (← findDocString? (← getEnv) fieldInfo.projFn)
+              -- No need to validate links because this docstring was already added to the environment previously
+              addDocStringCore' fieldDeclName (← findDocString? (← getEnv) fieldInfo.projFn)
               let infos := infos.push { ref := (← getRef)
                                         name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?,
                                         kind := StructFieldKind.copiedField }
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index c8a5c622d88e..fa64e24537ca 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -7,6 +7,7 @@ Authors: Wojciech Nawrocki, Marc Huisinga
 prelude
 import Lean.Server.FileWorker.InlayHints
 import Lean.Server.FileWorker.SemanticHighlighting
+import Lean.Server.FileWorker.RequestHandling.Hover
 import Lean.Server.Completion
 import Lean.Server.References
 
@@ -69,8 +70,9 @@ def handleHover (p : HoverParams)
     : RequestM (RequestTask (Option Hover)) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let mkHover (s : String) (r : String.Range) : Hover := {
-    contents := {
+  let mkHover (s : String) (r : String.Range) : Hover :=
+  let s := Hover.rewriteExamples s
+  { contents := {
       kind := MarkupKind.markdown
       value := s
     }
diff --git a/src/Lean/Server/FileWorker/RequestHandling/Hover.lean b/src/Lean/Server/FileWorker/RequestHandling/Hover.lean
new file mode 100644
index 000000000000..6bf4d3b20bd2
--- /dev/null
+++ b/src/Lean/Server/FileWorker/RequestHandling/Hover.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+/-!
+
+This module contains helpers used for formatting hovers according to docstring conventions. Links to
+the reference manual are updated in the module Lean.DocString.Links, because that functionality is
+not specific to hovers.
+
+-/
+
+set_option linter.missingDocs true
+
+namespace Lean.Server.FileWorker.Hover
+
+/--
+Adds a comment marker `-- ` to a line in an output code block, respecting indentation, if the line
+contains any non-space characters. Lines containing only spaces are returned unmodified.
+
+The comment marker is always added at the indicated indentation. If the content of the line is at
+least as indented, then its relative indentation is preserved. Otherwise, it's placed just after the
+line comment marker.
+-/
+private def addCommentAt (indent : Nat) (line : String) : String := Id.run do
+  if line.all (· == ' ') then return line
+  let s := String.join (.replicate indent " ") ++ "-- "
+  let mut iter := line.iter
+  for _i in [0:indent] do
+    if h : iter.hasNext then
+      if iter.curr' h == ' ' then
+        iter := iter.next' h
+      else
+        break
+    else
+      return s
+  return s ++ iter.remainingToString
+
+/--
+Splits a string into lines, preserving newline characters
+-/
+private def lines (s : String) : Array String := Id.run do
+  let mut result := #[]
+  let mut lineStart := s.iter
+  let mut iter := lineStart
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+    if c == '\n' then
+      result := result.push <| lineStart.extract iter
+      lineStart := iter
+
+  if iter != lineStart then
+    result := result.push <| lineStart.extract iter
+  return result
+
+/--
+Rewrites examples in docstring Markdown for output as hover Markdown.
+
+In particular, code blocks with the `output` class have line comment markers inserted. Editors do
+not typically distinguish between code block classes, so some other visual indication is needed to
+separate them. This function is not based on a compliant Markdown parser and may give unpredictable
+results when used with invalid Markdown.
+-/
+def rewriteExamples (docstring : String) : String := Id.run do
+  let lines := lines docstring
+  let mut result : String := ""
+  -- The current state, which tracks the context of the line being processed:
+  -- * `none` means we're not in a code block
+  -- * `some (none, k)` means we're in a non-output code block opened with `k` backticks
+  -- * `some (some i, k)` means we're in an output code block indented `i` columns, opened with
+  --   `k` backticks
+  let mut inOutput : Option (Option Nat × Nat) := none
+  for l in lines do
+    let indent := l.takeWhile (· == ' ') |>.length
+    let mut l' := l.trimLeft
+    -- Is this a code block fence?
+    if l'.startsWith "```" then
+      let count := l'.takeWhile (· == '`') |>.length
+      l' := l'.dropWhile (· == '`')
+      l' := l'.dropWhile (· == ' ')
+      match inOutput with
+      | none => -- not in a code block
+        if l'.startsWith "output" then
+          inOutput := some (some indent, count)
+        else
+          inOutput := some (none, count)
+        result := result ++ l
+      | some (some i, c) => -- in an output code block
+        if c == count then
+          inOutput := none
+          result := result ++ l
+        else
+          result := result ++ addCommentAt i l
+      | some (none, c) => -- in a non-output code block
+        if c == count then
+          inOutput := none
+        result := result ++ l
+    else -- Current line is not a fence ("```")
+      match inOutput with
+      | some (some i, _c) => -- in an output code block
+        -- append whitespace and comment marker
+        result := result ++ addCommentAt i l
+      | _ => -- Not in an output code block
+        result := result ++ l
+  return result
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 4b5b950d60b8..e14284c89337 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -3025,6 +3025,10 @@ static inline lean_obj_res lean_nat_pred(b_lean_obj_arg n) {
     return lean_nat_sub(n, lean_box(1));
 }
 
+static inline lean_obj_res lean_manual_get_root(lean_obj_arg _unit) {
+    return lean_mk_string(LEAN_MANUAL_ROOT);
+}
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/version.h.in b/src/version.h.in
index e44d0579907c..33500fe512eb 100644
--- a/src/version.h.in
+++ b/src/version.h.in
@@ -10,3 +10,5 @@
 #define LEAN_VERSION_STRING "@LEAN_VERSION_STRING@"
 
 #define LEAN_PLATFORM_TARGET "@LEAN_PLATFORM_TARGET@"
+
+#define LEAN_MANUAL_ROOT "@LEAN_MANUAL_ROOT@"
diff --git a/tests/lean/docstringLinkValidation.lean b/tests/lean/docstringLinkValidation.lean
new file mode 100644
index 000000000000..042cd92c73c1
--- /dev/null
+++ b/tests/lean/docstringLinkValidation.lean
@@ -0,0 +1,10 @@
+/-!
+# Error Locations for Links
+
+This test ensures that errors in reference manual link syntax are reported at the correct positions.
+-/
+
+/--
+foo [](lean-manual://) [](lean-manual://f)
+-/
+def x := 44
diff --git a/tests/lean/docstringLinkValidation.lean.expected.out b/tests/lean/docstringLinkValidation.lean.expected.out
new file mode 100644
index 000000000000..531ac8b6e373
--- /dev/null
+++ b/tests/lean/docstringLinkValidation.lean.expected.out
@@ -0,0 +1,2 @@
+docstringLinkValidation.lean:8:7-8:21: error: Missing documentation type
+docstringLinkValidation.lean:8:26-8:41: error: Unknown documentation type 'f'. Expected 'section'.
diff --git a/tests/lean/interactive/docstringLinksExamples.lean b/tests/lean/interactive/docstringLinksExamples.lean
new file mode 100644
index 000000000000..20cd8173f6a4
--- /dev/null
+++ b/tests/lean/interactive/docstringLinksExamples.lean
@@ -0,0 +1,95 @@
+import Lean
+
+/-!
+This file tests that the convention for Lean block examples is correctly displayed in hovers.
+
+Blocks that are indicated as output should be distinguished from blocks that are indicated as code
+when hovers are shown. This is done by prefixing them with line comment markers.
+
+This occurs only in hovers, so that other clients of this information can apply their own
+conventions.
+-/
+
+/-!
+# Ordinary Formatting
+-/
+
+/--
+Does something complicated with IO that involves output.
+
+```lean example
+#eval complicatedIOProgram
+```
+```output
+Hello!
+More output
+```
+-/
+def complicatedIOProgram : IO Unit := do
+           --^ textDocument/hover
+  IO.println "Hello!"
+  IO.println "More output"
+
+
+/-!
+# Indentation
+These tests check the handling of indentation for output blocks
+-/
+
+/--
+Does something complicated with IO that involves output.
+
+```lean example
+#eval anotherComplicatedIOProgram
+```
+
+  ```output
+  Hello!
+      More output
+  ```
+-/
+def anotherComplicatedIOProgram : IO Unit := do
+           --^ textDocument/hover
+  IO.println "Hello!"
+  IO.println "    More output"
+
+/--
+Does something complicated with IO that involves output.
+
+```lean example
+#eval yetAnotherComplicatedIOProgram
+```
+
+  ```output
+Hello!
+      More output
+  ```
+-/
+def yetAnotherComplicatedIOProgram : IO Unit := do
+           --^ textDocument/hover
+  IO.println "Hello!"
+  IO.println "    More output"
+
+
+/-!
+# Programmatic Access
+
+This test ensures that when looking up the docstring programmatically, the output blocks are not rewritten.
+-/
+
+/--
+info: Does something complicated with IO that involves output.
+
+```lean example
+#eval complicatedIOProgram
+```
+```output
+Hello!
+More output
+```
+-/
+#guard_msgs in
+open Lean Elab Command in
+#eval show CommandElabM Unit from do
+  let str ← Lean.findDocString? (← getEnv) ``complicatedIOProgram
+  str.forM (IO.println ·)
diff --git a/tests/lean/interactive/docstringLinksExamples.lean.expected.out b/tests/lean/interactive/docstringLinksExamples.lean.expected.out
new file mode 100644
index 000000000000..4ba51d7fb3cc
--- /dev/null
+++ b/tests/lean/interactive/docstringLinksExamples.lean.expected.out
@@ -0,0 +1,24 @@
+{"textDocument": {"uri": "file:///docstringLinksExamples.lean"},
+ "position": {"line": 27, "character": 13}}
+{"range":
+ {"start": {"line": 27, "character": 4}, "end": {"line": 27, "character": 24}},
+ "contents":
+ {"value":
+  "```lean\ncomplicatedIOProgram : IO Unit\n```\n***\nDoes something complicated with IO that involves output.\n\n```lean example\n#eval complicatedIOProgram\n```\n```output\n-- Hello!\n-- More output\n```\n",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///docstringLinksExamples.lean"},
+ "position": {"line": 50, "character": 13}}
+{"range":
+ {"start": {"line": 50, "character": 4}, "end": {"line": 50, "character": 31}},
+ "contents":
+ {"value":
+  "```lean\nanotherComplicatedIOProgram : IO Unit\n```\n***\nDoes something complicated with IO that involves output.\n\n```lean example\n#eval anotherComplicatedIOProgram\n```\n\n  ```output\n  -- Hello!\n  --     More output\n  ```\n",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///docstringLinksExamples.lean"},
+ "position": {"line": 67, "character": 13}}
+{"range":
+ {"start": {"line": 67, "character": 4}, "end": {"line": 67, "character": 34}},
+ "contents":
+ {"value":
+  "```lean\nyetAnotherComplicatedIOProgram : IO Unit\n```\n***\nDoes something complicated with IO that involves output.\n\n```lean example\n#eval yetAnotherComplicatedIOProgram\n```\n\n  ```output\n  -- Hello!\n  --     More output\n  ```\n",
+  "kind": "markdown"}}
diff --git a/tests/lean/run/3497.lean b/tests/lean/run/3497.lean
index e4d668182fd2..cfa9bac0b855 100644
--- a/tests/lean/run/3497.lean
+++ b/tests/lean/run/3497.lean
@@ -4,4 +4,4 @@ import Lean
 error: invalid doc string, declaration 'Nat.mul' is in an imported module
 -/
 #guard_msgs (error) in
-#eval show Lean.MetaM Unit from Lean.addDocString `Nat.mul "oh no"
+#eval show Lean.MetaM Unit from do Lean.addDocString `Nat.mul (← `(docComment| /-- oh no -/))
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
new file mode 100644
index 000000000000..aefc639e6414
--- /dev/null
+++ b/tests/lean/run/docstringRewrites.lean
@@ -0,0 +1,228 @@
+import Lean.DocString.Links
+import Lean.Elab.Command
+
+/-!
+These tests ensure that links to documentation are correctly validated, and that they are correctly rewritten.
+-/
+
+set_option guard_msgs.diff true
+
+open Lean Elab Command
+
+/--
+Tests the result of the link rewriting procedure.
+
+The result, along with any errors, are converted to readable info that can be captured in
+`#guard_msgs`. Errors are associated with their substrings to check that the association is correct
+as well. Finally, the actual manual URL is replaced with `MANUAL` in order to make the test robust
+in the face of changes to the underlying default.
+-/
+def checkResult (str : String) : CommandElabM Unit := do
+  let result ← rewriteManualLinksCore str
+
+  if !result.1.isEmpty then
+    let errMsgs := result.1.map fun (⟨s, e⟩, msg) => m!" • {repr <| str.extract s e}:{indentD msg}"
+    logInfo <| m!"Errors: {indentD <| MessageData.joinSep errMsgs.toList "\n"}\n\n"
+
+  let root ← manualRoot
+  logInfo m!"Result: {repr <| result.2.replace root "MANUAL/"}"
+
+
+/-- info: Result: "abc" -/
+#guard_msgs in
+#eval checkResult "abc"
+
+/-- info: Result: "abc []()" -/
+#guard_msgs in
+#eval checkResult "abc []()"
+
+/-- info: Result: "abc [](MANUAL/find/?domain=Verso.Genre.Manual.section&name=the-section-id)" -/
+#guard_msgs in
+#eval checkResult "abc [](lean-manual://section/the-section-id)"
+
+/--
+info: Result: "abc\n\nMANUAL/find/?domain=Verso.Genre.Manual.section&name=the-section-id\n\nmore text"
+-/
+#guard_msgs in
+#eval checkResult
+  "abc
+
+lean-manual://section/the-section-id
+
+more text"
+
+/--
+info: Result: "abc\n\nMANUAL/find/?domain=Verso.Genre.Manual.section&name=the-section-id\n\nmore text\n"
+-/
+#guard_msgs in
+#eval checkResult
+  "abc
+
+lean-manual://section/the-section-id
+
+more text
+"
+
+
+/--
+info: Errors: ⏎
+   • "lean-manual://":
+    Missing documentation type
+   • "lean-manual://f":
+    Unknown documentation type 'f'. Expected 'section'.
+   • "lean-manual://a/": Unknown documentation type 'a'. Expected 'section'.  ⏎
+---
+info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b"
+-/
+#guard_msgs in
+#eval checkResult "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b"
+
+/--
+info: Errors: ⏎
+   • "lean-manual://":
+    Missing documentation type
+   • "lean-manual://f":
+    Unknown documentation type 'f'. Expected 'section'.
+   • "lean-manual://a/b": Unknown documentation type 'a'. Expected 'section'.  ⏎
+---
+info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b "
+-/
+#guard_msgs in
+#eval checkResult "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b "
+
+
+/-- info: Result: "abc [](https://foo)" -/
+#guard_msgs in
+#eval checkResult "abc [](https://foo)"
+
+/--
+info: Errors: ⏎
+   • "lean-manual://":
+    Missing documentation type
+
+---
+info: Result: "a b c\nlean-manual://\n"
+-/
+#guard_msgs in
+#eval checkResult "a b c\nlean-manual://\n"
+
+
+/--
+error: Missing documentation type
+---
+error: Unknown documentation type 'f'. Expected 'section'.
+-/
+#guard_msgs in
+/--
+foo [](lean-manual://) [](lean-manual://f)
+-/
+def x := 44
+
+/-!
+# Environment Variable Tests
+
+These tests check that the `LEAN_MANUAL_ROOT` environment variable affects rewriting as expected.
+-/
+
+def checkResultWithRoot (root : Option String) (str : String) : IO Unit := do
+  let lean ← IO.appPath
+  IO.FS.withTempFile fun h path => do
+    h.putStrLn r###"
+import Lean.DocString.Links
+
+open Lean
+
+def main : IO Unit := do
+  let stdin ← IO.getStdin
+  let mut str := ""
+  let mut l ← stdin.getLine
+  while !l.isEmpty do
+    str := str ++ l
+    l ← stdin.getLine
+  IO.println (repr (← rewriteManualLinksCore str))
+"###
+    h.flush
+    let child ← IO.Process.spawn {
+      cmd := lean.toString,
+      args := #["--run", path.toString],
+      env := #[("LEAN_MANUAL_ROOT", root)],
+      stdout := .piped, stderr := .piped, stdin := .piped
+    }
+    let child ← do
+      let (stdin, child) ← child.takeStdin
+      stdin.putStrLn str
+      pure child
+    let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
+    let stderr ← child.stderr.readToEnd
+    let exitCode ← child.wait
+    let stdout ← IO.ofExcept stdout.get
+
+
+    IO.println s!"Exit code: {exitCode}"
+    IO.println "Stdout:"
+    IO.println stdout
+    IO.println "Stderr:"
+    IO.println stderr
+
+/--
+info: Exit code: 0
+Stdout:
+(#[], "\n")
+
+Stderr:
+-/
+#guard_msgs in
+#eval checkResultWithRoot "OVERRIDDEN_ROOT" ""
+
+/--
+info: Exit code: 0
+Stdout:
+(#[], "OVERRIDDEN_ROOT/find/?domain=Verso.Genre.Manual.section&name=foo\n")
+
+Stderr:
+-/
+#guard_msgs in
+#eval checkResultWithRoot "OVERRIDDEN_ROOT" "lean-manual://section/foo"
+
+/--
+info: Exit code: 0
+Stdout:
+(#[], "OVERRIDDEN_ROOT/find/?domain=Verso.Genre.Manual.section&name=foo\n")
+
+Stderr:
+-/
+#guard_msgs in
+#eval checkResultWithRoot "OVERRIDDEN_ROOT/" "lean-manual://section/foo"
+
+
+/--
+info: Exit code: 0
+Stdout:
+(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 22 } }, "Empty section ID")], "lean-manual://section/\n")
+
+Stderr:
+-/
+#guard_msgs in
+#eval checkResultWithRoot "OVERRIDDEN_ROOT" "lean-manual://section/"
+
+/--
+info: Exit code: 0
+Stdout:
+(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 21 } }, "Expected one item after 'section', but got []")],
+ "lean-manual://section\n")
+
+Stderr:
+-/
+#guard_msgs in
+#eval checkResultWithRoot "OVERRIDDEN_ROOT" "lean-manual://section"
+
+/--
+info: Exit code: 0
+Stdout:
+(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 15 } }, "Unknown documentation type 's'. Expected 'section'.")],
+ "lean-manual://s\n")
+
+Stderr:
+-/
+#guard_msgs in
+#eval checkResultWithRoot "OVERRIDDEN_ROOT" "lean-manual://s"

From 452a2fad2675fd8904424584836e3cacdba841a9 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Wed, 26 Feb 2025 13:31:19 +0100
Subject: [PATCH 02/12] chore: ask for stage0 update

---
 stage0/src/stdlib_flags.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index ee225c173430..8aab9e98423a 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,6 +1,7 @@
 #include "util/options.h"
 
-// update stage0
+// Dear CI: Please update stage0 after merging this.
+
 
 namespace lean {
 options get_default_options() {

From 7f951d1c0dfe72a0d9ca462f742fefd29840e765 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Wed, 26 Feb 2025 13:39:13 +0100
Subject: [PATCH 03/12] fix: add missing `prelude` spec to module

---
 src/Lean/Server/FileWorker/RequestHandling/Hover.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Server/FileWorker/RequestHandling/Hover.lean b/src/Lean/Server/FileWorker/RequestHandling/Hover.lean
index 6bf4d3b20bd2..6a5976392732 100644
--- a/src/Lean/Server/FileWorker/RequestHandling/Hover.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling/Hover.lean
@@ -3,6 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Thrane Christiansen
 -/
+prelude
+import Init.Prelude
+import Init.Notation
+import Lean.Elab.Do
 
 /-!
 

From 751bddc7617b60db67b9e0218f47ca6c5b92a910 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Wed, 26 Feb 2025 14:47:48 +0100
Subject: [PATCH 04/12] feat: kinder errors when docstrings contain invalid
 manual links

---
 src/Lean/DocString/Links.lean         | 11 ++++++-
 tests/lean/run/docstringRewrites.lean | 47 +++++++++++++++++++++++++++
 2 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
index 4eb224547b72..661393c4b355 100644
--- a/src/Lean/DocString/Links.lean
+++ b/src/Lean/DocString/Links.lean
@@ -132,7 +132,16 @@ This assumes that all such links have already been validated by `validateDocComm
 -/
 def rewriteManualLinks (docString : String) : BaseIO String := do
   let (errs, str) ← rewriteManualLinksCore docString
-  assert! errs.isEmpty
+  if !errs.isEmpty then
+    let errReport :=
+      r#"**Syntax Errors in Lean Language Reference Links**
+
+The `lean-manual` URL scheme is used to link to the version of the Lean reference manual that
+corresponds to this version of Lean. Errors occurred while processing the links in this documentation
+comment:
+"# ++
+      String.join (errs.toList.map (fun (⟨s, e⟩, msg) => s!" * ```{docString.extract s e}```: {msg}\n\n"))
+    return str ++ "\n\n" ++ errReport
   return str
 
 
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index aefc639e6414..eb7aa59087fb 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -1,4 +1,5 @@
 import Lean.DocString.Links
+import Lean.DocString
 import Lean.Elab.Command
 
 /-!
@@ -226,3 +227,49 @@ Stderr:
 -/
 #guard_msgs in
 #eval checkResultWithRoot "OVERRIDDEN_ROOT" "lean-manual://s"
+
+/-!
+# Syntax Errors in Manual Links
+
+Should an unvalidated docstring sneak into the environment, syntax errors in its Lean manual links
+are reported in the docstring.
+-/
+
+def bogus := "bogus"
+
+#eval Lean.addDocStringCore ``bogus
+  r#"See [the manual](lean-manual://invalid/link)
+
+It contains many things of lean-manual:// interest
+
+It contains many further things of even greater lean-manual://section/ interest
+
+It contains many further things of even greater lean-manual://section/aaaaa/bbbb interest
+"#
+
+/--
+info: See [the manual](lean-manual://invalid/link)
+
+It contains many things of lean-manual:// interest
+
+It contains many further things of even greater lean-manual://section/ interest
+
+It contains many further things of even greater lean-manual://section/aaaaa/bbbb interest
+
+
+**Syntax Errors in Lean Language Reference Links**
+
+The `lean-manual` URL scheme is used to link to the version of the Lean reference manual that
+corresponds to this version of Lean. Errors occurred while processing the links in this documentation:
+ * ```lean-manual://invalid/link```: Unknown documentation type 'invalid'. Expected 'section'.
+
+ * ```lean-manual://```: Missing documentation type
+
+ * ```lean-manual://section/```: Empty section ID
+
+ * ```lean-manual://section/aaaaa/bbbb```: Expected one item after 'section', but got [aaaaa, bbbb]
+-/
+#guard_msgs in
+#eval show CommandElabM Unit from do
+  let str ← Lean.findDocString? (← getEnv) ``bogus
+  str.forM (logInfo ·)

From 4e0a824d965bf7f8b7563cc6729b8987ce42b5d0 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Wed, 26 Feb 2025 18:16:40 +0100
Subject: [PATCH 05/12] fix: test phrasing

---
 tests/lean/run/docstringRewrites.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index eb7aa59087fb..3a821e982127 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -260,7 +260,8 @@ It contains many further things of even greater lean-manual://section/aaaaa/bbbb
 **Syntax Errors in Lean Language Reference Links**
 
 The `lean-manual` URL scheme is used to link to the version of the Lean reference manual that
-corresponds to this version of Lean. Errors occurred while processing the links in this documentation:
+corresponds to this version of Lean. Errors occurred while processing the links in this documentation
+comment:
  * ```lean-manual://invalid/link```: Unknown documentation type 'invalid'. Expected 'section'.
 
  * ```lean-manual://```: Missing documentation type

From 9b2cd035da597e16abbaa67a72b63ab8dfd24654 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 07:15:42 +0100
Subject: [PATCH 06/12] Improvements from code review

---
 src/Lean/DocString/Links.lean                 | 46 +++++++---------
 .../Hover.lean => ExampleHover.lean}          | 52 +++++++++++--------
 .../Server/FileWorker/RequestHandling.lean    | 15 +++---
 tests/lean/run/docstringRewrites.lean         |  2 +-
 4 files changed, 57 insertions(+), 58 deletions(-)
 rename src/Lean/Server/FileWorker/{RequestHandling/Hover.lean => ExampleHover.lean} (73%)

diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
index 661393c4b355..034f9c87bef6 100644
--- a/src/Lean/DocString/Links.lean
+++ b/src/Lean/DocString/Links.lean
@@ -61,22 +61,22 @@ def rewriteManualLinksCore (s : String) : BaseIO (Array (String.Range × String)
     iter := iter.next' h
 
     if lookingAt scheme iter.prev then
-        let start := iter.prev.forward scheme.length
-        let mut iter' := start
-        while h' : iter'.hasNext do
-          let c' := iter'.curr' h'
-          iter' := iter'.next' h'
-          if !urlChar c' || iter'.atEnd then
-            match rw (start.extract iter'.prev) with
-            | .error err =>
-              errors := errors.push (⟨iter.prev.i, iter'.prev.i⟩, err)
-              out := out.push c
-              break
-            | .ok path =>
-              out := out ++ (← manualRoot) ++ path
-              out := out.push c'
-              iter := iter'
-              break
+      let start := iter.prev.forward scheme.length
+      let mut iter' := start
+      while h' : iter'.hasNext do
+        let c' := iter'.curr' h'
+        iter' := iter'.next' h'
+        if !urlChar c' || iter'.atEnd then
+          match rw (start.extract iter'.prev) with
+          | .error err =>
+            errors := errors.push (⟨iter.prev.i, iter'.prev.i⟩, err)
+            out := out.push c
+            break
+          | .ok path =>
+            out := out ++ (← manualRoot) ++ path
+            out := out.push c'
+            iter := iter'
+            break
     else
       out := out.push c
   pure (errors, out)
@@ -99,16 +99,8 @@ where
   /--
   Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`.
   -/
-  lookingAt (goal : String) (iter : String.Iterator) : Bool := Id.run do
-    let mut iter := iter
-    let mut iter' := goal.iter
-    while h : (iter.hasNext ∧ iter'.hasNext) do
-      have ⟨h, h'⟩ := h
-      if iter.curr' h == iter'.curr' h' then
-        iter := iter.next' h
-        iter' := iter'.next' h'
-      else return false
-    return !iter'.hasNext
+  lookingAt (goal : String) (iter : String.Iterator) : Bool :=
+    iter.s.substrEq iter.i goal 0 goal.endPos.byteIdx
 
   rw (path : String) : Except String String := do
     match path.splitOn "/" with
@@ -134,7 +126,7 @@ def rewriteManualLinks (docString : String) : BaseIO String := do
   let (errs, str) ← rewriteManualLinksCore docString
   if !errs.isEmpty then
     let errReport :=
-      r#"**Syntax Errors in Lean Language Reference Links**
+      r#"**❌ Syntax Errors in Lean Language Reference Links**
 
 The `lean-manual` URL scheme is used to link to the version of the Lean reference manual that
 corresponds to this version of Lean. Errors occurred while processing the links in this documentation
diff --git a/src/Lean/Server/FileWorker/RequestHandling/Hover.lean b/src/Lean/Server/FileWorker/ExampleHover.lean
similarity index 73%
rename from src/Lean/Server/FileWorker/RequestHandling/Hover.lean
rename to src/Lean/Server/FileWorker/ExampleHover.lean
index 6a5976392732..63302677b3f7 100644
--- a/src/Lean/Server/FileWorker/RequestHandling/Hover.lean
+++ b/src/Lean/Server/FileWorker/ExampleHover.lean
@@ -4,16 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Thrane Christiansen
 -/
 prelude
-import Init.Prelude
-import Init.Notation
 import Lean.Elab.Do
 
 /-!
-
 This module contains helpers used for formatting hovers according to docstring conventions. Links to
 the reference manual are updated in the module Lean.DocString.Links, because that functionality is
 not specific to hovers.
-
 -/
 
 set_option linter.missingDocs true
@@ -29,21 +25,27 @@ least as indented, then its relative indentation is preserved. Otherwise, it's p
 line comment marker.
 -/
 private def addCommentAt (indent : Nat) (line : String) : String := Id.run do
-  if line.all (· == ' ') then return line
-  let s := String.join (.replicate indent " ") ++ "-- "
+  let s := "".pushn ' ' indent ++ "-- "
   let mut iter := line.iter
   for _i in [0:indent] do
     if h : iter.hasNext then
       if iter.curr' h == ' ' then
         iter := iter.next' h
       else
+        -- Non-whitespace found *before* the indentation level. This output should be indented
+        -- as if it were exactly at the indentation level.
         break
     else
-      return s
-  return s ++ iter.remainingToString
+      -- The line was entirely ' ', and was shorter than the indentation level. No `--` added.
+      return line
+  let remaining := iter.remainingToString
+  if remaining.all (· == ' ') then
+    return line
+  else
+    return s ++ remaining
 
 /--
-Splits a string into lines, preserving newline characters
+Splits a string into lines, preserving newline characters.
 -/
 private def lines (s : String) : Array String := Id.run do
   let mut result := #[]
@@ -60,6 +62,14 @@ private def lines (s : String) : Array String := Id.run do
     result := result.push <| lineStart.extract iter
   return result
 
+private inductive RWState where
+  /-- Not in a code block -/
+  | normal
+  /-- In a non-`output` code block opened with `ticks` backtick characters -/
+  | nonOutput (ticks : Nat)
+  /-- In an `output` code block indented `indent` columns opened with `ticks` backtick characters -/
+  | output (indent : Nat) (ticks : Nat)
+
 /--
 Rewrites examples in docstring Markdown for output as hover Markdown.
 
@@ -71,12 +81,8 @@ results when used with invalid Markdown.
 def rewriteExamples (docstring : String) : String := Id.run do
   let lines := lines docstring
   let mut result : String := ""
-  -- The current state, which tracks the context of the line being processed:
-  -- * `none` means we're not in a code block
-  -- * `some (none, k)` means we're in a non-output code block opened with `k` backticks
-  -- * `some (some i, k)` means we're in an output code block indented `i` columns, opened with
-  --   `k` backticks
-  let mut inOutput : Option (Option Nat × Nat) := none
+  -- The current state, which tracks the context of the line being processed
+  let mut inOutput : RWState := .normal
   for l in lines do
     let indent := l.takeWhile (· == ' ') |>.length
     let mut l' := l.trimLeft
@@ -86,25 +92,25 @@ def rewriteExamples (docstring : String) : String := Id.run do
       l' := l'.dropWhile (· == '`')
       l' := l'.dropWhile (· == ' ')
       match inOutput with
-      | none => -- not in a code block
+      | .normal =>
         if l'.startsWith "output" then
-          inOutput := some (some indent, count)
+          inOutput := .output indent count
         else
-          inOutput := some (none, count)
+          inOutput := .nonOutput count
         result := result ++ l
-      | some (some i, c) => -- in an output code block
+      | .output i c =>
         if c == count then
-          inOutput := none
+          inOutput := .normal
           result := result ++ l
         else
           result := result ++ addCommentAt i l
-      | some (none, c) => -- in a non-output code block
+      | .nonOutput c =>
         if c == count then
-          inOutput := none
+          inOutput := .normal
         result := result ++ l
     else -- Current line is not a fence ("```")
       match inOutput with
-      | some (some i, _c) => -- in an output code block
+      | .output i _c =>
         -- append whitespace and comment marker
         result := result ++ addCommentAt i l
       | _ => -- Not in an output code block
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index fa64e24537ca..17aad2645526 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki, Marc Huisinga
 -/
 prelude
+import Lean.Server.FileWorker.ExampleHover
 import Lean.Server.FileWorker.InlayHints
 import Lean.Server.FileWorker.SemanticHighlighting
-import Lean.Server.FileWorker.RequestHandling.Hover
 import Lean.Server.Completion
 import Lean.Server.References
 
@@ -71,13 +71,14 @@ def handleHover (p : HoverParams)
   let doc ← readDoc
   let text := doc.meta.text
   let mkHover (s : String) (r : String.Range) : Hover :=
-  let s := Hover.rewriteExamples s
-  { contents := {
-      kind := MarkupKind.markdown
-      value := s
+    let s := Hover.rewriteExamples s
+    {
+      contents := {
+        kind := MarkupKind.markdown
+        value := s
+      }
+      range? := r.toLspRange text
     }
-    range? := r.toLspRange text
-  }
 
   let hoverPos := text.lspPosToUtf8Pos p.position
   withWaitFindSnap doc (fun s => s.endPos > hoverPos)
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index 3a821e982127..5cb97982925f 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -257,7 +257,7 @@ It contains many further things of even greater lean-manual://section/ interest
 It contains many further things of even greater lean-manual://section/aaaaa/bbbb interest
 
 
-**Syntax Errors in Lean Language Reference Links**
+**❌ Syntax Errors in Lean Language Reference Links**
 
 The `lean-manual` URL scheme is used to link to the version of the Lean reference manual that
 corresponds to this version of Lean. Errors occurred while processing the links in this documentation

From dfcccd48d2536350256a806a40c71d62ca594b61 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 08:08:34 +0100
Subject: [PATCH 07/12] Update src/Lean/DocString/Links.lean

Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
---
 src/Lean/DocString/Links.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
index 034f9c87bef6..263158d6478d 100644
--- a/src/Lean/DocString/Links.lean
+++ b/src/Lean/DocString/Links.lean
@@ -148,6 +148,6 @@ This is intended to be used before saving a docstring that is later subject to r
 def validateBuiltinDocString (docString : String) : IO Unit := do
   let (errs, _) ← rewriteManualLinksCore docString
   if !errs.isEmpty then
-    throw <|IO.userError <|
+    throw <| IO.userError <|
       s!"Errors in builtin documentation comment:\n" ++
       String.join (errs.toList.map fun (⟨s, e⟩, msg) => s!" * {repr <| docString.extract s e}:\n    {msg}\n")

From d5dac99fb0920cbdc7fda5d547438f2c198f0499 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 11:17:23 +0100
Subject: [PATCH 08/12] perf: remove docstring link validation on adding
 builtin docstrings

Now it occurs in the test suite instead.
---
 src/Lean/DocString/Extension.lean     |  7 ++----
 tests/lean/run/docstringRewrites.lean | 36 +++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
index e0a3abc565e9..5e05d52f8eb2 100644
--- a/src/Lean/DocString/Extension.lean
+++ b/src/Lean/DocString/Extension.lean
@@ -22,13 +22,10 @@ builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclar
 /--
 Adds a builtin docstring to the compiler.
 
-Any links to the Lean reference manual are validated, and an IO exception is thrown if invalid links
-are present.
+Links to the Lean manual aren't validated.
 -/
+-- See the test `lean/run/docstringRewrites.lean` for the validation of builtin docstring links
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit := do
-  -- In practice, this will not happen, because this code is only called from contexts where the
-  -- links have been pre-validated. The check is in place in case this situation ever changes.
-  validateBuiltinDocString docString
   builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
 def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index 5cb97982925f..43ef416a3b11 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -10,6 +10,42 @@ set_option guard_msgs.diff true
 
 open Lean Elab Command
 
+/-!
+# Check All Built-In Docstrings
+
+Manual links in built-in docstrings aren't validated when adding them, so they are checked here.
+
+This is an over-approximation: it checks all the docstrings in Lean.
+-/
+
+/-!
+First, define one broken builtin docstring to make sure that the test actually catches them.
+-/
+def check := 5
+#eval addBuiltinDocString `check "Here's a broken manual link: lean-manual://oops\n"
+
+/-!
+Now validate the docstrings.
+-/
+
+/--
+error: Docstring errors for 'check': ⏎
+   • "lean-manual://oops":
+    Unknown documentation type 'oops'. Expected 'section'.
+-/
+#guard_msgs in
+#eval show CommandElabM Unit from do
+  let env ← getEnv
+  for (x, _) in env.constants do
+    if let some str ← findSimpleDocString? env x (includeBuiltin := true) then
+      let (errs, _) ← rewriteManualLinksCore str
+      if !errs.isEmpty then
+        let errMsgs := errs.map fun (⟨s, e⟩, msg) => m!" • {repr <| str.extract s e}:{indentD msg}"
+        logError <| m!"Docstring errors for '{x}': {indentD <| MessageData.joinSep errMsgs.toList "\n"}\n\n"
+
+
+/-! # Test Link Rewriting -/
+
 /--
 Tests the result of the link rewriting procedure.
 

From 2cc98f3a27807de76780d4bfa46d4269ea9e3ea7 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 11:18:28 +0100
Subject: [PATCH 09/12] fix: type error in benchmark

---
 tests/bench/identifier_completion.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/bench/identifier_completion.lean b/tests/bench/identifier_completion.lean
index 6042bba61d6d..5d69132168c7 100644
--- a/tests/bench/identifier_completion.lean
+++ b/tests/bench/identifier_completion.lean
@@ -16,7 +16,7 @@ def buildSyntheticEnv : Lean.CoreM Unit := do
       isUnsafe := false
       all := [name]
     }
-    addDocString name "A synthetic doc-string"
+    addDocStringCore name "A synthetic doc-string"
 
 #eval buildSyntheticEnv
 

From 9e65a99438ee2b9620f9ab8333f0e577a8d7b60e Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 12:55:32 +0100
Subject: [PATCH 10/12] fix: type error in the code used in the benchmark

The code comes from the LSP logfile, rather than the file on disk.
---
 tests/bench/identifier_completion_didOpen.log | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench/identifier_completion_didOpen.log b/tests/bench/identifier_completion_didOpen.log
index 6ea4dffa8d1b..eeab03db7485 100644
--- a/tests/bench/identifier_completion_didOpen.log
+++ b/tests/bench/identifier_completion_didOpen.log
@@ -1,3 +1,3 @@
-Content-Length: 992
+Content-Length: 996
 
-{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/mhuisi/Lean/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":952,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\nset_option debug.skipKernelTC true\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n  for i in [0:100000] do\n    let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n    addDecl <| Declaration.opaqueDecl {\n      name := name\n      levelParams := []\n      type := .const `Nat []\n      value := .const `Nat.zero []\n      isUnsafe := false\n      all := [name]\n    }\n    addDocString name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}}
\ No newline at end of file
+{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/mhuisi/Lean/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":952,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\nset_option debug.skipKernelTC true\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n  for i in [0:100000] do\n    let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n    addDecl <| Declaration.opaqueDecl {\n      name := name\n      levelParams := []\n      type := .const `Nat []\n      value := .const `Nat.zero []\n      isUnsafe := false\n      all := [name]\n    }\n    addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}}
\ No newline at end of file

From afbc678ddfac71b19e35b393b559b9ef00430d43 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 14:10:11 +0100
Subject: [PATCH 11/12] fix: deprecation warning in benchmark

---
 tests/bench/ilean_roundtrip.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/bench/ilean_roundtrip.lean b/tests/bench/ilean_roundtrip.lean
index b46a8c24a29f..53fe36983d18 100644
--- a/tests/bench/ilean_roundtrip.lean
+++ b/tests/bench/ilean_roundtrip.lean
@@ -35,7 +35,7 @@ def parse (s : String) : IO (Except String Lean.Json) := do
   return Lean.Json.parse s
 
 def main (args : List String) : IO Unit := do
-  let n := (args.get! 0).toNat!
+  let n := (args[0]!).toNat!
   let refs ← genModuleRefs n
   let compressStartTime ← IO.monoMsNow
   let s ← compress refs

From 45b02fc666b44a7140fb2a0e2fdc62fe4b9236fb Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 11 Mar 2025 14:36:20 +0100
Subject: [PATCH 12/12] chore: improve style of URL rewriting code for hovers

---
 src/Lean/DocString/Links.lean | 39 +++++++++++++++++++----------------
 1 file changed, 21 insertions(+), 18 deletions(-)

diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
index 263158d6478d..53b50150160e 100644
--- a/src/Lean/DocString/Links.lean
+++ b/src/Lean/DocString/Links.lean
@@ -60,25 +60,28 @@ def rewriteManualLinksCore (s : String) : BaseIO (Array (String.Range × String)
     let c := iter.curr' h
     iter := iter.next' h
 
-    if lookingAt scheme iter.prev then
-      let start := iter.prev.forward scheme.length
-      let mut iter' := start
-      while h' : iter'.hasNext do
-        let c' := iter'.curr' h'
-        iter' := iter'.next' h'
-        if !urlChar c' || iter'.atEnd then
-          match rw (start.extract iter'.prev) with
-          | .error err =>
-            errors := errors.push (⟨iter.prev.i, iter'.prev.i⟩, err)
-            out := out.push c
-            break
-          | .ok path =>
-            out := out ++ (← manualRoot) ++ path
-            out := out.push c'
-            iter := iter'
-            break
-    else
+    if !lookingAt scheme iter.prev then
       out := out.push c
+      continue
+
+    let start := iter.prev.forward scheme.length
+    let mut iter' := start
+    while h' : iter'.hasNext do
+      let c' := iter'.curr' h'
+      iter' := iter'.next' h'
+      if urlChar c' && !iter'.atEnd then
+        continue
+      match rw (start.extract iter'.prev) with
+      | .error err =>
+        errors := errors.push (⟨iter.prev.i, iter'.prev.i⟩, err)
+        out := out.push c
+        break
+      | .ok path =>
+        out := out ++ (← manualRoot) ++ path
+        out := out.push c'
+        iter := iter'
+        break
+
   pure (errors, out)
 
 where