From 0002ea8a3702a0c2191b03e1274aefc05b53ca8c Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Wed, 11 Jun 2025 10:52:08 -0400
Subject: [PATCH] feat: pre-stage0 groundwork for named error messages (#8649)

This PR adds the pre-stage0-update infrastructure for named error
messages. It adds macro syntax for registering and throwing named errors
(without elaborators), mechanisms for displaying error names in the
Infoview and at the command line, and the ability to link to error
explanations in the manual (once they are added).
---
 src/Lean/DocString/Links.lean                 | 40 ++++++---
 src/Lean/Exception.lean                       | 21 +++++
 src/Lean/Log.lean                             | 87 ++++++++++++++++++-
 src/Lean/Message.lean                         | 74 +++++++++++++++-
 src/Lean/Meta/Hint.lean                       |  7 +-
 src/Lean/Meta/Tactic/TryThis.lean             |  2 +-
 src/Lean/Parser/Command.lean                  |  8 ++
 src/Lean/Parser/Term.lean                     | 51 +++++++++++
 src/Lean/Widget/InteractiveDiagnostic.lean    |  3 +-
 .../docstringLinkValidation.lean.expected.out |  2 +-
 tests/lean/run/docstringRewrites.lean         | 27 +++---
 11 files changed, 289 insertions(+), 33 deletions(-)

diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
index e30026cf7b..d274b6b7bf 100644
--- a/src/Lean/DocString/Links.lean
+++ b/src/Lean/DocString/Links.lean
@@ -23,7 +23,7 @@ If the environment variable `LEAN_MANUAL_ROOT` is set, it is used as the root. I
 root is pre-configured for the current Lean executable (typically true for releases), then it is
 used. If neither are true, then `https://lean-lang.org/doc/reference/latest/` is used.
 -/
-def manualRoot : BaseIO String := do
+builtin_initialize manualRoot : String ←
   let r ←
     if let some root := (← IO.getEnv "LEAN_MANUAL_ROOT") then
       pure root
@@ -35,6 +35,22 @@ def manualRoot : BaseIO String := do
         pure root
   return if r.endsWith "/" then r else r ++ "/"
 
+/--
+The manual domain for error explanations.
+
+We expose this because it is used to populate the URL of the error message description widget.
+-/
+def errorExplanationManualDomain :=
+  "Manual.errorExplanation"
+
+-- TODO: we may wish to make this more general for domains that require additional arguments
+/-- Maps `lean-manual` URL paths to their corresponding manual domains. -/
+private def domainMap : Std.HashMap String String :=
+  Std.HashMap.ofList [
+    ("section", "Verso.Genre.Manual.section"),
+    ("errorExplanation", errorExplanationManualDomain)
+  ]
+
 /--
 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.
@@ -74,7 +90,7 @@ def rewriteManualLinksCore (s : String) : BaseIO (Array (String.Range × String)
         out := out.push c
         break
       | .ok path =>
-        out := out ++ (← manualRoot) ++ path
+        out := out ++ manualRoot ++ path
         out := out.push c'
         iter := iter'
         break
@@ -104,17 +120,19 @@ where
 
   rw (path : String) : Except String String := do
     match path.splitOn "/" with
-    | "section" :: args =>
-      if let [s] := args then
-        if s.isEmpty then
-          throw s!"Empty section ID"
-        return s!"find/?domain=Verso.Genre.Manual.section&name={s}"
-      else
-        throw s!"Expected one item after 'section', but got {args}"
     | [] | [""] =>
       throw "Missing documentation type"
-    | other :: _ =>
-      throw s!"Unknown documentation type '{other}'. Expected 'section'."
+    | 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}"
 
 
 /--
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index e4e44f3938..1c292e654b 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -80,6 +80,27 @@ def unknownIdentifierMessageTag : Name := `unknownIdentifier
 protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do
   withRef ref <| Lean.throwError msg
 
+/--
+Throw an error exception with the specified name, with position information from `getRef`.
+
+Note: Use the macro `throwNamedError`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «throwNamedError» [Monad m] [MonadError m] (name : Name) (msg : MessageData) : m α := do
+  let ref ← getRef
+  let msg := msg.tagWithErrorName name
+  let (ref, msg) ← AddErrorMessageContext.add ref msg
+  throw <| Exception.error ref msg
+
+/--
+Throw an error exception with the specified name at the position `ref`.
+
+Note: Use the macro `throwNamedErrorAt`, which validates error names, instead of calling this
+function directly.
+-/
+protected def «throwNamedErrorAt» [Monad m] [MonadError m] (ref : Syntax) (name : Name) (msg : MessageData) : m α :=
+  withRef ref <| Lean.throwNamedError name msg
+
 /--
 Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
 This tag is used by the 'import unknown identifier' code action to detect messages that should
diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean
index d3a09b3ad5..4ab0a6a25b 100644
--- a/src/Lean/Log.lean
+++ b/src/Lean/Log.lean
@@ -5,7 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.Sorry
+import Lean.Widget.Types
 import Lean.Message
+import Lean.DocString.Links
 
 namespace Lean
 
@@ -53,6 +55,48 @@ register_builtin_option warningAsError : Bool := {
   descr    := "treat warnings as errors"
 }
 
+/--
+A widget for displaying error names and explanation links.
+-/
+-- Note that we cannot tag this as a `builtin_widget_module` in this module because doing so would
+-- create circular imports. Instead, we add this attribute post-hoc in `Lean.ErrorExplanation`.
+def errorDescriptionWidget : Widget.Module where
+  javascript := "
+import { createElement } from 'react';
+export default function ({ code, explanationUrl }) {
+  const sansText = { fontFamily: 'var(--vscode-font-family)' }
+
+  const codeSpan = createElement('span', {}, [
+    createElement('span', { style: sansText }, 'Error code: '), code])
+  const brSpan = createElement('span', {}, '\\n')
+  const linkSpan = createElement('span', { style: sansText },
+    createElement('a', { href: explanationUrl }, 'View explanation'))
+
+  const all = createElement('div', { style: { marginTop: '1em' } }, [codeSpan, brSpan, linkSpan])
+  return all
+}"
+
+/--
+If `msg` is tagged as a named error, appends the error description widget displaying the
+corresponding error name and explanation link. Otherwise, returns `msg` unaltered.
+-/
+private def MessageData.appendDescriptionWidgetIfNamed (msg : MessageData) : MessageData :=
+  match errorNameOfKind? msg.kind with
+  | some errorName =>
+    let url := manualRoot ++ s!"find/?domain={errorExplanationManualDomain}&name={errorName}"
+    let inst := {
+      id := ``errorDescriptionWidget
+      javascriptHash := errorDescriptionWidget.javascriptHash
+      props := return json% {
+        code: $(toString errorName),
+        explanationUrl: $url
+      }
+    }
+    -- Note: we do not generate corresponding message data for the widget because it pollutes
+    -- console output
+    msg.composePreservingKind <| .ofWidget inst .nil
+  | none => msg
+
 /--
 Log the message `msgData` at the position provided by `ref` with the given `severity`.
 If `getRef` has position information but `ref` does not, we use `getRef`.
@@ -80,26 +124,63 @@ def logAt (ref : Syntax) (msgData : MessageData)
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
   logAt ref msgData MessageSeverity.error
 
+/--
+Log a named error message using the given message data. The position is provided by `ref`.
+
+Note: Use the macro `logNamedErrorAt`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «logNamedErrorAt» (ref : Syntax) (name : Name) (msgData : MessageData) : m Unit :=
+  logAt ref (msgData.tagWithErrorName name) MessageSeverity.error
+
 /-- Log a new warning message using the given message data. The position is provided by `ref`. -/
 def logWarningAt [MonadOptions m] (ref : Syntax) (msgData : MessageData) : m Unit := do
   logAt ref msgData .warning
 
+/--
+Log a named error warning using the given message data. The position is provided by `ref`.
+
+Note: Use the macro `logNamedWarningAt`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «logNamedWarningAt» (ref : Syntax) (name : Name) (msgData : MessageData) : m Unit :=
+  logAt ref (msgData.tagWithErrorName name) MessageSeverity.warning
+
 /-- Log a new information message using the given message data. The position is provided by `ref`. -/
 def logInfoAt (ref : Syntax) (msgData : MessageData) : m Unit :=
   logAt ref msgData MessageSeverity.information
 
 /-- Log a new error/warning/information message using the given message data and `severity`. The position is provided by `getRef`. -/
-def log (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error): m Unit := do
+def log (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error)
+    (isSilent : Bool := false) : m Unit := do
   let ref ← MonadLog.getRef
-  logAt ref msgData severity
+  logAt ref msgData severity isSilent
 
 /-- Log a new error message using the given message data. The position is provided by `getRef`. -/
 def logError (msgData : MessageData) : m Unit :=
   log msgData MessageSeverity.error
 
+/--
+Log a named error message using the given message data. The position is provided by `getRef`.
+
+Note: Use the macro `logNamedError`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «logNamedError» (name : Name) (msgData : MessageData) : m Unit :=
+  log (msgData.tagWithErrorName name) MessageSeverity.error
+
 /-- Log a new warning message using the given message data. The position is provided by `getRef`. -/
 def logWarning [MonadOptions m] (msgData : MessageData) : m Unit := do
-  log msgData (if warningAsError.get (← getOptions) then .error else .warning)
+  log msgData .warning
+
+/--
+Log a named warning using the given message data. The position is provided by `getRef`.
+
+Note: Use the macro `logNamedWarning`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «logNamedWarning» (name : Name) (msgData : MessageData) : m Unit :=
+  log (msgData.tagWithErrorName name) MessageSeverity.warning
 
 /-- Log a new information message using the given message data. The position is provided by `getRef`. -/
 def logInfo (msgData : MessageData) : m Unit :=
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 6699b47d2d..1313aefebd 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -15,11 +15,26 @@ import Lean.Util.Sorry
 
 namespace Lean
 
-def mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String) (endPos : Option Position := none) : String :=
+/--
+Creates a string describing an error message `msg` produced at `pos`, optionally ending at `endPos`,
+in `fileName`.
+
+Additional optional arguments can be used to prepend a label `kind` describing the severity of
+the error (e.g., `"warning"` or `"error"`) and a bracketed `name` label displaying the name of the
+error if it has one.
+-/
+def mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String)
+    (endPos : Option Position := none) (kind : Option String := none) (name : Option Name := none)
+    : String :=
   let endPos := match endPos with
     | some endPos => s!"-{endPos.line}:{endPos.column}"
     | none        => ""
-  s!"{fileName}:{pos.line}:{pos.column}{endPos}: {msg}"
+  let label := if name.isSome || kind.isSome then
+    let name := name.map (s!"({·})")
+    s!" {kind.getD ""}{name.getD ""}:"
+  else
+    ""
+  s!"{fileName}:{pos.line}:{pos.column}{endPos}:{label} {msg}"
 
 inductive MessageSeverity where
   | information | warning | error
@@ -154,6 +169,16 @@ def isTrace : MessageData → Bool
   | .trace _ _ _            => true
   | _                       => false
 
+/--
+`composePreservingKind msg msg'` appends the contents of `msg'` to the end of `msg` but ensures that
+the resulting message preserves the kind (as given by `MessageData.kind`) of `msg`.
+-/
+def composePreservingKind : MessageData → MessageData → MessageData
+  | withContext ctx msg     , msg' => withContext ctx (composePreservingKind msg msg')
+  | withNamingContext nc msg, msg' => withNamingContext nc (composePreservingKind msg msg')
+  | tagged t msg            , msg' => tagged t (compose msg msg')
+  | msg                     , msg' => compose msg msg'
+
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -401,6 +426,45 @@ structure SerialMessage extends BaseMessage String where
   kind          : Name
   deriving ToJson, FromJson
 
+/--
+A suffix added to diagnostic name-containing tags to indicate that they should be used as an error
+code.
+-/
+def errorNameSuffix := "_namedError"
+
+/--
+Produces a `MessageData` tagged with an identifier for error `name`.
+
+Note: this function generally should not be called directly; instead, use the macros `logNamedError`
+and `throwNamedError`.
+-/
+def MessageData.tagWithErrorName (msg : MessageData) (name : Name) : MessageData :=
+  .tagged (.str name errorNameSuffix) msg
+
+/--
+If the provided name is labeled as a diagnostic name, removes the label and returns the
+corresponding diagnostic name.
+
+Note: we use this labeling mechanism so that we can have error kinds that are not intended to be
+shown to the user, without having to validate the presence of an error explanation at runtime.
+-/
+def errorNameOfKind? : Name → Option Name
+  | .str p last => if last == errorNameSuffix then some p else none
+  | _ => none
+
+/--
+Returns the error name with which `msg` is tagged, if one exists.
+
+Note that this is distinct from `msg.kind`: the `kind` of a named-error message is not equal to its
+name, and there exist message kinds that are not error-name kinds.
+-/
+def MessageData.errorName? (msg : MessageData) : Option Name :=
+  errorNameOfKind? msg.kind
+
+@[inherit_doc MessageData.errorName?]
+def Message.errorName? (msg : Message) : Option Name :=
+  msg.data.errorName?
+
 namespace SerialMessage
 
 @[inline] def toMessage (msg : SerialMessage) : Message :=
@@ -413,8 +477,10 @@ protected def toString (msg : SerialMessage) (includeEndPos := false) : String :
     str := msg.caption ++ ":\n" ++ str
   match msg.severity with
   | .information => pure ()
-  | .warning     => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str
-  | .error       => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str
+  | .warning     =>
+    str := mkErrorStringWithPos msg.fileName msg.pos str endPos "warning" (errorNameOfKind? msg.kind)
+  | .error       =>
+    str := mkErrorStringWithPos msg.fileName msg.pos str endPos "error" (errorNameOfKind? msg.kind)
   if str.isEmpty || str.back != '\n' then
     str := str ++ "\n"
   return str
diff --git a/src/Lean/Meta/Hint.lean b/src/Lean/Meta/Hint.lean
index 2c2aa42daf..09a5d9bcbd 100644
--- a/src/Lean/Meta/Hint.lean
+++ b/src/Lean/Meta/Hint.lean
@@ -30,7 +30,12 @@ The props to this widget are of the following form:
     {"type": "unchanged", "text": "h"},
     {"type": "deletion", "text": "ello"},
     {"type": "insertion", "text": "i"}
-  ]
+  ],
+  "suggestion": "hi",
+  "range": {
+    "start": {"line": 100, "character": 0},
+    "end":   {"line": 100, "character": 5}
+  }
 }
 ```
 
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index 4c783474de..cb929cc045 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -86,7 +86,7 @@ export default function ({ suggestions, range, header, isInline, style }) {
     inner)
 }"
 
