refactor: handle error and warning logs consistently (#862)

Before, most Verso monads and functions threaded IO actions for logging
errors, and each monad had a bespoke error reporting function. These
grew organically, and were largely a set of IO actions attached to
various reader contexts.

Now, they're all unified with a single logging type class, a single
canonical monad transformer, as well as a single way to actually print
the error report to the console when finished. Many type parameters on
contexts could be removed. This makes it much easier to work on Verso.

Additionally, warning logs were added in order to prepare for an
upcoming feature.

Author: david-christiansen

doc/UsersGuide/Markup.lean

@@ -134,10 +134,10 @@ block_extension MarkupExample (title : String) where
   traverse _ _ _ := pure none
   toHtml := some fun _goI goB _id data contents => open Verso.Output.Html in do
     let .str title := data
-      | Verso.Doc.Html.HtmlT.logError s!"Expected a string, got {data.compress}"
+      | reportError s!"Expected a string, got {data.compress}"
         return .empty
     let #[stx, parsed] := contents
-      | Verso.Doc.Html.HtmlT.logError s!"Expected two blocks, got {contents.size}"
+      | reportError s!"Expected two blocks, got {contents.size}"
         return .empty
     pure {{
       <div class="markup-example">
@@ -212,10 +212,10 @@ r#"
   ]
   toTeX := some fun _goI _goB _id data contents => open Verso.Output.TeX in open Verso.Doc.TeX in do
     let .str title := data
-      | logError s!"Expected title as string, got {data.compress}"
+      | reportError s!"Expected title as string, got {data.compress}"
         return \TeX{}
     let #[.code stx, .code parsed] := contents
-      | logError s!"Expected two code blocks, got {contents.size}"
+      | reportError s!"Expected two code blocks, got {contents.size}"
         return \TeX{}
     pure \TeX{
       \begin{markupexample}{\Lean{title}}

doc/UsersGuide/Releases.lean

@@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import VersoManual
 
+import UsersGuide.Releases.«v4_31_0»
 import UsersGuide.Releases.«v4_30_0»
 import UsersGuide.Releases.«v4_29_0»
 import UsersGuide.Releases.«v4_28_0»
@@ -28,6 +29,7 @@ Verso versioning follows Lean's.
 This means that we release a new version for each Lean release, usually once per month.
 In particular, note that Verso doesn't follow the [semantic versioning model](https://semver.org/).
 
+{include 0 UsersGuide.Releases.«v4_31_0»}
 {include 0 UsersGuide.Releases.«v4_30_0»}
 {include 0 UsersGuide.Releases.«v4_29_0»}
 {include 0 UsersGuide.Releases.«v4_28_0»}

doc/UsersGuide/Releases/v4_31_0.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+
+open Verso.Genre Manual InlineLean
+
+
+#doc (Manual) "Verso 4.31.0 (unreleased)" =>
+%%%
+tag := "release-v4.31.0"
+file := "v4.31.0"
+%%%
+
+* Refactored the build's error reporting into a {ref "feat-build-log"}[logging abstraction] with severities and structured source locations, improving the consistency of Verso's internal APIs and external error reports.
+  While this was primarily an internal change, there is a {ref "feat-build-log-breaking"}[breaking change] to the signature of {name}`Verso.Genre.Manual.ExtraStep`.
+
+# Logging Abstraction
+%%%
+tag := "feat-build-log"
+%%%
+
+The build pipeline previously threaded a bare `String → IO Unit` error callback through traversal and output generation, and several monads carried their own ad-hoc error loggers.
+There was no way to emit a warning.
+
+This release introduces {name}`Verso.MonadBuildLog`, a uniform logging interface shared across the genres.
+A message carries a {name}`Verso.Severity` (either {name}`Verso.Severity.error` or {name}`Verso.Severity.warning`) and an optional source location.
+
+
+## Breaking Change: `ExtraStep`
+%%%
+tag := "feat-build-log-breaking"
+%%%
+
+{name}`Verso.Genre.Manual.ExtraStep` no longer takes a `String → IO Unit` error callback.
+Instead, it runs in a monad that has an instance of {name}`Verso.MonadBuildLog`, so a step can emit both errors and warnings with {name}`Verso.reportError` and {name}`Verso.reportWarning`.

src/tests/TestMain.lean

@@ -56,8 +56,8 @@ def testTexOutput
 
   let runTest : IO Unit  :=
     open Verso Genre Manual in do
-    let logError (msg : String) := IO.eprintln msg
-    ReaderT.run (emitTeX logError versoConfig doc.toPart) extension_impls%
+    let logger ← Verso.Logger.new
+    emitTeX versoConfig doc.toPart |>.run extension_impls% |>.run logger
 
   Verso.Integration.runTests { config with
     testDir := "src/tests/integration" / dir,
@@ -259,8 +259,99 @@ def testSetupLiterate (_ : Config) : IO Unit := do
 
   IO.println "  All setup-literate tests passed."
 
+open Verso in
+def testBuildLog (_ : Config) : IO Unit := do
+  IO.println "Running build-log tests..."
+  -- A message logged with a position is saved with that location (a location always names a file).
+  let logger ← Logger.new
+  let pos : Lean.Lsp.Position := { line := 4, character := 2 }
+  (reportError "boom" (some { file := "PosSave.lean", span := .pos pos }) : BuildLogT IO Unit).run logger
+  let errs ← logger.errors
+  let some m := errs[0]?
+    | throw <| IO.userError s!"expected 1 saved error, got {errs.size}"
+  unless m.severity == .error do throw <| IO.userError "expected error severity"
+  match m.loc with
+  | some { file := "PosSave.lean", span := .pos p } =>
+    unless p.line == 4 && p.character == 2 do
+      throw <| IO.userError "saved position does not match the logged span"
+  | _ => throw <| IO.userError "expected a saved `PosSave.lean` `pos` location"
+
+  -- A `range` span is likewise saved.
+  let logger2 ← Logger.new
+  let r : Lean.Lsp.Range :=
+    { start := { line := 1, character := 0 }, «end» := { line := 1, character := 5 } }
+  (reportWarning "careful" (some { file := "RangeSave.lean", span := .range r }) : BuildLogT IO Unit).run logger2
+  let some w := (← logger2.warnings)[0]?
+    | throw <| IO.userError "expected 1 saved warning"
+  match w.loc with
+  | some { span := .range _, .. } => pure ()
+  | _ => throw <| IO.userError "expected a `range` span to be saved"
+
+  -- Range formatting defers to Lean's `mkErrorStringWithPos`: `file:line:col-line:col`, 1-based
+  -- line, 0-based column, with the full end position even within one line (no `line:col-col` collapse).
+  let crossLine : LogMessage :=
+    { severity := .error, text := "msg",
+      loc := some { file := "CrossLine.lean",
+                    span := .range { start := { line := 19, character := 4 }, «end» := { line := 20, character := 7 } } } }
+  unless crossLine.format == "CrossLine.lean:20:4-21:7: msg" do
+    throw <| IO.userError s!"cross-line range formatted as \"{crossLine.format}\""
+  let sameLine : LogMessage :=
+    { severity := .error, text := "msg",
+      loc := some { file := "SameLine.lean",
+                    span := .range { start := { line := 42, character := 4 }, «end» := { line := 42, character := 21 } } } }
+  unless sameLine.format == "SameLine.lean:43:4-43:21: msg" do
+    throw <| IO.userError s!"same-line range formatted as \"{sameLine.format}\""
+
+  -- A located message is formatted uniformly as `file:line:col: text`.
+  let loggerF ← Logger.new
+  let errBufF ← IO.mkRef ({} : IO.FS.Stream.Buffer)
+  IO.withStderr (IO.FS.Stream.ofBuffer errBufF) <|
+    (reportError "bad term" (some { file := "FileLoc.lean", span := .pos { line := 6, character := 3 } })
+      : BuildLogT IO Unit).run loggerF
+  let some mF := (← loggerF.errors)[0]?
+    | throw <| IO.userError "expected 1 saved error with a file location"
+  unless mF.loc.map (·.file) == some "FileLoc.lean" do
+    throw <| IO.userError "saved location should carry the filename"
+  unless hasSubstring (String.fromUTF8! (← errBufF.get).data) "FileLoc.lean:7:3: bad term" do
+    throw <| IO.userError "a file location should format as file:line:col:"
+
+  -- A single logging action can emit both severities; errors set the exit code, warnings do not.
+  let logger3 ← Logger.new
+  (do reportError "e1"; reportWarning "w1"; reportError "e2" : BuildLogT IO Unit).run logger3
+  unless (← logger3.errors).size == 2 do throw <| IO.userError "expected 2 errors"
+  unless (← logger3.warnings).size == 1 do throw <| IO.userError "expected 1 warning"
+  unless (← logger3.exitCode) == 1 do throw <| IO.userError "errors must yield a non-zero exit code"
+
+  let logger4 ← Logger.new
+  (reportWarning "just a warning" : BuildLogT IO Unit).run logger4
+  unless (← logger4.exitCode) == 0 do
+    throw <| IO.userError "warnings must not affect the exit code"
+
+  -- Logging prints to the *ambient* stderr, resolved at log time: a logger created before a
+  -- stderr redirection still writes into the redirected stream, and nothing goes to stdout.
+  let logger5 ← Logger.new
+  let outBuf ← IO.mkRef ({} : IO.FS.Stream.Buffer)
+  let errBuf ← IO.mkRef ({} : IO.FS.Stream.Buffer)
+  IO.withStdout (IO.FS.Stream.ofBuffer outBuf) <|
+    IO.withStderr (IO.FS.Stream.ofBuffer errBuf) <|
+      (do
+        reportError "first problem" (some { file := "X.lean", span := .pos { line := 0, character := 0 } })
+        reportWarning "second problem" : BuildLogT IO Unit).run logger5
+  let errText := String.fromUTF8! (← errBuf.get).data
+  let outText := String.fromUTF8! (← outBuf.get).data
+  unless hasSubstring errText "X.lean:1:0: first problem" do
+    throw <| IO.userError s!"stderr buffer is missing the formatted error; got: {errText}"
+  unless hasSubstring errText "second problem" do
+    throw <| IO.userError s!"stderr buffer is missing the warning; got: {errText}"
+  unless outText.isEmpty do
+    throw <| IO.userError s!"logging must not write to stdout; got: {outText}"
+  unless (← logger5.errors).size == 1 && (← logger5.warnings).size == 1 do
+    throw <| IO.userError "redirected logging should still accumulate into the logger's buffers"
+  IO.println "  All build-log tests passed."
+
 open Verso.Integration in
 def tests := [
+  testBuildLog,
   testSerialization,
   testSearchJs,
   testBlog,

src/tests/Tests/GenericCode.lean

@@ -58,7 +58,7 @@ info: Verso.Output.Html.tag
               (Verso.Output.Html.text true "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n")])])
 -/
 #guard_msgs in
-  #eval Doc.Genre.none.toHtml (m:=Id) {logError := fun _ => ()} () () {} {} {} code1.toPart |>.run .empty |>.fst
+  #eval Doc.Genre.none.toHtml (m := Id) {} () () {} {} {} code1.toPart |>.run .empty |>.fst
 
 
 /- ----- -/

src/tests/Tests/TexUtil.lean

@@ -19,23 +19,24 @@ This requires the `IO` monad because `TraverseM` does.
 -/
 def toTex (block : Doc.Block Genre.Manual) : IO Output.TeX := do
   let extension_impls := extension_impls%
+  let logger ← Verso.Logger.new
 
   -- Traversal monadic data
-  let traverseContext : TraverseContext := {
-    logError msg := IO.println msg,
-  }
+  let traverseContext : TraverseContext := {}
   let traverseState : TraverseState := .initialize {}
 
   -- Traverse the block. This shadows both `block` and `traverseState`.
   -- This is where we engage with the IO at the bottom of TraverseM.
-  let ⟨block, traverseState⟩ ← Doc.Genre.traverseBlock Genre.Manual block
-    |>.run extension_impls traverseContext traverseState
+  let ⟨block, traverseState⟩ ←
+    Doc.Genre.traverseBlock Genre.Manual block
+      |>.run extension_impls traverseContext traverseState logger
 
   -- Options for TeX
-  let options : Doc.TeX.Options Genre.Manual (ReaderT ExtensionImpls IO) := {
-    headerLevel := none,
-    logError msg := IO.println msg,
+  let options : Doc.TeX.Options Genre.Manual := {
+    headerLevel := none
   }
 
   -- Convert the block to TeX
-  block.toTeX.run ⟨options, traverseContext, traverseState, {}⟩ |>.run' {} |>.run extension_impls
+  block.toTeX
+    |>.run ⟨options, traverseContext, traverseState, {}⟩
+    |>.run' {} |>.run extension_impls |>.run logger

src/verso-blog/VersoBlog.lean

@@ -835,39 +835,33 @@ Optional parameters:
 def blogMain (theme : Theme) (site : Site) (linkTargets : Code.LinkTargets TraverseContext := {})
     (options : List String) (components : Components := by exact %registered_components)
     (header : String := Html.doctype) :
-    IO UInt32 := do
-  let hasError ← IO.mkRef false
-  let logError msg := do hasError.set true; IO.eprintln msg
-  let cfg ← opts {logError := logError} options
-  let (site, xref) ← site.traverse cfg components
-  let initGenCtx : Generate.Context := {
-    theme, site,
-    ctxt := { path := .root, config := cfg, components },
-    xref := xref,
-    dir := cfg.destination,
-    config := cfg,
-    header := header,
-    linkTargets := linkTargets,
-    components := components
-  }
-  let (((), st), _) ← site.generate theme initGenCtx .empty {}
-  IO.FS.writeFile (cfg.destination.join "-verso-docs.json") (toString st.dedup.docJson)
-  for (name, content, srcMap?) in xref.jsFiles do
-    FS.ensureDir (cfg.destination.join "-verso-data")
-    IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
-    if let some (name, content) := srcMap? then
+    IO UInt32 :=
+  withLogger fun logger => do
+    let cfg ← opts {} options
+    let (site, xref) ← site.traverse cfg components |>.run logger
+    let initGenCtx : Generate.Context := {
+      theme, site,
+      ctxt := { path := .root, config := cfg, components },
+      xref := xref,
+      dir := cfg.destination,
+      config := cfg,
+      header := header,
+      linkTargets := linkTargets,
+      components := components
+    }
+    let (((), st), _) ← site.generate theme initGenCtx .empty {} |>.run logger
+    IO.FS.writeFile (cfg.destination.join "-verso-docs.json") (toString st.dedup.docJson)
+    for (name, content, srcMap?) in xref.jsFiles do
+      FS.ensureDir (cfg.destination.join "-verso-data")
+      IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
+      if let some (name, content) := srcMap? then
+        IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
+    for (name, content, _) in theme.jsFiles do
+      FS.ensureDir (cfg.destination.join "-verso-data")
+      IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
+    for (name, content) in theme.cssFiles ++ xref.cssFiles do
+      FS.ensureDir (cfg.destination.join "-verso-data")
       IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
-  for (name, content, _) in theme.jsFiles do
-    FS.ensureDir (cfg.destination.join "-verso-data")
-    IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
-  for (name, content) in theme.cssFiles ++ xref.cssFiles do
-    FS.ensureDir (cfg.destination.join "-verso-data")
-    IO.FS.writeFile (cfg.destination.join "-verso-data" |>.join name) content
-  if (← hasError.get) then
-    IO.eprintln "Errors were encountered!"
-    return 1
-  else
-    return 0
 where
   opts (cfg : Config)
     | ("--output"::dir::more) => opts {cfg with destination := dir} more

src/verso-blog/VersoBlog/Basic.lean

@@ -220,7 +220,6 @@ structure Config where
   destination : System.FilePath := "./_site"
   showDrafts : Bool := false
   postName : Date → String → String := defaultPostName
-  logError : String → IO Unit
   remoteInfoConfigPath : Option System.FilePath := none
   verbose : Bool := false
 deriving Inhabited
@@ -230,8 +229,9 @@ class MonadConfig (m : Type → Type u) where
 
 export MonadConfig (currentConfig)
 
-def logError [Monad m] [MonadConfig m] [MonadLiftT IO m] (message : String) : m Unit := do
-  (← currentConfig).logError message
+@[deprecated "Use `Verso.reportError` instead." (since := "2026-05-29")]
+def logError [MonadBuildLog m] (message : String) : m Unit :=
+  Verso.reportError message
 
 structure Components where
   /--
@@ -483,7 +483,7 @@ instance : BEq TraverseState where
       err1.toList == err2.toList &&
       rem1 == rem2
 
-abbrev TraverseM := ReaderT Blog.TraverseContext (StateT Blog.TraverseState IO)
+abbrev TraverseM := ReaderT Blog.TraverseContext (StateT Blog.TraverseState (BuildLogT IO))
 
 instance : MonadConfig TraverseM where
   currentConfig := do pure (← read).config

src/verso-blog/VersoBlog/Component.lean

@@ -83,7 +83,7 @@ def State.freshId (state : State) : String × State := Id.run do
 
 end Component
 
-abbrev ComponentM := ReaderT Components (StateT Component.State IO)
+abbrev ComponentM := ReaderT Components (StateT Component.State (BuildLogT IO))
 
 abbrev HtmlM genre := HtmlT genre ComponentM
 
@@ -259,7 +259,7 @@ def deJson [Monad m] [MonadQuotation m]
   let (x, t) := b
   `(Lean.Parser.Term.doSeqItem| let $x ← match FromJson.fromJson? (α := $t) $x with
       | .error e => do
-        (HtmlT.logError e : HtmlM Page Unit)
+        (reportError e : HtmlM Page Unit)
         return Html.empty
       | .ok v => pure v)
 
@@ -288,7 +288,7 @@ elab_rules : command
                   $noJson*
                   ($tm id json goI goB contents)
                 | _ => do
-                  HtmlT.logError s!"Expected array, got {json}"
+                  reportError s!"Expected array, got {json}"
                   return .empty)
     let other := toHtml.toArray ++ other
     let cmd2 ←
@@ -340,7 +340,7 @@ elab_rules : command
                   $noJson*
                   ($tm id json goI contents)
                 | _ => do
-                  HtmlT.logError s!"Expected array, got {json}"
+                  reportError s!"Expected array, got {json}"
                   return .empty)
     let other := toHtml.toArray ++ other
     let cmd2 ←