feat: docstrings with Verso syntax (#10307)

This PR upstreams the Verso parser and adds preliminary support for
Verso in docstrings. This will allow the compiler to check examples and
cross-references in documentation.

After a `stage0` update, a follow-up PR will add the appropriate
attributes that allow the feature to be used. The parser tests from
Verso also remain to be upstreamed, and user-facing documentation will
be added once the feature has been used on more internals.

src/Lean/BuiltinDocAttr.lean

@@ -34,6 +34,7 @@ builtin_initialize
     add   := fun decl stx _ => do
       Attribute.Builtin.ensureNoArgs stx
       declareBuiltinDocStringAndRanges decl
+    applicationTime := AttributeApplicationTime.afterCompilation
   }
 
 end Lean

src/Lean/Data/EditDistance.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2024-2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+module
+prelude
+public import Init
+
+set_option linter.missingDocs true
+
+namespace Lean.EditDistance
+
+/--
+Computes the Levenshtein distance between two strings, up to some cutoff.
+
+If the return value is `none`, then the distance is certainly greater than the cutoff value, but a
+returned `some` does not necessarily indicate that the edit distance is less than or equal to the
+cutoff.
+-/
+public def levenshtein (str1 str2 : String) (cutoff : Nat) : Option Nat := Id.run do
+  let len1 := str1.length
+  let len2 := str2.length
+
+  -- The lower bound on the Levenshtein distance is the difference in lengths
+  if max len1 len2 - min len1 len2 > cutoff then return none
+
+  let mut v0 := Vector.replicate (len2 + 1) 0
+  let mut v1 := v0
+
+  for h : i in [0:v0.size] do
+    v0 := v0.set i i
+  let mut iter1 := str1.iter
+  let mut i := 0
+  while h1 : iter1.hasNext do
+    v1 := v1.set 0 (i+1)
+    let mut iter2 := str2.iter
+    let mut j : Fin (len2 + 1) := 0
+    while h2 : iter2.hasNext do
+      let j' : Fin _ := j + 1
+      let deletionCost := v0[j'] + 1
+      let insertionCost := v1[j] + 1
+      let substCost :=
+        if iter1.curr' h1 == iter2.curr' h2 then v0[j]
+        else v0[j] + 1
+      let cost := min (min deletionCost insertionCost) substCost
+      v1 := v1.set j' cost
+      iter2 := iter2.next' h2
+      j := j + 1
+    iter1 := iter1.next' h1
+    i := i + 1
+    -- Terminate early if it's impossible that the result is below the cutoff
+    if v1.all (· > cutoff) then return none
+    v0 := v1
+  some v0[len2]

src/Lean/DocString/Add.lean

@@ -7,11 +7,17 @@ Authors: David Thrane Christiansen
 module
 
 prelude
-public import Lean.Environment
-public import Lean.Exception
-public import Lean.Log
-public import Lean.DocString.Extension
-public import Lean.DocString.Links
+import Lean.Environment
+import Lean.Exception
+import Lean.Log
+import Lean.Elab.DocString
+import Lean.DocString.Extension
+import Lean.DocString.Links
+import Lean.Parser.Types
+import Lean.DocString.Parser
+import Lean.ResolveName
+public import Lean.Elab.Term.TermElabM
+import Std.Data.HashMap
 
 public section
 
@@ -19,6 +25,8 @@ set_option linter.missingDocs true
 
 namespace Lean
 
+open Lean.Elab.Term (TermElabM)
+
 /--
 Validates all links to the Lean reference manual in `docstring`.
 
@@ -26,9 +34,8 @@ This is intended to be used before saving a docstring that is later subject to r
 `rewriteManualLinks`.
 -/
 def validateDocComment
-    [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
     (docstring : TSyntax `Lean.Parser.Command.docComment) :
-    m Unit := do
+    TermElabM Unit := do
   let str := docstring.getDocString
   let pos? := docstring.raw[1].getHeadInfo? >>= (·.getPos?)
 
@@ -42,27 +49,131 @@ def validateDocComment
     else
       logError err
 
+
+open Lean.Doc in
+open Parser in
 /--
-Adds a docstring to the environment, validating documentation links.
+Adds a Verso docstring to the specified declaration, which should already be present in the
+environment.
 -/
-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
+def versoDocString
+    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
+
+  let text ← getFileMap
+  -- TODO fallback to string version without nice interactivity
+  let some startPos := docComment.raw[1].getPos? (canonicalOnly := true)
+    | throwErrorAt docComment m!"Documentation comment has no source location, cannot parse"
+  let some endPos := docComment.raw[1].getTailPos? (canonicalOnly := true)
+    | throwErrorAt docComment m!"Documentation comment has no source location, cannot parse"
+
+  -- Skip trailing `-/`
+  let endPos := text.source.prev <| text.source.prev endPos
+  let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos
+  have endPos_valid : endPos ≤ text.source.endPos := by
+    unfold endPos
+    split <;> simp [*]
+
+  let env ← getEnv
+  let ictx : InputContext :=
+    .mk text.source (← getFileName) (fileMap := text)
+      (endPos := endPos) (endPos_valid := endPos_valid)
+  let pmctx : ParserModuleContext := {
+    env,
+    options := ← getOptions,
+    currNamespace := (← getCurrNamespace),
+    openDecls := (← getOpenDecls)
+  }
+  let s := mkParserState text.source |>.setPos startPos
+  -- TODO parse one block at a time for error recovery purposes
+  let s := (Doc.Parser.document).run ictx pmctx (getTokenTable env) s
+
+  if !s.allErrors.isEmpty then
+    for (pos, _, err) in s.allErrors do
+      logMessage {
+        fileName := (← getFileName),
+        pos := text.toPosition pos,
+        -- TODO end position
+        data := err.toString
+      }
+    return (#[], #[])
+  else
+    let stx := s.stxStack.back
+    let stx := stx.getArgs
+    Doc.elabBlocks (stx.map (⟨·⟩)) |>.exec declName binders
+
+/--
+Adds a Markdown docstring to the environment, validating documentation links.
+-/
+def addMarkdownDocString (declName : Name) (docComment : TSyntax `Lean.Parser.Command.docComment) : TermElabM Unit := do
   if declName.isAnonymous then
     -- This case might happen on partial elaboration; ignore instead of triggering any panics below
     return
+  let throwImported {α} : TermElabM α :=
+    throwError m!"invalid doc string, declaration `{.ofConstName declName}` is in an imported module"
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError "invalid doc string, declaration `{.ofConstName declName}` is in an imported module"
+    throwImported
   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.
+Adds an elaborated Verso docstring to the environment.
+-/
+def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m]
+    (declName : Name) (docs : VersoDocString) : m Unit := do
+  let throwImported {α} : m α :=
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwImported
+  modifyEnv fun env =>
+    versoDocStringExt.insert env declName docs --addEntry (asyncMode := .async .asyncEnv)
+      --env (declName, p) -- Using .insert env declName ⟨blocks, parts⟩ leads to panics
+
+/--
+Adds a Verso docstring to the environment.
+-/
+def addVersoDocString (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) : TermElabM Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  let (blocks, parts) ← versoDocString declName binders docComment
+  addVersoDocStringCore declName ⟨blocks, parts⟩
+
+/--
+Adds a docstring to the environment. If `isVerso` is `false`, then the docstring is interpreted as
+Markdown.
+-/
+def addDocStringOf
+    (isVerso : Bool) (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
+    TermElabM Unit := do
+  if isVerso then
+    addVersoDocString declName binders docComment
+  else
+    addMarkdownDocString declName docComment
+
+/--
+Adds a docstring to the environment.
+
+If the option `doc.verso` is `true`, the docstring is processed as a Verso docstring.
+
+Otherwise, it is considered a Markdown docstring, and documentation links are validated.
+-/
+def addDocString
+    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
+    TermElabM Unit := do
+  addDocStringOf (doc.verso.get (← getOptions)) declName binders docComment
+
+/--
+Adds a docstring to the environment, if it is provided. If no docstring is provided, nothing
+happens.
+
+If the option `doc.verso` is `true`, the docstring is processed as a Verso docstring.
+
+Otherwise, it is considered a Markdown docstring, and documentation links are validated.
 -/
 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 :=
+    (declName : Name) (binders : Syntax) (docString? : Option (TSyntax `Lean.Parser.Command.docComment)) :
+    TermElabM Unit :=
   match docString? with
-  | some docString => addDocString declName docString
+  | some docString => addDocString declName binders docString
   | none => return ()

src/Lean/DocString/Extension.lean

@@ -7,9 +7,12 @@ module
 
 prelude
 public import Lean.DeclarationRange
+public import Lean.Data.Options
 public import Lean.DocString.Links
 public import Lean.MonadEnv
 public import Init.Data.String.Extra
+public import Lean.DocString.Types
+import Lean.DocString.Markdown
 
 public section
 
@@ -20,8 +23,48 @@ public section
 
 namespace Lean
 
+
+/--
+Saved data that describes the contents. The `name` should determine both the type of the value and
+its interpretation; if in doubt, use the name of the elaborator that produces the data.
+-/
+structure ElabInline where
+  name : Name
+  val : Dynamic
+
+private instance : Doc.MarkdownInline ElabInline where
+  -- TODO extensibility
+  toMarkdown go _i content := content.forM go
+
+
+/--
+Saved data that describes the contents. The `name` should determine both the type of the value and
+its interpretation; if in doubt, use the name of the elaborator that produces the data.
+-/
+structure ElabBlock where
+  name : Name
+  value : Dynamic
+
+-- TODO extensible toMarkdown
+private instance : Doc.MarkdownBlock ElabInline ElabBlock where
+  toMarkdown _goI goB _b content := content.forM goB
+
+structure VersoDocString where
+  text : Array (Doc.Block ElabInline ElabBlock)
+  subsections : Array (Doc.Part ElabInline ElabBlock Empty)
+deriving Inhabited
+
+register_builtin_option doc.verso : Bool := {
+  defValue := false,
+  descr := "whether to use Verso syntax in docstrings"
+  group := "doc"
+}
+
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension (asyncMode := .async .asyncEnv)
+
+private builtin_initialize builtinVersoDocStrings : IO.Ref (NameMap VersoDocString) ← IO.mkRef {}
+builtin_initialize versoDocStringExt : MapDeclarationExtension VersoDocString ← mkMapDeclarationExtension (asyncMode := .async .asyncEnv)
 
 /--
 Adds a builtin docstring to the compiler.
@@ -32,28 +75,56 @@ Links to the Lean manual aren't validated.
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit := do
   builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
-def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) (docString : String) : m Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError "invalid doc string, declaration `{.ofConstName declName}` is in an imported module"
+    throwError m!"invalid doc string, declaration `{.ofConstName declName}` is in an imported module"
   modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
-def addDocStringCore' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+def addDocStringCore' [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with
   | some docString => addDocStringCore declName docString
   | none => return ()
 
 /--
 Finds a docstring without performing any alias resolution or enrichment with extra metadata.
+For Markdown docstrings, the result is a string; for Verso docstrings, it's a `VersoDocString`.
 
 Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
 -/
-def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
-  if let some docStr := docStringExt.find? env declName then
-    return some docStr
-  else if includeBuiltin then
-    return (← builtinDocStrings.get).find? declName
-  else
-    return none
+def findInternalDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option (String ⊕ VersoDocString)) := do
+  match docStringExt.find? env declName with
+  | some md => return some (.inl md)
+  | none => pure ()
+  match versoDocStringExt.find? env declName with
+  | some v => return some (.inr v)
+  | none => pure ()
+  if includeBuiltin then
+    if let some docStr := (← builtinDocStrings.get).find? declName then
+      return some (.inl docStr)
+    else if let some doc := (← builtinVersoDocStrings.get).find? declName then
+      return some (.inr doc)
+  return none
+
+/--
+Finds a docstring without performing any alias resolution or enrichment with extra metadata. The
+result is rendered as Markdown.
+
+Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
+-/
+def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
+  match (← findInternalDocString? env declName (includeBuiltin := includeBuiltin)) with
+  | some (.inl str) => return some str
+  | some (.inr verso) => return some (toMarkdown verso)
+  | none => return none
+
+where
+  toMarkdown : VersoDocString → String
+  | .mk bs ps => Doc.MarkdownM.run' do
+      for b in bs do
+        Doc.ToMarkdown.toMarkdown b
+      for p in ps do
+        Doc.ToMarkdown.toMarkdown p
+
 
 structure ModuleDoc where
   doc : String

src/Lean/DocString/Links.lean

@@ -55,6 +55,38 @@ private def domainMap : Std.HashMap String String :=
     ("errorExplanation", errorExplanationManualDomain)
   ]
 
+/-- The valid domain abbreviations in the manual. -/
+def manualDomains : List String := domainMap.keys
+
+/--
+Constructs a link to the manual.
+-/
+def manualLink (kind name : String) : Except String String :=
+  if let some domain := domainMap.get? kind then
+    return manualRoot ++ s!"find/?domain={domain}&name={name}"
+  else
+    let acceptableKinds := ", ".intercalate <| domainMap.toList.map fun (k, _) => s!"`{k}`"
+    throw s!"Unknown documentation type `{kind}`. Expected one of the following: {acceptableKinds}"
+
+private def rw (path : String) : Except String String := do
+  match path.splitOn "/" with
+  | [] | [""] =>
+    throw "Missing documentation type"
+  | kind :: args =>
+    if let some domain := domainMap.get? kind then
+      if let [s] := args then
+        if s.isEmpty then
+          throw s!"Empty {kind} ID"
+        return s!"find/?domain={domain}&name={s}"
+      else
+        throw s!"Expected one item after `{kind}`, but got {args}"
+    else
+      let acceptableKinds := ", ".intercalate <| domainMap.toList.map fun (k, _) => s!"`{k}`"
+      throw s!"Unknown documentation type `{kind}`. Expected one of the following: {acceptableKinds}"
+
+
+
+
 /--
 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.
@@ -122,23 +154,6 @@ where
   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
-    | [] | [""] =>
-      throw "Missing documentation type"
-    | kind :: args =>
-      if let some domain := domainMap.get? kind then
-        if let [s] := args then
-          if s.isEmpty then
-            throw s!"Empty {kind} ID"
-          return s!"find/?domain={domain}&name={s}"
-        else
-          throw s!"Expected one item after `{kind}`, but got {args}"
-      else
-        let acceptableKinds := ", ".intercalate <| domainMap.toList.map fun (k, _) => s!"`{k}`"
-        throw s!"Unknown documentation type `{kind}`. Expected one of the following: {acceptableKinds}"
-
-
 /--
 Rewrites Lean reference manual links in `docstring` to point at the reference manual.
 

src/Lean/DocString/Markdown.lean

@@ -0,0 +1,295 @@
+/-
+Copyright (c) 2023-2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+module
+
+prelude
+
+import Init.Data.Repr
+import Init.Data.Ord
+public import Lean.DocString.Types
+
+set_option linter.missingDocs true
+
+namespace Lean.Doc
+
+namespace MarkdownM
+
+/--
+The surrounding context of Markdown that's being generated, in order to prevent nestings that
+Markdown doesn't allow.
+-/
+public structure Context where
+  /-- The current code is inside emphasis. -/
+  inEmph : Bool := false
+  /-- The current code is inside strong emphasis. -/
+  inBold : Bool := false
+  /-- The current code is inside a link. -/
+  inLink : Bool := false
+  /-- The prefix that should be added to each line (typically for indentation). -/
+  linePrefix : String := ""
+
+/-- The state of a Markdown generation task. -/
+public structure State where
+  /-- The blocks prior to the one being generated. -/
+  priorBlocks : String := ""
+  /-- The block being generated. -/
+  currentBlock : String := ""
+  /-- Footnotes -/
+  footnotes : Array (String × String) := #[]
+
+private def combineBlocks (prior current : String) :=
+  if prior.isEmpty then current
+  else if current.isEmpty then prior
+  else if prior.endsWith "\n\n" then prior ++ current
+  else if prior.endsWith "\n" then prior ++ "\n" ++ current
+  else prior ++ "\n\n" ++ current
+
+private def State.endBlock (state : State) : State :=
+  { state with
+    priorBlocks :=
+      combineBlocks state.priorBlocks state.currentBlock ++
+      (if state.footnotes.isEmpty then ""
+       else state.footnotes.foldl (init := "\n\n") fun s (n, txt) => s ++ s!"[^{n}]:{txt}\n\n"),
+    currentBlock := "",
+    footnotes := #[]
+  }
+
+private def State.render (state : State) : String :=
+  state.endBlock.priorBlocks
+
+private def State.push (state : State) (txt : String) : State :=
+  { state with currentBlock := state.currentBlock ++ txt }
+
+end MarkdownM
+
+open MarkdownM in
+/--
+The monad for generating Markdown output.
+-/
+public abbrev MarkdownM := ReaderT Context (StateM State)
+
+/--
+Generates Markdown, rendering the result from the final state.
+-/
+public def MarkdownM.run (act : MarkdownM α) (context : Context := {}) (state : State := {}) : (α × String) :=
+  let (val, state) := act context state
+  (val, state.render)
+
+/--
+Generates Markdown, rendering the result from the final state, without producing a value.
+-/
+public def MarkdownM.run' (act : MarkdownM Unit) (context : Context := {}) (state : State := {}) : String :=
+  act.run context state |>.2
+
+private def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
+
+private def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
+
+private def MarkdownM.indent: MarkdownM α → MarkdownM α :=
+  withReader fun st => { st with linePrefix := st.linePrefix ++ "  " }
+
+/--
+A means of transforming values to Markdown representations.
+-/
+public class ToMarkdown (α : Type u) where
+  /--
+  A function that transforms an `α` into a Markdown representation.
+  -/
+  toMarkdown : α → MarkdownM Unit
+
+/--
+A way to transform inline elements extended with `i` into Markdown.
+-/
+public class MarkdownInline (i : Type u) where
+  /--
+  A function that transforms an `i` and its contents into Markdown, given a way to transform the
+  contents.
+  -/
+  toMarkdown : (Inline i → MarkdownM Unit) → i → Array (Inline i) → MarkdownM Unit
+
+public instance : MarkdownInline Empty where
+  toMarkdown := nofun
+
+/--
+A way to transform block elements extended with `b` that contain inline elements extended with `i`
+into Markdown.
+-/
+public class MarkdownBlock (i : Type u) (b : Type v) where
+  /--
+  A function that transforms a `b` and its contents into Markdown, given a way to transform the
+  contents.
+  -/
+  toMarkdown :
+    (Inline i → MarkdownM Unit) → (Block i b → MarkdownM Unit) →
+    b → Array (Block i b) → MarkdownM Unit
+
+public instance : MarkdownBlock i Empty where
+  toMarkdown := nofun
+
+private def escape (s : String) : String := Id.run do
+  let mut s' := ""
+  let mut iter := s.iter
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+    if isSpecial c then
+      s' := s'.push '\\'
+    s' := s'.push c
+  return s'
+where
+  isSpecial c := "*_`-+.!<>[]{}()#".any (· == c)
+
+private def quoteCode (str : String) : String := Id.run do
+  let mut longest := 0
+  let mut current := 0
+  let mut iter := str.iter
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+    if c == '`' then
+      current := current + 1
+    else
+      longest := max longest current
+      current := 0
+  let backticks := "".pushn '`' (max longest current + 1)
+  let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
+  backticks ++ str ++ backticks
+
+open MarkdownM in
+private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
+  | .text s =>
+    push (escape s)
+  | .linebreak s => do
+    push <| s.replace "\n" ("\n" ++ (← read).linePrefix )
+  | .emph xs => do
+    unless (← read).inEmph do
+      push "*"
+    withReader (fun ρ => { ρ with inEmph := true }) do
+      for i in xs do inlineMarkdown i
+    unless (← read).inEmph do
+      push "*"
+  | .bold xs => do
+    unless (← read).inEmph do
+      push "**"
+    withReader (fun ρ => { ρ with inEmph := true }) do
+      for i in xs do inlineMarkdown i
+    unless (← read).inEmph do
+      push "**"
+  | .concat xs =>
+    for i in xs do inlineMarkdown i
+  | .link content url => do
+    if (← read).inLink then
+      for i in content do inlineMarkdown i
+    else
+      push "["
+      for i in content do inlineMarkdown i
+      push "]("
+      push url
+      push ")"
+  | .image alt url =>
+    push s!"![{escape alt}]({url})"
+  | .footnote name content => do
+    push s!"[ˆ^{name}]"
+    let footnoteContent := (content.forM inlineMarkdown) {} {} |>.2.render
+    modify fun st => { st with footnotes := st.footnotes.push (name, footnoteContent) }
+  | .code str =>
+    push (quoteCode str)
+  | .math .display m => push s!"$${m}$$"
+  | .math .inline m => push s!"${m}$"
+  | .other container content => do
+    MarkdownInline.toMarkdown inlineMarkdown container content
+
+public instance [MarkdownInline i] : ToMarkdown (Inline i) where
+  toMarkdown inline := private inlineMarkdown inline
+
+private def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
+  let mut longest := 2
+  let mut current := 0
+  let mut iter := str.iter
+  let mut out := ""
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+    if c == '`' then
+      current := current + 1
+    else
+      longest := max longest current
+      current := 0
+    out := out.push c
+    if c == '\n' then
+      out := out.pushn ' ' indent
+  let backticks := "" |>.pushn ' ' indent |>.pushn '`' (max longest current + 1)
+  backticks ++ "\n" ++ out ++ "\n" ++ backticks ++ "\n"
+
+open MarkdownM in
+private partial def blockMarkdown [MarkdownInline i] [MarkdownBlock i b] : Block i b → MarkdownM Unit
+  | .para xs => do
+    for i in xs do
+      ToMarkdown.toMarkdown i
+    endBlock
+  | .concat bs =>
+    for b in bs do
+      blockMarkdown b
+  | .blockquote bs => do
+    withReader (fun ρ => { ρ with linePrefix := ρ.linePrefix ++ "> " })
+      for b in bs do
+        blockMarkdown b
+    endBlock
+  | .ul items => do
+    for item in items do
+      push <| (← read).linePrefix ++ "* "
+      withReader (fun ρ => { ρ with linePrefix := ρ.linePrefix ++ "  " }) do
+        for b in item.contents do
+          blockMarkdown b
+    endBlock
+  | .ol start items => do
+    let mut n := max 1 start.toNat
+    for item in items do
+      push <| (← read).linePrefix ++ s!"{n}. "
+      withReader (fun ρ => { ρ with linePrefix := ρ.linePrefix ++ "  " }) do
+        for b in item.contents do
+          blockMarkdown b
+      n := n + 1
+    endBlock
+  | .dl items => do
+    for item in items do
+      push <| (← read).linePrefix ++ "* "
+      withReader (fun ρ => { ρ with linePrefix := ρ.linePrefix ++ "  " }) do
+        inlineMarkdown (.bold item.term)
+        inlineMarkdown (.text ": " : Inline i)
+        push "\n"
+        push (← read).linePrefix
+        blockMarkdown (.concat item.desc)
+    endBlock
+  | .code str => do
+    unless (← get).currentBlock.isEmpty || (← get).currentBlock.endsWith "\n" do
+      push "\n"
+    push <| quoteCodeBlock (← read).linePrefix.length str
+    endBlock
+  | .other container content =>
+    MarkdownBlock.toMarkdown (i := i) (b := b) inlineMarkdown blockMarkdown container content
+
+
+public instance [MarkdownInline i] [MarkdownBlock i b] : ToMarkdown (Block i b) where
+  toMarkdown block := private blockMarkdown block
+
+open MarkdownM in
+open ToMarkdown in
+private partial def partMarkdown [MarkdownInline i] [MarkdownBlock i b] (level : Nat) (part : Part i b p) : MarkdownM Unit := do
+  push ("".pushn '#' (level + 1))
+  push " "
+  for i in part.title do
+    toMarkdown i
+  endBlock
+  for b in part.content do
+    toMarkdown b
+  endBlock
+  for p in part.subParts do
+    partMarkdown (level + 1) p
+
+public instance [MarkdownInline i] [MarkdownBlock i b] : ToMarkdown (Part i b p) where
+  toMarkdown part := private partMarkdown 0 part

src/Lean/DocString/Syntax.lean

@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+module
+
+prelude
+
+import Init.Prelude
+import Init.Notation
+public import Lean.Parser.Types
+import Lean.Syntax
+import Lean.Parser.Extra
+public import Lean.Parser.Term
+meta import Lean.Parser.Term
+
+
+/-!
+
+This module contains an internal syntax that's used to represent documents.
+
+Ordinarily, a syntax declaration is used to extend the Lean parser. The parser produces `Syntax`,
+which is flexible enough to represent essentially anything. However, each syntax declaration will
+produce parsed syntax trees with a predictable form, and these syntax trees can be matched using
+quasiquotation patterns. In other words, syntax declarations really do all of the following:
+
+ * They extend Lean's parser
+ * They establish expectations for valid subsets of `Syntax`
+ * They provide a way to pattern-match against the valid `Syntax` that they induce
+
+The syntax declarations in this module are used somewhat differently. They're not generally intended
+for direct use with the Lean parser, because the concrete syntax of Verso documents falls outside
+what can be implemented with Lean's parsing framework. Thus, Verso has a separate parser, written
+using the lower-level parts of Lean's parser. These syntax declarations are, however, a
+specification for the syntax trees produced by said parser. The Verso parser is in the module
+`Lean.DocString.Parser`. Specifying the Verso document syntax as is done here also allows
+quasiquotation patterns that match against the output of the Verso parser.
+
+Importantly, Lean quasiquotation patterns do not match the string contents of atoms. This means that
+the Verso parser may produce a node of kind `` `Lean.Doc.Syntax.li `` in which the first atom is
+`"1."` rather than `"*'` when parsing an ordered list.
+
+Parsed Verso documents are transformed into Lean syntax that represents Verso document ASTs (see
+module `Lean.DocString.Types`). This process potentially invokes user-written metaprograms - while
+Verso's concrete syntax is not extensible, roles, directives and code blocks all contain explicit
+hooks for extensibility. This translation step is defined in the module `Lean.DocString.Elab`.
+
+-/
+
+open Lean.Parser (rawIdent)
+
+namespace Lean.Doc.Syntax
+
+public section
+
+/-- Argument values -/
+declare_syntax_cat arg_val
+scoped syntax (name:=arg_str) str : arg_val
+scoped syntax (name:=arg_ident) ident : arg_val
+scoped syntax (name:=arg_num) num : arg_val
+
+/-- Arguments -/
+declare_syntax_cat doc_arg
+/-- Anonymous positional arguments -/
+scoped syntax (name:=anon) arg_val : doc_arg
+/-- Named arguments -/
+scoped syntax (name:=named) "(" ident " := " arg_val ")": doc_arg
+/-- Named arguments, without parentheses. -/
+scoped syntax (name:=named_no_paren) ident " := " arg_val : doc_arg
+/-- Boolean flags, turned on -/
+scoped syntax (name:=flag_on) "+" ident : doc_arg
+/-- Boolean flags, turned off -/
+scoped syntax (name:=flag_off) "-" ident : doc_arg
+
+/-- Link targets, which may be URLs or named references -/
+declare_syntax_cat link_target
+/-- A reference to a URL -/
+scoped syntax (name:=url) "(" str ")" : link_target
+/-- A named reference -/
+scoped syntax (name:=ref) "[" str "]" : link_target
+
+/--
+Verso inline objects. These are part of the ordinary text flow of a paragraph.
+
+This syntax uses the following conventions:
+ * Sequences of inline items are in square brackets
+ * Literal data, like strings or numbers, are in parentheses
+ * Verso metaprogram names and arguments are in curly braces
+-/
+declare_syntax_cat inline
+scoped syntax (name:=text) str : inline
+/-- Emphasis (often rendered as italics) -/
+scoped syntax (name:=emph) "_[" inline* "]" : inline
+/-- Bold emphasis   -/
+scoped syntax (name:=bold) "*[" inline* "]" : inline
+/-- Link -/
+scoped syntax (name:=link) "link[" inline* "]" link_target : inline
+/-- Image -/
+scoped syntax (name:=image) "image(" str ")" link_target : inline
+/-- A footnote use -/
+scoped syntax (name:=footnote) "footnote(" str ")" : inline
+/-- Line break -/
+scoped syntax (name:=linebreak) "line!" str : inline
+/-- Literal code. If the first and last characters are space, and it contains at least one non-space
+  character, then the resulting string has a single space stripped from each end.-/
+scoped syntax (name:=code) "code(" str ")" : inline
+/-- A _role_: an extension to the Verso document language in an inline position -/
+scoped syntax (name:=role) "role{" ident doc_arg* "}" "[" inline* "]"  : inline
+/-- Inline mathematical notation (equivalent to LaTeX's `$` notation) -/
+scoped syntax (name:=inline_math) "\\math" code : inline
+/-- Display-mode mathematical notation -/
+scoped syntax (name:=display_math) "\\displaymath" code : inline
+
+/--
+Block-level elements, such as paragraphs, headers, and lists.
+
+Conventions:
+ * When there's concrete syntax that can be written as Lean atoms, do so (code blocks are ` ``` `,
+   directives `:::`)
+ * When Verso's syntax requires a newline, use `|` because `"\n"` is not a valid Lean token
+ * Directive bodies are in `{` and `}` to avoid quotation parsing issues with `:::` ... `:::`
+ * If there's no concrete syntax per se, such as for paragraphs or lists, use a name with brackets
+   and braces
+ * Use parentheses around required literals, such as the starting number of an ordered list
+ * Use square brackets around sequences of literals
+ * Use curly braces around blocks or lists items (because names and arguments a la roles are always
+   newline-separated for directives and code)
+-/
+declare_syntax_cat block
+
+/-- Items from both ordered and unordered lists -/
+declare_syntax_cat list_item
+/-- List item -/
+syntax (name:=li) "*" block* : list_item
+
+/-- A description of an item -/
+declare_syntax_cat desc_item
+/-- A description of an item -/
+scoped syntax (name:=desc) ":" inline* "=>" block* : desc_item
+
+scoped syntax (name:=para) "para[" inline+ "]" : block
+/-- Unordered List -/
+scoped syntax (name:=ul) "ul{" list_item* "}" : block
+/-- Definition list -/
+scoped syntax (name:=dl) "dl{" desc_item* "}" : block
+/-- Ordered list -/
+scoped syntax (name:=ol) "ol(" num ")" "{" list_item* "}" : block
+/-- Literal code -/
+scoped syntax (name:=codeblock) "```" (ident doc_arg*)? "|" str "```" : block
+/-- Quotation -/
+scoped syntax (name:=blockquote) ">" block* : block
+/-- A link reference definition -/
+scoped syntax (name:=link_ref)  "[" str "]:" str : block
+/-- A footnote definition -/
+scoped syntax (name:=footnote_ref) "[^" str "]:" inline* : block
+/-- Custom directive -/
+scoped syntax (name:=directive) ":::" rawIdent doc_arg* "{" block:max* "}" : block
+/-- A header -/
+scoped syntax (name:=header) "header(" num ")" "{" inline+ "}" : block
+open Lean.Parser.Term in
+
+open Lean.Parser Term in
+meta def metadataContents : Parser :=
+  structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
+
+/-- Metadata for this section, defined by the current genre -/
+scoped syntax (name:=metadata_block) "%%%" metadataContents "%%%" : block
+
+/-- A block-level command -/
+scoped syntax (name:=command) "command{" rawIdent doc_arg* "}" : block

src/Lean/DocString/Types.lean

@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2023-2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+module
+
+prelude
+
+public import Init.Data.Repr
+public import Init.Data.Ord
+
+set_option linter.missingDocs true
+
+namespace Lean.Doc
+
+public section
+
+/--
+How to render mathematical content.
+-/
+inductive MathMode where
+  /-- The math content is part of the text flow. -/
+  | inline
+  /-- The math content is set apart from the text flow, with more space. -/
+  | display
+deriving Repr, BEq, Hashable, Ord
+
+/--
+Inline content that is part of the text flow.
+-/
+inductive Inline (i : Type u) : Type u where
+  /--
+  Textual content.
+  -/
+  | text (string : String)
+  /--
+  Emphasis, typically rendered using italic text.
+  -/
+  | emph (content : Array (Inline i))
+  /--
+  Strong emphasis, typically rendered using bold text.
+  -/
+  | bold (content : Array (Inline i))
+  /--
+  Inline literal code, typically rendered in a monospace font.
+  -/
+  | code (string : String)
+  /--
+  Embedded TeX math, to be rendered by an engine such as TeX or KaTeX. The `mode` determines whether
+  it is rendered in inline mode or display mode; even display-mode math is an inline element for
+  purposes of document structure.
+  -/
+  | math (mode : MathMode) (string : String)
+  /--
+  A user's line break. These are typically ignored when rendering, but don't need to be.
+  -/
+  | linebreak (string : String)
+  /--
+  A link to some URL.
+  -/
+  | link (content : Array (Inline i)) (url : String)
+  /--
+  A footnote. In Verso's concrete syntax, their contents are specified elsewhere, but elaboration
+  places the contents at the use site.
+  -/
+  | footnote (name : String) (content : Array (Inline i))
+  /--
+  An image. `alt` should be displayed if the image can't be shown.
+  -/
+  | image (alt : String) (url : String)
+  /--
+  A sequence of inline elements.
+  -/
+  | concat (content : Array (Inline i))
+  /--
+  A genre-specific inline element. `container` specifies what kind of element it is, and `content`
+  specifies the contained elements.
+  -/
+  | other (container : i) (content : Array (Inline i))
+deriving BEq, Ord, Repr, Inhabited
+
+/-- Rewrites using a proof that two inline element types are equal. -/
+def Inline.cast (inlines_eq : i = i') (x : Inline i) : Inline i' :=
+  inlines_eq ▸ x
+
+instance : Append (Inline i) where
+  append
+    | .concat #[], x => x
+    | x, .concat #[] => x
+    | .concat xs, .concat ys => .concat (xs ++ ys)
+    | .concat xs, x => .concat (xs.push x)
+    | x, .concat xs => .concat (#[x] ++ xs)
+    | x, y => .concat #[x, y]
+
+/-- No inline content. -/
+def Inline.empty : Inline i := .concat #[]
+
+/-- An item in either an ordered or unordered list. -/
+structure ListItem (α : Type u) where
+  /-- The contents of the list item. -/
+  contents : Array α
+deriving Repr, BEq, Ord, Inhabited
+
+/-- An item in a description list. -/
+structure DescItem (α : Type u) (β : Type v) where
+  /-- The term being described. -/
+  term : Array α
+  /-- The description itself. -/
+  desc : Array β
+deriving Repr, BEq, Ord, Inhabited
+
+/--
+Block-level content in a document.
+-/
+inductive Block (i : Type u) (b : Type v) : Type (max u v) where
+  /--
+  A paragraph.
+  -/
+  | para (contents : Array (Inline i))
+  /--
+  A code block.
+  -/
+  | code (content : String)
+  /--
+  An unordered list.
+  -/
+  | ul (items : Array (ListItem (Block i b)))
+  /--
+  An ordered list.
+  -/
+  | ol (start : Int) (items : Array (ListItem (Block i b)))
+  /--
+  A description list that associates explanatory text with shorter items.
+  -/
+  | dl (items : Array (DescItem (Inline i) (Block i b)))
+  /--
+  A quotation.
+  -/
+  | blockquote (items : Array (Block i b))
+  /--
+  Multiple blocks, merged.
+  -/
+  | concat (content : Array (Block i b))
+  /--
+  A genre-specific block. `container` specifies what kind of block it is, while `content` specifies
+  the content within the block.
+  -/
+  | other (container : b) (content : Array (Block i b))
+deriving BEq, Ord, Repr, Inhabited
+
+/-- An empty block with no content. -/
+def Block.empty : Block i b := .concat #[]
+
+/-- Rewrites using proofs that two inline element types and two block types are equal. -/
+def Block.cast (inlines_eq : i = i') (blocks_eq : b = b') (x : Block i b) : Block i' b' :=
+  inlines_eq ▸ blocks_eq ▸ x
+
+/--
+A logical division of a document.
+-/
+structure Part (i : Type u) (b : Type v) (p : Type w) : Type (max u v w) where
+  /-- The part's title -/
+  title : Array (Inline i)
+  /--
+  A string approximation of the part's title, for use in contexts where formatted text is invalid.
+  -/
+  titleString : String
+  /-- Genre-specific metadata -/
+  metadata : Option p
+  /-- The part's textual content -/
+  content : Array (Block i b)
+  /-- Sub-parts (e.g. subsections of a section, sections of a chapter) -/
+  subParts : Array (Part i b p)
+deriving BEq, Ord, Repr, Inhabited
+
+/-- Rewrites using proofs that inline element types, block types, and metadata types are equal. -/
+def Part.cast (inlines_eq : i = i') (blocks_eq : b = b') (metadata_eq : p = p')
+    (x : Part i b p) : Part i' b' p' :=
+  inlines_eq ▸ blocks_eq ▸ metadata_eq ▸ x

src/Lean/Elab.lean

@@ -60,5 +60,7 @@ public import Lean.Elab.Time
 public import Lean.Elab.RecommendedSpelling
 public import Lean.Elab.InfoTrees
 public import Lean.Elab.ErrorExplanation
+public import Lean.Elab.DocString
+public import Lean.Elab.DocString.Builtin
 
 public section

src/Lean/Elab/Binders.lean

@@ -14,6 +14,7 @@ public import Lean.Elab.PreDefinition.TerminationHint
 public import Lean.Elab.Match
 public import Lean.Compiler.MetaAttr
 meta import Lean.Parser.Term
+meta import Lean.Parser.Tactic
 import Lean.Linter.Basic
 
 public section

src/Lean/Elab/BuiltinCommand.lean

@@ -505,7 +505,7 @@ open Lean.Parser.Command.InternalSyntax in
       -- 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 doc
+    runTermElabM fun _ => addDocString declName (mkNullNode #[]) doc
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab

src/Lean/Elab/Command.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Range.Polymorphic.Stream
 public import Lean.Meta.Diagnostics
 public import Lean.Elab.Binders
+public import Lean.Elab.Command.Scope
 public import Lean.Elab.SyntheticMVars
 public import Lean.Elab.SetOption
 public import Lean.Language.Basic
@@ -19,75 +20,6 @@ public section
 
 namespace Lean.Elab.Command
 
-/--
-A `Scope` records the part of the `CommandElabM` state that respects scoping,
-such as the data for `universe`, `open`, and `variable` declarations, the current namespace,
-and currently enabled options.
-The `CommandElabM` state contains a stack of scopes, and only the top `Scope`
-on the stack is read from or modified. There is always at least one `Scope` on the stack,
-even outside any `section` or `namespace`, and each new pushed `Scope`
-starts as a modified copy of the previous top scope.
--/
-structure Scope where
-  /--
-  The component of the `namespace` or `section` that this scope is associated to.
-  For example, `section a.b.c` and `namespace a.b.c` each create three scopes with headers
-  named `a`, `b`, and `c`.
-  This is used for checking the `end` command. The "base scope" has `""` as its header.
-  -/
-  header        : String
-  /--
-  The current state of all set options at this point in the scope. Note that this is the
-  full current set of options and does *not* simply contain the options set
-  while this scope has been active.
-  -/
-  opts          : Options := {}
-  /-- The current namespace. The top-level namespace is represented by `Name.anonymous`. -/
-  currNamespace : Name := Name.anonymous
-  /-- All currently `open`ed namespaces and names. -/
-  openDecls     : List OpenDecl := []
-  /-- The current list of names for universe level variables to use for new declarations. This is managed by the `universe` command. -/
-  levelNames    : List Name := []
-  /--
-  The current list of binders to use for new declarations.
-  This is managed by the `variable` command.
-  Each binder is represented in `Syntax` form, and it is re-elaborated
-  within each command that uses this information.
-
-  This is also used by commands, such as `#check`, to create an initial local context,
-  even if they do not work with binders per se.
-  -/
-  varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
-  /--
-  Globally unique internal identifiers for the `varDecls`.
-  There is one identifier per variable introduced by the binders
-  (recall that a binder such as `(a b c : Ty)` can produce more than one variable),
-  and each identifier is the user-provided variable name with a macro scope.
-  This is used by `TermElabM` in `Lean.Elab.Term.Context` to help with processing macros
-  that capture these variables.
-  -/
-  varUIds       : Array Name := #[]
-  /-- `include`d section variable names (from `varUIds`) -/
-  includedVars  : List Name := []
-  /-- `omit`ted section variable names (from `varUIds`) -/
-  omittedVars  : List Name := []
-  /--
-  If true (default: false), all declarations that fail to compile
-  automatically receive the `noncomputable` modifier.
-  A scope with this flag set is created by `noncomputable section`.
-
-  Recall that a new scope inherits all values from its parent scope,
-  so all sections and namespaces nested within a `noncomputable` section also have this flag set.
-  -/
-  isNoncomputable : Bool := false
-  isPublic : Bool := false
-  /--
-  Attributes that should be applied to all matching declaration in the section. Inherited from
-  parent scopes.
-  -/
-  attrs : List (TSyntax ``Parser.Term.attrInstance) := []
-  deriving Inhabited
-
 structure State where
   env            : Environment
   messages       : MessageLog := {}

src/Lean/Elab/Command/Scope.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Data.Options
+public import Lean.Parser.Term
+
+public section
+
+namespace Lean.Elab.Command
+/--
+A `Scope` records the part of the `CommandElabM` state that respects scoping,
+such as the data for `universe`, `open`, and `variable` declarations, the current namespace,
+and currently enabled options.
+The `CommandElabM` state contains a stack of scopes, and only the top `Scope`
+on the stack is read from or modified. There is always at least one `Scope` on the stack,
+even outside any `section` or `namespace`, and each new pushed `Scope`
+starts as a modified copy of the previous top scope.
+-/
+structure Scope where
+  /--
+  The component of the `namespace` or `section` that this scope is associated to.
+  For example, `section a.b.c` and `namespace a.b.c` each create three scopes with headers
+  named `a`, `b`, and `c`.
+  This is used for checking the `end` command. The "base scope" has `""` as its header.
+  -/
+  header        : String
+  /--
+  The current state of all set options at this point in the scope. Note that this is the
+  full current set of options and does *not* simply contain the options set
+  while this scope has been active.
+  -/
+  opts          : Options := {}
+  /-- The current namespace. The top-level namespace is represented by `Name.anonymous`. -/
+  currNamespace : Name := Name.anonymous
+  /-- All currently `open`ed namespaces and names. -/
+  openDecls     : List OpenDecl := []
+  /-- The current list of names for universe level variables to use for new declarations. This is managed by the `universe` command. -/
+  levelNames    : List Name := []
+  /--
+  The current list of binders to use for new declarations.
+  This is managed by the `variable` command.
+  Each binder is represented in `Syntax` form, and it is re-elaborated
+  within each command that uses this information.
+
+  This is also used by commands, such as `#check`, to create an initial local context,
+  even if they do not work with binders per se.
+  -/
+  varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
+  /--
+  Globally unique internal identifiers for the `varDecls`.
+  There is one identifier per variable introduced by the binders
+  (recall that a binder such as `(a b c : Ty)` can produce more than one variable),
+  and each identifier is the user-provided variable name with a macro scope.
+  This is used by `TermElabM` in `Lean.Elab.Term.Context` to help with processing macros
+  that capture these variables.
+  -/
+  varUIds       : Array Name := #[]
+  /-- `include`d section variable names (from `varUIds`) -/
+  includedVars  : List Name := []
+  /-- `omit`ted section variable names (from `varUIds`) -/
+  omittedVars  : List Name := []
+  /--
+  If true (default: false), all declarations that fail to compile
+  automatically receive the `noncomputable` modifier.
+  A scope with this flag set is created by `noncomputable section`.
+
+  Recall that a new scope inherits all values from its parent scope,
+  so all sections and namespaces nested within a `noncomputable` section also have this flag set.
+  -/
+  isNoncomputable : Bool := false
+  isPublic : Bool := false
+  /--
+  Attributes that should be applied to all matching declaration in the section. Inherited from
+  parent scopes.
+  -/
+  attrs : List (TSyntax ``Parser.Term.attrInstance) := []
+  deriving Inhabited

src/Lean/Elab/DeclModifiers.lean

@@ -85,7 +85,7 @@ inductive ComputeKind where
 structure Modifiers where
   /-- Input syntax, used for adjusting declaration range (unless missing) -/
   stx             : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩
-  docString?      : Option (TSyntax ``Parser.Command.docComment) := none
+  docString?      : Option (TSyntax ``Parser.Command.docComment × Bool) := none
   visibility      : Visibility := Visibility.regular
   isProtected     : Bool := false
   computeKind     : ComputeKind := .regular
@@ -187,7 +187,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
       RecKind.partial
     else
       RecKind.nonrec
-  let docString? := docCommentStx.getOptional?.map TSyntax.mk
+  let docString? := docCommentStx.getOptional?.map (TSyntax.mk ·, doc.verso.get (← getOptions))
   let visibility ← match visibilityStx.getOptional? with
     | none   => pure .regular
     | some v =>
@@ -276,6 +276,10 @@ structure ExpandDeclIdResult where
   declName   : Name
   /-- Universe parameter names provided using the `universe` command and `.{...}` notation. -/
   levelNames : List Name
+  /-- The docstring, and whether it's Verso -/
+  docString? : Option (TSyntax ``Parser.Command.docComment × Bool)
+
+open Lean.Elab.Term (TermElabM)
 
 /--
 Given a declaration identifier (e.g., `ident (".{" ident,+ "}")?`) that may contain explicit universe parameters
@@ -287,7 +291,7 @@ The result also contains the universe parameters provided using `universe` comma
 
 This commands also stores the doc string stored in `modifiers`.
 -/
-def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) : m ExpandDeclIdResult := do
+def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) : TermElabM ExpandDeclIdResult := do
   -- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
   let (shortName, optUnivDeclStx) := expandDeclIdCore declId
   let levelNames ← if optUnivDeclStx.isNone then
@@ -303,8 +307,8 @@ def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : S
           pure (id :: levelNames))
       currLevelNames
   let (declName, shortName) ← withRef declId <| mkDeclName currNamespace modifiers shortName
-  addDocString' declName modifiers.docString?
-  return { shortName := shortName, declName := declName, levelNames := levelNames }
+  let docString? := modifiers.docString?
+  return { shortName, declName, levelNames, docString? }
 
 end Methods
 

src/Lean/Elab/Declaration.lean

@@ -109,7 +109,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let (binders, typeStx) := expandDeclSig stx[2]
   runTermElabM fun vars => do
     let scopeLevelNames ← Term.getLevelNames
-    let ⟨shortName, declName, allUserLevelNames⟩ ← Term.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
+    let ⟨shortName, declName, allUserLevelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
     addDeclarationRangesForBuiltin declName modifiers.stx stx
     Term.withAutoBoundImplicit do
     Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
@@ -136,12 +136,15 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
         trace[Elab.axiom] "{declName} : {type}"
         Term.ensureNoUnassignedMVars decl
         addDecl decl
-        withSaveInfoContext do  -- save new env
-          Term.addTermInfo' declId (← mkConstWithLevelParams declName) (isBinder := true)
+
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking
         if isExtern (← getEnv) declName then
           compileDecl decl
+        if let some (doc, isVerso) := docString? then
+          addDocStringOf isVerso declName binders doc
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
+        withSaveInfoContext do  -- save new env with docstring and decl
+          Term.addTermInfo' declId (← mkConstWithLevelParams declName) (isBinder := true)
 open Lean.Parser.Command.InternalSyntax in
 /--
 Macro that expands a declaration with a complex name into an explicit `namespace` block.

src/Lean/Elab/DefView.lean

@@ -118,6 +118,8 @@ structure DefView where
   binders       : Syntax
   type?         : Option Syntax
   value         : Syntax
+  /-- The docstring, if present, and whether it's Verso -/
+  docString?    : Option (TSyntax ``Parser.Command.docComment × Bool)
   /--
   Snapshot for incremental processing of this definition.
 
@@ -145,20 +147,22 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let modifiers       := modifiers.addAttr { name := `inline }
   let modifiers       := modifiers.addAttr { name := `reducible }
   { ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.abbrev, modifiers,
-    declId := stx[1], binders, type? := type, value := stx[3] }
+    declId := stx[1], binders, type? := type, value := stx[3], docString? := modifiers.docString? }
 
 def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
   let (binders, type) := expandOptDeclSig stx[2]
   let deriving? := if stx[4].isNone then none else some stx[4][1].getSepArgs
   { ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.def, modifiers,
-    declId := stx[1], binders, type? := type, value := stx[3], deriving? }
+    declId := stx[1], binders, type? := type, value := stx[3], deriving?,
+    docString? := modifiers.docString? }
 
 def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "theorem " >> declId >> declSig >> declVal
   let (binders, type) := expandDeclSig stx[2]
   { ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.theorem, modifiers,
-    declId := stx[1], binders, type? := some type, value := stx[3] }
+    declId := stx[1], binders, type? := some type, value := stx[3],
+    docString? := modifiers.docString? }
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
@@ -179,7 +183,8 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx[1] id (canonical := true), mkNullNode]
   return {
     ref := stx, headerRef := mkNullNode stx.getArgs[*...5], kind := DefKind.instance, modifiers := modifiers,
-    declId := declId, binders := binders, type? := type, value := stx[5]
+    declId := declId, binders := binders, type? := type, value := stx[5],
+    docString? := modifiers.docString?
   }
 
 def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
@@ -192,7 +197,8 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
       `(Parser.Command.declValSimple| := $val)
   return {
     ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.opaque, modifiers := modifiers,
-    declId := stx[1], binders := binders, type? := some type, value := val
+    declId := stx[1], binders := binders, type? := some type, value := val,
+    docString? := modifiers.docString?
   }
 
 def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
@@ -201,7 +207,8 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let id              := mkIdentFrom stx[0] `_example (canonical := true)
   let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
   { ref := stx, headerRef := mkNullNode stx.getArgs[*...2], kind := DefKind.example, modifiers := modifiers,
-    declId := declId, binders := binders, type? := type, value := stx[2] }
+    declId := declId, binders := binders, type? := type, value := stx[2],
+     docString? := modifiers.docString? }
 
 def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind

