feat: language reference links and examples in docstrings

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 ·)

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 ()

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 ()
 
 /--

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")

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

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 =>

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

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"
   }

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]

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 }