From eb58f46ce7b41a9b6b273bb2dae2dc11abd78246 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 12 Mar 2025 10:17:27 +0100
Subject: [PATCH] feat: language reference links and examples in docstrings
 (#7240)

This PR adds a canonical syntax for linking to sections in the language
reference along with formatting of examples in docstrings according to
the docstring style guide.


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. To provide
the best possible error messages in case of validation failures,
`Lean.addDocString` now takes a `TSyntax ``docComment` instead of a
string; clients should adapt by removing the step that extracts the
string, or by calling the lower-level `addDocStringCore` in cases where
the docstring in question is obtained from the environment and has thus
already had its links validated.

A stage0 update is required to make the documentation site configurable
at build time and for releases. A local commit on top of a stage0 update
that will be sent in a followup PR includes the configurable reference
manual root and updates to the release checklist.

---------

Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
---
 src/Lean/DocString.lean                       |   4 +-
 src/Lean/DocString/Add.lean                   |  61 ++++
 src/Lean/DocString/Extension.lean             |  15 +-
 src/Lean/DocString/Links.lean                 | 156 +++++++++
 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 +-
 src/Lean/Server/FileWorker/ExampleHover.lean  | 118 +++++++
 .../Server/FileWorker/RequestHandling.lean    |  15 +-
 src/include/lean/lean.h                       |   4 +
 src/version.h.in                              |   2 +
 stage0/src/stdlib_flags.h                     |   3 +-
 tests/bench/identifier_completion.lean        |   2 +-
 tests/bench/identifier_completion_didOpen.log |   4 +-
 tests/bench/ilean_roundtrip.lean              |   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         | 312 ++++++++++++++++++
 24 files changed, 824 insertions(+), 26 deletions(-)
 create mode 100644 src/Lean/DocString/Add.lean
 create mode 100644 src/Lean/DocString/Links.lean
 create mode 100644 src/Lean/Server/FileWorker/ExampleHover.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 15c0fb12b2..453aaca395 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 0000000000..42131d9e32
--- /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 fe434c61a9..5e05d52f8e 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,23 @@ 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.
+
+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
   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 0000000000..53b5015016
--- /dev/null
+++ b/src/Lean/DocString/Links.lean
@@ -0,0 +1,156 @@
+/-
+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
+      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
+  /--
+  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 :=
+    iter.s.substrEq iter.i goal 0 goal.endPos.byteIdx
+
+  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
+  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
+
+
+/--
+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 7734a59ccc..5e6a940a2a 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 043e418853..c33445aad1 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 dc4a91f086..d5d2139b39 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 ecc5f31651..84c855be5a 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 45b2574629..63dd0114a1 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 5461cad822..baafbcbb00 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/ExampleHover.lean b/src/Lean/Server/FileWorker/ExampleHover.lean
new file mode 100644
index 0000000000..63302677b3
--- /dev/null
+++ b/src/Lean/Server/FileWorker/ExampleHover.lean
@@ -0,0 +1,118 @@
+/-
+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.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
+
+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
+  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
+      -- 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.
+-/
+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
+
+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.
+
+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
+  let mut inOutput : RWState := .normal
+  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
+      | .normal =>
+        if l'.startsWith "output" then
+          inOutput := .output indent count
+        else
+          inOutput := .nonOutput count
+        result := result ++ l
+      | .output i c =>
+        if c == count then
+          inOutput := .normal
+          result := result ++ l
+        else
+          result := result ++ addCommentAt i l
+      | .nonOutput c =>
+        if c == count then
+          inOutput := .normal
+        result := result ++ l
+    else -- Current line is not a fence ("```")
+      match inOutput with
+      | .output i _c =>
+        -- 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/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index c8a5c622d8..17aad26455 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -5,6 +5,7 @@ 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.Completion
@@ -69,13 +70,15 @@ 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 := {
-      kind := MarkupKind.markdown
-      value := s
+  let mkHover (s : String) (r : String.Range) : Hover :=
+    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/src/include/lean/lean.h b/src/include/lean/lean.h
index 4b5b950d60..e14284c893 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 e44d057990..33500fe512 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/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index ee225c1734..8aab9e9842 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() {
diff --git a/tests/bench/identifier_completion.lean b/tests/bench/identifier_completion.lean
index 6042bba61d..5d69132168 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
 
diff --git a/tests/bench/identifier_completion_didOpen.log b/tests/bench/identifier_completion_didOpen.log
index 6ea4dffa8d..eeab03db74 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
diff --git a/tests/bench/ilean_roundtrip.lean b/tests/bench/ilean_roundtrip.lean
index b46a8c24a2..53fe36983d 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
diff --git a/tests/lean/docstringLinkValidation.lean b/tests/lean/docstringLinkValidation.lean
new file mode 100644
index 0000000000..042cd92c73
--- /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 0000000000..531ac8b6e3
--- /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 0000000000..20cd8173f6
--- /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 0000000000..4ba51d7fb3
--- /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 e4d668182f..cfa9bac0b8 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 0000000000..43ef416a3b
--- /dev/null
+++ b/tests/lean/run/docstringRewrites.lean
@@ -0,0 +1,312 @@
+import Lean.DocString.Links
+import Lean.DocString
+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
+
+/-!
+# 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.
+
+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"
+
+/-!
+# 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
+comment:
+ * ```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 ·)