src/Lean/Elab/DocString/Builtin.lean

@@ -0,0 +1,985 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+module
+prelude
+public import Lean.Elab.DocString
+import Lean.DocString.Links
+public import Lean.DocString.Syntax
+public import Lean.Elab.InfoTree
+public import Lean.Elab.Term.TermElabM
+import Lean.Elab.Open
+public import Lean.Parser
+import Lean.Meta.Hint
+import Lean.Elab.Tactic.Doc
+import Lean.Data.EditDistance
+
+
+namespace Lean.Doc
+open Lean Elab Term
+open Lean.Parser
+open Lean.EditDistance
+open scoped Lean.Doc.Syntax
+
+set_option linter.missingDocs true
+
+public section
+
+/-- Create an identifier while directly copying info -/
+private def mkIdentFrom' (src : Syntax) (val : Name) : Ident :=
+  ⟨Syntax.ident src.getHeadInfo (toString val).toSubstring val []⟩
+
+/-- The code represents a global constant. -/
+structure Data.Const where
+  /-- The constant's name. -/
+  name : Name
+deriving TypeName
+
+/-- The code represents a local variable. -/
+structure Data.Local where
+  /-- The local variable's name. -/
+  name : Name
+  /-- The local variable's ID. -/
+  fvarId : FVarId
+  /-- The local variable's context. -/
+  lctx : LocalContext
+  /-- The local variable's type. -/
+  type : Expr
+deriving TypeName
+
+/-- The code represents a tactic. -/
+structure Data.Tactic where
+  /-- The name of the tactic's syntax kind. -/
+  name : Name
+deriving TypeName
+
+/-- The code represents a conv tactic. -/
+structure Data.ConvTactic where
+  /-- The name of the tactic's syntax kind. -/
+  name : Name
+deriving TypeName
+
+/-- The code represents an attribute application `@[...]`. -/
+structure Data.Attributes where
+  /-- The attribute syntax. -/
+  stx : Syntax
+deriving TypeName
+
+/-- The code represents a single attribute. -/
+structure Data.Attribute where
+  /-- The attribute syntax. -/
+  stx : Syntax
+deriving TypeName
+
+/-- The code represents syntax to set an option. -/
+structure Data.SetOption where
+  /-- The `set_option ...` syntax. -/
+  stx : Syntax
+deriving TypeName
+
+/-- The code represents an option. -/
+structure Data.Option where
+  /-- The option's name. -/
+  name : Name
+deriving TypeName
+
+/-- The code represents an atom drawn from some syntax. -/
+structure Data.Atom where
+  /-- The syntax kind's name. -/
+  name : Name
+  /-- The syntax category -/
+  category : Name
+deriving TypeName
+
+/-- The code represents a syntax category name. -/
+structure Data.SyntaxCat where
+  /-- The syntax category. -/
+  name : Name
+deriving TypeName
+
+/-- The code represents syntax in a given category. -/
+structure Data.Syntax where
+  /-- The syntax category. -/
+  category : Name
+  /-- The parsed syntax. -/
+  stx : Lean.Syntax
+deriving TypeName
+
+private def onlyCode (xs : TSyntaxArray `inline) : DocM StrLit := do
+  if h : xs.size = 1 then
+    match xs[0] with
+    | `(inline|code($s)) => return s
+    | other => throwErrorAt other "Expected code"
+  else
+    throwError "Expected precisely 1 code argument"
+
+/--
+Displays a name, without attempting to elaborate implicit arguments.
+-/
+--@[builtin_doc_role]
+def name (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  let x := s.getString.toName
+  let n := mkIdentFrom' s x
+  if let some (e, fields) := (← resolveLocalName n.getId) then
+    let t ← Meta.inferType e
+    if fields.isEmpty then
+      pushInfoLeaf <| .ofTermInfo {
+        elaborator := .anonymous
+        stx := n
+        lctx := ← getLCtx
+        expr := e
+        expectedType? := some t
+      }
+      let data : Data.Local := {name := x, lctx := ← getLCtx, type := t, fvarId := e.fvarId!}
+      return .other {
+        name := ``Data.Local, val := .mk data
+      } #[.code s.getString]
+  let x ← realizeGlobalConstNoOverloadWithInfo n
+  return .other (.mk ``Data.Const (.mk (Data.Const.mk x))) #[.code s.getString]
+
+private def parseStrLit (p : ParserFn) (s : StrLit) : DocM Syntax := do
+  let text ← getFileMap
+  let env ← getEnv
+  let endPos := s.raw.getTailPos? true |>.get!
+  let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos
+  let ictx :=
+    mkInputContext text.source (← getFileName)
+      (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])
+  -- TODO fallback for non-original syntax
+  let s := (mkParserState text.source).setPos (s.raw.getPos? (canonicalOnly := true)).get!
+  let s := p.run ictx { env, options := ← getOptions } (getTokenTable env) s
+
+  if !s.allErrors.isEmpty  then
+    throwError (s.toErrorMsg ictx)
+  else if ictx.atEnd s.pos then
+    pure s.stxStack.back
+  else
+    throwError ((s.mkError "end of input").toErrorMsg ictx)
+
+private def parseStrLit' (p : ParserFn) (s : StrLit) : DocM (Syntax × Bool) := do
+  let text ← getFileMap
+  let env ← getEnv
+  let endPos := s.raw.getTailPos? true |>.get!
+  let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos
+  let ictx :=
+    mkInputContext text.source (← getFileName)
+      (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])
+  -- TODO fallback for non-original syntax
+  let s := (mkParserState text.source).setPos (s.raw.getPos? (canonicalOnly := true)).get!
+  let s := p.run ictx { env, options := ← getOptions } (getTokenTable env) s
+
+  let err ←
+    if !s.allErrors.isEmpty then
+      logError (s.toErrorMsg ictx)
+      pure true
+    else if !ictx.atEnd s.pos then
+      logError ((s.mkError "end of input").toErrorMsg ictx)
+      pure true
+    else pure false
+  pure (s.stxStack.back, err)
+
+private def introduceAntiquotes (stx : Syntax) : DocM Unit :=
+  discard <| stx.rewriteBottomUpM fun stx' =>
+    match stx' with
+    | .node _ (.str k "antiquot") #[_dollar, _, name, _] => do
+      let k := if let .str k' "pseudo" := k then k' else k
+      let ty ← Meta.mkAppM ``TSyntax #[← Meta.mkListLit (.const ``SyntaxNodeKind []) [toExpr k]]
+      let lctx ← do
+        let lctx ← getLCtx
+        let fv ← mkFreshFVarId
+        let lctx := lctx.mkLocalDecl fv name.getId ty
+        addTermInfo' name (.fvar fv) (lctx? := some lctx) (isBinder := true) (expectedType? := some ty)
+        pure lctx
+      modify (fun st => { st with lctx })
+      pure stx'
+    | _ => pure stx'
+
+/--
+A reference to a tactic.
+
+In `` {tactic}`T` ``, `T` can be any of the following:
+ * The name of a tactic syntax kind (e.g. `Lean.Parser.Tactic.induction`)
+ * The first token of a tactic (e.g. `induction`)
+ * Valid tactic syntax, potentially including antiquotations (e.g. `intro $x*`)
+-/
+--@[builtin_doc_role]
+def tactic (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  withRef s do
+    let asString := s.getString
+    let asName := asString.toName
+    let allTactics ← Tactic.Doc.allTacticDocs
+    let found := allTactics.filter fun tac => tac.userName == asString || tac.internalName == asName
+    let mut exns := #[]
+    if h : found.size = 0 then
+      let (s, msg) ← AddErrorMessageContext.add s m!"Tactic `{asString}` not found"
+      exns := exns.push <| Exception.error s msg
+    else if h : found.size > 1 then
+      let found := found.map (MessageData.ofConstName ·.internalName) |>.toList
+      let (s, msg) ←
+        AddErrorMessageContext.add s m!"Tactic name `{asString}` matches {.andList found}"
+      exns := exns.push <| Exception.error s msg
+    else
+      let found := found[0]
+      addConstInfo s found.internalName
+      return .other {
+          name := ``Data.Tactic, val := .mk { name := found.internalName : Data.Tactic}
+        } #[.code s.getString]
+    try
+      let p := whitespace >> categoryParserFn `tactic
+      let stx ← parseStrLit p s
+      introduceAntiquotes stx
+      return .code s.getString
+    catch
+      | e => exns := exns.push e
+    if h : exns.size = 1 then
+      throw exns[0]
+    else
+      throwErrorWithNestedErrors m!"Couldn't resolve tactic" exns
+
+private def getConvTactic (name : StrLit) : DocM Name := do
+    let p := rawIdentFn
+    let stx ← parseStrLit p name
+    let name := stx.getId
+    let parserState := parserExtension.getState (← getEnv)
+    let some convs := parserState.categories.find? `conv
+      | throwError "Couldn't find conv tactic list"
+    let found := convs.kinds.toArray.filterMap fun ⟨x, _⟩ =>
+      if name.isSuffixOf x then some x else none
+    if h : found.size = 0 then throwError m!"Conv tactic not found: `{name}`"
+    else if h : found.size > 1 then
+      let opts := (found.map MessageData.ofConstName).toList
+      throwError m!"Multiple matching conv tactics: {.andList opts}"
+    else
+      return found[0]
+
+private def throwOrNest (msg : MessageData) (exns : Array Exception) : DocM α :=
+  if h : exns.size = 1 then
+    throw exns[0]
+  else
+    throwErrorWithNestedErrors msg exns
+
+/--
+A reference to a conv tactic.
+
+In `` {conv}`T` ``, `T` can be any of the following:
+ * The name of a conv tactic syntax kind (e.g. `Lean.Parser.Tactic.Conv.lhs`)
+ * Valid conv tactic syntax, potentially including antiquotations (e.g. `lhs`)
+-/
+--@[builtin_doc_role]
+def conv (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  withRef s do
+    let mut exns := #[]
+    try
+      let t ← getConvTactic s
+      addConstInfo s t
+      return .other {
+          name := ``Data.ConvTactic, val := .mk { name := t : Data.Tactic}
+        } #[.code s.getString]
+    catch
+      | e => exns := exns.push e
+    try
+      let p := whitespace >> categoryParserFn `conv
+      let stx ← parseStrLit p s
+      introduceAntiquotes stx
+      return .code s.getString
+    catch
+      | e => exns := exns.push e
+    throwOrNest m!"Couldn't resolve conv tactic" exns
+
+open Lean.Parser.Term in
+/--
+A reference to an attribute or attribute-application syntax.
+-/
+--@[builtin_doc_role]
+def attr (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  withRef s do
+    let mut exns := #[]
+
+    try
+      let stx ← parseStrLit attributes.fn s
+      let `(attributes|@[$_attrs,*]) := stx
+        | throwError "Not `@[attribute]` syntax"
+      return .other {name := ``Data.Attributes, val := .mk <| Data.Attributes.mk stx} #[
+        .code s.getString
+      ]
+    catch
+      | e => exns := exns.push e
+
+    try
+      let stx ← parseStrLit attrParser.fn s
+      if stx.getKind == ``Lean.Parser.Attr.simple then
+        let attrName := stx[0].getId.eraseMacroScopes
+        unless isAttribute (← getEnv) attrName do
+          let nameStr := attrName.toString
+          let threshold := max 2 (nameStr.length / 3)
+          let attrs := getAttributeNames (← getEnv) |>.toArray |>.filterMap fun x =>
+            let x := x.toString
+            levenshtein x nameStr threshold |>.map (x, ·)
+          let attrs := attrs.qsort (fun (_, i) (_, j) => i < j) |>.map (·.1)
+          let hint ←
+            if attrs.isEmpty then pure m!""
+            else m!"Use a known attribute:".hint attrs (ref? := s)
+          logErrorAt stx m!"Unknown attribute `{attrName}`{hint}"
+
+      return .other {name := ``Data.Attribute, val := .mk <| Data.Attribute.mk stx} #[
+        .code s.getString
+      ]
+    catch
+      | e => exns := exns.push e
+
+    throwOrNest m!"Couldn't parse attributes" exns
+
+private def optionNameAndVal (stx : Syntax) : DocM (Ident × DataValue) := do
+  let id := stx[1]
+  let val := stx[3]
+
+  let val ←
+    if let some s := val.isStrLit? then pure <| .ofString s
+    else if let some n := val.isNatLit? then pure <| .ofNat n
+    else if val matches .atom _ "true" then pure <| .ofBool true
+    else if val matches .atom _ "false" then pure <| .ofBool false
+    else throwErrorAt val m!"Invalid option value. Expected a string, a number, `true`, or `false`,\
+      but got {val}."
+  return (⟨id⟩, val)
+
+open Lean.Parser.Command («set_option») in
+/--
+A reference to an option.
+
+In `` {option}`O` ``, `O` can be either:
+ * The name of an option (e.g. `pp.all`)
+ * Syntax to set an option to a particular value (e.g. `set_option pp.all true`)
+-/
+--@[builtin_doc_role]
+def option (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  withRef s do
+    let spec : Syntax ⊕ Syntax ←
+      try
+        let stx ← parseStrLit «set_option».fn s
+        pure (Sum.inl stx)
+      catch
+      | e1 =>
+        try
+          -- Here it's important to get the partial syntax in order to add completion info,
+          -- but then abort processing.
+          let (stx, err) ← parseStrLit' (nodeFn nullKind identWithPartialTrailingDot.fn) s
+          addCompletionInfo <| CompletionInfo.option stx[0]
+          if err then throw e1 else pure (Sum.inr stx[0])
+        catch
+        | e2 =>
+          throwOrNest m!"Expected an option name or a valid `set_option`" #[e1, e2]
+    match spec with
+    | .inl stx =>
+      let (id, val) ← optionNameAndVal stx
+      -- For completion purposes, we discard `val` and any later arguments. We include the first
+      -- argument (the keyword) for position information in case `id` is `missing`.
+      addCompletionInfo <| CompletionInfo.option (stx.setArgs (stx.getArgs[*...3]))
+      let optionName := id.getId.eraseMacroScopes
+      try
+        let decl ← getOptionDecl optionName
+        pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
+        validateOptionValue optionName decl val
+
+        return .other {name := ``Data.SetOption, val := .mk <| Data.SetOption.mk stx} #[
+          .code s.getString
+        ]
+      catch
+        | e =>
+          let ref := e.getRef
+          let ref ← if ref.isMissing then getRef else pure ref
+          logErrorAt ref e.toMessageData
+          return .code s.getString
+    | .inr stx =>
+      let optionName := stx.getId.eraseMacroScopes
+      try
+        let decl ← getOptionDecl optionName
+        pushInfoLeaf <| .ofOptionInfo { stx, optionName, declName := decl.declName }
+
+        return .other {name := ``Data.Option, val := .mk <| Data.Option.mk optionName} #[
+          .code s.getString
+        ]
+      catch
+        | e =>
+          let ref := e.getRef
+          let ref ← if ref.isMissing then getRef else pure ref
+          logErrorAt ref e.toMessageData
+          return .code s.getString
+
+/--
+Checks whether a syntax descriptor's value contains the given atom.
+-/
+private partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
+  let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM Bool := do
+    match p.getAppFnArgs with
+    | (``ParserDescr.node, #[_, _, p]) => containsAtom p atom
+    | (``ParserDescr.trailingNode, #[_, _, _, p]) => containsAtom p atom
+    | (``ParserDescr.unary, #[.app _ (.lit (.strVal _)), p]) => containsAtom p atom
+    | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => containsAtom p atom
+    | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (tk.trim == atom)
+    | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (tk.trim == atom)
+    | (``Parser.withAntiquot, #[_, p]) => containsAtom p atom
+    | (``Parser.leadingNode, #[_, _, p]) => containsAtom p atom
+    | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
+      containsAtom p1 atom <||> containsAtom p2 atom
+    | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (tk.trim == atom)
+    | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (tk.trim == atom)
+    | (``Parser.symbol, #[_nonlit]) => pure false
+    | (``Parser.withCache, #[_, p]) => containsAtom p atom
+    | _ => if tryWhnf then attempt (← Meta.whnf p) false else pure false
+  attempt e true
+
+
+private def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
+  let env ← getEnv
+  let some catContents := (Lean.Parser.parserExtension.getState env).categories.find? cat
+    | return #[]
+  let kinds := catContents.kinds
+  let mut found := #[]
+  for (k, _) in kinds do
+    if let some d := env.find? k |>.bind (·.value?) then
+      if (← containsAtom d atom) then
+        found := found.push k
+  return found
+
+private def kwImpl (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
+    (suggest : Bool)
+    (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  let atom := s.getString
+  let env ← getEnv
+  let parsers := Lean.Parser.parserExtension.getState env
+  let cat' := cat.getId
+  let of' ← do
+    let x := of.getId
+    if x.isAnonymous then pure x else realizeGlobalConstNoOverloadWithInfo of
+  let cats ←
+    if cat'.isAnonymous then
+      pure parsers.categories.toArray
+    else
+      if let some catImpl := parsers.categories.find? cat' then
+        pure #[(cat', catImpl)]
+      else throwError m!"Syntax category `{cat'}` not found"
+
+  let mut candidates := #[]
+  for (catName, category) in cats do
+    if !of'.isAnonymous then
+      if category.kinds.contains of' then
+        if let some d := env.find? of' |>.bind (·.value?) then
+          if (← containsAtom d atom) then
+            candidates := candidates.push (catName, of')
+    else
+      let which ← withAtom catName atom
+      candidates := candidates ++ (which.map (catName, ·))
+
+  if h : candidates.size = 0 then
+    logErrorAt s m!"No syntax found with atom `{atom}`"
+    return .code atom
+  else if h : candidates.size > 1 then
+    let choices := .andList (candidates.map (fun (c, k) => m!"{.ofConstName k} : {c}")).toList
+    let catSuggs := categorySuggestions cat' candidates
+    let ofSuggs ← ofSuggestions of' candidates
+    let hintText :=
+      if catSuggs.isEmpty then
+        if ofSuggs.isEmpty then m!""
+        else m!"Specify the syntax kind:"
+      else
+        if ofSuggs.isEmpty then m!"Specify the category:"
+        else m!"Specify the category or syntax kind:"
+
+    let range? :=
+      match ← getRef with
+      | `(inline|role{$name $args*}[$_]) =>
+        (mkNullNode (#[name] ++ args)).getRange?
+      | _ => none
+
+    let hint ← makeHint hintText (ofSuggs ++ catSuggs)
+
+    logErrorAt s m!"Multiple syntax entries found with atom `{atom}`: {choices}{hint.getD m!""}"
+    return .code atom
+  else
+    let (catName, k) := candidates[0]
+    addConstInfo s k
+    if of'.isAnonymous && suggest then
+      let k' ← unresolveNameGlobalAvoidingLocals k
+      if let some h ← makeHint m!"Specify the syntax kind:" #[s!" (of := {k'})"] then
+        logInfo h
+
+    return .other {name := ``Data.Atom, val := .mk (Data.Atom.mk k catName)} #[.code atom]
+where
+  categorySuggestions (c candidates) := Id.run do
+    if c.isAnonymous then
+      let mut counts : NameMap Nat := {}
+      for (cat, _) in candidates do
+        counts := counts.alter cat (some <| 1 + ·.getD 0)
+      counts := counts.filter fun _ n => n == 1
+      let sorted := counts.keys.toArray.qsort (fun x y => x.toString < y.toString)
+      return sorted.map (s!" (cat := {·})")
+    else return #[]
+  ofSuggestions (o candidates) : DocM (Array String):= do
+    if o.isAnonymous then
+      let sorted := candidates |>.map (·.2) |>.qsort (fun x y => x.toString < y.toString)
+      sorted.mapM fun k => do
+        let k ← unresolveNameGlobalAvoidingLocals k
+        pure s!" (of := {k})"
+    else return #[]
+  makeHint (hintText) (suggestions : Array String) : DocM (Option MessageData) := do
+    let range? :=
+      match ← getRef with
+      | `(inline|role{$name $args*}[$_]) =>
+        (mkNullNode (#[name] ++ args)).getRange?
+      | _ => none
+    if let some ⟨b, e⟩ := range? then
+      let str := (← getFileMap).source.extract b e
+      let str := if str.startsWith "kw?" then "kw" ++ str.drop 3 else str
+      let stx := Syntax.mkStrLit str (info := .synthetic b e (canonical := true))
+      let suggs := suggestions.map (fun (s : String) => {suggestion := str ++ s})
+      some <$> MessageData.hint hintText suggs (ref? := some stx)
+    else pure none
+
+/--
+A reference to a particular syntax kind, via one of its atoms.
+
+It is an error if the syntax kind can't be automatically determined to contain the atom, or if
+multiple syntax kinds contain it. If the parser for the syntax kind is sufficiently complex,
+detection may fail.
+
+Specifying the category or kind using the named arguments `cat` and `of` can narrow down the
+process.
+
+Use `kw?` to receive a suggestion of a specific kind.
+-/
+--@[builtin_doc_role]
+def kw (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
+    (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) :=
+  kwImpl (cat := cat) (of := of) false xs
+
+@[inherit_doc kw /-, builtin_doc_role -/]
+def kw? (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
+    (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) :=
+  kwImpl (cat := cat) (of := of) true xs
+
+private def validateCat (x : Ident) : DocM Bool := do
+  let c := x.getId
+  let parsers := parserExtension.getState (← getEnv)
+  if parsers.categories.contains c then
+    return true
+  else
+    let allCats := parsers.categories.toArray.map (toString ·.1) |>.qsort
+    let allCats := allCats.map (fun c => { suggestion := c })
+    let h ← MessageData.hint m!"Use a syntax category name:" allCats (ref? := x)
+    logErrorAt x m!"Unknown syntax category `{c}`{h}"
+    return false
+
+/--
+A reference to a syntax category.
+-/
+--@[builtin_doc_role]
+def syntaxCat (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  let x ← parseStrLit rawIdentFn s
+  let c := x.getId
+  if (← validateCat ⟨x⟩) then
+    return .other {name := ``Data.SyntaxCat, val := .mk (Data.SyntaxCat.mk c)} #[.code (toString c)]
+  else
+    return .code (toString c)
+
+/--
+A description of syntax in the provided category.
+-/
+--@[builtin_doc_role]
+def «syntax» (cat : Ident) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  if (← validateCat cat) then
+    let cat := cat.getId
+    let stx ← parseStrLit (categoryParserFn cat) s
+    introduceAntiquotes stx
+    return .other {name := ``Data.Syntax, val := .mk (Data.Syntax.mk cat stx)} #[.code s.getString]
+  else
+    return .code s.getString
+
+/--
+A metavariable to be discussed in the remainder of the docstring.
+
+There are two syntaxes that can be used:
+ * `` {given}`x` `` establishes `x`'s type as a metavariable.
+ * `` {given}`x : A`` uses `A` as the type for metavariable `x`.
+-/
+--@[builtin_doc_role]
+def given (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  let p : ParserFn := whitespace >> nodeFn nullKind (identFn >> optionalFn (symbolFn ":" >> termParser.fn))
+  let stx ← parseStrLit p s
+  let x := stx[0]
+  let ty := stx[1][1]
+  let ty' ←
+    if !ty.isMissing then elabType ty
+    else
+      withoutErrToSorry <| Meta.mkFreshExprMVar none
+  let lctx ← do
+    let lctx ← getLCtx
+    let fv ← mkFreshFVarId
+    let lctx := lctx.mkLocalDecl fv x.getId ty'
+    addTermInfo' x (.fvar fv) (lctx? := some lctx) (isBinder := true) (expectedType? := some ty')
+    pure lctx
+  modify (fun st => { st with lctx })
+  pure .empty
+
+private def firstToken? (stx : Syntax) : Option Syntax :=
+  stx.find? fun
+    | .ident info .. => usable info
+    | .atom info .. => usable info
+    | _ => false
+where
+  usable
+    | .original .. => true
+    | _ => false
+
+private builtin_initialize
+  leanOutputExt : EnvExtension (NameMap (Array (MessageSeverity × String))) ←
+    registerEnvExtension (asyncMode := .local) (pure {})
+
+/--
+Elaborates a sequence of Lean commands as examples.
+
+To make examples self-contained, elaboration ignores the surrouncing section scopes. Modifications
+to the environment are preserved during a single documentation comment, and discarded afterwards.
+
+The named argument `name` allows a name to be assigned to the code block; any messages created by
+elaboration are saved under this name.
+
+The flags `error` and `warning` indicate that an error or warning is expected in the code.
+-/
+--@[builtin_doc_code_block]
+def lean (name : Option Ident := none) (error warning : flag false) (code : StrLit) : DocM (Block ElabInline ElabBlock) := do
+  let text ← getFileMap
+  let env ← getEnv
+  let p := andthenFn whitespace (categoryParserFnImpl `command)
+  -- TODO fallback for non-original syntax
+  let pos := code.raw.getPos? true |>.get!
+  let endPos := code.raw.getTailPos? true |>.get!
+  let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos
+  let ictx :=
+    mkInputContext text.source (← getFileName)
+      (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])
+  let cctx : Command.Context := {fileName := ← getFileName, fileMap := text, snap? := none, cancelTk? := none}
+  let scopes := (← get).scopes
+  let mut cmdState : Command.State := { env, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes }
+  let mut pstate : Parser.ModuleParserState := {pos := pos, recovering := false}
+  let mut cmds := #[]
+  repeat
+    let scope := cmdState.scopes.head!
+    let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
+    let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages
+    cmds := cmds.push cmd
+    pstate := ps'
+    cmdState := { cmdState with messages := messages }
+    cmdState ← runCommand (Command.elabCommand cmd) cmd cctx cmdState
+    if Parser.isTerminalCommand cmd then break
+  setEnv cmdState.env
+  modify fun st => { st with scopes := cmdState.scopes }
+  for t in cmdState.infoState.trees do
+    pushInfoTree t
+  -- TODO Nice highlighted code
+  let mut output := #[]
+  for msg in cmdState.messages.toArray do
+    let b := text.ofPosition msg.pos
+    let e := msg.endPos |>.map text.ofPosition |>.getD (text.source.next b)
+    let msgStr := text.source.extract b e
+    let msgStx := Syntax.mkStrLit msgStr (info := .synthetic b e (canonical := true))
+    unless msg.isSilent do
+      if name.isSome then output := output.push (msg.severity, ← msg.data.toString)
+      if msg.severity == .error && !error then
+        let hint ← flagHint m!"The `+error` flag indicates that errors are expected:" #[" +error"]
+        logErrorAt msgStx m!"Unexpected error:{indentD msg.data}{hint.getD m!""}"
+      if msg.severity == .warning && !warning then
+        let hint ← flagHint m!"The `+error` flag indicates that warnings are expected:" #[" +warning"]
+        logErrorAt msgStx m!"Unexpected warning:{indentD msg.data}{hint.getD m!""}"
+      else
+        withRef msgStx <| log msg.data (severity := .information) (isSilent := true)
+    if let some x := name then
+      modifyEnv (leanOutputExt.modifyState · (·.insert x.getId output))
+  pure (Block.code (toString (mkNullNode cmds)))
+where
+  runCommand (act : Command.CommandElabM Unit) (stx : Syntax)
+      (cctx : Command.Context) (cmdState : Command.State) :
+      DocM Command.State := do
+    let (output, cmdState) ←
+      match (← liftM <| IO.FS.withIsolatedStreams <| EIO.toIO' <| (act.run cctx).run cmdState) with
+      | (output, .error e) => Lean.logError e.toMessageData; pure (output, cmdState)
+      | (output, .ok ((), cmdState)) => pure (output, cmdState)
+
+    if output.trim.isEmpty then return cmdState
+
+    let log : MessageData → Command.CommandElabM Unit :=
+      if let some tok := firstToken? stx then logInfoAt tok
+      else logInfo
+
+    match (← liftM <| EIO.toIO' <| ((log output).run cctx).run cmdState) with
+    | .error _ => pure cmdState
+    | .ok ((), cmdState) => pure cmdState
+
+  flagHint (hintText) (suggestions : Array String) : DocM (Option MessageData) := do
+    let range? :=
+      match ← getRef with
+      | `(block|```$name $args* | $s ```) =>
+        (mkNullNode (#[name] ++ args)).getRange?
+      | `(inline|role{$name $args*}[$_]) =>
+        (mkNullNode (#[name] ++ args)).getRange?
+      | _ => none
+    if let some ⟨b, e⟩ := range? then
+      let str := (← getFileMap).source.extract b e
+      let str := if str.startsWith "kw?" then "kw" ++ str.drop 3 else str
+      let stx := Syntax.mkStrLit str (info := .synthetic b e (canonical := true))
+      let suggs := suggestions.map (fun (s : String) => {suggestion := str ++ s})
+      some <$> MessageData.hint hintText suggs (ref? := some stx)
+    else pure none
+
+/--
+Displays output from a named Lean code block.
+-/
+--@[builtin_doc_code_block]
+def output (name : Ident) (severity : Option (WithSyntax MessageSeverity) := none) (code : StrLit) : DocM (Block ElabInline ElabBlock) := do
+  let allOut := leanOutputExt.getState (← getEnv)
+  let some outs := allOut.find? name.getId
+    | let possible := allOut.keysArray.map ({suggestion := ·.toString})
+      let h ← MessageData.hint m!"Use one of the named blocks:" possible
+      logErrorAt name m!"Output from block `{name.getId}` not found{h}"
+      return .code code.getString
+  let codeStr := code.getString
+  for (sev, out) in outs do
+    if out.trim == codeStr.trim then
+      if let some s := severity then
+        if s.val != sev then
+          let sevName :=
+            match sev with
+            | .error => ``MessageSeverity.error
+            | .warning => ``MessageSeverity.warning
+            | .information => ``MessageSeverity.information
+          let sevName ← unresolveNameGlobalAvoidingLocals sevName
+          let h ← MessageData.hint m!"Update severity:" #[{suggestion := sevName.toString}] (ref? := some s.stx)
+          logErrorAt s.stx m!"Mismatched severity. Message has severity `{sev}`.{h}"
+      return .code codeStr
+  let outs := sortByDistance codeStr outs
+  let h ← m!"Use one of the outputs:".hint (outs.map (withNl ·.2)) (ref? := code)
+  logErrorAt code m!"Output not found.{h}"
+  return .code codeStr
+where
+  withNl (s : String) :=
+    if s.endsWith "\n" then s else s ++ "\n"
+
+  sortByDistance {α} (target : String) (strings : Array (α × String)) : Array (α × String) :=
+    let withDistance := strings.map fun (x, s) =>
+      let d := levenshtein target s target.length
+      (x, s, d.getD target.length)
+    withDistance.qsort (fun (_, _, d1) (_, _, d2) => d1 < d2) |>.map fun (x, s, _) => (x, s)
+
+
+/--
+Treats the provided term as Lean syntax in the documentation's scope.
+-/
+--@[builtin_doc_role lean]
+def leanTerm (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  let p : ParserFn := whitespace >> termParser.fn
+  let stx ← parseStrLit p s
+  discard <| withoutErrToSorry <| elabTerm stx none
+  pure (.code s.getString)
+
+/--
+Opens a namespace in the remainder of the documentation comment.
+
+The `+scoped` flag causes scoped instances and attributes to be activated, but no identifiers are
+brought into scope. The named argument `only`, which can be repeated, specifies a subset of names to
+bring into scope from the namespace.
+-/
+--@[builtin_doc_command]
+def «open» (n : Ident) («scoped» : flag false) («only» : many Ident) : DocM (Block ElabInline ElabBlock) := do
+  let nss ← resolveNamespace n
+  if only.isEmpty then
+    for ns in nss do
+      unless «scoped» do
+        let d := .simple ns []
+        modify fun st => { st with openDecls := d :: st.openDecls }
+      activateScoped ns
+  else
+    if «scoped» then
+      throwError "`scoped` and `only` cannot be used together"
+    for idStx in only do
+      let declName ← OpenDecl.resolveNameUsingNamespacesCore nss idStx
+      let d := .explicit idStx.getId declName
+      modify fun st => { st with openDecls := d :: st.openDecls }
+      if (← getInfoState).enabled then
+        addConstInfo idStx declName
+  return .empty
+
+/--
+Sets the specified option to the specified value for the remainder of the comment.
+-/
+--@[builtin_doc_command]
+def «set_option» (option : Ident) (value : DataValue) : DocM (Block ElabInline ElabBlock) := do
+  addCompletionInfo <| CompletionInfo.option option
+  let optionName := option.getId
+  let decl ← withRef option <| getOptionDecl optionName
+  pushInfoLeaf <| .ofOptionInfo { stx := option, optionName, declName := decl.declName }
+  validateOptionValue optionName decl value
+  let o ← getOptions
+  modify fun s => { s with options := o.insert optionName value }
+  return .empty
+
+/--
+Constructs a link to the Lean langauge reference. Two positional arguments are expected:
+ * `domain` should be one of the valid domains, such as `section`.
+ * `name` should be the content's canonical name in the domain.
+-/
+--@[builtin_doc_role]
+def manual (domain : Ident) (name : String) (content : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let domStr := domain.getId.toString
+  if domStr ∉ manualDomains then
+    let h ← MessageData.hint "Use one of the valid documentation domains:"
+      (manualDomains.map ({ suggestion := · })).toArray
+      (ref? := some domain)
+    throwErrorAt domain m!"Invalid documentation domain.{h}"
+  match manualLink domStr name with
+  | .ok url => return .link (← content.mapM elabInline) url
+  | .error e => throwError e
+
+/--
+Suggests the `name` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestName (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let stx ← parseStrLit identFn code
+  try
+    discard <| realizeGlobalConstNoOverload stx
+    return #[.mk ``name none none]
+  catch
+    | _ =>
+    if let some (_, []) := (← resolveLocalName stx.getId) then
+      return #[.mk ``name none none]
+  return #[]
+
+/--
+Suggests the `lean` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestLean (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let p : ParserFn := whitespace >> termParser.fn
+  try
+    let stx ← parseStrLit p code
+    discard <| withoutErrToSorry <| elabTerm stx none
+    return #[.mk ``lean none none]
+  catch | _ => return #[]
+
+/--
+Suggests the `tactic` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestTactic (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let asString := code.getString
+  let asName := asString.toName
+  let allTactics ← Tactic.Doc.allTacticDocs
+  let found := allTactics.filter fun tac => tac.userName == asString || tac.internalName == asName
+  if found.size = 1 then return #[.mk ``tactic none none]
+  else
+    let p := whitespace >> categoryParserFn `tactic
+    try
+      discard <| parseStrLit p code
+      return #[.mk ``tactic none none]
+    catch | _ => return #[]
+
+open Lean.Parser.Term in
+/--
+Suggests the `attr` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestAttr (code : StrLit) : DocM (Array CodeSuggestion) := do
+  try
+    let stx ← parseStrLit attributes.fn code
+    let `(attributes|@[$_attrs,*]) := stx
+      | return #[]
+    return #[.mk ``attr none none]
+  catch
+    | _ => pure ()
+  try
+    discard <| parseStrLit attrParser.fn code
+    return #[.mk ``attr none none]
+  catch
+    | _ => pure ()
+  return #[]
+
+open Lean.Parser.Command in
+/--
+Suggests the `option` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestOption (code : StrLit) : DocM (Array CodeSuggestion) := do
+  try
+    discard <| parseStrLit Command.«set_option».fn code
+    return #[CodeSuggestion.mk ``option none none]
+  catch
+  | _ =>
+    try
+      let stx ← parseStrLit rawIdentFn code
+      let name := stx.getId.eraseMacroScopes
+      discard <| getOptionDecl name
+      return #[CodeSuggestion.mk ``option none none]
+    catch
+    | _ =>
+      return #[]
+
+/--
+Suggests the `kw` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestKw (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let atom := code.getString
+  let env ← getEnv
+  let parsers := Lean.Parser.parserExtension.getState env
+  let cats := parsers.categories.toArray
+
+  let mut candidates := #[]
+  for (catName, _) in cats do
+    let which ← withAtom catName atom
+    candidates := candidates ++ (which.map (catName, ·))
+
+  candidates.mapM fun (cat, of) => do
+    return .mk ``kw (some s!"(of := {of})") (some s!"(in `{cat}`)")
+
+/--
+Suggests the `syntaxCat` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestCat (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let env ← getEnv
+  let parsers := Lean.Parser.parserExtension.getState env
+  if parsers.categories.contains code.getString.toName then
+    return #[.mk ``syntaxCat none none]
+  else
+    return #[]
+
+/--
+Suggests the `syntax` role, if applicable.
+-/
+--@[builtin_doc_code_suggestions]
+def suggestSyntax (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let env ← getEnv
+  let parsers := Lean.Parser.parserExtension.getState env
+  let cats := parsers.categories.toArray
+
+  let mut candidates := #[]
+  for (catName, _) in cats do
+    try
+      discard <| parseStrLit (whitespace >> (categoryParser catName 0).fn) code
+      candidates := candidates.push catName
+    catch | _ => pure ()
+
+  candidates.mapM fun cat => do
+    return .mk ``«syntax» (some s!"{cat}") none

src/Lean/Elab/ErrorExplanation.lean

@@ -118,7 +118,7 @@ open Command in
     throwErrorAt id m!"Invalid name `{name}`: Error explanation names must have two components"
       ++ .note m!"The first component of an error explanation name identifies the package from \
         which the error originates, and the second identifies the error itself."
-  validateDocComment docStx
+  runTermElabM fun _ => validateDocComment docStx
   let doc ← getDocStringText docStx
   if errorExplanationExt.getState (← getEnv) |>.contains name then
     throwErrorAt id m!"Cannot add explanation: An error explanation already exists for `{name}`"

src/Lean/Elab/Inductive.lean

@@ -28,7 +28,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
   let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
-  let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
+  let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
   addDeclarationRangesForBuiltin declName modifiers.stx decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     /-
@@ -41,7 +41,8 @@ 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? := some ⟨leadingDocComment⟩ }
+      ctorModifiers := { ctorModifiers with
+        docString? := some (⟨leadingDocComment⟩, doc.verso.get (← getOptions)) }
     if ctorModifiers.isPrivate && modifiers.isPrivate then
       let hint ← do
         let .original .. := modifiersStx.getHeadInfo | pure .nil
@@ -63,7 +64,6 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
     let ctorName := declName ++ ctorName
     let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
     let (binders, type?) := expandOptDeclSig ctor[4]
-    addDocString' ctorName ctorModifiers.docString?
     addDeclarationRangesFromSyntax ctorName ctor ctor[3]
     if modifiers.isMeta then
       modifyEnv (addMeta · ctorName)
@@ -84,6 +84,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
     declId, modifiers, isClass, declName, levelNames
     binders, type?, ctors
     computedFields
+    docString?
   }
 
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do

src/Lean/Elab/InfoTree/Main.lean

@@ -273,6 +273,11 @@ def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo
   | some ctx, ofTacticInfo i => some { ctx with mctx := i.mctxAfter }
   | ctx?, _ => ctx?
 
+def PartialContextInfo.format (ctx : PartialContextInfo) : Format :=
+  match ctx with
+  | .commandCtx _ => "command"
+  | .parentDeclCtx n => s!"parent[{n}]"
+
 partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do
   match tree with
   | hole id     => return .nestD f!"• ?{toString id.name}"

src/Lean/Elab/InheritDoc.lean

@@ -6,10 +6,9 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import Lean.Elab.InfoTree.Main
-public import Lean.DocString.Extension
-
-public section
+import Lean.Elab.InfoTree.Main
+import Lean.DocString.Extension
+import Lean.DocString.Add
 
 namespace Lean
 
@@ -19,7 +18,7 @@ Uses documentation from a specified declaration.
 `@[inherit_doc decl]` is used to inherit the documentation from the declaration `decl`.
 -/
 @[builtin_doc]
-builtin_initialize
+public builtin_initialize
   registerBuiltinAttribute {
     name := `inherit_doc
     descr := "inherit documentation from a specified declaration"
@@ -33,9 +32,14 @@ builtin_initialize
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
         if (← findSimpleDocString? (← getEnv) decl (includeBuiltin := false)).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
-        let some doc ← findSimpleDocString? (← getEnv) declName
+        let some doc ← findInternalDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
-        -- This docstring comes from the environment, so documentation links have already been validated
-        addDocStringCore decl doc
+        match doc with
+        | .inl md =>
+          -- This docstring comes from the environment, so documentation links have already been validated
+          addDocStringCore decl md
+        | .inr verso =>
+          addVersoDocStringCore decl verso
       | _  => throwError "Invalid `[inherit_doc]` attribute syntax"
+    applicationTime := AttributeApplicationTime.afterCompilation
   }

src/Lean/Elab/LetRec.lean

@@ -54,11 +54,12 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       if decls.any fun decl => decl.declName == declName then
         withRef declId do
           throwError "`{.ofConstName declName}` has already been declared"
+      let binders := decl[1]
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
-      addDocString' declName docStr?
+      addDocString' declName binders docStr?
       addDeclarationRangesFromSyntax declName decl declId
-      let binders := decl[1].getArgs
+      let binders := binders.getArgs
       let typeStx := expandOptType declId decl[2]
       let (type, binderIds) ← elabBindersEx binders fun xs => do
           let type ← elabType typeStx

src/Lean/Elab/MutualDef.lean

@@ -206,7 +206,7 @@ private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandD
     -- Can we reuse the result for a body? For starters, all headers (even those below the body)
     -- must be reusable
     let mut reuseBody := views.all (·.headerSnap?.any (·.old?.isSome))
-    for view in views, ⟨shortDeclName, declName, levelNames⟩ in expandedDeclIds,
+    for view in views, ⟨shortDeclName, declName, levelNames, docString?⟩ in expandedDeclIds,
         tacPromise in tacPromises, bodyPromise in bodyPromises do
       let mut reusableResult? := none
       let mut oldBodySnap? := none
@@ -1048,6 +1048,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
       ref         := getDeclarationSelectionRef header.ref
       kind        := header.kind
       declName    := header.declName
+      binders     := header.binders
       levelParams := [], -- we set it later
       modifiers   := header.modifiers
       type, value, termination
@@ -1071,6 +1072,7 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
       ref         := c.ref
       declName    := c.toLift.declName
       levelParams := [] -- we set it later
+      binders     := mkNullNode -- No docstrings, so we don't need these
       modifiers   := { modifiers with attrs := c.toLift.attrs }
       kind, type, value,
       termination := c.toLift.termination
@@ -1297,8 +1299,6 @@ where
        headers.any (·.modifiers.attrs.any (·.name == `expose)))) do
     let headers := headers.map fun header =>
       { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
-    for view in views, funFVar in funFVars do
-      addLocalVarInfo view.declId funFVar
     let values ← try
       let values ← elabFunValues headers vars sc
       Term.synthesizeSyntheticMVarsNoPostponing
@@ -1323,6 +1323,9 @@ where
       let whereFinally ← declValToWhereFinally header.value
       let exprsWithHoles := (exprsWithHoles.getD header.declName #[]).push { ref := header.ref, expr := value }
       fillHolesFromWhereFinally header.declName exprsWithHoles whereFinally
+    -- Compilation should take place without unused section vars, but all section vars should be
+    -- present when elaborating documentation.
+    let docCtx := (← getLCtx, ← getLocalInstances)
     (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then
        -- do not repeat checks already done in `elabFunValues`
        withHeaderSecVars (check := false) vars sc headers
@@ -1343,7 +1346,10 @@ where
       let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
       for preDef in preDefs do
         trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
-      addPreDefinitions preDefs
+      addPreDefinitions docCtx preDefs
+    for view in views, funFVar in funFVars do
+      addLocalVarInfo view.declId funFVar
+
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
       if let some classStxs := view.deriving? then

src/Lean/Elab/MutualInductive.lean

@@ -19,7 +19,9 @@ public import Lean.Elab.DefView
 public import Lean.Elab.DeclUtil
 public import Lean.Elab.Deriving.Basic
 public import Lean.Elab.DeclarationRange
+public import Lean.Parser.Command
 import Lean.Elab.ComputedFields
+import Lean.DocString.Extension
 import Lean.Meta.Constructions.CtorIdx
 import Lean.Meta.Constructions.CtorElim
 import Lean.Meta.IndPredBelow
@@ -110,6 +112,8 @@ structure InductiveView where
   ctors           : Array CtorView
   computedFields  : Array ComputedFieldView
   derivingClasses : Array DerivingClassView
+  /-- The declaration docstring, and whether it's Verso -/
+  docString?      : Option (TSyntax ``Lean.Parser.Command.docComment × Bool)
   deriving Inhabited
 
 /-- Elaborated header for an inductive type before fvars for each inductive are added to the local context. -/
@@ -1071,6 +1075,18 @@ private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res
     for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking
     for elab' in finalizers do elab'.finalize
   applyDerivingHandlers views
+  -- Docstrings are added during postprocessing to allow them to have checked references to
+  -- the type and its constructors, but before attributes to enable e.g. `@[inherit_doc X]`
+  runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
+    for view in views do
+      withRef view.declId do
+        if let some (doc, verso) := view.docString? then
+          addDocStringOf verso view.declName view.binders doc
+      for ctor in view.ctors do
+        withRef ctor.declId do
+          if let some (doc, verso) := ctor.modifiers.docString? then
+            addDocStringOf verso ctor.declName ctor.binders doc
+
   runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
     for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
 

src/Lean/Elab/Open.lean

@@ -34,7 +34,7 @@ instance : MonadResolveName (M (m := m)) where
   getCurrNamespace   := return (← get).currNamespace
   getOpenDecls       := return (← get).openDecls
 
-def resolveId (ns : Name) (idStx : Syntax) : M (m := m) Name := do
+def resolveId [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do
   let declName := ns ++ idStx.getId
   if (← getEnv).contains declName then
     return declName
@@ -44,7 +44,13 @@ def resolveId (ns : Name) (idStx : Syntax) : M (m := m) Name := do
 private def addOpenDecl (decl : OpenDecl) : M (m:=m) Unit :=
   modify fun s => { s with openDecls := decl :: s.openDecls }
 
-private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) : M (m:=m) Name := do
+/--
+Uniquely resolves the identifier `idStx` in the provided namespaces `nss`.
+
+If the identifier does not indicate a name in exactly one of the namespaces, an exception is thrown.
+-/
+def resolveNameUsingNamespacesCore [MonadResolveName m]
+    (nss : List Name) (idStx : Syntax) : m Name := do
   let mut exs := #[]
   let mut result := #[]
   for ns in nss do
@@ -105,7 +111,7 @@ def elabOpenDecl [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.
 
 def resolveNameUsingNamespaces [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name := do
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
-    resolveNameUsingNamespacesCore nss idStx
+    resolveNameUsingNamespacesCore (m := M) nss idStx
 
 end OpenDecl
 

src/Lean/Elab/PreDefinition/Basic.lean

@@ -41,6 +41,7 @@ structure PreDefinition where
   levelParams : List Name
   modifiers   : Modifiers
   declName    : Name
+  binders     : Syntax
   type        : Expr
   value       : Expr
   termination : TerminationHints
@@ -173,7 +174,28 @@ private def checkMeta (preDef : PreDefinition) : TermElabM Unit := do
       | _, _ => pure ()
     return true
 
-private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit :=
+/--
+Adds the docstring, if relevant.
+
+This should be done just after compilation so the predefinition can be executed in examples in its
+docstring. If code generation will not occur, then it should be done after adding the declaration
+to the environment.
+-/
+def addPreDefDocs (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) : TermElabM Unit := do
+  if let some (doc, isVerso) := preDef.modifiers.docString? then
+    withLCtx docCtx.1 docCtx.2 do
+      addDocStringOf isVerso preDef.declName preDef.binders doc
+
+/--
+Adds constant info to the definition name. This should occur after executing post-compilation
+attributes, in case they have an effect on hovers.
+-/
+def addPreDefInfo (preDef : PreDefinition) : TermElabM Unit := do
+  withSaveInfoContext do  -- save new env that includes docstring and constant
+    addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
+
+
+private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs (cache := cacheProofs) preDef
     let preDef ← letToHaveType preDef
@@ -207,8 +229,6 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
       | DefKind.def | DefKind.example => mkDefDecl
       | DefKind.«instance» => if ← Meta.isProp preDef.type then mkThmDecl else mkDefDecl
     addDecl decl
-    withSaveInfoContext do  -- save new env
-      addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     match preDef.modifiers.computeKind with
     | .meta          => modifyEnv (addMeta · preDef.declName)
@@ -220,13 +240,17 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
     if applyAttrAfterCompilation then
       enableRealizationsForConst preDef.declName
       generateEagerEqns preDef.declName
+    addPreDefDocs docCtx preDef
+    if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
+    addPreDefInfo preDef
 
-def addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) (cleanupValue := false) : TermElabM Unit := do
-  addNonRecAux preDef (compile := true) (all := all) (cleanupValue := cleanupValue)
 
-def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit := do
-  addNonRecAux preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs) (cleanupValue := cleanupValue)
+def addAndCompileNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (all : List Name := [preDef.declName]) (cleanupValue := false) : TermElabM Unit := do
+  addNonRecAux docCtx preDef (compile := true) (all := all) (cleanupValue := cleanupValue)
+
+def addNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit := do
+  addNonRecAux docCtx preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs) (cleanupValue := cleanupValue)
 
 /--
   Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module
@@ -240,7 +264,10 @@ def eraseRecAppSyntaxExpr (e : Expr) : CoreM Expr := do
 def eraseRecAppSyntax (preDef : PreDefinition) : CoreM PreDefinition :=
   return { preDef with value := (← eraseRecAppSyntaxExpr preDef.value) }
 
-def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit := do
+def addAndCompileUnsafe
+    (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition)
+    (safety := DefinitionSafety.unsafe) :
+    TermElabM Unit := do
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
   withRef preDefs[0]!.ref do
     let all  := preDefs.toList.map (·.declName)
@@ -253,18 +280,21 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSaf
         safety, all
       }
     addDecl decl
-    withSaveInfoContext do  -- save new env
-      for preDef in preDefs do
-        addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
     compileDecl decl
+    for preDef in preDefs do
+      addPreDefDocs docCtx preDef
     applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
+    for preDef in preDefs do
+      addPreDefInfo preDef
     return ()
 
-def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit := do
+def addAndCompilePartialRec
+    (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) :
+    TermElabM Unit := do
   if preDefs.all shouldGenCodeFor then
     withEnableInfoTree false do
-      addAndCompileUnsafe (safety := DefinitionSafety.partial) <| preDefs.map fun preDef =>
+      addAndCompileUnsafe docCtx (safety := DefinitionSafety.partial) <| preDefs.map fun preDef =>
         { preDef with
           declName  := Compiler.mkUnsafeRecName preDef.declName
           value     := preDef.value.replace fun e => match e with

src/Lean/Elab/PreDefinition/Main.lean

@@ -19,7 +19,9 @@ namespace Lean.Elab
 open Meta
 open Term
 
-private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := false) : TermElabM Unit := do
+private def addAndCompilePartial
+    (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) (useSorry := false) :
+    TermElabM Unit := do
   for preDef in preDefs do
     trace[Elab.definition] "processing {preDef.declName}"
     let all := preDefs.toList.map (·.declName)
@@ -29,11 +31,11 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
       else
         let msg := m!"failed to compile 'partial' definition `{preDef.declName}`"
         liftM <| mkInhabitantFor msg xs type
-      addNonRec { preDef with
+      addNonRec docCtx { preDef with
         kind  := DefKind.«opaque»
         value
       } (all := all)
-  addAndCompilePartialRec preDefs
+  addAndCompilePartialRec docCtx preDefs
 
 private def isNonRecursive (preDef : PreDefinition) : Bool :=
   Option.isNone $ preDef.value.find? fun
@@ -139,7 +141,8 @@ private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array
     else
       return preDef
 
-private def addSorried (preDefs : Array PreDefinition) : TermElabM Unit := do
+private def addSorried (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) :
+    TermElabM Unit := do
   for preDef in preDefs do
     unless (← hasConst preDef.declName) do
       let value ← mkSorry (synthetic := true) preDef.type
@@ -160,10 +163,10 @@ private def addSorried (preDefs : Array PreDefinition) : TermElabM Unit := do
           value
         }
       addDecl decl
-      withSaveInfoContext do  -- save new env
-        addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
       applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
+      addPreDefDocs docCtx preDef
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
+      addPreDefInfo preDef
 
 def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM Unit := do
   preDefs.forM fun preDef =>
@@ -301,7 +304,8 @@ def shouldUseWF (preDefs : Array PreDefinition) : Bool :=
     preDef.termination.decreasingBy?.isSome
 
 
-def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
+def addPreDefinitions (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) :
+    TermElabM Unit := withLCtx {} {} do
   profileitM Exception "process pre-definitions" (← getOptions) do
     withTraceNode `Elab.def.processPreDef (fun _ => return m!"process pre-definitions") do
       for preDef in preDefs do
@@ -320,12 +324,12 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
           let preDef ← eraseRecAppSyntax preDefs[0]!
           ensureEqnReservedNamesAvailable preDef.declName
           if preDef.modifiers.isNoncomputable then
-            addNonRec preDef (cleanupValue := true)
+            addNonRec docCtx preDef (cleanupValue := true)
           else
-            addAndCompileNonRec preDef (cleanupValue := true)
+            addAndCompileNonRec docCtx preDef (cleanupValue := true)
           preDef.termination.ensureNone "not recursive"
         else if preDefs.any (·.modifiers.isUnsafe) then
-          addAndCompileUnsafe preDefs
+          addAndCompileUnsafe docCtx preDefs
           preDefs.forM (·.termination.ensureNone "unsafe")
         else
           if preDefs.any (·.modifiers.isInferredPartial) then
@@ -339,7 +343,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
                   isPartial := false
 
             if isPartial then
-              addAndCompilePartial preDefs
+              addAndCompilePartial docCtx preDefs
               preDefs.forM (·.termination.ensureNone "partial")
               continue
 
@@ -349,16 +353,16 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
             checkTerminationByHints preDefs
             let termMeasures?s ← elabTerminationByHints preDefs
             if shouldUseStructural preDefs then
-              structuralRecursion preDefs termMeasures?s
+              structuralRecursion docCtx preDefs termMeasures?s
             else if shouldUsePartialFixpoint preDefs then
-              partialFixpoint preDefs
+              partialFixpoint docCtx preDefs
             else if shouldUseWF preDefs then
-              wfRecursion preDefs termMeasures?s
+              wfRecursion docCtx preDefs termMeasures?s
             else
               withRef (preDefs[0]!.ref) <| mapError
                 (orelseMergeErrors
-                  (structuralRecursion preDefs termMeasures?s)
-                  (wfRecursion preDefs termMeasures?s))
+                  (structuralRecursion docCtx preDefs termMeasures?s)
+                  (wfRecursion docCtx preDefs termMeasures?s))
                 (fun msg =>
                   let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
                   m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
@@ -370,13 +374,13 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
                 -- try to add as partial definition
                 withOptions (Elab.async.set · false) do
                   try
-                    addAndCompilePartial preDefs (useSorry := true)
+                    addAndCompilePartial docCtx preDefs (useSorry := true)
                   catch _ =>
                     -- Compilation failed try again just as axiom
                     s.restore
-                    addSorried preDefs
+                    addSorried docCtx preDefs
               else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
-                addSorried preDefs
+                addSorried docCtx preDefs
             catch _ => s.restore
 
 builtin_initialize

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -30,7 +30,7 @@ where
       withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
         go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
 
-def addPreDefsFromUnary (preDefs : Array PreDefinition) (preDefsNonrec : Array PreDefinition)
+def addPreDefsFromUnary (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) (preDefsNonrec : Array PreDefinition)
     (unaryPreDefNonRec : PreDefinition) (cacheProofs := true) : TermElabM Unit := do
   /-
   We must remove `implemented_by` attributes from the auxiliary application because
@@ -45,11 +45,11 @@ def addPreDefsFromUnary (preDefs : Array PreDefinition) (preDefsNonrec : Array P
   -- we recognize that below and then do not set @[irreducible]
   withOptions (allowUnsafeReducibility.set · true) do
     if unaryPreDefNonRec.declName = preDefs[0]!.declName then
-      addNonRec preDefNonRec (applyAttrAfterCompilation := false) (cacheProofs := cacheProofs)
+      addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (cacheProofs := cacheProofs)
     else
       withEnableInfoTree false do
-        addNonRec preDefNonRec (applyAttrAfterCompilation := false) (cacheProofs := cacheProofs)
-      preDefsNonrec.forM (addNonRec · (applyAttrAfterCompilation := false) (all := declNames) (cacheProofs := cacheProofs))
+        addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (cacheProofs := cacheProofs)
+      preDefsNonrec.forM (addNonRec docCtx · (applyAttrAfterCompilation := false) (all := declNames) (cacheProofs := cacheProofs))
 
 /--
 Cleans the right-hand-sides of the predefinitions, to prepare for inclusion in the EqnInfos:

src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean

@@ -78,7 +78,7 @@ private def mkMonoPProd : (hmono₁ hmono₂ : Expr × Expr) → MetaM (Expr ×
   let hmonoProof ← mkAppOptM ``PProd.monotone_mk #[none, none, none, inst₁, inst₂, inst, none, none, hmono1Proof, hmono2Proof]
   return (← inferType hmonoProof, hmonoProof)
 
-def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
+def partialFixpoint (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) : TermElabM Unit := do
   -- We expect all functions in the clique to have `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` syntax
   let hints := preDefs.filterMap (·.termination.partialFixpoint?)
   assert! preDefs.size = hints.size
@@ -217,8 +217,8 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
         let value ← mkLambdaFVars (etaReduce := true) params value
         pure { preDef with value }
 
-    Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec
-    addAndCompilePartialRec preDefs
+    Mutual.addPreDefsFromUnary docCtx preDefs preDefsNonrec preDefNonRec
+    addAndCompilePartialRec docCtx preDefs
     let preDefs ← preDefs.mapM (Mutual.cleanPreDef ·)
     PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms (hints.map (·.fixpointType))
     Mutual.addPreDefAttributes preDefs

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -183,7 +183,10 @@ def reportTermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit :=
     Tactic.TryThis.addSuggestion ref stx
 
 
-def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
+def structuralRecursion
+    (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition)
+    (termMeasure?s : Array (Option TerminationMeasure)) :
+    TermElabM Unit := do
   let names := preDefs.map (·.declName)
   let ((recArgPoss, preDefsNonRec, fixedParamPerms), state) ← run <| inferRecArgPos preDefs termMeasure?s
   for recArgPos in recArgPoss, preDef in preDefs do
@@ -194,9 +197,9 @@ def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (
     prependError m!"structural recursion failed, produced type incorrect term" do
       -- We create the `_unsafe_rec` before we abstract nested proofs.
       -- Reason: the nested proofs may be referring to the _unsafe_rec.
-      addNonRec preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
+      addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
   let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
-  addAndCompilePartialRec preDefs
+  addAndCompilePartialRec docCtx preDefs
   for preDef in preDefs, recArgPos in recArgPoss do
     let mut preDef := preDef
     unless preDef.kind.isTheorem do
@@ -208,7 +211,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (
         See issue #2327
         -/
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
-    addSmartUnfoldingDef preDef recArgPos
+    addSmartUnfoldingDef docCtx preDef recArgPos
     markAsRecursive preDef.declName
   for preDef in preDefs do
     -- must happen in separate loop so realizations can see eqnInfos of all other preDefs

src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -64,12 +64,14 @@ where
       | _ => processApp e
     | _ => return e
 
-partial def addSmartUnfoldingDef (preDef : PreDefinition) (recArgPos : Nat) : TermElabM Unit := do
+partial def addSmartUnfoldingDef
+    (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (recArgPos : Nat) :
+    TermElabM Unit := do
   if (← isProp preDef.type) then
     return ()
   else
     withEnableInfoTree false do
       let preDefSUnfold ← addSmartUnfoldingDefAux preDef recArgPos
-      addNonRec preDefSUnfold (cleanupValue := true)
+      addNonRec docCtx preDefSUnfold (cleanupValue := true)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -23,7 +23,7 @@ namespace Lean.Elab
 open WF
 open Meta
 
-def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
+def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
   let termMeasures? := termMeasure?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← floatRecApp preDef.value) }
@@ -75,8 +75,8 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
 
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefsNonrec ← preDefsFromUnaryNonRec fixedParamPerms argsPacker preDefs preDefNonRec
-  Mutual.addPreDefsFromUnary (cacheProofs := false) preDefs preDefsNonrec preDefNonRec
-  addAndCompilePartialRec preDefs
+  Mutual.addPreDefsFromUnary (cacheProofs := false) docCtx preDefs preDefsNonrec preDefNonRec
+  addAndCompilePartialRec docCtx preDefs
   let unaryPreDef ← Mutual.cleanPreDef (cacheProofs := false) unaryPreDef
   let preDefs ← preDefs.mapM (Mutual.cleanPreDef (cacheProofs := false) ·)
   registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms argsPacker

src/Lean/Elab/SetOption.lean

@@ -14,6 +14,35 @@ namespace Lean.Elab
 
 variable [Monad m] [MonadOptions m] [MonadError m] [MonadLiftT (EIO Exception) m] [MonadInfoTree m]
 
+private def throwUnconfigurable {α} (optionName : Name) : m α :=
+  throwError "Invalid `set_option` command: The option `{optionName}` cannot be configured using \
+    `set_option`"
+
+/--
+Returns the type corresponding to the given `DataValue`, or `none` if the corresponding type
+cannot be specified using `set_option` notation.
+-/
+private def ctorType? : DataValue → Option Expr
+  | .ofString .. => mkConst ``String
+  | .ofNat .. => mkConst ``Nat
+  | .ofBool .. => mkConst ``Bool
+  | .ofInt .. => none
+  | .ofName .. => none
+  | .ofSyntax .. => none
+
+def validateOptionValue (optionName : Name) (decl : OptionDecl) (val : DataValue) : m Unit := do
+  unless decl.defValue.sameCtor val do
+    throwMistypedOptionValue val decl.defValue
+where
+  throwMistypedOptionValue (found defVal : DataValue) := do
+    match ctorType? defVal with
+    | some defValType =>
+      let foundType := ctorType? found |>.get!
+      throwError "set_option value type mismatch: The value{indentD (toMessageData found)}\nhas type\
+        {indentD (toMessageData foundType)}\nbut the option `{optionName}` expects a value of type\
+        {indentExpr defValType}"
+    | _ => throwUnconfigurable optionName
+
 def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
@@ -23,7 +52,7 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
   pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
   let rec setOption (val : DataValue) : m Options := do
-    unless decl.defValue.sameCtor val do throwMistypedOptionValue optionName val decl.defValue
+    validateOptionValue optionName decl val
     return (← getOptions).insert optionName val
   match val.isStrLit? with
   | some str => setOption (DataValue.ofString str)
@@ -39,30 +68,5 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
       throwError "Unexpected set_option value `{val}`; expected a literal of type `{ctorType}`"
     else
       throwUnconfigurable optionName
-where
-  throwMistypedOptionValue (optionName : Name) (found defVal : DataValue) := do
-    match ctorType? defVal with
-    | some defValType =>
-      let foundType := ctorType? found |>.get!
-      throwError "set_option value type mismatch: The value{indentD (toMessageData found)}\nhas type\
-        {indentD (toMessageData foundType)}\nbut the option `{optionName}` expects a value of type\
-        {indentExpr defValType}"
-    | _ => throwUnconfigurable optionName
-
-  throwUnconfigurable {α} (optionName : Name) : m α :=
-    throwError "Invalid `set_option` command: The option `{optionName}` cannot be configured using \
-      `set_option`"
-
-  /--
-  Returns the type corresponding to the given `DataValue`, or `none` if the corresponding type
-  cannot be specified using `set_option` notation.
-  -/
-  ctorType? : DataValue → Option Expr
-  | .ofString .. => mkConst ``String
-  | .ofNat .. => mkConst ``Nat
-  | .ofBool .. => mkConst ``Bool
-  | .ofInt .. => none
-  | .ofName .. => none
-  | .ofSyntax .. => none
 
 end Lean.Elab

src/Lean/Elab/Structure.lean

@@ -281,7 +281,6 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
       let declName ← applyVisibility ctorModifiers declName
       -- `binders` is type parameter binder overrides; this will be validated when the constructor is created in `Structure.mkCtor`.
       let binders := ctor[2]
-      addDocString' declName ctorModifiers.docString?
       addDeclarationRangesFromSyntax declName ctor[1]
       if structModifiers.isMeta then
         modifyEnv (addMeta · declName)
@@ -387,7 +386,6 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
         throwErrorAt ident "Invalid field name `{name.eraseMacroScopes}`: Field names must be atomic"
       let declName := structDeclName ++ name
       let declName ← applyVisibility fieldModifiers declName
-      addDocString' declName fieldModifiers.docString?
       return views.push {
         ref        := ident
         modifiers  := fieldModifiers
@@ -417,7 +415,7 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
   let isClass   := stx[0].getKind == ``Parser.Command.classTk
   let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
   let declId    := stx[1]
-  let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
+  let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
   addDeclarationRangesForBuiltin declName modifiers.stx stx
   let (binders, type?) := expandOptDeclSig stx[2]
   let exts := stx[3]
@@ -463,6 +461,7 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
     fields
     computedFields := #[]
     derivingClasses
+    docString?
   }
 
 
@@ -1538,6 +1537,17 @@ def elabStructureCommand : InductiveElabDescr where
                 withOptions (warn.sorry.set · false) do
                   mkRemainingProjections levelParams params view
               setStructureParents view.declName parentInfos
+
+              if let some (doc, isVerso) := view.docString? then
+                addDocStringOf isVerso view.declName view.binders doc
+              if let some (doc, isVerso) := view.ctor.modifiers.docString? then
+                addDocStringOf isVerso view.ctor.declName view.ctor.binders doc
+              for field in view.fields do
+                  -- may not exist if overriding inherited field
+                if (← getEnv).contains field.declName then
+                  if let some (doc, isVerso) := field.modifiers.docString? then
+                    addDocStringOf isVerso field.declName field.binders doc
+
               withSaveInfoContext do  -- save new env
                 for field in view.fields do
                   -- may not exist if overriding inherited field

src/Lean/Elab/Tactic/Doc.lean

@@ -6,7 +6,7 @@ Authors: David Thrane Christiansen
 module
 
 prelude
-public import Lean.DocString
+import Lean.DocString
 public import Lean.Elab.Command
 
 public section
@@ -23,9 +23,9 @@ open Lean.Parser.Command
     let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
 
     if let some tgt' := alternativeOfTactic (← getEnv) tacName then
-        throwErrorAt tac "`{tacName}` is an alternative form of `{tgt'}`"
+        throwErrorAt tac "`{.ofConstName tacName}` is an alternative form of `{.ofConstName tgt'}`"
     if !(isTactic (← getEnv) tacName) then
-      throwErrorAt tac "`{tacName}` is not a tactic"
+      throwErrorAt tac "`{.ofConstName tacName}` is not a tactic"
 
     modifyEnv (tacticDocExtExt.addEntry · (tacName, docs.getDocString))
     pure ()

src/Lean/Elab/Util.lean

@@ -123,7 +123,7 @@ unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespa
       if (← getEnv).contains kind && (← getInfoState).enabled then
         addConstInfo stx[1] kind none
       return kind
-    onAdded       := fun builtin declName => do
+    onAdded       := fun builtin declName kind => do
       if builtin then
         declareBuiltinDocStringAndRanges declName
   } attrDeclName

src/Lean/Exception.lean

@@ -150,7 +150,7 @@ Throw an unknown constant error message.
 The end position of the range of `ref` should point at the unknown identifier.
 See also `mkUnknownIdentifierMessage`.
 -/
-def throwUnknownConstantAt [Monad m] [MonadEnv m] [MonadError m] (ref : Syntax) (constName : Name) : m α := do
+def throwUnknownConstantAt [Monad m] [MonadEnv m] [MonadError m] (ref : Syntax) (constName : Name) : m α :=
   throwUnknownIdentifierAt (declHint := constName) ref m!"Unknown constant `{.ofConstName constName}`"
 
 /--

src/Lean/KeyedDeclsAttribute.lean

@@ -46,7 +46,7 @@ structure Def (γ : Type) where
     if (← getEnv).contains kind && (← Elab.getInfoState).enabled then
       Elab.addConstInfo stx kind none
     pure kind)
-  onAdded (builtin : Bool) (declName : Name) : AttrM Unit := pure ()
+  onAdded (builtin : Bool) (declName : Name) (key : Key) : AttrM Unit := pure ()
   deriving Inhabited
 
 structure OLeanEntry where
@@ -139,7 +139,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact de
             /- builtin_initialize @addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(declName) $(mkConst declName) -/
             let val := mkAppN (mkConst ``addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, toExpr declName, mkConst declName]
             declareBuiltin declName val
-            df.onAdded true declName
+            df.onAdded true declName key
         | _ => throwUnexpectedType
       applicationTime := AttributeApplicationTime.afterCompilation
     }
@@ -157,7 +157,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact de
       | none =>
         let val ← evalConstCheck γ df.valueTypeName declName
         ext.add { key := key, declName := declName, value := val } attrKind
-        df.onAdded false declName
+        df.onAdded false declName key
       | _ =>
         -- If the declaration contains `sorry`, we skip `evalConstCheck` to avoid unnecessary bizarre error message
         pure ()

src/Lean/Linter.lean

@@ -10,6 +10,7 @@ public import Lean.Linter.Util
 public import Lean.Linter.Builtin
 public import Lean.Linter.ConstructorAsVariable
 public import Lean.Linter.Deprecated
+public import Lean.Linter.DocsOnAlt
 public import Lean.Linter.UnusedVariables
 public import Lean.Linter.MissingDocs
 public import Lean.Linter.Omit

src/Lean/Linter/DocsOnAlt.lean

@@ -0,0 +1,62 @@
+/-
+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
+-/
+module
+
+prelude
+import Lean.Parser.Syntax
+public import Lean.Data.Options
+import Lean.Elab.Command
+import Lean.Linter.Basic
+import Lean.Server.InfoUtils
+
+public section
+
+namespace Lean.Linter
+open Elab.Command Parser Command
+open Parser.Term hiding «set_option»
+
+register_builtin_option linter.tactic.docsOnAlt : Bool := {
+  defValue := true
+  descr := "enable the 'documentation on tactic alternatives' linter"
+}
+
+private def getLinterDocsOnAlt (o : LinterOptions) : Bool :=
+  getLinterValue linter.tactic.docsOnAlt o
+
+namespace DocsOnAlt
+
+
+private partial def docsOnAlt : Linter where
+  run stx := do
+    if getLinterDocsOnAlt (← getLinterOptions) then
+      if let some mods := stx.find? (·.getKind ∈ [``declModifiers, ``Command.syntax]) then
+        if mods.find? isAltAttr |>.isSome then
+          if let some doc := mods.find? (·.getKind == ``docComment) then
+            let msg := m!"Documentation is ignored on a tactic alternative."
+            logLint linter.tactic.docsOnAlt doc msg
+      else if let some cmd := stx.find? (·.getKind == ``Command.attribute) then
+        let attrs := cmd[2]
+        let names := cmd[4].getArgs
+        if (attrs.find? isAltAttr).isSome then
+          let infoTrees := (← get).infoState.trees.toArray
+          for tree in infoTrees do
+            tree.visitM' (postNode := fun ci info _ => do
+              match info with
+              | .ofTermInfo ti =>
+                if names.contains ti.stx then
+                  if let some (x, _) := ti.expr.const? then
+                    if (← findInternalDocString? ci.env x).isSome then
+                      let msg := m!"Documentation for `{.ofConstName x}` is ignored because it is \
+                        a tactic alternative."
+                      logLint linter.tactic.docsOnAlt ti.stx msg
+              | _ => pure ())
+where
+  isAltAttr : Syntax → Bool
+    | `(attr|tactic_alt $_) => true
+    | _ => false
+
+
+builtin_initialize addLinter docsOnAlt

src/Lean/Parser/Basic.lean

@@ -97,6 +97,9 @@ def andthenFn (p q : ParserFn) : ParserFn := fun c s =>
   firstTokens   := p.firstTokens.seq q.firstTokens
 }
 
+instance : AndThen ParserFn where
+  andThen p1 p2 := andthenFn p1 (p2 ())
+
 /-- The `andthen(p, q)` combinator, usually written as adjacency in syntax declarations (`p q`),
 parses `p` followed by `q`.
 
@@ -269,6 +272,9 @@ def orelseFn (p q : ParserFn) : ParserFn :=
   firstTokens   := p.firstTokens.merge q.firstTokens
 }
 
+instance : OrElse ParserFn where
+  orElse p1 p2 := orelseFn p1 (p2 ())
+
 /--
   Run `p`, falling back to `q` if `p` failed without consuming any input.
 
@@ -314,21 +320,22 @@ Recover from errors in `p` using `recover` to consume input until a known-good s
 If `recover` fails itself, then no recovery is performed.
 
 `recover` is provided with information about the failing parser's effects , and it is run in the
-state immediately after the failure. -/
+state immediately after the failure.
+-/
 def recoverFn (p : ParserFn) (recover : RecoveryContext → ParserFn) : ParserFn := fun c s =>
   let iniPos := s.pos
   let iniSz := s.stxStack.size
-  let s' := p c s
-  if let some msg := s'.errorMsg then
-    let s' := recover ⟨iniPos, iniSz⟩ c {s' with errorMsg := none}
-    if s'.hasError then s'
-    else {s' with
-            pos := s'.pos,
-            lhsPrec := s'.lhsPrec,
-            cache := s'.cache,
-            errorMsg := none,
-            recoveredErrors := s'.recoveredErrors.push (s'.pos, s'.stxStack, msg) }
-  else s'
+  let s := p c s
+  if let some msg := s.errorMsg then
+    let s' := recover ⟨iniPos, iniSz⟩ c {s with errorMsg := none}
+    if s'.hasError then s
+    else {s with
+      pos := s'.pos,
+      errorMsg := none,
+      stxStack := s'.stxStack,
+      recoveredErrors := s.recoveredErrors.push (s'.pos, s'.stxStack, msg) }
+  else s
+
 
 /--
 Recover from errors in `parser` using `handler` to consume input until a known-good state has appeared.
@@ -676,14 +683,19 @@ In particular, string gaps (`"\" newline whitespace*`).
 def quotedStringFn : ParserFn :=
   quotedCharCoreFn isQuotableCharDefault true
 
-/-- Push `(Syntax.node tk <new-atom>)` onto syntax stack if parse was successful. -/
-def mkNodeToken (n : SyntaxNodeKind) (startPos : String.Pos) : ParserFn := fun c s => Id.run do
+/--
+Push `(Syntax.node tk <new-atom>)` onto syntax stack if parse was successful.
+
+If `includeWhitespace` is `false`, trailing whitespace is left behind.
+-/
+def mkNodeToken (n : SyntaxNodeKind) (startPos : String.Pos)
+    (includeWhitespace := true) : ParserFn := fun c s => Id.run do
   if s.hasError then
     return s
   let stopPos   := s.pos
   let leading   := c.mkEmptySubstringAt startPos
   let val       := c.extract startPos stopPos
-  let s         := whitespace c s
+  let s         := if includeWhitespace then whitespace c s else s
   let wsStopPos := s.pos
   let trailing  := c.substring (startPos := stopPos) (stopPos := wsStopPos)
   let info      := SourceInfo.original leading startPos trailing stopPos
@@ -701,19 +713,19 @@ def charLitFnAux (startPos : String.Pos) : ParserFn := fun c s =>
       let i    := s.pos
       let curr := c.get i
       let s    := s.setPos (c.next i)
-      if curr == '\'' then mkNodeToken charLitKind startPos c s
+      if curr == '\'' then mkNodeToken charLitKind startPos true c s
       else s.mkUnexpectedError "missing end of character literal"
 
-partial def strLitFnAux (startPos : String.Pos) : ParserFn := fun c s =>
+partial def strLitFnAux (startPos : String.Pos) (includeWhitespace := false) : ParserFn := fun c s =>
   let i := s.pos
   if h : c.atEnd i then s.mkUnexpectedErrorAt "unterminated string literal" startPos
   else
     let curr := c.get' i h
     let s    := s.setPos (c.next' i h)
     if curr == '\"' then
-      mkNodeToken strLitKind startPos c s
+      mkNodeToken strLitKind startPos true c s
     else if curr == '\\' then andthenFn quotedStringFn (strLitFnAux startPos) c s
-    else strLitFnAux startPos c s
+    else strLitFnAux startPos includeWhitespace c s
 
 /--
 Raw strings have the syntax `r##...#"..."#...##` with zero or more `#`'s.
@@ -770,7 +782,7 @@ where
       let s    := s.setPos (c.next' i h)
       if curr == '\"' then
         if num == 0 then
-          mkNodeToken strLitKind startPos c s
+          mkNodeToken strLitKind startPos true c s
         else
           closingState num 0 c s
       else
@@ -788,7 +800,7 @@ where
       let s    := s.setPos (c.next' i h)
       if curr == '#' then
         if closingNum + 1 == num then
-          mkNodeToken strLitKind startPos c s
+          mkNodeToken strLitKind startPos true c s
         else
           closingState num (closingNum + 1) c s
       else if curr == '\"' then
@@ -816,25 +828,26 @@ partial def takeDigitsFn (isDigit : Char → Bool) (expecting : String) (needDig
     else if needDigit then s.mkUnexpectedError "unexpected character" (expected := [expecting])
     else s
 
-def decimalNumberFn (startPos : String.Pos) (c : ParserContext) : ParserState → ParserState := fun s =>
+def decimalNumberFn (startPos : String.Pos) (includeWhitespace := true)
+    (c : ParserContext) (s : ParserState) : ParserState :=
   let s := takeDigitsFn (fun c => c.isDigit) "decimal number" false c s
   let i := s.pos
   if h : c.atEnd i then
-    mkNodeToken numLitKind startPos c s
+    mkNodeToken numLitKind startPos true c s
   else
     let curr := c.get' i h
     let j := c.next i
     if ∃ hj : ¬ c.atEnd j, curr = '.' && c.get' j hj = '.' then
-      mkNodeToken numLitKind startPos c s
+      mkNodeToken numLitKind startPos includeWhitespace c s
     else if curr == '.' || curr == 'e' || curr == 'E' then
       parseScientific s
     else
-      mkNodeToken numLitKind startPos c s
+      mkNodeToken numLitKind startPos includeWhitespace c s
 where
   parseScientific s :=
     let s := parseOptDot s
     let s := parseOptExp s
-    mkNodeToken scientificLitKind startPos c s
+    mkNodeToken scientificLitKind startPos includeWhitespace c s
 
   parseOptDot s :=
     let i     := s.pos
@@ -863,19 +876,23 @@ where
     else
       s
 
-def binNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
+def binNumberFn (startPos : String.Pos) (includeWhitespace := true) : ParserFn := fun c s =>
   let s := takeDigitsFn (fun c => c == '0' || c == '1') "binary number" true c s
-  mkNodeToken numLitKind startPos c s
+  mkNodeToken numLitKind startPos includeWhitespace c s
 
-def octalNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
+def octalNumberFn (startPos : String.Pos) (includeWhitespace := true) : ParserFn := fun c s =>
   let s := takeDigitsFn (fun c => '0' ≤ c && c ≤ '7') "octal number" true c s
-  mkNodeToken numLitKind startPos c s
+  mkNodeToken numLitKind startPos includeWhitespace c s
 
-def hexNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
-  let s := takeDigitsFn (fun c => ('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')) "hexadecimal number" true c s
-  mkNodeToken numLitKind startPos c s
+@[inline]
+private def isHexDigit (c : Char) : Bool :=
+  ('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')
 
-def numberFnAux : ParserFn := fun c s =>
+def hexNumberFn (startPos : String.Pos) (includeWhitespace := true) : ParserFn := fun c s =>
+  let s := takeDigitsFn isHexDigit "hexadecimal number" true c s
+  mkNodeToken numLitKind startPos includeWhitespace c s
+
+def numberFnAux (includeWhitespace := true) : ParserFn := fun c s =>
   let startPos := s.pos
   if h : c.atEnd startPos then s.mkEOIError
   else
@@ -884,15 +901,15 @@ def numberFnAux : ParserFn := fun c s =>
       let i    := c.next' startPos h
       let curr := c.get i
       if curr == 'b' || curr == 'B' then
-        binNumberFn startPos c (s.next c i)
+        binNumberFn startPos includeWhitespace c (s.next c i)
       else if curr == 'o' || curr == 'O' then
-        octalNumberFn startPos c (s.next c i)
+        octalNumberFn startPos includeWhitespace c (s.next c i)
       else if curr == 'x' || curr == 'X' then
-        hexNumberFn startPos c (s.next c i)
+        hexNumberFn startPos includeWhitespace c (s.next c i)
       else
-        decimalNumberFn startPos c (s.setPos i)
+        decimalNumberFn startPos includeWhitespace c (s.setPos i)
     else if curr.isDigit then
-      decimalNumberFn startPos c (s.next c startPos)
+      decimalNumberFn startPos includeWhitespace c (s.next c startPos)
     else
       s.mkError "numeral"
 
@@ -934,13 +951,15 @@ def mkTokenAndFixPos (startPos : String.Pos) (tk : Option Token) : ParserFn := f
       let atom      := mkAtom (SourceInfo.original leading startPos trailing stopPos) tk
       s.pushSyntax atom
 
-def mkIdResult (startPos : String.Pos) (tk : Option Token) (val : Name) : ParserFn := fun c s =>
+def mkIdResult (startPos : String.Pos) (tk : Option Token) (val : Name)
+    (includeWhitespace : Bool := true) :
+    ParserFn := fun c s =>
   let stopPos           := s.pos
   if isToken startPos stopPos tk then
     mkTokenAndFixPos startPos tk c s
   else
     let rawVal          := c.substring startPos stopPos
-    let s               := whitespace c s
+    let s               := if includeWhitespace then whitespace c s else s
     let trailingStopPos := s.pos
     let leading         := c.mkEmptySubstringAt startPos
     let trailing        := c.substring (startPos := stopPos) (stopPos := trailingStopPos)
@@ -948,7 +967,9 @@ def mkIdResult (startPos : String.Pos) (tk : Option Token) (val : Name) : Parser
     let atom            := mkIdent info rawVal val
     s.pushSyntax atom
 
-partial def identFnAux (startPos : String.Pos) (tk : Option Token) (r : Name) : ParserFn :=
+partial def identFnAux (startPos : String.Pos) (tk : Option Token) (r : Name)
+    (includeWhitespace : Bool := true) :
+    ParserFn :=
   let rec parse (r : Name) (c s) :=
     let i := s.pos
     if h : c.atEnd i then
@@ -968,7 +989,7 @@ partial def identFnAux (startPos : String.Pos) (tk : Option Token) (r : Name) :
             let s := s.next c s.pos
             parse r c s
           else
-            mkIdResult startPos tk r c s
+            mkIdResult startPos tk r includeWhitespace c s
       else if isIdFirst curr then
         let startPart := i
         let s         := takeWhileFn isIdRest c (s.next c i)
@@ -978,7 +999,7 @@ partial def identFnAux (startPos : String.Pos) (tk : Option Token) (r : Name) :
           let s := s.next c s.pos
           parse r c s
         else
-          mkIdResult startPos tk r c s
+          mkIdResult startPos tk r includeWhitespace c s
       else
         mkTokenAndFixPos startPos tk c s
   parse r
@@ -987,7 +1008,7 @@ private def isIdFirstOrBeginEscape (c : Char) : Bool :=
   isIdFirst c || isIdBeginEscape c
 
 private def nameLitAux (startPos : String.Pos) : ParserFn := fun c s =>
-  let s := identFnAux startPos none .anonymous c (s.next c startPos)
+  let s := identFnAux startPos none .anonymous (includeWhitespace := true) c (s.next c startPos)
   if s.hasError then
     s
   else
@@ -1002,11 +1023,11 @@ private def tokenFnAux : ParserFn := fun c s =>
   let i     := s.pos
   let curr  := c.get i
   if curr == '\"' then
-    strLitFnAux i c (s.next c i)
+    strLitFnAux i true c (s.next c i)
   else if curr == '\'' && c.getNext i != '\'' then
     charLitFnAux i c (s.next c i)
   else if curr.isDigit then
-    numberFnAux c s
+    numberFnAux true c s
   else if curr == '`' && isIdFirstOrBeginEscape (c.getNext i) then
     nameLitAux i c s
   else if curr == 'r' && isRawStrLitStart c (c.next i) then
@@ -1016,7 +1037,7 @@ private def tokenFnAux : ParserFn := fun c s =>
       have := c.endPos_valid
       rw [String.endPos] at this
       omega
-    identFnAux i tk .anonymous c s
+    identFnAux i tk .anonymous (includeWhitespace := true) c s
 
 private def updateTokenCache (startPos : String.Pos) (s : ParserState) : ParserState :=
   -- do not cache token parsing errors, which are rare and usually fatal and thus not worth an extra field in `TokenCache`
@@ -1057,10 +1078,10 @@ def peekToken (c : ParserContext) (s : ParserState) : ParserState × Except Pars
     peekTokenAux c s
 
 /-- Treat keywords as identifiers. -/
-def rawIdentFn : ParserFn := fun c s =>
+def rawIdentFn (includeWhitespace := true) : ParserFn := fun c s =>
   let i := s.pos
   if c.atEnd i then s.mkEOIError
-  else identFnAux i none .anonymous c s
+  else identFnAux i none .anonymous (includeWhitespace := includeWhitespace) c s
 
 def satisfySymbolFn (p : String → Bool) (expected : List String) : ParserFn := fun c s => Id.run do
   let iniPos := s.pos
@@ -1933,7 +1954,7 @@ def fieldIdxFn : ParserFn := fun c s =>
   let curr     := c.get iniPos
   if curr.isDigit && curr != '0' then
     let s     := takeWhileFn (fun c => c.isDigit) c s
-    mkNodeToken fieldIdxKind iniPos c s
+    mkNodeToken fieldIdxKind iniPos true c s
   else
     s.mkErrorAt "field index" iniPos initStackSz
 

src/Lean/Parser/StrInterpolation.lean

@@ -25,12 +25,12 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
       let curr := c.get i
       let s    := s.setPos (c.next i)
       if curr == '\"' then
-        let s := mkNodeToken interpolatedStrLitKind startPos c s
+        let s := mkNodeToken interpolatedStrLitKind startPos true c s
         s.mkNode interpolatedStrKind stackSize
       else if curr == '\\' then
         andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant true) (parse startPos) c s
       else if curr == '{' then
-        let s := mkNodeToken interpolatedStrLitKind startPos c s
+        let s := mkNodeToken interpolatedStrLitKind startPos true c s
         let s := p c s
         if s.hasError then s
         else

src/Lean/Parser/Tactic/Doc.lean

@@ -6,11 +6,12 @@ Authors: David Thrane Christiansen
 module
 
 prelude
-public import Lean.Attributes
-public import Lean.DocString.Extension
-public import Lean.Elab.InfoTree.Main
+public import Lean.Environment
+import Lean.Attributes
+import Lean.DocString.Extension
+import Lean.Elab.InfoTree.Main
 meta import Lean.Parser.Attr
-public import Lean.Parser.Extension
+import Lean.Parser.Extension
 
 public section
 
@@ -25,9 +26,7 @@ open Lean.Parser.Attr
 def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
   let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
     | return false
-  for (tac, _) in tactics.kinds do
-    if kind == tac then return true
-  return false
+  return tactics.kinds.contains kind
 
 /--
 Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
@@ -83,15 +82,18 @@ builtin_initialize
       let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
 
       if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "`{tgtName}` is not a tactic"
-      -- If this condition is true, then we're in an `attribute` command and can validate here.
-      if (← getEnv).find? decl |>.isSome then
-        if !(isTactic (← getEnv) decl) then throwError "`{decl}` is not a tactic"
+      -- If the target is a known syntax kind, ensure that it's a tactic
+      let mut cats := #[]
+      for (catName, cat) in parserExtension.getState (← getEnv) |>.categories do
+        if cat.kinds.contains decl then cats := cats.push catName
+      if !cats.isEmpty && cats.all (· ≠ `tactic) then
+        let catNames := cats.map fun c => m!"`{c}`"
+        let s := if catNames.size > 1 then m!"ies" else m!"y"
+        throwError "`{decl}` is not a tactic (it is in the categor{s} {.andList catNames.toList})"
 
       if let some tgt' := alternativeOfTactic (← getEnv) tgtName then
         throwError "`{tgtName}` is itself an alternative for `{tgt'}`"
       modifyEnv fun env => tacticAlternativeExt.addEntry env (decl, tgtName)
-      if (← findSimpleDocString? (← getEnv) decl).isSome then
-        logWarningAt stx m!"Docstring for `{decl}` will be ignored because it is an alternative"
 
     descr :=
       "Register a tactic parser as an alternative form of an existing tactic, so they " ++
@@ -101,7 +103,7 @@ builtin_initialize
     -- when the attribute is applied after definition, using an `attribute` command (error checking
     -- for the `@[tactic_alt TAC]` syntax is performed by the parser attribute hook). If this
     -- attribute ran later, then the decl would already be present.
-    applicationTime := .beforeElaboration
+    applicationTime := .afterCompilation --.beforeElaboration
   }
 
 
@@ -278,7 +280,7 @@ where
 Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
 tactics.
 -/
-def tacticDocsOnTactics : ParserAttributeHook where
+private def tacticDocsOnTactics : ParserAttributeHook where
   postAdd (catName declName : Name) (_builtIn : Bool) := do
     if catName == `tactic then
       return

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -100,7 +100,6 @@ def handleHover (p : HoverParams)
           let docStr ← findDocString? snap.env kind
           return docStr.map (·, stx.getRange?.get!)
         | none => pure none
-
       -- now try info tree
       if let some result := snap.infoTree.hoverableInfoAtM? (m := Id) hoverPos then
         let ctx := result.ctx

src/shell/CMakeLists.txt

@@ -180,6 +180,17 @@ FOREACH(T ${LEANTESTS})
   endif()
 ENDFOREACH(T)
 
+# LEAN DOCSTRING PARSER TESTS
+file(GLOB_RECURSE LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/docparse/*_[0-9][0-9][0-9][0-9]")
+FOREACH(T ${LEANTESTS})
+  if(NOT T MATCHES "\\.#" AND NOT T MATCHES "run.lean")
+    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+    add_test(NAME "leandocparsetest_${T_NAME}"
+             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/docparse"
+             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
+  endif()
+ENDFOREACH(T)
+
 # Create a lake test for each test and examples subdirectory of `lake`
 # which contains a `test.sh` file, excluding the following test(s):
 # bootstrap: too slow

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
-// Please update stage0
+
+// Dear CI, won't you please update stage0?
+
 namespace lean {
 options get_default_options() {
     options opts;
@@ -11,12 +13,12 @@ options get_default_options() {
     opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with
     // builtin elaborators
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // changes to builtin parsers may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/docparse/arg_0001

@@ -0,0 +1 @@
+x

tests/lean/docparse/arg_0001.expected.out

@@ -0,0 +1,4 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_ident `x))
+All input consumed.

tests/lean/docparse/arg_0002

@@ -0,0 +1 @@
+x:=1

tests/lean/docparse/arg_0002.expected.out

@@ -0,0 +1,6 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.named_no_paren
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_num (num "1")))
+All input consumed.

tests/lean/docparse/arg_0003

@@ -0,0 +1 @@
+(x:=1)

tests/lean/docparse/arg_0003.expected.out

@@ -0,0 +1,8 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_num (num "1"))
+   ")")
+All input consumed.

tests/lean/docparse/arg_0004

@@ -0,0 +1,2 @@
+
+(x:=1)

tests/lean/docparse/arg_0004.expected.out

@@ -0,0 +1,4 @@
+Failure @0 (⟨1, 0⟩): expected '(', '+', '-', expected identifier, string, or number or token
+Final stack:
+  <missing>
+Remaining: "\n(x:=1)"

tests/lean/docparse/arg_0005

@@ -0,0 +1 @@
++foo

tests/lean/docparse/arg_0005.expected.out

@@ -0,0 +1,3 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.flag_on "+" `foo)
+All input consumed.

tests/lean/docparse/arg_0006

@@ -0,0 +1 @@
+-other

tests/lean/docparse/arg_0006.expected.out

@@ -0,0 +1,3 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.flag_off "-" `other)
+All input consumed.

tests/lean/docparse/arg_0007

@@ -0,0 +1 @@
+- other

tests/lean/docparse/arg_0007.expected.out

@@ -0,0 +1,4 @@
+Failure @2 (⟨1, 2⟩): expected no space before
+Final stack:
+  (Lean.Doc.Syntax.flag_off "-" `other)
+Remaining: "other"

tests/lean/docparse/arg_0008

@@ -0,0 +1 @@
+(x:=1)

tests/lean/docparse/arg_0008.expected.out

@@ -0,0 +1,9 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_num (num "1"))
+   ")")
+Remaining:
+"\n"

tests/lean/docparse/arg_0009

@@ -0,0 +1 @@
+x:=y

tests/lean/docparse/arg_0009.expected.out

@@ -0,0 +1,6 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.named_no_paren
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_ident `y))
+All input consumed.

tests/lean/docparse/arg_0010

@@ -0,0 +1 @@
+(x:=y)

tests/lean/docparse/arg_0010.expected.out

@@ -0,0 +1,8 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_ident `y)
+   ")")
+All input consumed.

tests/lean/docparse/arg_0011

@@ -0,0 +1 @@
+x:="y"

tests/lean/docparse/arg_0011.expected.out

@@ -0,0 +1,6 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.named_no_paren
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_str (str "\"y\"")))
+All input consumed.

tests/lean/docparse/arg_0012

@@ -0,0 +1 @@
+x:="y

tests/lean/docparse/arg_0012.expected.out

@@ -0,0 +1,7 @@
+Failure @3 (⟨1, 3⟩): unterminated string literal
+Final stack:
+ • `x
+ • ":="
+ • (Lean.Doc.Syntax.arg_str <missing>)
+
+Remaining: "\"y"

tests/lean/docparse/arg_0013

@@ -0,0 +1 @@
+(x:="y)

tests/lean/docparse/arg_0013.expected.out

@@ -0,0 +1,13 @@
+2 failures:
+  @7 (⟨1, 7⟩): expected ')'
+    ""
+  @7 (⟨1, 7⟩): unterminated string literal
+    ""
+
+Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_str <missing>)
+   <missing>)

tests/lean/docparse/arg_0014

@@ -0,0 +1 @@
+42

tests/lean/docparse/arg_0014.expected.out

@@ -0,0 +1,4 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_num (num "42")))
+All input consumed.

tests/lean/docparse/arg_0015

@@ -0,0 +1 @@
+(42)

tests/lean/docparse/arg_0015.expected.out

@@ -0,0 +1,17 @@
+4 failures:
+  @4 (⟨1, 4⟩): expected ')'
+    ""
+  @4 (⟨1, 4⟩): expected ':='
+    ""
+  @4 (⟨1, 4⟩): expected token
+    ""
+  @4 (⟨1, 4⟩): unexpected end of input
+    ""
+
+Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   <missing>
+   <missing>
+   <missing>
+   <missing>)

tests/lean/docparse/arg_0016

@@ -0,0 +1 @@
+(x 42)

tests/lean/docparse/arg_0016.expected.out

@@ -0,0 +1,15 @@
+3 failures:
+  @6 (⟨1, 6⟩): expected ')'
+    ""
+  @6 (⟨1, 6⟩): expected ':='
+    ""
+  @6 (⟨1, 6⟩): unexpected end of input
+    ""
+
+Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   <missing>
+   <missing>
+   <missing>)

tests/lean/docparse/arg_0017

@@ -0,0 +1,2 @@
+(x := 42
+)

tests/lean/docparse/arg_0017.expected.out

@@ -0,0 +1,9 @@
+Failure @8 (⟨1, 8⟩): expected ')'
+Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_num (num "42"))
+   <missing>)
+Remaining: "\n)"

tests/lean/docparse/arg_0018

@@ -0,0 +1,2 @@
+(x := 42
+a

tests/lean/docparse/arg_0018.expected.out

@@ -0,0 +1,9 @@
+Failure @8 (⟨1, 8⟩): expected ')'
+Final stack:
+  (Lean.Doc.Syntax.named
+   "("
+   `x
+   ":="
+   (Lean.Doc.Syntax.arg_num (num "42"))
+   <missing>)
+Remaining: "\na"

tests/lean/docparse/arg_val_0001

@@ -0,0 +1 @@
+1

tests/lean/docparse/arg_val_0001.expected.out

@@ -0,0 +1,4 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_num (num "1")))
+All input consumed.

tests/lean/docparse/arg_val_0002

@@ -0,0 +1 @@
+3

tests/lean/docparse/arg_val_0002.expected.out

@@ -0,0 +1,4 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_num (num "3")))
+All input consumed.

tests/lean/docparse/arg_val_0003.expected.out

@@ -0,0 +1,4 @@
+Failure @0 (⟨1, 0⟩): unexpected end of input; expected '(', '+' or '-'
+Final stack:
+  <missing>
+Remaining: ""

tests/lean/docparse/arg_val_0004

@@ -0,0 +1 @@
+"a b c	 d"

tests/lean/docparse/arg_val_0004.expected.out

@@ -0,0 +1,5 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_str
+    (str "\"a b c\t d\"")))
+All input consumed.

tests/lean/docparse/arg_val_0005

@@ -0,0 +1 @@
+"a b c	 d"

tests/lean/docparse/arg_val_0005.expected.out

@@ -0,0 +1,5 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_str
+    (str "\"a b c\t d\"")))
+All input consumed.

tests/lean/docparse/arg_val_0006

@@ -0,0 +1,2 @@
+43
+"foo"

tests/lean/docparse/arg_val_0006.expected.out

@@ -0,0 +1,5 @@
+Success! Final stack:
+  (Lean.Doc.Syntax.anon
+   (Lean.Doc.Syntax.arg_num (num "43")))
+Remaining:
+"\n\"foo\""

tests/lean/docparse/arg_val_0007

@@ -0,0 +1 @@
+"foo

tests/lean/docparse/arg_val_0007.expected.out

@@ -0,0 +1,4 @@
+Failure @0 (⟨1, 0⟩): unterminated string literal; expected '(', '+', '-' or token
+Final stack:
+  (Lean.Doc.Syntax.arg_str <missing>)
+Remaining: "\"foo"