--- Because we can't reference `builtin_widget_module` in `Lean.Meta.Hint`, we add the attribute here
+-- Because we can't use `builtin_widget_module` in `Lean.Meta.Hint`, we add the attribute here
 attribute [builtin_widget_module] Hint.tryThisDiffWidget
 
 /-! # Code action -/
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 67aeeb136c..20e769bb24 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -858,6 +858,14 @@ builtin_initialize
   register_parser_alias                                                 openDecl
   register_parser_alias                                                 docComment
 
+/--
+Registers an error explanation.
+
+Note that the error name is not relativized to the current namespace.
+-/
+@[builtin_command_parser] def registerErrorExplanationStx := leading_parser
+  docComment >> "register_error_explanation " >> ident >> termParser
+
 end Command
 
 namespace Term
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 637cd2ddb8..98b44d7f97 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -1091,6 +1091,57 @@ def matchExprAlts (rhsParser : Parser) :=
 @[builtin_term_parser] def letExpr := leading_parser:leadPrec
   withPosition ("let_expr " >> matchExprPat >> " := " >> termParser >> checkColGt >> " | " >> termParser) >> optSemicolon termParser
 
+/--
+Throws an error exception, tagging the associated message as a named error with the specified name
+and validating that an associated error explanation exists. The message may be passed as an
+interpolated string or a `MessageData` term. The result of `getRef` is used as position information.
+-/
+@[builtin_term_parser] def throwNamedErrorMacro := leading_parser
+  "throwNamedError " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
+/--
+Throws an error exception, tagging the associated message as a named error with the specified name
+and validating that an associated error explanation exists. The error name must be followed by a
+`Syntax` at which the error is to be thrown. The message is the final argument and may be passed as
+an interpolated string or a `MessageData` term.
+-/
+@[builtin_term_parser] def throwNamedErrorAtMacro := leading_parser
+  "throwNamedErrorAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
+/--
+Logs an error, tagging the message as a named error with the specified name and validating that an
+associated error explanation exists. The message may be passed as an interpolated string or a
+`MessageData` term. The result of `getRef` is used as position information.
+-/
+@[builtin_term_parser] def logNamedErrorMacro := leading_parser
+  "logNamedError " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
+/--
+Logs an error, tagging the message as a named error with the specified name and validating that an
+associated error explanation exists. The error name must be followed by a `Syntax` at which the
+error is to be logged. The message is the final argument and may be passed as an interpolated string
+or a `MessageData` term.
+-/
+@[builtin_term_parser] def logNamedErrorAtMacro := leading_parser
+  "logNamedErrorAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
+/--
+Logs a warning, tagging the message as a named diagnostic with the specified name and validating
+that an associated error explanation exists. The message may be passed as an interpolated string or
+a `MessageData` term. The result of `getRef` is used as position information.
+-/
+@[builtin_term_parser] def logNamedWarningMacro := leading_parser
+  "logNamedWarning " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
+/--
+Logs a warning, tagging the message as a named diagnostic with the specified name and validating
+that an associated error explanation exists. The error name must be followed by a `Syntax` at which
+the warning is to be logged. The message is the final argument and may be passed as an interpolated
+string or a `MessageData` term.
+-/
+@[builtin_term_parser] def logNamedWarningAtMacro := leading_parser
+  "logNamedWarningAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 3489373948..66a1207394 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -246,6 +246,7 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool
   let message := match (← msgToInteractive m.data hasWidgets |>.toBaseIO) with
     | .ok msg => msg
     | .error ex => TaggedText.text s!"[error when printing message: {ex.toString}]"
