From 85dcca32998ace20c62a86a4f59022642791ca68 Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Tue, 24 Jun 2025 05:52:11 +0200
Subject: [PATCH 01/10] feat: add error explanation elaboration and manual page

---
 Manual.lean                       |   3 +
 Manual/ErrorExplanations.lean     |  83 ++++
 Manual/Meta/ErrorExplanation.lean | 705 ++++++++++++++++++++++++++++++
 static/search/domain-mappers.js   |  17 +
 static/search/search-box.css      |   1 +
 5 files changed, 809 insertions(+)
 create mode 100644 Manual/ErrorExplanations.lean
 create mode 100644 Manual/Meta/ErrorExplanation.lean

diff --git a/Manual.lean b/Manual.lean
index e936c652..15c023b7 100644
--- a/Manual.lean
+++ b/Manual.lean
@@ -14,6 +14,7 @@ import Manual.Defs
 import Manual.Classes
 import Manual.Axioms
 import Manual.Terms
+import Manual.ErrorExplanations
 import Manual.Tactics
 import Manual.Simp
 import Manual.BasicTypes
@@ -129,6 +130,8 @@ Overview of the standard library, including types from the prelude and those tha
 
 {include 0 Manual.BuildTools}
 
+{include 0 Manual.ErrorExplanations}
+
 {include 0 Manual.Releases}
 
 # Index
diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
new file mode 100644
index 00000000..92759350
--- /dev/null
+++ b/Manual/ErrorExplanations.lean
@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joseph Rotella
+-/
+
+import Manual.Meta.ErrorExplanation
+
+open Lean
+open Verso Doc Elab Genre Manual
+
+namespace Manual
+
+set_option pp.rawOnError true
+set_option guard_msgs.diff true
+
+
+def Inline.errorExplanationLink (errorName : Name) : Manual.Inline where
+  name := `Manual.Inline.errorExplanationLink
+  data := toJson errorName
+
+@[inline_extension Inline.errorExplanationLink]
+def Inline.errorExplanationLink.descr : InlineDescr where
+  traverse := fun _ _ _ => pure none
+  toTeX  := none
+  toHtml := some fun go _ data content =>
+    open Verso.Output.Html Verso.Doc.Html.HtmlT in do
+    let xref ← state
+    let .ok name := FromJson.fromJson? (α := String) data
+      | logError s!"Failed to parse error explanation link JSON: expected string, but found:\n{data}"
+        content.mapM go
+    let some obj := (← read).traverseState.getDomainObject? errorExplanationDomain name
+      | logError s!"Could not find explanation domain entry for name '{name}'"
+        content.mapM go
+    let some id := obj.getId
+      | logError s!"Could not find retrieve ID from explanation domain entry for name '{name}'"
+        content.mapM go
+    if let some { path, htmlId } := xref.externalTags.get? id then
+      let addr := path.link (some htmlId.toString)
+      pure {{<a class="technical-term" href={{addr}}>{{← content.mapM go}}</a>}}
+    else
+      logError s!"Could not find external tag for error explanation '{name}' corresponding to ID '{id}'"
+      content.mapM go
+
+@[block_role_expander error_explanation_table]
+def error_explanation_table : BlockRoleExpander
+  | #[], #[] => do
+    let entries ← getErrorExplanationsSorted
+    let columns := 4
+    let header := true
+    let name := "diagnostic-table"
+    let alignment : Option TableConfig.Alignment := none
+    let headers ← #["Name", "Summary", "Severity", "Since"]
+      |>.mapM fun s => ``(Verso.Doc.Block.para #[Doc.Inline.text $(quote s)])
+    let vals ← entries.flatMapM fun (name, explan) => do
+      let sev := quote <|
+        if explan.metadata.severity == .warning then "Warning" else "Error"
+      let sev ← ``(Doc.Inline.text $sev)
+      let nameStr := toString name
+      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name)) #[Doc.Inline.text $(quote nameStr)])
+      let summary ← ``(Doc.Inline.text $(quote explan.metadata.summary))
+      let since ← ``(Doc.Inline.text $(quote explan.metadata.sinceVersion))
+      #[nameLink, summary, sev, since]
+        |>.mapM fun s => ``(Verso.Doc.Block.para #[$s])
+    let blocks := (headers ++ vals).map fun c => Syntax.TSepArray.mk #[c]
+    pure #[← ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name) $(quote alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])]
+  | _, _ => throwError "unexpected syntax"
+
+-- Elaborating explanations can exceed the default heartbeat maximum:
+set_option maxHeartbeats 1000000
+
+#doc (Manual) "Error Explanations" =>
+%%%
+number := false
+htmlToc := false
+%%%
+
+This section provides explanations of errors and warnings that may be generated
+by Lean when processing a source file.
+
+{error_explanation_table}
+
+{make_explanations}
diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
new file mode 100644
index 00000000..d4f4926e
--- /dev/null
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -0,0 +1,705 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joseph Rotella
+-/
+
+import VersoManual
+
+import Manual.Meta
+
+import Lean.ErrorExplanations
+
+open Lean Elab
+open Verso.ArgParse
+open Verso.Doc Elab
+open Verso.Genre.Manual Markdown InlineLean
+open SubVerso.Highlighting
+
+set_option pp.rawOnError true
+set_option guard_msgs.diff true
+
+namespace Manual
+
+/--
+The directory in which MWE JSON files are written in the preprocessing step.
+-/
+private def exampleJSONDirectory : System.FilePath :=
+  "error_explanation_examples"
+
+/-- Loads the JSON data file for the preprocessed MWE code block `name`. -/
+def loadPreprocessedMWE (name : Name) (contents : String)
+    : MetaM (Highlighted × Array (MessageSeverity × String)) := do
+  let fileName : String := name.toString ++ ".json"
+  let path := exampleJSONDirectory / fileName
+  unless (← System.FilePath.pathExists path) do
+    throwError m!"Did not find expected preprocessed code block file `{path}`. \
+      Run `lake build error_explanations`."
+  let fileContents ← IO.FS.readFile path
+  let json ← ofExcept <| Json.parse fileContents
+  let hls ← ofExcept <| json.getObjVal? "highlighted"
+    >>= FromJson.fromJson? (α := Highlighted)
+  let messages ← ofExcept <| json.getObjVal? "messages"
+    >>= FromJson.fromJson? (α := Array (MessageSeverity × String))
+  let fileHash ← ofExcept <| json.getObjVal? "hash"
+    >>= FromJson.fromJson? (α := UInt64)
+  let fileVersion ← ofExcept <| json.getObjVal? "version" >>= Json.getStr?
+  unless fileHash == hash contents && fileVersion == Lean.versionString do
+    throwError m!"Preprocessed code block data file `{path}` is out of date. \
+      Run `lake build error_explanations`."
+  return (hls, messages)
+
+/--
+A modified version of `Verso.Genre.Manual.InlineLean.lean` for rendering an MWE
+in an error explanation.
+-/
+def explanationMWE : CodeBlockExpander
+  | args, str => Manual.withoutAsync <| do
+    let config ← LeanBlockConfig.parse.run args
+
+    let some name := config.name
+      | throwError "Explanation MWE is missing a name"
+    let (hls, msgs) ← loadPreprocessedMWE name str.getString
+    saveOutputs name msgs.toList
+
+    pure #[← ``(Block.other
+      (Block.lean $(quote hls) (some $(quote (← getFileName))) none)
+      #[Block.code $str])]
+
+/--
+A tabbed container for MWEs in an error explanation example. Must satisfy the
+invariant that `titles.size` is equal to the number of children of this block.
+-/
+def Block.tabbedMWEs (titles : Array String) : Block where
+  name := `Manual.Block.tabbedMWEs
+  data := toJson titles
+
+@[block_extension Block.tabbedMWEs]
+def Block.tabbedMWEs.descr : BlockDescr where
+  traverse id data _blocks := do
+    let name :=
+      match FromJson.fromJson? (α := Option String) data with
+      | .ok (some name) => name
+      | _ => "error-example"
+    discard <| externalTag id (← read).path name
+    pure none
+  toTeX := none
+  extraCss := [r#"
+.error-example-tabpanel-hidden {
+  display: none;
+}
+.error-example-container:not(:last-child) {
+  border-bottom: 1px solid gray;
+  padding-bottom: var(--verso--box-padding);
+}
+.error-example-tab-list [role="tab"] {
+  position: relative;
+  z-index: 1;
+  background: white;
+  border: 0;
+  padding: 0.2em;
+  cursor: pointer;
+}
+.error-example-tab-list [role="tab"]:not(:last-child) {
+  margin-right: 1rem;
+}
+.error-example-tab-list [role="tab"][aria-selected="true"] {
+  border-bottom: 1px solid gray;
+}
+  "#]
+  extraJs := [r#"
+window.addEventListener('DOMContentLoaded', () => {
+  const tabLists = document.querySelectorAll('.error-example-tab-list')
+  tabLists.forEach(tabList => {
+    const tabs = tabList.querySelectorAll(':scope > [role="tab"]')
+
+    const setActiveTab = (e) => {
+      for (const tab of tabs) {
+        const controllee = document.getElementById(tab.getAttribute('aria-controls'))
+        if (tab === e.target) {
+          tab.setAttribute('aria-selected', true)
+          controllee.classList.remove('error-example-tabpanel-hidden')
+        } else {
+          tab.setAttribute('aria-selected', false)
+          controllee.classList.add('error-example-tabpanel-hidden')
+        }
+      }
+    }
+
+    tabs.forEach(tab => {
+      tab.addEventListener('click', setActiveTab)
+    })
+
+    let focusedIdx = 0
+    tabList.addEventListener('keydown', e => {
+      if (e.key === 'ArrowRight' || e.key === 'ArrowLeft') {
+        tabs[focusedIdx].setAttribute('tabindex', -1)
+        focusedIdx =
+          e.key === 'ArrowRight'
+          ? (focusedIdx + 1) % tabs.length
+          : (focusedIdx - 1 + tabs.length) % tabs.length
+        tabs[focusedIdx].setAttribute('tabindex', 0)
+        tabs[focusedIdx].focus()
+      }
+    })
+  })
+})
+  "#]
+  toHtml := some fun _goI goB id info contents =>
+    open Verso.Doc.Html in
+    open Verso.Output Html in do
+    let .ok titles := FromJson.fromJson? (α := Array String) info
+      | HtmlT.logError "Invalid titles JSON for example block"
+        pure .empty
+    unless titles.size == contents.size do
+      HtmlT.logError s!"Mismatched number of titles and contents for example block: \
+        Found {contents.size} tab panels but {titles.size} titles."
+      return .empty
+    let some { htmlId, .. } := (← HtmlT.state).externalTags[id]?
+      | HtmlT.logError "Could not find tag for error example"
+        pure .empty
+    let buttons ← titles.mapIdxM fun i (title : String) => do
+      let (tabIndex, selected) := if i == 0 then ("0", "true") else ("-1", "false")
+      let idxStr := toString i
+      return {{
+        <button type="button" role="tab"
+            aria-selected={{selected}}
+            tabindex={{tabIndex}}
+            id={{s!"{htmlId.toString}-button-{idxStr}"}}
+            aria-controls={{s!"{htmlId.toString}-panel-{idxStr}"}}>
+          {{title}}
+        </button>
+      }}
+    let panels ← contents.mapIdxM fun i b => do
+      let className := if i == 0 then "" else "error-example-tabpanel-hidden"
+      let idxStr := toString i
+      return {{
+        <div role="tabpanel"
+            class={{className}}
+            id={{s!"{htmlId.toString}-panel-{idxStr}"}}
+            aria-labelledby={{s!"{htmlId.toString}-button-{i}"}}>
+          {{ ← goB b }}
+        </div>
+      }}
+    pure {{
+      <div class="error-example-container">
+        <div class="error-example-tab-list" role="tablist" aria-label="Code Samples">
+          {{buttons}}
+        </div>
+        <div class="error-example-tab-view">
+          {{panels}}
+        </div>
+      </div>
+    }}
+
+/--
+Given the name of the explanation in which it occurs and its index among all
+code blocks therein, generates a name for a code block in an error explanation.
+This is used for output tracking and to locate its corresponding JSON file.
+-/
+private def mkExampleName (errorName : Name) (idx : Nat) : Name :=
+  errorName ++ s!"block{idx}".toName
+
+structure ExplanCodeElabM.Context where
+  name : Name
+
+structure ExplanCodeElabM.State where
+  codeBlockIdx : Nat
+
+/--
+The monad in which code blocks within an error explanation are elaborated.
+-/
+abbrev ExplanCodeElabM :=
+  ReaderT ExplanCodeElabM.Context (StateT ExplanCodeElabM.State DocElabM)
+
+/--
+Attempts to elaborate block code in an error explanation: Lean (and unlabeled)
+blocks should have a corresponding preprocessing cache file, output blocks are
+checked against their corresponding Lean block's output, and all other code
+blocks are rendered using the default Verso code element.
+-/
+def tryElabErrorExplanationCodeBlock (errorName : Name) (errorSev : MessageSeverity)
+    (info? _lang : Option String) (str : String) : ExplanCodeElabM Term := do
+  if let some info := info? then
+    let { lang, kind?, .. } ← match ErrorExplanation.CodeInfo.parse info with
+      | .ok x => pure x
+      | .error e => throwError e
+    if lang == "output" then
+      let codeBlockIdx := (← get).codeBlockIdx - 1
+      let name := mkExampleName errorName codeBlockIdx
+      let args := #[(← `(argument| $(mkIdent name):ident))]
+      let parsedArgs ← parseArgs args
+      let blocks ← try
+        withFreshMacroScope <| leanOutput parsedArgs (quote str)
+      catch
+        | .error ref msg =>
+          let kindStr := kind?.map (s!" ({·} example)") |>.getD ""
+          -- Log rather than throw so we can detect all invalid outputs in a
+          -- single build
+          logErrorAt ref m!"Invalid output for {(← read).name} code block \
+            #{codeBlockIdx}{kindStr}: {msg}"
+          pure #[← ``(Verso.Doc.Block.code "<invalid output>")]
+        | e@(.internal ..) => throw e
+      return (← ``(Verso.Doc.Block.concat #[$blocks,*]))
+    else if lang == "" || lang == "lean" then
+      let mut args := #[]
+      let name := mkExampleName errorName (← get).codeBlockIdx
+      args := args.push (← `(argument| name := $(mkIdent name):ident))
+      if let some kind := kind? then
+        let errorVal ← if kind == .broken && errorSev == .error then
+          `(arg_val|true)
+        else
+          `(arg_val|false)
+        args := args.push (← `(argument| error := $errorVal))
+      let parsedArgs ← parseArgs args
+      let blocks ← withFreshMacroScope <| explanationMWE parsedArgs (quote str)
+      modify fun s => { s with codeBlockIdx := s.codeBlockIdx + 1 }
+      return (← ``(Verso.Doc.Block.concat #[$blocks,*]))
+  -- If this isn't labeled as an MWE, fall back on a basic code block
+  ``(Verso.Doc.Block.code $(quote str))
+
+/-- The code contents of an example, not including any subsequent description. -/
+private structure ExampleContents where
+  title : Array Term
+  codeBlocks : Array (Term × Option String)
+  descrBlocks : Array Term
+
+structure ExplanElabM.Context where
+  /-- The blocks in the error explanation to elaborate. -/
+  blocks : Array MD4Lean.Block
+  /-- Name of the error described by the explanation being elaborated. -/
+  name : Name
+  /-- Severity of error described by the explanation being elaborated. -/
+  severity : MessageSeverity
+
+structure ExplanElabM.State where
+  /-- The index of the next block in the context's `blocks` to elaborate. -/
+  blockIdx : Nat := 0
+  /-- Active Markdown header levels that can be closed by subsequent Markdown -/
+  levels : List (Nat × Nat) := []
+  /-- The index of the current code block within this explanation. -/
+  codeBlockIdx : Nat := 0
+
+/-- The monad in which error explanations are elaborated. -/
+abbrev ExplanElabM := ReaderT ExplanElabM.Context (StateT ExplanElabM.State PartElabM)
+
+def ExplanElabM.run (x : ExplanElabM α) (name : Name)
+    (severity : MessageSeverity) (blocks : Array MD4Lean.Block) :
+    PartElabM (α × ExplanElabM.State) :=
+  ReaderT.run x { name, blocks, severity } |>.run {}
+
+def ExplanElabM.nextBlock? : ExplanElabM (Option MD4Lean.Block) := do
+  let curBlockIdx := (← get).blockIdx
+  let blocks := (← read).blocks
+  if h : curBlockIdx ≥ blocks.size then
+    return none
+  else
+    modify fun s => { s with blockIdx := s.blockIdx + 1 }
+    return blocks[curBlockIdx]
+
+def ExplanElabM.backtrack : ExplanElabM Unit := do
+  modify fun s => { s with blockIdx := s.blockIdx - 1 }
+
+def ExplanElabM.liftExplanCodeElabM (x : ExplanCodeElabM α) : ExplanElabM α := do
+  let { codeBlockIdx, .. } ← get
+  let { name, .. } ← read
+  let (res, st) ← x.run { name } { codeBlockIdx }
+  modify fun s => { s with codeBlockIdx := st.codeBlockIdx }
+  return res
+
+instance : MonadLift ExplanCodeElabM ExplanElabM where
+  monadLift := ExplanElabM.liftExplanCodeElabM
+
+/--
+Elaborates inline code in strict mode, restoring the state afterward.
+
+We have to do state restoration after each inline elaboration because the block
+elaborator needs to have its `TermElabM` state changes persisted, as the part
+elaborator modifies this state during elaboration.
+-/
+private def tryElabInlineCodeStrictRestoringState
+    (tactics : Array Tactic.Doc.TacticDoc) (keywords : Array String)
+    (prevWord? : Option String) (str : String) : ExplanElabM Term := do
+  let b ← (saveState : TermElabM _)
+  try
+    let t ← tryElabInlineCodeStrict tactics keywords prevWord? str
+    Term.synthesizeSyntheticMVarsUsingDefault
+    pure t
+  finally
+    b.restore
+
+/-- Returns a Verso term corresponding to `b`. -/
+def blockFromExplanationMarkdown (b : MD4Lean.Block) : ExplanElabM Term := do
+  let { name, severity .. } ← read
+  let tactics ← Elab.Tactic.Doc.allTacticDocs
+  let keywords := tactics.map (·.userName)
+  let ref ← getRef
+  blockFromMarkdown b
+    (handleHeaders := Markdown.strongEmphHeaders)
+    (elabInlineCode := some (tryElabInlineCodeStrictRestoringState tactics keywords))
+    (elabBlockCode := some fun i l s => withRef ref <|
+      tryElabErrorExplanationCodeBlock name severity i l s)
+
+/-- Add block(s) corresponding to `b` to the current document part. -/
+def addPartFromExplanationMarkdown (b : MD4Lean.Block) : ExplanElabM Unit := do
+  let tactics ← Elab.Tactic.Doc.allTacticDocs
+  let keywords := tactics.map (·.userName)
+  let ref ← getRef
+  let {name, severity .. } ← read
+  let ls ← addPartFromMarkdown b
+    (handleHeaders := Markdown.strongEmphHeaders)
+    (elabInlineCode := some (tryElabInlineCodeStrictRestoringState tactics keywords))
+    (elabBlockCode := some fun i l s => withRef ref <|
+      tryElabErrorExplanationCodeBlock name severity i l s)
+  modifyThe ExplanElabM.State ({ · with levels := ls })
+
+/-- Extracts and parses the info string of a code block. -/
+private def infoOfCodeBlock : MD4Lean.Block → Except String ErrorExplanation.CodeInfo
+  | .code info _ _ _ => do
+    let txt ← attr' info
+    ErrorExplanation.CodeInfo.parse txt
+  | el => .error s!"Cannot get code block info from non-code block element:\n{repr el}"
+
+/--
+Returns `true` if `b` is a block with language `expLang` and, if
+`expKind? = some expKind`, kind `expKind`.
+-/
+private def blockHasExplanationCodeInfo
+    (b : MD4Lean.Block) (expLang : String)
+    (expKind? : Option ErrorExplanation.CodeInfo.Kind := none)
+    : DocElabM Bool := do
+  let { kind?, lang, .. } ← match infoOfCodeBlock b with
+  | .ok x => pure x
+  | .error _ => return false
+  let optMatch {α : Type} [BEq α] (expected? : Option α) (actual? : Option α) :=
+    if let some expected := expected? then
+      some expected == actual?
+    else
+      true
+  return lang == expLang && optMatch expKind? kind?
+
+/-- Throws an error if `b` is not a code block with language `expLang` and kind `expKind`. -/
+private def expectExplanationCodeInfo
+    (b : MD4Lean.Block) (expLang : String) (expKind : ErrorExplanation.CodeInfo.Kind)
+    : DocElabM Unit := do
+  let { kind?, lang, .. } ← match infoOfCodeBlock b with
+    | .ok x => pure x
+    | .error e => throwError  e
+  unless lang == expLang do
+    throwError "Expected a code block with language `{expLang}`, but found `{lang}`"
+  unless kind? == some expKind do
+    let str := kind?.map toString |>.getD "unspecified"
+    throwError "Expected a code block of kind `{expKind}`, but found `{str}`"
+
+/-- Returns `true` if `txt` is the "Examples" header text. -/
+private def isExamplesHeaderText (txt : Array MD4Lean.Text) : Bool :=
+  if _ : txt.size = 1 then
+    match txt[0] with
+    | .normal str => str.trim == "Examples"
+    | _ => false
+  else false
+
+/-- Convert the accumulated contents of an example into a Verso block term. -/
+private def makeExample (contents : ExampleContents) : DocElabM Term := do
+  let {title, codeBlocks, descrBlocks } := contents
+  let titles := codeBlocks.mapIdx fun i (_, title?) =>
+    let fallback :=
+      if i == 0 then
+        "Original"
+      else if codeBlocks.size == 2 then
+        "Fixed"
+      else
+        s!"Fixed {i}"
+    title?.getD fallback
+  let codeBlocks := codeBlocks.map Prod.fst
+  let codeExample ←
+    ``(Block.other (Block.tabbedMWEs $(quote titles)) #[$codeBlocks,*])
+  ``(Block.other (Block.example none (opened := true))
+      #[Block.para #[$title,*], $codeExample, $descrBlocks,*])
+
+private def titleOfCodeBlock? (b : MD4Lean.Block) : Option String := do
+  let info ← infoOfCodeBlock b |>.toOption
+  info.title?
+
+/-- Closes the last-opened section, throwing an error on failure. -/
+def closeEnclosingSection : PartElabM Unit := do
+  -- We use `default` as the source position because the Markdown doesn't have one
+  if let some ctxt' := (← getThe PartElabM.State).partContext.close default then
+    modifyThe PartElabM.State fun st => {st with partContext := ctxt'}
+  else
+    throwError m!"Failed to close the last-opened explanation part"
+
+/-- Adds explanation blocks until the "Examples" header is reached. -/
+def addNonExampleBlocks := do
+  repeat
+    let some block ← ExplanElabM.nextBlock?
+      | return
+    if let MD4Lean.Block.header 1 txt := block then
+      if isExamplesHeaderText txt then
+        addPartFromExplanationMarkdown block
+        break
+    addPartFromExplanationMarkdown block
+
+/--
+Get the next code block if it's a broken Lean block along with its title.
+
+Note that this function errors on failure, since we never backtrack if a broken
+code block is missing, and doing so allows us to provide more granular error
+messages.
+-/
+def getBrokenTermAndTitle : ExplanElabM (Term × Option String) := do
+  let some brokenBlock ← ExplanElabM.nextBlock?
+    | throwError "Found a header for a new example, but no following `broken` code block"
+  -- We don't bother backtracking here since we can't recover
+  expectExplanationCodeInfo brokenBlock "lean" .broken
+  let brokenTerm ← blockFromExplanationMarkdown brokenBlock
+  let title? := titleOfCodeBlock? brokenBlock
+  return (brokenTerm, title?)
+
+/-- Execute `x` until it returns `none`. -/
+partial def repeatedly (x : ExplanElabM (Option α)) : ExplanElabM (Array α) :=
+  go x #[]
+where
+  go x acc := do
+    if let some result := (← x) then
+      go x (acc.push result)
+    else
+      return acc
+
+/-- Get the next block if it is an output code block. -/
+def getOutputTerm? : ExplanElabM (Option Term) := do
+  let some block ← ExplanElabM.nextBlock?
+    | return none
+  if (← blockHasExplanationCodeInfo block "output") then
+    return some (← blockFromExplanationMarkdown block)
+  else
+    ExplanElabM.backtrack
+    return none
+
+/-- Get the next code block if it is a fixed Lean block, and, if so, its title if it has one. -/
+def getFixedTermAndTitle? : ExplanElabM (Option (Term × Option String)) := do
+  let some block ← ExplanElabM.nextBlock?
+    | return none
+  if (← blockHasExplanationCodeInfo block "lean" (some .fixed)) then
+    let title? := titleOfCodeBlock? block
+    return some (← blockFromExplanationMarkdown block, title?)
+  else
+    ExplanElabM.backtrack
+    return none
+
+/-- Get the next block(s) if they are a fixed code block with zero or more outputs. -/
+def getFixedTermAndOutputs? : ExplanElabM (Option (Term × Array Term × Option String)) := do
+  let some (fixedTerm, fixedTitle?) ← getFixedTermAndTitle? | return none
+  let outputs ← repeatedly getOutputTerm?
+  return some (fixedTerm, outputs, fixedTitle?)
+
+/-- Get the next block to elaborate if it's not an example-terminating header. -/
+def getExampleDescriptionTerm? : ExplanElabM (Option Term) := do
+  let some block ← ExplanElabM.nextBlock?
+    | return none
+  if block matches .header 1 _ | .header 2 _ then
+    ExplanElabM.backtrack
+    return none
+  else
+    return some (← blockFromExplanationMarkdown block)
+
+/--
+Add blocks corresponding to the "Examples" section of the explanation. Assumes
+that the "Examples" header itself has already been added, and will repeatedly
+add examples beginning with a level-2 header, followed by broken and fixed code
+blocks with outputs, and descriptions thereof.
+-/
+def addExampleBlocks : ExplanElabM Unit := do
+  repeat
+    let some block@(.header 2 titleTexts) ← ExplanElabM.nextBlock? | return
+    let `(Verso.Doc.Block.other #[$titleStxs,*]) ← blockFromMarkdown block
+        [fun (stxs : Array Term) => ``(Verso.Doc.Block.other #[$stxs,*])]
+      | throwError "Unexpected output when elaborating example header"
+    let title := titleStxs.getElems
+    let titleStr := String.join
+      (titleTexts.mapM stringFromMarkdownText |>.toOption.getD #[]).toList
+
+    -- Broken code and output(s)
+    let (brokenCodeTerm, brokenTitle?) ← getBrokenTermAndTitle
+    let brokenOutputTerms ← repeatedly getOutputTerm?
+    if brokenOutputTerms.isEmpty then
+      throwError m!"Missing output for broken code snippet in example '{titleStr}'"
+    let brokenWithTitle :=
+      (← ``(Block.concat #[$brokenCodeTerm, $brokenOutputTerms,*]), brokenTitle?)
+
+    -- Fixed version(s) with optional output(s)
+    let fixedTermsAndOutputs ← repeatedly getFixedTermAndOutputs?
+    if fixedTermsAndOutputs.isEmpty then
+      throwError m!"Found a `broken` code block but no following `fixed` code block for example '{titleStr}'"
+    let fixedWithTitles ← fixedTermsAndOutputs.mapM fun (code, outs, title?) =>
+      return (← ``(Block.concat #[$code, $outs,*]), title?)
+
+    -- Arbitrary description of above code blocks
+    let exampleDescrs ← repeatedly getExampleDescriptionTerm?
+    let exampleInfo : ExampleContents := {
+      title
+      codeBlocks := #[brokenWithTitle] ++ fixedWithTitles
+      descrBlocks := exampleDescrs
+    }
+    let ex ← makeExample exampleInfo
+    PartElabM.addBlock ex
+
+/--
+Adds blocks constituting the explanation body to the document. The topmost
+routine for rendering an explanation in `ExplanElabM`.
+-/
+def addExplanationBodyBlocks : ExplanElabM Unit := do
+  addNonExampleBlocks
+  addExampleBlocks
+
+deriving instance Quote for ErrorExplanation.Metadata
+
+def Block.errorExplanationMetadata (metadata : ErrorExplanation.Metadata) : Block where
+  name := `Manual.Block.errorExplanationMetadata
+  data := toJson metadata
+
+@[block_extension Block.errorExplanationMetadata]
+def Block.errorExplanationMetadata.descr : BlockDescr where
+  traverse _ _ _ := pure none
+  toTeX := none
+  extraCss := ["
+  .error-explanation-metadatum:not(:last-child):after {
+    content: '|';
+    margin: 0 10px;
+  }
+  .error-explanation-removed-warning {
+    border: 1px solid var(--verso-warning-color);
+    border-radius: 0.5rem;
+    padding-left: var(--verso--box-padding);
+    padding-right: var(--verso--box-padding);
+  }
+  "]
+  toHtml := some fun _goI _goB _id info _contents =>
+    open Verso.Doc.Html in
+    open Verso.Output Html in do
+    let .ok metadata := FromJson.fromJson? (α := ErrorExplanation.Metadata) info
+      | HtmlT.logError "Failed to parse info for error explanation metadata block:\n{metadata}"
+        pure .empty
+    let deprecatedWarning :=
+      if metadata.removedVersion?.isSome then
+        {{ <div class="error-explanation-removed-warning">
+             <p><strong>"Note: "</strong> "This diagnostic is no longer produced."</p>
+           </div> }}
+      else
+        .empty
+    let sevText := if metadata.severity matches .warning then "Warning" else "Error"
+    let entries := #[("Severity", sevText), ("Since", metadata.sinceVersion)]
+      ++ (metadata.removedVersion?.map fun v => #[("Removed", v)]).getD #[]
+    let entries := entries.map fun (label, data) =>
+      {{ <span class="error-explanation-metadatum">
+           <strong>{{Html.text true label}}": "</strong>
+           {{Html.text true data}}
+          </span> }}
+    return {{
+      <div class="error-explanation-metadata">
+        {{deprecatedWarning}}
+        <p><em>{{metadata.summary}}</em></p>
+        <p>{{entries}}</p>
+        <hr />
+      </div>
+    }}
+
+/-- Adds the specified explanation metadata to the document. -/
+def addExplanationMetadata (metadata : ErrorExplanation.Metadata) : PartElabM Unit := do
+  PartElabM.addBlock (← ``(Block.other (Block.errorExplanationMetadata $(quote metadata)) #[]))
+
+/-- Adds the metadata and bofy of the explanation with name `name` to the document. -/
+def addExplanationBlocksFor (name : Name) : PartElabM Unit := do
+  let explan? ← getErrorExplanation? name
+  match explan? with
+  | .none =>
+    throwError m!"Adding explanation blocks failed: Could not find explanation for {name}"
+  | some explan =>
+    try
+      let some ast := MD4Lean.parse explan.doc
+        | throwErrorAt (← getRef) "Failed to parse docstring as Markdown"
+      addExplanationMetadata explan.metadata
+      let (_, { levels, .. }) ← addExplanationBodyBlocks.run name explan.metadata.severity ast.blocks
+      for _ in levels do
+        closeEnclosingSection
+    catch
+      | .error ref msg => throw <| .error ref m!"Failed to process explanation for {name}: {msg}"
+      | e => throw e
+
+def errorExplanationDomain := `Manual.errorExplanation
+
+def Inline.errorExplanation (errorName : Name) (summary : String) : Inline where
+  name := `Manual.Inline.errorExplanation
+  data := toJson #[errorName.toString, summary]
+
+@[inline_extension Inline.errorExplanation]
+def Inline.errorExplanation.descr : InlineDescr where
+  init st := st
+    |>.setDomainTitle errorExplanationDomain "Error Explanations"
+    |>.setDomainDescription errorExplanationDomain
+        "Explanations of error messages and warnings produced during compilation"
+
+  traverse id info _ := do
+    let .ok #[errorName, summary] := FromJson.fromJson? (α := Array String) info
+      | logError s!"Invalid JSON for error explanation:\n{info}"; pure none
+    modify fun s =>
+      s |>.saveDomainObject errorExplanationDomain errorName id
+        |>.saveDomainObjectData errorExplanationDomain errorName (json%{"summary": $summary})
+    let path ← (·.path) <$> read
+    discard <| Verso.Genre.Manual.externalTag id path errorName
+    pure none
+
+  toTeX := none
+  toHtml := some fun go id _info contents =>
+    open Verso.Doc.Html in
+    open Verso.Output Html in do
+    let xref ← HtmlT.state
+    let idAttr := xref.htmlId id
+    return {{
+      <span {{idAttr}}>
+        {{← contents.mapM go}}
+      </span>
+    }}
+
+/-- Configuration for an `explanation` block. -/
+structure ExplanationConfig where
+  name : Ident
+
+def ExplanationConfig.parser [Monad m] [MonadError m] : ArgParse m ExplanationConfig :=
+  ExplanationConfig.mk <$> .positional `name {
+    description := "name of error whose explanation to display",
+    get := fun
+      | .name x => pure x
+      | other => throwError "Expected error name, got {repr other}"
+  }
+
+/-- Renders the error explanation for `name` via `{explanation name}`. -/
+@[part_command Verso.Syntax.block_role]
+def explanation : PartCommand
+  | `(block|block_role{explanation $args*}) => do
+    let config ← ExplanationConfig.parser.run (← parseArgs args)
+    addExplanationBlocksFor config.name.getId
+  | _ => Lean.Elab.throwUnsupportedSyntax
+
+open Verso Doc Elab ArgParse in
+open Lean in
+/-- Renders all error explanations as parts of the current page. -/
+@[part_command Verso.Syntax.block_role]
+def make_explanations : PartCommand
+  | `(block|block_role{make_explanations}) => do
+    let explans ← getErrorExplanationsSorted
+    for (name, explan) in explans do
+      let titleString := name.toString
+      let titleBits := #[← ``(Inline.other
+        (Inline.errorExplanation $(quote name) $(quote explan.metadata.summary))
+        #[Inline.text $(quote titleString)])]
+      PartElabM.push {
+        titleSyntax := quote (k := `str) titleString,
+        expandedTitle := some (titleString, titleBits),
+        metadata := none,
+        blocks := #[],
+        priorParts := #[]
+      }
+      addExplanationBlocksFor name
+      closeEnclosingSection
+  | _ => throwUnsupportedSyntax
diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js
index 7162507b..16010b6a 100644
--- a/static/search/domain-mappers.js
+++ b/static/search/domain-mappers.js
@@ -225,6 +225,22 @@ const lakeTomlTableMapper = {
   displayName: "Lake TOML Table",
 };
 
+/**
+ * @type {DomainMapper}
+ */
+const errorExplanationMapper = {
+  dataToSearchables: (domainData) =>
+    Object.entries(domainData.contents).map(([key, value]) => {
+      return {
+        searchKey: key,
+        address: `${value[0].address}#${value[0].id}`,
+        domainId: "Manual.errorExplanation",
+        ref: value,
+      }}),
+  className: "error-explanation-domain",
+  displayName: "Error Explanation",
+};
+
 export const domainMappers = {
   "Verso.Genre.Manual.doc": docDomainMapper,
   "Verso.Genre.Manual.doc.option": docOptionDomainMapper,
@@ -240,4 +256,5 @@ export const domainMappers = {
   "Manual.lakeTomlField": lakeTomlFieldMapper,
   "Manual.elanCommand": elanCommandMapper,
   "Manual.elanOpt": elanOptMapper,
+  "Manual.errorExplanation": errorExplanationMapper
 };
diff --git a/static/search/search-box.css b/static/search/search-box.css
index 9d783b5b..a5da3816 100644
--- a/static/search/search-box.css
+++ b/static/search/search-box.css
@@ -120,6 +120,7 @@
 #search-wrapper .search-result.elan-option-domain,
 #search-wrapper .search-result.env-var-domain,
 #search-wrapper .search-result.lake-command-domain,
+#search-wrapper .search-result.error-explanation-domain,
 #search-wrapper .search-result.elan-command-domain {
   font-family: var(--verso-code-font-family);
 }

From 922b7a0ac7a58d58a2e729dda85c66e8a2454a02 Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Wed, 25 Jun 2025 21:08:36 +0200
Subject: [PATCH 02/10] chore: update for new preprocessing scheme

---
 Manual/Meta/ErrorExplanation.lean | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index d4f4926e..28f8c6c8 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -10,6 +10,8 @@ import Manual.Meta
 
 import Lean.ErrorExplanations
 
+import PreprocessedExplanations
+
 open Lean Elab
 open Verso.ArgParse
 open Verso.Doc Elab
@@ -21,17 +23,11 @@ set_option guard_msgs.diff true
 
 namespace Manual
 
-/--
-The directory in which MWE JSON files are written in the preprocessing step.
--/
-private def exampleJSONDirectory : System.FilePath :=
-  "error_explanation_examples"
-
 /-- Loads the JSON data file for the preprocessed MWE code block `name`. -/
 def loadPreprocessedMWE (name : Name) (contents : String)
     : MetaM (Highlighted × Array (MessageSeverity × String)) := do
   let fileName : String := name.toString ++ ".json"
-  let path := exampleJSONDirectory / fileName
+  let path := preprocessedExplanationsRoot / fileName
   unless (← System.FilePath.pathExists path) do
     throwError m!"Did not find expected preprocessed code block file `{path}`. \
       Run `lake build error_explanations`."

From 0eb502ba4967d6cba09328a799185e0bbff12191 Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Wed, 25 Jun 2025 21:15:59 +0200
Subject: [PATCH 03/10] chore: adopt new macros for `{block,inline}_extension`

---
 Manual/ErrorExplanations.lean     |  6 +-----
 Manual/Meta/ErrorExplanation.lean | 14 +++-----------
 2 files changed, 4 insertions(+), 16 deletions(-)

diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
index 92759350..9b4be432 100644
--- a/Manual/ErrorExplanations.lean
+++ b/Manual/ErrorExplanations.lean
@@ -15,12 +15,8 @@ set_option pp.rawOnError true
 set_option guard_msgs.diff true
 
 
-def Inline.errorExplanationLink (errorName : Name) : Manual.Inline where
-  name := `Manual.Inline.errorExplanationLink
+inline_extension Inline.errorExplanationLink (errorName : Name) where
   data := toJson errorName
-
-@[inline_extension Inline.errorExplanationLink]
-def Inline.errorExplanationLink.descr : InlineDescr where
   traverse := fun _ _ _ => pure none
   toTeX  := none
   toHtml := some fun go _ data content =>
diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index 28f8c6c8..3a720254 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -62,16 +62,12 @@ def explanationMWE : CodeBlockExpander
       (Block.lean $(quote hls) (some $(quote (← getFileName))) none)
       #[Block.code $str])]
 
-/--
+/-
 A tabbed container for MWEs in an error explanation example. Must satisfy the
 invariant that `titles.size` is equal to the number of children of this block.
 -/
-def Block.tabbedMWEs (titles : Array String) : Block where
-  name := `Manual.Block.tabbedMWEs
+block_extension Block.tabbedMWEs (titles : Array String) where
   data := toJson titles
-
-@[block_extension Block.tabbedMWEs]
-def Block.tabbedMWEs.descr : BlockDescr where
   traverse id data _blocks := do
     let name :=
       match FromJson.fromJson? (α := Option String) data with
@@ -550,12 +546,8 @@ def addExplanationBodyBlocks : ExplanElabM Unit := do
 
 deriving instance Quote for ErrorExplanation.Metadata
 
-def Block.errorExplanationMetadata (metadata : ErrorExplanation.Metadata) : Block where
-  name := `Manual.Block.errorExplanationMetadata
+block_extension Block.errorExplanationMetadata (metadata : ErrorExplanation.Metadata) where
   data := toJson metadata
-
-@[block_extension Block.errorExplanationMetadata]
-def Block.errorExplanationMetadata.descr : BlockDescr where
   traverse _ _ _ := pure none
   toTeX := none
   extraCss := ["

From d538c5cd83fd6cdd64691eeec2a6f0bd8c89d482 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Thu, 26 Jun 2025 06:20:50 +0200
Subject: [PATCH 04/10] chore: make prose linter skip error explanations

---
 .vale/scripts/rewrite_html.py | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.vale/scripts/rewrite_html.py b/.vale/scripts/rewrite_html.py
index 4639b910..c6d29718 100644
--- a/.vale/scripts/rewrite_html.py
+++ b/.vale/scripts/rewrite_html.py
@@ -30,6 +30,13 @@ def process_html_file(filepath, output_filepath):
         elif code_tag.attrs and 'class' in code_tag.attrs and 'hl' in code_tag['class'] and 'lean' in code_tag['class']:
             code_tag.decompose()
 
+    # Delete all content in error explanation pages. This comes from the lean4 repo
+    # and shouldn't be linted here.
+    for element in soup.find_all(class_='error-example-container'):
+        in_sections = element.find_parents('section')
+        if in_sections:
+            in_sections[-1].decompose()
+
     # Delete docstring content (for now)
     for element in soup.find_all(class_="namedocs"):
         element.decompose()

From 25fc82df8f5838edfa7b18cd6a819e409e1896ca Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Thu, 26 Jun 2025 20:34:49 +0200
Subject: [PATCH 05/10] fix: stop explanation example descriptions from
 "jumping" on tab switch

---
 Manual/Meta/ErrorExplanation.lean | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index 3a720254..ad38c869 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -77,9 +77,6 @@ block_extension Block.tabbedMWEs (titles : Array String) where
     pure none
   toTeX := none
   extraCss := [r#"
-.error-example-tabpanel-hidden {
-  display: none;
-}
 .error-example-container:not(:last-child) {
   border-bottom: 1px solid gray;
   padding-bottom: var(--verso--box-padding);
@@ -97,6 +94,22 @@ block_extension Block.tabbedMWEs (titles : Array String) where
 }
 .error-example-tab-list [role="tab"][aria-selected="true"] {
   border-bottom: 1px solid gray;
+}
+/* this rule and the following ensure that all tabs are the same height */
+.error-example-tab-view {
+  display: flex;
+}
+.error-example-tabpanel {
+  margin-right: -100%;
+  width: 100%;
+  display: block;
+}
+.error-example-tabpanel.error-example-tabpanel-hidden {
+  visibility: hidden;
+}
+.error-example-tabpanel .hl.lean .token {
+  /* unset transition to avoid lag when switching panels */
+  transition: visibility 0s;
 }
   "#]
   extraJs := [r#"
@@ -163,7 +176,7 @@ window.addEventListener('DOMContentLoaded', () => {
         </button>
       }}
     let panels ← contents.mapIdxM fun i b => do
-      let className := if i == 0 then "" else "error-example-tabpanel-hidden"
+      let className := "error-example-tabpanel" ++ if i == 0 then "" else " error-example-tabpanel-hidden"
       let idxStr := toString i
       return {{
         <div role="tabpanel"

From d7fc1bee33c99d4ff2261b965ff7519089945b46 Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Thu, 26 Jun 2025 20:42:58 +0200
Subject: [PATCH 06/10] chore: use code font for explanation names

---
 Manual/ErrorExplanations.lean     | 4 ++--
 Manual/Meta/ErrorExplanation.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
index 9b4be432..e186adcd 100644
--- a/Manual/ErrorExplanations.lean
+++ b/Manual/ErrorExplanations.lean
@@ -44,7 +44,7 @@ def error_explanation_table : BlockRoleExpander
     let entries ← getErrorExplanationsSorted
     let columns := 4
     let header := true
-    let name := "diagnostic-table"
+    let name := "error-explanation-table"
     let alignment : Option TableConfig.Alignment := none
     let headers ← #["Name", "Summary", "Severity", "Since"]
       |>.mapM fun s => ``(Verso.Doc.Block.para #[Doc.Inline.text $(quote s)])
@@ -53,7 +53,7 @@ def error_explanation_table : BlockRoleExpander
         if explan.metadata.severity == .warning then "Warning" else "Error"
       let sev ← ``(Doc.Inline.text $sev)
       let nameStr := toString name
-      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name)) #[Doc.Inline.text $(quote nameStr)])
+      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name)) #[Doc.Inline.code $(quote nameStr)])
       let summary ← ``(Doc.Inline.text $(quote explan.metadata.summary))
       let since ← ``(Doc.Inline.text $(quote explan.metadata.sinceVersion))
       #[nameLink, summary, sev, since]
diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index ad38c869..405c33d8 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -693,7 +693,7 @@ def make_explanations : PartCommand
       let titleString := name.toString
       let titleBits := #[← ``(Inline.other
         (Inline.errorExplanation $(quote name) $(quote explan.metadata.summary))
-        #[Inline.text $(quote titleString)])]
+        #[Inline.code $(quote titleString)])]
       PartElabM.push {
         titleSyntax := quote (k := `str) titleString,
         expandedTitle := some (titleString, titleBits),

From 0c92d66ca10f479ee36cf4f3037e0c9ea4b944ad Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Thu, 26 Jun 2025 22:38:02 +0200
Subject: [PATCH 07/10] chore: update remaining non-macro extension

---
 Manual/Meta/ErrorExplanation.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index 405c33d8..32328181 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -629,12 +629,8 @@ def addExplanationBlocksFor (name : Name) : PartElabM Unit := do
 
 def errorExplanationDomain := `Manual.errorExplanation
 
-def Inline.errorExplanation (errorName : Name) (summary : String) : Inline where
-  name := `Manual.Inline.errorExplanation
+inline_extension Inline.errorExplanation (errorName : Name) (summary : String) where
   data := toJson #[errorName.toString, summary]
-
-@[inline_extension Inline.errorExplanation]
-def Inline.errorExplanation.descr : InlineDescr where
   init st := st
     |>.setDomainTitle errorExplanationDomain "Error Explanations"
     |>.setDomainDescription errorExplanationDomain

From a6000da9e66b1cb704b21b9bbbf2dc92084448fd Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Fri, 27 Jun 2025 01:32:17 +0200
Subject: [PATCH 08/10] fix: improve error name rendering in narrower viewports

This commit drops error name prefixes from the table and sidebar and allows hyphenation at reasonable split points.
---
 Manual/ErrorExplanations.lean     | 24 +++++++++++++++++++-----
 Manual/Meta/ErrorExplanation.lean | 20 +++++++++++++++++++-
 2 files changed, 38 insertions(+), 6 deletions(-)

diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
index e186adcd..b0cc94a7 100644
--- a/Manual/ErrorExplanations.lean
+++ b/Manual/ErrorExplanations.lean
@@ -38,6 +38,20 @@ inline_extension Inline.errorExplanationLink (errorName : Name) where
       logError s!"Could not find external tag for error explanation '{name}' corresponding to ID '{id}'"
       content.mapM go
 
+/- Renders the suffix of an error explanation, allowing line breaks before capital letters. -/
+inline_extension Inline.errorExplanationShortName (errorName : Name) where
+  data := toJson (getBreakableSuffix errorName)
+  traverse := fun _ _ _ => pure none
+  extraCss := [".error-explanation-short-name { hyphenate-character: ''; }"]
+  toTeX := none
+  toHtml := some fun _go _id info _content =>
+    open Verso.Output Html in do
+    let .ok (some errorName) := fromJson? (α := Option String) info
+      | HtmlT.logError "Invalid data for explanation name element"
+        pure .empty
+    let html := {{ <code class="error-explanation-short-name">{{errorName}}</code> }}
+    return html
+
 @[block_role_expander error_explanation_table]
 def error_explanation_table : BlockRoleExpander
   | #[], #[] => do
@@ -49,11 +63,10 @@ def error_explanation_table : BlockRoleExpander
     let headers ← #["Name", "Summary", "Severity", "Since"]
       |>.mapM fun s => ``(Verso.Doc.Block.para #[Doc.Inline.text $(quote s)])
     let vals ← entries.flatMapM fun (name, explan) => do
-      let sev := quote <|
-        if explan.metadata.severity == .warning then "Warning" else "Error"
+      let sev := quote <| if explan.metadata.severity == .warning then "Warning" else "Error"
       let sev ← ``(Doc.Inline.text $sev)
-      let nameStr := toString name
-      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name)) #[Doc.Inline.code $(quote nameStr)])
+      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name))
+        #[Doc.Inline.other (Inline.errorExplanationShortName $(quote name)) #[]])
       let summary ← ``(Doc.Inline.text $(quote explan.metadata.summary))
       let since ← ``(Doc.Inline.text $(quote explan.metadata.sinceVersion))
       #[nameLink, summary, sev, since]
@@ -72,7 +85,8 @@ htmlToc := false
 %%%
 
 This section provides explanations of errors and warnings that may be generated
-by Lean when processing a source file.
+by Lean when processing a source file. All error names listed below have the
+`lean` package prefix.
 
 {error_explanation_table}
 
diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index 32328181..c98fe2d9 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -678,6 +678,22 @@ def explanation : PartCommand
     addExplanationBlocksFor config.name.getId
   | _ => Lean.Elab.throwUnsupportedSyntax
 
+/--
+Returns the suffix of `name` as a string containing soft-hyphen characters at reasonable split points.
+-/
+def getBreakableSuffix (name : Name) : Option String := do
+  let suffix ← match name with
+    | .str _ s => s
+    | .num _ n => toString n
+    | .anonymous => none
+  let breakableHtml := softHyphenateIdentifiers.rwText (.text false suffix)
+  htmlText breakableHtml
+where
+  htmlText : Verso.Output.Html → String
+    | .text _ txt => txt
+    | .seq elts => elts.foldl (· ++ htmlText ·) ""
+    | .tag _nm _attrs children => htmlText children
+
 open Verso Doc Elab ArgParse in
 open Lean in
 /-- Renders all error explanations as parts of the current page. -/
@@ -690,10 +706,12 @@ def make_explanations : PartCommand
       let titleBits := #[← ``(Inline.other
         (Inline.errorExplanation $(quote name) $(quote explan.metadata.summary))
         #[Inline.code $(quote titleString)])]
+      let some shortTitleString := getBreakableSuffix name
+        | throwError m!"Found invalid explanation name `{name}` when generating explanations section"
       PartElabM.push {
         titleSyntax := quote (k := `str) titleString,
         expandedTitle := some (titleString, titleBits),
-        metadata := none,
+        metadata := some (← `({ shortTitle := $(quote shortTitleString) })),
         blocks := #[],
         priorParts := #[]
       }

From 0f0d2ce2f5570a857c8b0cc09d4c2d7b72472f7a Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Fri, 27 Jun 2025 02:07:22 +0200
Subject: [PATCH 09/10] chore: add workaround for regression in latest nightly

---
 Manual/Meta/ErrorExplanation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index c98fe2d9..f18e2f62 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -435,7 +435,7 @@ def closeEnclosingSection : PartElabM Unit := do
     throwError m!"Failed to close the last-opened explanation part"
 
 /-- Adds explanation blocks until the "Examples" header is reached. -/
-def addNonExampleBlocks := do
+def addNonExampleBlocks : ExplanElabM Unit := do
   repeat
     let some block ← ExplanElabM.nextBlock?
       | return

From d959a6ae7f0d7d10d99f05f8ddff5726b0cb0986 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 27 Jun 2025 05:58:32 +0200
Subject: [PATCH 10/10] chore: replace <hr> with some vertical space

For consistency with the rest of the manual
---
 Manual/Meta/ErrorExplanation.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
index f18e2f62..c890b675 100644
--- a/Manual/Meta/ErrorExplanation.lean
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -564,6 +564,10 @@ block_extension Block.errorExplanationMetadata (metadata : ErrorExplanation.Meta
   traverse _ _ _ := pure none
   toTeX := none
   extraCss := ["
+  .error-explanation-metadata {
+    margin-bottom: 2rem; /* Double the paragraph margin */
+  }
+
   .error-explanation-metadatum:not(:last-child):after {
     content: '|';
     margin: 0 10px;
@@ -601,7 +605,6 @@ block_extension Block.errorExplanationMetadata (metadata : ErrorExplanation.Meta
         {{deprecatedWarning}}
         <p><em>{{metadata.summary}}</em></p>
         <p>{{entries}}</p>
-        <hr />
       </div>
     }}