feat: add the Errata test framework

.github/workflows/ci.yml

@@ -70,11 +70,13 @@ jobs:
 
             - name: Check for orphaned modules
               run: |
-                  # These are all the library modules; docs and tests are excluded
+                  # These are all the library modules plus the Errata self-tests, whose modules
+                  # must stay reachable from their root for the test driver to run them; docs and
+                  # the remaining test libraries are excluded
                   out="$(lake query VersoUtil:orphanMods Verso:orphanMods MultiVerso:orphanMods \
                     VersoSearch:orphanMods VersoBlog:orphanMods VersoManual:orphanMods \
                     VersoIlluminate:orphanMods VersoTutorial:orphanMods VersoLiterate:orphanMods \
-                    VersoLiterateCode:orphanMods)"
+                    VersoLiterateCode:orphanMods Errata:orphanMods ErrataTests:orphanMods)"
                   if [ -n "$(printf '%s' "$out" | tr -d '[:space:]')" ]; then
                     echo "Found orphaned modules:"
                     echo "$out"

.github/workflows/no-eval-in-source.yml

@@ -25,10 +25,11 @@ jobs:
                     fi
                   done < <(find ./src -path ./src/tests -prune -o \
                     -path ./src/test-projects -prune -o \
+                    -path ./src/errata-tests -prune -o \
                     -name "*.lean" -type f -print0)
 
                   if [ ${#OFFENDING_FILES[@]} -gt 0 ]; then
-                    echo "Found #eval statements in module source files (should be in src/tests/):"
+                    echo "Found #eval statements in module source files (should be in src/tests/ or src/errata-tests/):"
                     printf '%s\n' "${OFFENDING_FILES[@]}"
                     echo ""
                     echo "Offending lines:"

doc/UsersGuide/Releases/Entries.lean

@@ -24,4 +24,5 @@ public import UsersGuide.Releases.Entries.MethodInMultiVerso
 public import UsersGuide.Releases.Entries.ReleaseNotesChapter
 public import UsersGuide.Releases.Entries.RoleDiagnostics
 public import UsersGuide.Releases.Entries.SearchPriority
+public import UsersGuide.Releases.Entries.TestFramework
 public import UsersGuide.Releases.Entries.VersionedReleaseNotes

doc/UsersGuide/Releases/Entries/TestFramework.lean

@@ -0,0 +1,31 @@
+/-
+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
+-/
+module
+
+public import UsersGuide.Releases.Entry
+
+open Verso.Genre Manual InlineLean UsersGuide.Releases
+
+release_note
+  version := ⟨4, 34, 0⟩
+  breaking := false
+  tag := "feat-test-framework"
+  prs := [956]
+
+#doc (Manual) "Test Framework" =>
+
+Added `Errata`, a testing framework with test discovery, uniform failure reporting, and CI-friendly report formats.
+
+Previously, Verso's tests were all essentially _ad hoc_ IO actions that were run in sequence or elaborations that would fail.
+Each item was tested with the appropriate tool for the job (random testing, golden testing, traditional unit tests, etc), but there was no overarching test code.
+In particular, there were no universal conventions about output or failure reporting, and it could be difficult to see which test had actually failed at a glance.
+`Errata` unifies reporting and eliminates the need to plumb lists of tests through the system.
+
+Tests are marked with the `@[test]` attribute, and a test's value can have any type with an `IsTest` instance.
+Each test's docstring and source range are saved for failure reporting.
+The test runner discovers every test in the package; it can restrict the run to named libraries, rerun property tests with a fixed seed, update golden files, fail the run on warnings with `--wfail`, and write JUnit XML, JSON, and Markdown reports.
+
+Elaboration-time tests can be written with `#test_msgs` and `#test_guard`, variants of `#guard_msgs` and `#guard` that run their check at compile time and record the outcome as a test case, reported together with the rest of the suite.

lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/illuminate",
+ [{"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",

lakefile.lean

@@ -5,6 +5,7 @@ require subverso from git "https://github.com/leanprover/subverso"@"main"
 require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 require plausible from git "https://github.com/leanprover-community/plausible"@"main"
 require illuminate from git "https://github.com/leanprover/illuminate"@"main"
+require Cli from git "https://github.com/leanprover/lean4-cli"@"main"
 
 package verso where
   precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30
@@ -144,6 +145,224 @@ lean_exe «verso-tests» where
   srcDir := "src/tests"
   supportInterpreter := true
 
+-- Everything below is Errata's own implementation: its library, its self-tests, the generated
+-- discovery runner, and the runner script.
+namespace Errata
+
+@[default_target]
+lean_lib Errata where
+  srcDir := "src/errata"
+  roots := #[`Errata]
+
+-- Tests that exercise Errata using Errata itself.
+@[default_target]
+lean_lib ErrataTests where
+  srcDir := "src/errata-tests"
+  roots := #[`ErrataTests]
+
+-- The directory below the package's Lake directory where the Errata driver writes the generated
+-- runner sources.
+def errataRunnerDir : System.FilePath := defaultLakeDir / "errata-runner"
+
+-- The selected test set, written by the driver. The generated targets depend on it, so changing
+-- the selection changes their trace and Lake rebuilds them rather than relinking a stale object.
+input_file errataSelection where
+  text := true
+  path := errataRunnerDir / "selection"
+
+-- The generated discovered-tests module (`allTests`), written by the Errata driver.
+lean_lib ErrataGenerated where
+  srcDir := errataRunnerDir
+  roots := #[`ErrataDiscovered]
+  needs := #[errataSelection]
+
+-- The generated, discovered test runner. Its source is written by the Errata test driver.
+lean_exe «errata-runner» where
+  root := `ErrataRunnerMain
+  srcDir := errataRunnerDir
+  supportInterpreter := true
+  needs := #[errataSelection]
+
+/--
+Reads a built module's `.olean` header: whether it participates in the module system, and whether
+it records any `@[test]` (including those generated by `#test_msgs` and `#test_guard`).
+-/
+private def moduleInfo (oleanFile : System.FilePath) : IO (Bool × Bool) := do
+  let (data, region) ← Lean.readModuleData oleanFile
+  let hasTests := data.entries.any fun (name, entries) => name == `Errata.test && entries.size > 0
+  let isModule := data.isModule
+  unsafe region.free
+  return (isModule, hasTests)
+
+/--
+The modules that sit under a library's roots on disk without being among the modules the library
+actually builds. Nothing imports them and no glob covers them, so they are never compiled, and any
+tests they define never run. `known` is the library's module set.
+-/
+private def unreachableModules (lib : Lake.LeanLib) (known : Lean.NameSet) :
+    IO (Array Lean.Name) := do
+  let found ← IO.mkRef (#[] : Array Lean.Name)
+  for root in lib.config.roots do
+    try
+      Lake.Glob.submodules root |>.forEachModuleIn lib.srcDir fun m => do
+        unless known.contains m do found.modify (·.push m)
+    catch
+      -- Thrown for a root with no corresponding directory, which has no submodules to orphan.
+      | .noFileOrDirectory .. => pure ()
+      | e => throw e
+  found.get
+
+/--
+Generate the bridge module: `import all` the module-system test modules so their private tests
+are reachable, gathering them into `allTests` through `getAllTests%`.
+-/
+private def discoveredSource (packageName : String) (mods : Array Lean.Name) : String :=
+  let imports := "\n".intercalate ("public import Errata" :: mods.toList.map (s!"import all {·}"))
+  let modList := " ".intercalate (mods.toList.map (·.toString))
+  s!"module\n\n{imports}\n\n\
+    public def allTests : Array Errata.TestEntry := getAllTests% \"{packageName}\" {modList}\n"
+
+/--
+Generate the non-module main: import the bridge module and the non-module test modules (which a
+`module` cannot import), then run their combined tests.
+-/
+private def mainSource (packageName : String) (mods : Array Lean.Name) (discovered : Lean.Name) :
+    String :=
+  let imports := "\n".intercalate
+    ("import Errata" :: s!"import {discovered}" :: mods.toList.map (s!"import {·}"))
+  let modList := " ".intercalate (mods.toList.map (·.toString))
+  s!"{imports}\n\n\
+    def main (args : List String) : IO UInt32 :=\n  \
+    Errata.runMain (allTests ++ getAllTests% \"{packageName}\" {modList}) args\n"
+
+/--
+Splits driver arguments at the `--test-options` marker into library names and runner passthrough
+arguments. Library names precede the marker and may not look like options; everything after the
+marker goes to the runner.
+-/
+private def splitArgs (args : List String) : Except String (List String × List String) :=
+  let (names, rest) :=
+    match args.span (· != "--test-options") with
+    | (names, _ :: after) => (names, after)
+    | (names, []) => (names, [])
+  match names.find? (·.startsWith "-") with
+  | some opt =>
+    .error s!"unexpected option '{opt}': arguments before the `--test-options` marker name the \
+      libraries to test. Put runner options after the marker, \
+      e.g. `lake run Errata.run --test-options {opt}`."
+  | none => .ok (names, rest)
+
+/-- Usage information for `lake run Errata.run`. -/
+private def usage : String := include_str "src/errata/Errata/usage.txt"
+
+script run (args) do
+  let ws ← getWorkspace
+  -- Answer the driver's own `--help` before discovering or building anything. A `--help` after the
+  -- marker asks for the runner's options, so it goes to the runner along with the other arguments.
+  if (args.takeWhile (· != "--test-options")).any (fun a => a == "--help" || a == "-h") then
+    IO.println usage
+    return 0
+  let (libNames, runnerArgs) ←
+    match splitArgs args with
+    | .ok result => pure result
+    | .error msg =>
+      IO.eprintln s!"error: {msg}"
+      IO.eprintln usage
+      return 1
+  -- `--wfail` is the runner's warnings-as-errors flag; the driver's own warnings honor it too.
+  let wfail := runnerArgs.contains "--wfail"
+  -- Search the named libraries, or every library in the package by default. A name may be a bare
+  -- `Library` in this package or a `package/Library` reaching into a dependency, following Lake's
+  -- target syntax. A library whose source lives in the generated-runner directory has no source
+  -- until this script writes it, and no tests of its own.
+  let candidates := ws.root.leanLibs.filter (·.config.srcDir != errataRunnerDir)
+  let libs ←
+    if libNames.isEmpty then pure candidates
+    else do
+      let mut chosen : Array Lake.LeanLib := #[]
+      for spec in libNames do
+        let lib? ←
+          match spec.splitOn "/" with
+          | [libName] => pure (candidates.find? (·.name == libName.toName))
+          | [pkgName, libName] =>
+            let pkgName := if pkgName.startsWith "@" then pkgName.drop 1 else pkgName
+            let pkg? := if pkgName.isEmpty then some ws.root else ws.findPackageByName? pkgName.toName
+            match pkg? with
+            | some pkg => pure (pkg.findLeanLib? libName.toName)
+            | none =>
+              IO.eprintln s!"error: no package named '{pkgName}'"
+              return 1
+          | _ =>
+            IO.eprintln s!"error: invalid library spec '{spec}' (expected `Library` or `package/Library`)"
+            return 1
+        match lib? with
+        | some lib => chosen := chosen.push lib
+        | none =>
+          IO.eprintln s!"error: no library matches '{spec}'"
+          return 1
+      pure chosen
+  -- Build every module in the selected libraries; their compiled `.olean` headers are authoritative
+  -- on which modules carry tests.
+  let (modInfos, libMods) ← runBuild do
+    let mut oleanJobs := #[]
+    let mut infos : Array (Lean.Name × System.FilePath) := #[]
+    let mut libMods : Array (Lake.LeanLib × Array Lean.Name) := #[]
+    for lib in libs do
+      let mods ← (← lib.modules.fetch).await
+      libMods := libMods.push (lib, mods.map (·.name))
+      for m in mods do
+        oleanJobs := oleanJobs.push (← m.olean.fetch)
+        infos := infos.push (m.name, m.oleanFile)
+    pure <| (Job.collectArray oleanJobs).map (sync := true) fun _ => (infos, libMods)
+  -- A test module is one whose `.olean` records a test. Module-system test modules go in the bridge
+  -- module (`import all`); non-module ones can only be imported by the non-module main.
+  let mut moduleMods : Array Lean.Name := #[]
+  let mut nonModuleMods : Array Lean.Name := #[]
+  for (moduleName, oleanFile) in modInfos do
+    let (isModule, hasTests) ← moduleInfo oleanFile
+    if hasTests then
+      if isModule then moduleMods := moduleMods.push moduleName
+      else nonModuleMods := nonModuleMods.push moduleName
+  -- A module that sits under a library's roots without being reachable from them is never built, so
+  -- any tests it defines are silently left out. A library is checked when it was named on the
+  -- command line, since naming it declares that its tests are expected, or when its built modules
+  -- carry tests. That is a configuration slip rather than a test failure, so report it and run
+  -- anyway.
+  let testMods := moduleMods ++ nonModuleMods
+  let mut unreachable : Array (Lake.LeanLib × Array Lean.Name) := #[]
+  for (lib, mods) in libMods do
+    if !libNames.isEmpty || mods.any (testMods.contains ·) then
+      let known := mods.foldl (init := Lean.NameSet.empty) (·.insert ·)
+      let missed ← unreachableModules lib known
+      unless missed.isEmpty do unreachable := unreachable.push (lib, missed)
+  unless unreachable.isEmpty do
+    let level := if wfail then "error" else "warning"
+    IO.eprintln s!"{level}: these modules are not reachable from their library's roots, so any \
+      tests they define are not discovered. Import them from a root, or widen the library's \
+      `globs` (e.g. `globs := #[Glob.andSubmodules `Root]`):"
+    for (lib, mods) in unreachable do
+      for mod in mods do
+        IO.eprintln s!"  {lib.name}: {mod}"
+    if wfail then return 1
+  -- Write the generated sources, plus a `selection` file naming the chosen test set. The generated
+  -- targets depend on that file, so a changed selection invalidates them through Lake's own trace.
+  let dir := ws.root.dir / errataRunnerDir
+  IO.FS.createDirAll dir
+  let selection := "\n".intercalate ((moduleMods ++ nonModuleMods).map (·.toString) |>.qsort (· < ·)).toList
+  for (name, src) in
+      [("selection", selection ++ "\n"),
+       ("ErrataDiscovered.lean", discoveredSource ws.root.prettyName moduleMods),
+       ("ErrataRunnerMain.lean", mainSource ws.root.prettyName nonModuleMods `ErrataDiscovered)] do
+    let file := dir / name
+    let changed ← if ← file.pathExists then pure ((← IO.FS.readFile file) != src) else pure true
+    if changed then IO.FS.writeFile file src
+  -- Build and run the discovered runner.
+  let exePath ← runBuild «errata-runner».fetch
+  let child ← IO.Process.spawn { cmd := exePath.toString, args := runnerArgs.toArray }
+  child.wait
+
+end Errata
+
 -- The release notes compute the version under development from this file while they elaborate,
 -- so its contents are an input to the library.
 input_file leanToolchain where