-  pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent? }
+  let code? := (errorNameOfKind? m.kind).map (.string ·.toString)
+  pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent?, code? }
 
 end Lean.Widget
diff --git a/tests/lean/docstringLinkValidation.lean.expected.out b/tests/lean/docstringLinkValidation.lean.expected.out
index 531ac8b6e3..d25926d6fd 100644
--- a/tests/lean/docstringLinkValidation.lean.expected.out
+++ b/tests/lean/docstringLinkValidation.lean.expected.out
@@ -1,2 +1,2 @@
 docstringLinkValidation.lean:8:7-8:21: error: Missing documentation type
-docstringLinkValidation.lean:8:26-8:41: error: Unknown documentation type 'f'. Expected 'section'.
+docstringLinkValidation.lean:8:26-8:41: error: Unknown documentation type `f`. Expected one of the following: `section`, `errorExplanation`
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index 9f4bdc9e89..41109d2a78 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -31,7 +31,7 @@ Now validate the docstrings.
 /--
 error: Docstring errors for 'check': ⏎
    • "lean-manual://oops":
-    Unknown documentation type 'oops'. Expected 'section'.
+    Unknown documentation type `oops`. Expected one of the following: `section`, `errorExplanation`
 -/
 #guard_msgs in
 #eval show CommandElabM Unit from do
