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..5e05d52f8eb2 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 000000000000..53b50150160e
--- /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 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/ExampleHover.lean b/src/Lean/Server/FileWorker/ExampleHover.lean
new file mode 100644
index 000000000000..63302677b3f7
--- /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 c8a5c622d88e..17aad2645526 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 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/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() {
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
 
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
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
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..43ef416a3b11
--- /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 ·)