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

Author: jrr6

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

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

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

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

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}
+  }
 }
 ```
 

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

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