@@ -61,7 +61,7 @@ def checkResult (str : String) : CommandElabM Unit := do
     let errMsgs := result.1.map fun (⟨s, e⟩, msg) => m!" • {repr <| str.extract s e}:{indentD msg}"
     logInfo <| m!"Errors: {indentD <| MessageData.joinSep errMsgs.toList "\n"}\n\n"
 
-  let root ← manualRoot
+  let root := manualRoot
   logInfo m!"Result: {repr <| result.2.replace root "MANUAL/"}"
 
 
@@ -77,6 +77,10 @@ def checkResult (str : String) : CommandElabM Unit := do
 #guard_msgs in
 #eval checkResult "abc [](lean-manual://section/the-section-id)"
 
+/-- info: Result: "abc [](MANUAL/find/?domain=Manual.errorExplanation&name=Lean.MyErrorName)" -/
+#guard_msgs in
+#eval checkResult "abc [](lean-manual://errorExplanation/Lean.MyErrorName)"
+
 /--
 info: Result: "abc\n\nMANUAL/find/?domain=Verso.Genre.Manual.section&name=the-section-id\n\nmore text"
 -/
@@ -106,9 +110,9 @@ info: Errors: ⏎
    • "lean-manual://":
     Missing documentation type
    • "lean-manual://f":
