{{errorName}} }}
+ return html
+
+@[block_role_expander error_explanation_table]
+def error_explanation_table : BlockRoleExpander
+ | #[], #[] => do
+ let entries ← getErrorExplanationsSorted
+ let columns := 4
+ let header := true
+ 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)])
+ 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 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]
+ |>.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. All error names listed below have the
+`lean` package prefix.
+
+{error_explanation_table}
+
+{make_explanations}
diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
new file mode 100644
index 00000000..c890b675
--- /dev/null
+++ b/Manual/Meta/ErrorExplanation.lean
@@ -0,0 +1,723 @@
+/-
+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
+
+import PreprocessedExplanations
+
+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
+
+/-- 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 := preprocessedExplanationsRoot / 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.
+-/
+block_extension Block.tabbedMWEs (titles : Array String) where
+ data := toJson titles
+ 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-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;
+}
+/* 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#"
+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 {{
+
+ }}
+ let panels ← contents.mapIdxM fun i b => do
+ let className := "error-example-tabpanel" ++ if i == 0 then "" else " error-example-tabpanel-hidden"
+ let idxStr := toString i
+ return {{
+ "Note: " "This diagnostic is no longer produced."
+