-    Unknown documentation type 'f'. Expected 'section'.
+    Unknown documentation type `f`. Expected one of the following: `section`, `errorExplanation`
    • "lean-manual://a/":
-    Unknown documentation type 'a'. Expected 'section'.
+    Unknown documentation type `a`. Expected one of the following: `section`, `errorExplanation`
 
 ---
 info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b"
@@ -121,9 +125,9 @@ info: Errors: ⏎
    • "lean-manual://":
     Missing documentation type
    • "lean-manual://f":
-    Unknown documentation type 'f'. Expected 'section'.
+    Unknown documentation type `f`. Expected one of the following: `section`, `errorExplanation`
    • "lean-manual://a/b":
-    Unknown documentation type 'a'. Expected 'section'.
+    Unknown documentation type `a`. Expected one of the following: `section`, `errorExplanation`
 
 ---
 info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b "
@@ -151,7 +155,7 @@ info: Result: "a b c\nlean-manual://\n"
 /--
 error: Missing documentation type
 ---
-error: Unknown documentation type 'f'. Expected 'section'.
+error: Unknown documentation type `f`. Expected one of the following: `section`, `errorExplanation`
 -/
 #guard_msgs in
 /--
@@ -249,7 +253,7 @@ Stderr:
 /--
 info: Exit code: 0
 Stdout:
-(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 21 } }, "Expected one item after 'section', but got []")],
+(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 21 } }, "Expected one item after `section`, but got []")],
  "lean-manual://section\n")
 
 Stderr:
@@ -260,7 +264,8 @@ Stderr:
 /--
 info: Exit code: 0
 Stdout:
-(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 15 } }, "Unknown documentation type 's'. Expected 'section'.")],
+(#[({ start := { byteIdx := 0 }, stop := { byteIdx := 15 } },
+    "Unknown documentation type `s`. Expected one of the following: `section`, `errorExplanation`")],
  "lean-manual://s\n")
 
 Stderr:
@@ -302,13 +307,13 @@ It contains many further things of even greater lean-manual://section/aaaaa/bbbb
 The `lean-manual` URL scheme is used to link to the version of the Lean reference manual that
 corresponds to this version of Lean. Errors occurred while processing the links in this documentation
 comment:
- * ```lean-manual://invalid/link```: Unknown documentation type 'invalid'. Expected 'section'.
+ * ```lean-manual://invalid/link```: Unknown documentation type `invalid`. Expected one of the following: `section`, `errorExplanation`
 
  * ```lean-manual://```: Missing documentation type
 
  * ```lean-manual://section/```: Empty section ID
 
- * ```lean-manual://section/aaaaa/bbbb```: Expected one item after 'section', but got [aaaaa, bbbb]
+ * ```lean-manual://section/aaaaa/bbbb```: Expected one item after `section`, but got [aaaaa, bbbb]
 -/
 #guard_msgs in
 #eval show CommandElabM Unit from do