From 5af14b7153a390942e7549a36c34eed21f16b9a9 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 14 Aug 2026 10:25:29 +0200 Subject: [PATCH 01/32] feat: add the Errata test framework Errata is a test framework, designed to be something we can extract to its own repo after we get some experience with it here (so it can be used e.g. in verso-slides and lean-sqlite). In Errata, tests are marked by the `@[test]` attribute. Their docstring and source range are saved for failure reporting. The value of a test can have any type with an `IsTest` instance. Some machinery in the Lakefile enumerates all tests, providing them to the runner. Elaboration-time tests can also be implemented using `#test_msgs` and `#test_guard`, which are versions of `#guard_msgs` and `#guard` that run the compile-time test but save the result as a test case for reporting together with the rest of the tests. Errata also supports saving JUnit XML, which various GitHub actions can conveniently display for us. --- .github/workflows/ci.yml | 4 + .github/workflows/no-eval-in-source.yml | 3 +- doc/UsersGuide/Releases/Entries.lean | 1 + .../Releases/Entries/TestFramework.lean | 26 ++ lakefile.lean | 228 +++++++++++++ src/errata-tests/ErrataTests.lean | 164 +++++++++ src/errata/Errata.lean | 22 ++ src/errata/Errata/Assertions.lean | 80 +++++ src/errata/Errata/CompileTime.lean | 151 +++++++++ src/errata/Errata/CompileTime/Helpers.lean | 48 +++ src/errata/Errata/Context.lean | 56 +++ src/errata/Errata/Discovery.lean | 127 +++++++ src/errata/Errata/Golden.lean | 87 +++++ src/errata/Errata/Here.lean | 32 ++ src/errata/Errata/IsTest.lean | 42 +++ src/errata/Errata/Process.lean | 23 ++ src/errata/Errata/Property.lean | 35 ++ src/errata/Errata/Report.lean | 319 ++++++++++++++++++ src/errata/Errata/Result.lean | 186 ++++++++++ src/errata/Errata/Runner.lean | 184 ++++++++++ src/errata/Errata/TestM.lean | 191 +++++++++++ src/errata/Errata/usage.txt | 21 ++ 22 files changed, 2029 insertions(+), 1 deletion(-) create mode 100644 doc/UsersGuide/Releases/Entries/TestFramework.lean create mode 100644 src/errata-tests/ErrataTests.lean create mode 100644 src/errata/Errata.lean create mode 100644 src/errata/Errata/Assertions.lean create mode 100644 src/errata/Errata/CompileTime.lean create mode 100644 src/errata/Errata/CompileTime/Helpers.lean create mode 100644 src/errata/Errata/Context.lean create mode 100644 src/errata/Errata/Discovery.lean create mode 100644 src/errata/Errata/Golden.lean create mode 100644 src/errata/Errata/Here.lean create mode 100644 src/errata/Errata/IsTest.lean create mode 100644 src/errata/Errata/Process.lean create mode 100644 src/errata/Errata/Property.lean create mode 100644 src/errata/Errata/Report.lean create mode 100644 src/errata/Errata/Result.lean create mode 100644 src/errata/Errata/Runner.lean create mode 100644 src/errata/Errata/TestM.lean create mode 100644 src/errata/Errata/usage.txt diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d68f7852..f4a8b601 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -149,6 +149,10 @@ jobs: run: | lake test -- --verbose --check-tex + - name: Run Errata's self-tests + run: | + lake run Errata.run ErrataTests --test-options --verbose + - name: Test the dev server run: | ./src/tests/run_serve_test.sh diff --git a/.github/workflows/no-eval-in-source.yml b/.github/workflows/no-eval-in-source.yml index 29b5e75a..671d654f 100644 --- a/.github/workflows/no-eval-in-source.yml +++ b/.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:" diff --git a/doc/UsersGuide/Releases/Entries.lean b/doc/UsersGuide/Releases/Entries.lean index d2dd7cd0..ffdacb0f 100644 --- a/doc/UsersGuide/Releases/Entries.lean +++ b/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 diff --git a/doc/UsersGuide/Releases/Entries/TestFramework.lean b/doc/UsersGuide/Releases/Entries/TestFramework.lean new file mode 100644 index 00000000..1f0e1794 --- /dev/null +++ b/doc/UsersGuide/Releases/Entries/TestFramework.lean @@ -0,0 +1,26 @@ +/- +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 := [] + +#doc (Manual) "Test Framework" => + +Added Errata, a test framework with test discovery, uniform failure reporting, and CI-friendly report formats. + +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, 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. diff --git a/lakefile.lean b/lakefile.lean index b13eee02..cf9bd1e5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -144,6 +144,234 @@ 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] +input_file errataUsageFile where + text := true + path := "src/errata/Errata/usage.txt" + +lean_lib Errata where + srcDir := "src/errata" + roots := #[`Errata] + needs := #[errataUsageFile] + +-- Tests that exercise Errata using Errata itself. +lean_lib ErrataTests where + srcDir := "src/errata-tests" + roots := #[`ErrataTests] + +-- 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 := ".lake/errata-runner/selection" + +-- The generated discovered-tests module (`allTests`), written by the Errata driver. +lean_lib ErrataGenerated where + srcDir := ".lake/errata-runner" + 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 := ".lake/errata-runner" + supportInterpreter := true + needs := #[errataSelection] + +/-- +Whether a source file introduces Errata tests, by an `@[test]` attribute (applied inline or with a +separate `attribute [test] …`), a `#test_msgs` command, or a `#test_guard` command. This drives the +glob-coverage check, which reads source files before anything is built; test discovery itself reads +the compiled modules. +-/ +private def sourceHasTests (lines : List String) : Bool := + lines.any fun line => + let t := line.trimAsciiStart + t.startsWith "@[test]" || t.startsWith "attribute [test" || + t.startsWith "#test_msgs" || t.startsWith "#test_guard" + +/-- 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) + +/-- 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 test -- --test-options {opt}`." + | none => .ok (names, rest) + +/-- Usage information for `lake test`, shared with `Errata.usage` through one text file. -/ +private def usage : String := include_str "src/errata/Errata/usage.txt" + +/-- Every `.lean` file below a directory, recursively. -/ +private partial def leanFiles (dir : System.FilePath) : IO (Array System.FilePath) := do + unless ← dir.pathExists do return #[] + let mut out := #[] + for entry in ← dir.readDir do + if ← entry.path.isDir then + out := out ++ (← leanFiles entry.path) + else if entry.path.extension == some "lean" then + out := out.push entry.path + return out + +/-- The module name of a `.lean` file relative to a source directory, if it lies within it. -/ +private def moduleOfPath (srcDir path : System.FilePath) : Option Lean.Name := do + guard (path.extension == some "lean") + let stem ← path.fileStem + let parent ← path.parent + guard (srcDir.components.isPrefixOf parent.components) + let comps := parent.components.drop srcDir.components.length ++ [stem] + some (".".intercalate comps).toName + +/-- +Warns about modules that look like they define tests but whose library's globs do not cover them, so +the tests would be silently undiscovered. A module within a library's root that is not matched by the +library's globs, in a file that introduces tests, is the signal. The check reads source text and is a +heuristic, so it warns rather than failing the run. +-/ +private def warnUncoveredTestModules (ws : Lake.Workspace) : IO Unit := do + let mut missed : Array Lean.Name := #[] + for lib in ws.root.leanLibs do + if lib.name == `ErrataGenerated then continue + let srcDir := lib.srcDir + for path in ← leanFiles srcDir do + let some mod := moduleOfPath srcDir path | continue + let withinRoot := lib.roots.any (·.isPrefixOf mod) + let globbed := lib.config.globs.any (·.matches mod) + if withinRoot && !globbed && !missed.contains mod then + let lines := (← IO.FS.readFile path).splitOn "\n" + if sourceHasTests lines then + missed := missed.push mod + unless missed.isEmpty do + IO.eprintln "warning: these modules look like they define tests but their library's globs do \ + not cover them, so the tests are not discovered. Widen the library's `globs` \ + (e.g. `globs := #[Glob.andSubmodules `Root]`):" + for mod in missed do + IO.eprintln s!" {mod}" + +script run (args) do + let ws ← getWorkspace + -- Answer `--help` before discovering or building anything. + if args.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 + -- 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. The generated runner lib has no source until this script writes it, and no tests. + let candidates := ws.root.leanLibs.filter (·.name != `ErrataGenerated) + 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 + -- Modules that look like they define tests but escape their library's globs are likely a + -- configuration slip; warn, but run the discovered suite anyway. + warnUncoveredTestModules ws + -- Build every module in the selected libraries; their compiled `.olean` headers are authoritative + -- on which modules carry tests, so no test is dropped by a source-level heuristic. + let modInfos ← runBuild do + let mut oleanJobs := #[] + let mut infos : Array (Lean.Name × System.FilePath) := #[] + for lib in libs do + let mods ← (← lib.modules.fetch).await + 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 + -- 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 + -- 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 / ".lake" / "errata-runner" + 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 diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean new file mode 100644 index 00000000..349a8c7b --- /dev/null +++ b/src/errata-tests/ErrataTests.lean @@ -0,0 +1,164 @@ +/- +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 + +Tests that exercise Errata using Errata itself. +-/ +module + +public import Errata +public meta import Errata + +open Errata + +/-- A bare boolean is a passing test. -/ +@[test] +def onePlusOne : Bool := 1 + 1 == 2 + +/-- An assertion-based test. -/ +@[test] +def equality : Test := do + assertEq 4 (2 + 2) + +/-- A test with named results. -/ +@[test] +def named : Test := do + result "first" (assertEq 1 1) + result "second" (assertContains "b" "abc") + +/-- A test that completes without any check is a bare success. -/ +@[test] +def emptyBody : Test := pure () + +/-- A test that expects a failure. -/ +@[test] +def expectsFailure : Test := + expectFail (assertEq 1 2) + +/-- A data-driven family expressed as a plain loop. -/ +@[test] +def squares : Test := do + for (n, sq) in [(1, 1), (2, 4), (3, 9)] do + result s!"square {n}" (assertEq sq (n * n)) + +/-- A subprocess test. -/ +@[test] +def echoRuns : Test := do + let out ← IO.Process.output { cmd := "echo", args := #["hello"] } + assertExitCode 0 out + assertContains "hello" out.stdout + +/-- info: 3 -/ +#test_msgs in +#eval 1 + 2 + +-- The expected block is read from the source, so `#test_msgs` works in verso docstring mode. +set_option doc.verso true in +/-- info: 7 -/ +#test_msgs in +#eval 3 + 4 + +/-- A property test. -/ +@[test] +def addComm : Test := + property (∀ a b : Nat, a + b = b + a) + +open Lean (toJson fromJson?) + +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Position +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Location +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for TestFailure +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Status +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Output +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for OutputLog +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Result + +/-- The JSON encoding of a result round-trips: decoding the encoding recovers the result. -/ +@[test] +def jsonRoundTrips : Test := + property (∀ r : Result, (fromJson? (toJson r)).toOption = some r) + +/-- A temp-directory fixture with a golden file. -/ +@[test] +def goldenRoundTrip : Test := + IO.FS.withTempDir fun dir => do + let goldenPath := dir / "expected.txt" + IO.FS.writeFile goldenPath "contents\n" + assertFileExists goldenPath + goldenFile goldenPath "contents\n" + +/-- The `Verbosity` predicates and accumulation behave as the report relies on. -/ +@[test] +def verbosityLevels : Test := do + assertEq false Verbosity.silent.showsPasses + assertEq true Verbosity.quiet.showsPasses + assertEq true Verbosity.verbose.showsPasses + assertEq true Verbosity.superVerbose.showsPasses + assertEq false Verbosity.silent.truncates + assertEq true Verbosity.quiet.truncates + assertEq false Verbosity.verbose.truncates + assertEq false Verbosity.superVerbose.truncates + assertEq false Verbosity.verbose.showsAllDocstrings + assertEq true Verbosity.superVerbose.showsAllDocstrings + assertEq Verbosity.quiet Verbosity.silent.increase + assertEq Verbosity.verbose Verbosity.quiet.increase + assertEq Verbosity.superVerbose Verbosity.verbose.increase + assertEq Verbosity.superVerbose Verbosity.superVerbose.increase + +/-- At silent verbosity the report hides passes but shows failures and the summary line. -/ +@[test] +def reportSilent : Test := do + let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass } + let fail : Result := { package := "p", moduleName := "M", test := "u", status := .fail { message := "boom" } } + let out ← captureOutput do discard <| humanReport .silent #[pass, fail] + assertContains "FAIL p/M u: boom" out.stdout + assertContains "1 passed, 1 failed, 0 errors, 0 skipped" out.stdout + assertEq 1 (out.stdout.splitOn "ok ").length + +/-- At verbose verbosity the report shows passes too. -/ +@[test] +def reportVerbose : Test := do + let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass } + let out ← captureOutput do discard <| humanReport .verbose #[pass] + assertContains "ok p/M t" out.stdout + +/-- A test's results are truncated after the cap at quiet verbosity, with a summary, but not at verbose. -/ +@[test] +def reportTruncates : Test := do + let many := (Array.range 60).map fun i => + ({ package := "p", moduleName := "M", test := "many", resultPath := #[s!"case {i}"], status := .pass } : Result) + let quiet ← captureOutput do discard <| humanReport .quiet many + assertEq 51 (quiet.stdout.splitOn "ok ").length + assertContains "(... and 10 more passed, 0 more failed)" quiet.stdout + let verbose ← captureOutput do discard <| humanReport .verbose many + assertEq 61 (verbose.stdout.splitOn "ok ").length + assertEq 1 (verbose.stdout.splitOn "(... and").length + +/-- `humanReport` returns the number of failures and errors. -/ +@[test] +def reportFailureCount : Test := do + let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass } + let fail : Result := { package := "p", moduleName := "M", test := "u", status := .fail { message := "x" } } + let err : Result := { package := "p", moduleName := "M", test := "v", status := .error "oops" } + assertEq 2 (← humanReport .silent #[pass, fail, err]) + +/-- `markdownReport` gives a tally, an open collapsible per failure, and a per-module table. -/ +@[test] +def reportMarkdown : Test := do + let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass } + let f : TestFailure := { message := "boom", detail? := some "expected 1\nactual 2" } + let fail : Result := { package := "p", moduleName := "M", test := "u", status := .fail f } + let md := markdownReport #[pass, fail] + assertContains "**1** passed · **1** failed" md + assertContains "
❌ p/M u: boom" md + assertContains "expected 1\nactual 2" md + assertContains "Summary by module" md + +/-- `failure` from the `Alternative` instance fails a test. -/ +@[test] +def alternativeFailure : Test := expectFail failure + +/-- `<|>` recovers from an assertion failure by running the alternative. -/ +@[test] +def alternativeOrElse : Test := failure <|> assertEq 1 1 diff --git a/src/errata/Errata.lean b/src/errata/Errata.lean new file mode 100644 index 00000000..1760f91c --- /dev/null +++ b/src/errata/Errata.lean @@ -0,0 +1,22 @@ +/- +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 Errata.Result +public import Errata.Context +public import Errata.Here +public import Errata.TestM +public import Errata.IsTest +public import Errata.Assertions +public import Errata.Process +public import Errata.Golden +public import Errata.Report +public import Errata.Runner +public import Errata.Discovery +public import Errata.CompileTime +public import Errata.Property + +set_option doc.verso true diff --git a/src/errata/Errata/Assertions.lean b/src/errata/Errata/Assertions.lean new file mode 100644 index 00000000..ce2d59eb --- /dev/null +++ b/src/errata/Errata/Assertions.lean @@ -0,0 +1,80 @@ +/- +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 Errata.TestM +public import Errata.Here + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- +Asserts that a condition holds. In a {lit}`do` block, {lit}`assert cond` and +{lit}`assert cond msg` invoke this assertion. +-/ +def assert (cond : Bool) (message : String := "assertion failed") + (loc : Location := by exact here%) : TestM Unit := + unless cond do failAt loc message + +-- The `assert` statement of `do` blocks parses its whole argument list as one term, so an +-- application there is the condition followed by the message. +macro_rules + | `(doElem| assert $p:term) => + match p with + | `($cond $message) => `(doElem| Errata.assert $cond $message) + | cond => `(doElem| Errata.assert $cond) + +/-- Asserts that the actual value equals the expected value, reporting both when they differ. -/ +def assertEq {α} [BEq α] [Repr α] (expected actual : α) + (loc : Location := by exact here%) : TestM Unit := + unless actual == expected do + failAt loc "values are not equal" (detail? := some s!"expected: {repr expected}\nactual: {repr actual}") + +/-- Asserts that the actual value differs from the unexpected value. -/ +def assertNe {α} [BEq α] [Repr α] (unexpected actual : α) + (loc : Location := by exact here%) : TestM Unit := do + if actual == unexpected then + failAt loc "values are equal but should differ" (detail? := some s!"both: {repr actual}") + +/-- Asserts that the actual string contains the expected substring. -/ +def assertContains (expected actual : String) (message : String := "substring not found") + (loc : Location := by exact here%) : TestM Unit := do + unless (actual.find? expected).isSome do + failAt loc message (detail? := some s!"expected to contain: {expected}\nactual: {actual}") + +/-- Asserts that the actual string does not contain the unexpected substring. -/ +def assertNotContains (unexpected actual : String) (message : String := "unexpected substring found") + (loc : Location := by exact here%) : TestM Unit := + unless (actual.find? unexpected).isNone do + failAt loc message (detail? := some s!"expected not to contain: {unexpected}\nactual: {actual}") + +/-- Asserts that a file exists. -/ +def assertFileExists (path : System.FilePath) + (loc : Location := by exact here%) : TestM Unit := do + unless ← path.pathExists do + failAt loc s!"file does not exist: {path}" + +/-- Asserts that an option is absent. -/ +def assertNone {α} [Repr α] (value : Option α) + (loc : Location := by exact here%) : Test := do + if let some v := value then + failAt loc s!"expected none, got {repr v}" + +/-- Asserts that an option is present, returning its contents. -/ +def assertSome {α} (value : Option α) + (loc : Location := by exact here%) : TestM α := + match value with + | some v => pure v + | none => throw { message := "expected some, got none", location? := some loc } + +/-- Asserts that an option is present, without inspecting its contents. -/ +def assertIsSome {α} (value : Option α) + (loc : Location := by exact here%) : Test := + discard (assertSome value loc) diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean new file mode 100644 index 00000000..06c349f7 --- /dev/null +++ b/src/errata/Errata/CompileTime.lean @@ -0,0 +1,151 @@ +/- +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 Errata.Result +public meta import Errata.CompileTime.Helpers +public import Lean.Elab.Command +public import Lean.Data.Options + +open Lean Elab Command Errata.CompileTime + +public section + +set_option doc.verso true + +/-- +When true, a failing Errata compile-time test is an elaboration error rather than a warning. +-/ +register_option errata.failOnError : Bool := { + defValue := false + descr := "Make a failing Errata compile-time test an elaboration error rather than a warning." +} + +namespace Errata + +/-- +Checks that the command below produces the messages given in the preceding doc comment. + +This is a version of `#guard_msgs` that is specialized for use in Errata. If the messages +don't match, it is not a compile-time error unless the option {lit}`errata.failOnError` is +{name}`true`. This allows failing compile-time tests to appear in the test output together +with failing run-time tests. +-/ +syntax (name := testMsgsCmd) (plainDocComment)? "#test_msgs" "in" command : command + +@[command_elab testMsgsCmd] +meta def elabTestMsgs : Command.CommandElab + | `($[$dc?:docComment]? #test_msgs%$tk in $cmd) => do + let expected := ((← dc?.mapM (getDocStringText ·)).getD "").trimAscii.copy + -- Elaborate the command, capturing its messages instead of letting them surface. Both the + -- synchronous log and the asynchronous snapshot tasks are collected, so messages from linters + -- (which run after elaboration) are included, as `#guard_msgs` does. + let saved := (← get).messages + modify ({ · with messages := {} }) + withReader ({ · with snap? := none }) do + elabCommandTopLevel cmd #[] + let produced := (← get).messages ++ + (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) .empty) .empty + modify ({ · with messages := saved, snapshotTasks := #[] }) + let visible := produced.toList.filter (!·.isSilent) + let strings ← (visible.mapM formatMessage : IO (List String)) + -- Multiple messages are separated by `---`, matching the block `#guard_msgs` compares against. + let actual := ("---\n".intercalate strings).trimAscii.copy + let passed := messagesMatch expected actual + -- Reify the verdict into a discovered test, named after the source position. The module name + -- qualifies it so that two modules with a `#test_msgs` at the same position do not collide. + let fileMap ← getFileMap + let startPos := fileMap.toPosition (tk.getPos?.getD 0) + let endPos := fileMap.toPosition (tk.getTailPos?.getD 0) + let declName := `_root_ ++ (← getMainModule) ++ + Name.mkSimple s!"errataMsgTest_L{startPos.line}_C{startPos.column}" + let verdict ← + if passed then + `(Errata.TestResult.pass) + else + `(Errata.TestResult.mismatch "compile-time messages do not match" $(quote actual) + $(quote (← getFileName)) + $(quote startPos.line) $(quote startPos.column) + $(quote endPos.line) $(quote endPos.column)) + elabCommand (← `(@[test] def $(mkIdent declName) : Errata.TestResult := $verdict)) + -- Report a mismatch at build time, offering the corrected expected block as a fix. + unless passed do + let fixRef := (dc?.map (·.raw)).getD tk + let hint ← liftCoreM <| MessageData.hint m!"Update the expected output:" + #[{ suggestion := suggestedDoc actual }] (ref? := some fixRef) + let body := m!"Errata #test_msgs: the messages do not match.\n\n\ + Expected:\n{expected}\n\nActual:\n{actual}" + if (← getOptions).getBool `errata.failOnError false then + logErrorAt tk (body ++ hint) + else + logWarningAt tk (body ++ hint) + | _ => throwUnsupportedSyntax + +/-- +Checks that a Boolean expression evaluates to {lean}`true`, registering the verdict as a test. + +This is a version of `#guard` that is specialized for use in Errata. If the condition does not +hold, it is not a compile-time error unless the option {lit}`errata.failOnError` is +{name}`true`. This allows failing compile-time tests to appear in the test output together +with failing run-time tests. + +-/ +syntax (name := testGuardCmd) "#test_guard" term : command + +@[command_elab testGuardCmd] +meta def elabTestGuard : Command.CommandElab + | `(#test_guard%$tk $e:term) => do + -- Evaluate the expression to a `Bool` at elaboration time, as `#guard` does. + let passed ← Command.liftTermElabM do + let v ← Term.elabTermEnsuringType e (mkConst ``Bool) + Term.synthesizeSyntheticMVarsNoPostponing + let v ← instantiateMVars v + let mvars ← Lean.Meta.getMVars v + if mvars.isEmpty then + unsafe Lean.Meta.evalExpr (checkMeta := false) Bool (mkConst ``Bool) v + else + discard <| Term.logUnassignedUsingErrorInfos mvars + pure false + -- The checked expression's source text and span, for naming, location, and detail. + let fileMap ← getFileMap + let startStr := e.raw.getPos?.getD 0 + let endStr := e.raw.getTailPos?.getD startStr + let source := ({ str := fileMap.source, startPos := startStr, stopPos := endStr } : Substring.Raw).toString + let startPos := fileMap.toPosition startStr + let endPos := fileMap.toPosition endStr + -- Name the test after the first line of the expression, in the current namespace, marking a + -- truncated multi-line expression with an ellipsis and disambiguating against earlier ones. + let lines := source.splitOn "\n" + -- Strip guillemets so an escaped name in the source does not nest inside the test's own name. + let firstLine := lines.headD source |>.trimAscii |>.replace "«" "" |>.replace "»" "" + let base := + if (lines.drop 1).any (fun l => !l.trimAscii.isEmpty) then firstLine ++ "…" else firstLine + let ns ← getCurrNamespace + let env ← getEnv + let mut name := base + let mut n := 1 + -- In a `module`, the generated definition is private, so probe its mangled name as well. + while env.contains (ns ++ Name.mkSimple name) + || env.contains (mkPrivateName env (ns ++ Name.mkSimple name)) do + n := n + 1 + name := s!"{base} ({n})" + let verdict ← + if passed then + `(Errata.TestResult.pass) + else + `(Errata.TestResult.mismatch "expression did not evaluate to `true`" $(quote source) + $(quote (← getFileName)) + $(quote startPos.line) $(quote startPos.column) + $(quote endPos.line) $(quote endPos.column)) + elabCommand (← `(@[test] def $(mkIdent (Name.mkSimple name)) : Errata.TestResult := $verdict)) + -- Report a failure at build time, as `#test_msgs` does. + unless passed do + let body := m!"Errata #test_guard: the expression did not evaluate to `true`:\n{source}" + if (← getOptions).getBool `errata.failOnError false then + logErrorAt tk body + else + logWarningAt tk body + | _ => throwUnsupportedSyntax diff --git a/src/errata/Errata/CompileTime/Helpers.lean b/src/errata/Errata/CompileTime/Helpers.lean new file mode 100644 index 00000000..50f58f87 --- /dev/null +++ b/src/errata/Errata/CompileTime/Helpers.lean @@ -0,0 +1,48 @@ +/- +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 + +Non-meta helpers for the `#test_msgs` command, kept separate so the command elaborator is the +only meta definition. +-/ +module + +public import Lean.Message +public import Lean.Elab.GuardMsgs + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata.CompileTime + +/-- Renders a message with a severity prefix, in the form the expected block is compared against. -/ +def formatMessage (msg : Lean.Message) : IO String := do + let mut str ← msg.data.toString + unless msg.caption == "" do + str := msg.caption ++ ":\n" ++ str + -- The severity is followed by a space only when the body stays on the same line, matching the + -- rendering that `#guard_msgs` compares against. + unless str.startsWith "\n" do str := " " ++ str + str := + if msg.isTrace then "trace:" ++ str + else match msg.severity with + | .information => "info:" ++ str + | .warning => "warning:" ++ str + | .error => "error:" ++ str + unless str.endsWith "\n" do str := str ++ "\n" + return str + +open Lean.Elab.Tactic.GuardMsgs (WhitespaceMode) in +/-- Whether the expected and actual message blocks match, normalizing whitespace as `#guard_msgs` does. -/ +def messagesMatch (expected actual : String) : Bool := + let norm := fun s => (WhitespaceMode.normalized.apply s).trimAscii.copy + norm expected == norm actual + +/-- The doc comment that would make the expected block match the actual output. -/ +def suggestedDoc (actual : String) : String := + if actual.isEmpty then "" + else if actual.contains '\n' then s!"/--\n{actual}\n-/\n" + else s!"/-- {actual} -/\n" diff --git a/src/errata/Errata/Context.lean b/src/errata/Errata/Context.lean new file mode 100644 index 00000000..d72d8060 --- /dev/null +++ b/src/errata/Errata/Context.lean @@ -0,0 +1,56 @@ +/- +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 Std.Data.HashSet +public import Errata.Result + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +open Std (HashMap HashSet) + +/-- A multi-map from option names to all the values supplied for them. -/ +abbrev OptionMap := HashMap String (Array String) + +/-- The run-wide configuration and per-test state threaded through every test. -/ +structure Context where + /-- The reporting verbosity. -/ + verbosity : Verbosity := .silent + /-- Whether golden checks rewrite their expected files instead of comparing. -/ + updateGolden : Bool := false + /-- Project-specific options, as a multi-map so repeated options accumulate. -/ + options : OptionMap := {} + /-- The seed used for property tests, or {lean}`none` to draw a fresh one. -/ + seed : Option Nat := none + /-- The package that defines the running test. -/ + package : String := "" + /-- The module that defines the running test, as a dotted name. -/ + moduleName : String := "" + /-- The running test declaration's name below its module. -/ + test : String := "" + /-- The running test's docstring, rendered as Markdown, when it has one. -/ + description? : Option String := none + /-- The named result currently being recorded, below the test. -/ + resultPath : Array String := #[] + /-- + The source location reported for the next failure. The runner seeds it with the test's own + source range; the assertion language refines it to each call site. + -/ + location : Location := default + /-- The results collected so far during the current test. -/ + log : IO.Ref (Array Result) + /-- The option names read during the run, shared across all tests, for reporting unused options. -/ + usedOptions : IO.Ref (HashSet String) + /-- + Receives each captured output fragment as it is written, in order. The default discards them; a + live runner sets it to stream output as the test produces it. + -/ + writeOutput : Output → IO Unit := fun _ => pure () diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean new file mode 100644 index 00000000..e39527ad --- /dev/null +++ b/src/errata/Errata/Discovery.lean @@ -0,0 +1,127 @@ +/- +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 Errata.IsTest +public import Errata.Runner +public import Lean +public meta import Lean + +open Lean Meta Elab Term + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- +Verifies that a tagged declaration can be run as a test: it is not {lit}`meta`, and it has an +{name}`IsTest` instance. +-/ +meta def checkIsTest (decl : Name) : MetaM Unit := do + let env ← getEnv + if isMarkedMeta env decl then + throwError m!"A test must not be `meta`" + let info ← getConstInfo decl + let goal := mkApp (mkConst ``IsTest) info.type + match ← trySynthInstance goal with + | .some _ => pure () + | _ => + throwError m!"`@[test]` requires an `Errata.IsTest` instance for the test's type{indentExpr info.type}" + +/-- +A recorded test: its declaration name and the source file that defines it. The file is captured +when the attribute is applied; the declaration's line and column are recovered later, once the +declaration ranges are available. +-/ +structure TestDecl where + /-- The test declaration's name. -/ + name : Name + /-- The source file that defines the test. -/ + file : String + /-- The test's docstring, rendered as Markdown, captured when the attribute is applied. -/ + docstring? : Option String := none +deriving Inhabited + +/-- +The tests recorded by {lit}`@[test]`, per module. The attribute is an elaboration-time feature: +tests are recorded as modules are elaborated, and {lit}`getAllTests%` reads them back at elaboration +time to build the runnable test array. +-/ +meta initialize testExt : SimplePersistentEnvExtension TestDecl (Array TestDecl) ← + registerSimplePersistentEnvExtension { + name := `Errata.test + addEntryFn := Array.push + addImportedFn := fun es => es.foldl Array.append #[] + } + +/-- Records a declaration as a test, capturing the source file that defines it and its docstring. +The docstring is read here, while it is still in the live environment, since a downstream build does +not load the imported docstrings. -/ +meta def recordTest (decl : Name) : AttrM Unit := do + (checkIsTest decl).run' + let docstring? ← findDocString? (← getEnv) decl + modifyEnv (testExt.addEntry · { name := decl, file := ← getFileName, docstring? }) + +/-- Marks a definition as a test, discovered and run by the Errata test runner. -/ +meta initialize + registerBuiltinAttribute { + ref := `Errata.test + name := `test + descr := "Marks a definition as a test, discovered and run by the Errata test runner." + -- Applied after compilation so the declaration's docstring is in the environment to capture. + applicationTime := .afterCompilation + add := fun decl stx kind => do + Attribute.Builtin.ensureNoArgs stx + unless kind == AttributeKind.global do throwAttrMustBeGlobal `test kind + recordTest decl + } + +/-- The test's name below its module: the declaration's components past the module prefix, dotted. -/ +meta def testNameBelow (moduleName declName : Name) : String := + let below := + if moduleName.isPrefixOf declName then declName.components.drop moduleName.components.length + else declName.components + ".".intercalate (below.map (·.toString)) + +/-- +{lit}`getAllTests% "package" Mod.A Mod.B ...` reads the tests recorded by {lit}`@[test]` in the +named modules and expands to the array of {name}`TestEntry` values that run them. Each module must +be imported, with {lit}`import all` for module-system modules, so its tests are reachable. +-/ +syntax (name := getAllTests) "getAllTests%" str ident* : term + +/-- Expands {lit}`getAllTests%` by reading the recorded tests of the named modules. -/ +@[term_elab getAllTests] +meta def elabGetAllTests : TermElab := fun stx expectedType? => do + let `(getAllTests% $pkg:str $mods:ident*) := stx + | throwUnsupportedSyntax + let package := pkg.getString + let env ← getEnv + let mut entries : Array Term := #[] + for modStx in mods do + let moduleName := modStx.getId + let some idx := env.getModuleIdx? moduleName | continue + let moduleStr := moduleName.toString + for test in testExt.getModuleEntries env idx do + let userName := privateToUserName test.name + let testName := testNameBelow moduleName userName + let range ← findDeclarationRanges? test.name + let pos := (range.map (·.range.pos)).getD ⟨0, 0⟩ + let endPos := (range.map (·.range.endPos)).getD ⟨0, 0⟩ + -- The docstring captured when the attribute was applied, so the report and widget can show it. + let docStx ← match test.docstring? with + | some doc => `(some $(quote doc)) + | none => `((none : Option String)) + entries := entries.push <| ← + `(Errata.TestEntry.of $(quote package) $(quote moduleStr) $(quote testName) + (Errata.Location.mk $(quote test.file) + (Errata.Position.mk $(quote pos.line) $(quote pos.column)) + (Errata.Position.mk $(quote endPos.line) $(quote endPos.column))) + (@$(mkIdent userName)) (docstring? := $docStx)) + elabTerm (← `(#[$entries,*])) expectedType? diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean new file mode 100644 index 00000000..5aba57d0 --- /dev/null +++ b/src/errata/Errata/Golden.lean @@ -0,0 +1,87 @@ +/- +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 Errata.TestM +import Lean.Util.Diff + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- +A line-by-line diff of expected against actual output. Lines marked {lit}`-` are in the expected +output only, and lines marked {lit}`+` are in the actual output only. +-/ +private def goldenDiff (expected actual : String) : String := + let diff := Lean.Diff.diff (expected.splitOn "\n").toArray (actual.splitOn "\n").toArray + "- expected, + actual:\n" ++ Lean.Diff.linesToString diff + +/-- Compares a produced string against a golden file, or rewrites it under `--update-golden`. -/ +def goldenFile (expected : System.FilePath) (actual : String) + (loc : Location := by exact here%) : TestM Unit := do + let ctx ← read + if ctx.updateGolden then + if let some parent := expected.parent then IO.FS.createDirAll parent + IO.FS.writeFile expected actual + else if ← expected.pathExists then + let want ← IO.FS.readFile expected + unless want == actual do + failAt loc s!"golden mismatch for {expected}" (detail? := some (goldenDiff want actual)) + else + failAt loc s!"missing golden file {expected}" + (detail? := some "Run with --update-golden to create it.") + +/-- All files below a directory, recursively, in a deterministic order. -/ +partial def filesUnder (dir : System.FilePath) : IO (Array System.FilePath) := do + let mut out : Array System.FilePath := #[] + for entry in ← dir.readDir do + if ← entry.path.isDir then + out := out ++ (← filesUnder entry.path) + else + out := out.push entry.path + return out.qsort (·.toString < ·.toString) + +/-- The path of a file relative to a base directory. -/ +private def relativeTo (base file : System.FilePath) : String := + (file.toString.drop (base.toString.length + 1)).copy + +/-- Compares a produced directory tree against a golden tree, or rewrites it under `--update-golden`. -/ +def goldenDir (expected actual : System.FilePath) + (loc : Location := by exact here%) : TestM Unit := do + let ctx ← read + let actualFiles ← filesUnder actual + if ctx.updateGolden then + let actualRels := actualFiles.map (relativeTo actual) + for file in actualFiles do + let dest := expected / relativeTo actual file + if let some parent := dest.parent then IO.FS.createDirAll parent + IO.FS.writeFile dest (← IO.FS.readFile file) + -- Remove expected files that the produced output no longer contains. + if ← expected.pathExists then + for file in ← filesUnder expected do + unless actualRels.contains (relativeTo expected file) do + IO.FS.removeFile file + return + unless ← expected.pathExists do + failAt loc s!"missing golden directory {expected}" + (detail? := some "Run with --update-golden to create it.") + for file in actualFiles do + let rel := relativeTo actual file + let want := expected / rel + unless ← want.pathExists do + failAt loc s!"file not present in the golden directory: {rel}" + let wantContent ← IO.FS.readFile want + let gotContent ← IO.FS.readFile file + unless wantContent == gotContent do + failAt loc s!"golden mismatch for {rel}" (detail? := some (goldenDiff wantContent gotContent)) + for file in ← filesUnder expected do + let rel := relativeTo expected file + unless ← (actual / rel).pathExists do + failAt loc s!"file missing from the produced output: {rel}" diff --git a/src/errata/Errata/Here.lean b/src/errata/Errata/Here.lean new file mode 100644 index 00000000..5486a74b --- /dev/null +++ b/src/errata/Errata/Here.lean @@ -0,0 +1,32 @@ +/- +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 Errata.Result +public meta import Lean + +open Lean Elab Term + +public section + +set_option doc.verso true + +/-- +`here%` elaborates to the {name}`Errata.Location` of its own occurrence. Used as a default argument +(`by exact here%`), it is elaborated at each call site, so it captures the caller's position. +-/ +syntax (name := hereStx) "here%" : term + +@[term_elab hereStx] +meta def elabHere : TermElab := fun _stx _expectedType? => do + let ref ← getRef + let fileMap ← getFileMap + let startPos := fileMap.toPosition (ref.getPos?.getD 0) + let endPos := fileMap.toPosition (ref.getTailPos?.getD (ref.getPos?.getD 0)) + let file ← getFileName + elabTerm (← `(Errata.Location.mk $(quote file) + (Errata.Position.mk $(quote startPos.line) $(quote startPos.column)) + (Errata.Position.mk $(quote endPos.line) $(quote endPos.column)))) none diff --git a/src/errata/Errata/IsTest.lean b/src/errata/Errata/IsTest.lean new file mode 100644 index 00000000..1f4d1728 --- /dev/null +++ b/src/errata/Errata/IsTest.lean @@ -0,0 +1,42 @@ +/- +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 Errata.TestM +public import Errata.Result + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- Runs a returned verdict as a test action. -/ +def TestResult.toTest : TestResult → TestM Unit + | .pass => pure () + | .fail f => throw f + | .skip reason => Errata.skip reason + +/-- Types that can serve as the body of a test. -/ +class IsTest (α : Type) where + /-- Runs the value as a test action. -/ + toTest : α → TestM Unit + +instance : IsTest (TestM Unit) where + toTest act := act + +instance : IsTest TestResult where + toTest := TestResult.toTest + +instance : IsTest (IO TestResult) where + toTest act := do (← act).toTest + +instance : IsTest Bool where + toTest b := unless b do failHere "expected true, got false" + +instance : IsTest (IO Bool) where + toTest act := do unless (← act) do failHere "expected true, got false" diff --git a/src/errata/Errata/Process.lean b/src/errata/Errata/Process.lean new file mode 100644 index 00000000..4209e322 --- /dev/null +++ b/src/errata/Errata/Process.lean @@ -0,0 +1,23 @@ +/- +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 Errata.TestM +public import Errata.Here + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- Asserts that a process exited with the expected code, showing its output otherwise. -/ +def assertExitCode (expected : UInt32) (output : IO.Process.Output) + (loc : Location := by exact here%) : TestM Unit := + unless output.exitCode == expected do + failAt loc s!"process exited with code {output.exitCode}, expected {expected}" + (detail? := some s!"stdout:\n{output.stdout}\nstderr:\n{output.stderr}") diff --git a/src/errata/Errata/Property.lean b/src/errata/Errata/Property.lean new file mode 100644 index 00000000..12aa48d6 --- /dev/null +++ b/src/errata/Errata/Property.lean @@ -0,0 +1,35 @@ +/- +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 Errata.TestM +public import Plausible +public import Plausible.ArbitraryFueled + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +open Plausible + +open scoped Plausible.Decorations in +/-- Checks a property with Plausible, failing with the counterexample if it is falsified. -/ +def property (p : Prop) (cfg : Configuration := {}) (loc : Location := by exact here%) + (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : TestM Unit := do + let ctx ← read + let cfg := { cfg with + quiet := true, + randomSeed := ctx.seed.orElse (fun _ => cfg.randomSeed) + } + match ← Testable.checkIO p' (cfg := cfg) with + | .success _ => pure () + | .gaveUp n => failAt loc s!"property gave up after discarding {n} cases" + | .failure _ counterExample _ => + failAt loc "property falsified" (detail? := some ("\n".intercalate counterExample)) diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean new file mode 100644 index 00000000..e220b50f --- /dev/null +++ b/src/errata/Errata/Report.lean @@ -0,0 +1,319 @@ +/- +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 Errata.Result +public import Lean.Data.Json + +public section + +open Lean (Json ToJson FromJson) + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- The number of results that did not pass. -/ +def failureCount (results : Array Result) : Nat := + results.foldl (fun n r => if r.status.isSuccess then n else n + 1) 0 + +private def indentLines (text : String) : String := + "\n".intercalate ((text.splitOn "\n").map (fun l => " " ++ l)) + +/-- A source location rendered as the clickable `file:line:col` of the span's start. -/ +private def locationText (l : Location) : String := + s!"{l.file}:{l.startPos.line}:{l.startPos.column}" + +/-- Prints one result: its status line, its docstring when shown, and for a failure its detail and +captured output. A failure or error shows its docstring; a pass or skip shows it only when the +verbosity does. -/ +private def printResult (verbosity : Verbosity) (r : Result) : IO Unit := do + let name := s!"{r.moduleTarget} {r.testName}" + let printDoc : IO Unit := do + if verbosity.showsAllDocstrings || !r.status.isSuccess then + if let some d := r.description? then IO.println (indentLines d) + match r.status with + | .pass => IO.println s!"ok {name} ({r.durationMs}ms)"; printDoc + | .skip reason => IO.println s!"skip {name}: {reason}"; printDoc + | .fail f => + IO.println s!"FAIL {name}: {f.message}" + printDoc + if let some l := f.location? then IO.println (indentLines (locationText l)) + if let some d := f.detail? then IO.println (indentLines d) + unless r.output.isEmpty do IO.println (indentLines s!"output:\n{r.output.all}") + | .error m => + IO.println s!"ERROR {name}: {m}" + printDoc + unless r.output.isEmpty do IO.println (indentLines s!"output:\n{r.output.all}") + +/-- A running tally of results suppressed by truncation. -/ +private structure Suppressed where + passed : Nat := 0 + failed : Nat := 0 + errors : Nat := 0 + skipped : Nat := 0 + +/-- Counts one more suppressed result. -/ +private def Suppressed.add (s : Suppressed) : Status → Suppressed + | .pass => { s with passed := s.passed + 1 } + | .fail _ => { s with failed := s.failed + 1 } + | .error _ => { s with errors := s.errors + 1 } + | .skip _ => { s with skipped := s.skipped + 1 } + +/-- The number of suppressed results. -/ +private def Suppressed.total (s : Suppressed) : Nat := + s.passed + s.failed + s.errors + s.skipped + +/-- Prints the truncation summary for a test whose results were capped, if any were suppressed. -/ +private def printSuppressed (s : Suppressed) : IO Unit := do + if s.total > 0 then + let parts := #[s!"{s.passed} more passed", s!"{s.failed} more failed"] + ++ (if s.errors > 0 then #[s!"{s.errors} more errors"] else #[]) + ++ (if s.skipped > 0 then #[s!"{s.skipped} more skipped"] else #[]) + IO.println s!" (... and {", ".intercalate parts.toList})" + +/-- +Prints a human-readable report and returns the number of failures. Verbosity 0 shows only failures +and errors; 1 also shows passes and skips but truncates each test's results after a cap, summarizing +the rest; 2 shows everything. +-/ +def humanReport (verbosity : Verbosity) (results : Array Result) : IO Nat := do + let cap := 50 + let mut passed := 0 + let mut failed := 0 + let mut errors := 0 + let mut skipped := 0 + let mut curKey : Option (String × String) := none + let mut shown := 0 + let mut more : Suppressed := {} + for r in results do + match r.status with + | .pass => passed := passed + 1 + | .fail _ => failed := failed + 1 + | .error _ => errors := errors + 1 + | .skip _ => skipped := skipped + 1 + -- Results of one test are contiguous; truncation is per test (its data-driven sub-results). + let key := (r.moduleTarget, r.test) + if curKey != some key then + printSuppressed more + curKey := some key + shown := 0 + more := {} + let displayable := + match r.status with + | .pass | .skip _ => verbosity.showsPasses + | .fail _ | .error _ => true + if displayable then + if verbosity.truncates && shown ≥ cap then + more := more.add r.status + else + printResult verbosity r + shown := shown + 1 + printSuppressed more + IO.println s!"{passed} passed, {failed} failed, {errors} errors, {skipped} skipped" + return failed + errors + +/-- +Drops the control characters XML 1.0 forbids even when escaped: those below {lit}`U+0020` other than +tab, newline, and carriage return. +-/ +private def dropXmlForbidden (s : String) : String := + s.foldl (init := "") fun acc c => + if c == '\t' || c == '\n' || c == '\r' || Nat.ble 0x20 c.toNat then acc.push c else acc + +/-- +Escapes text for XML and drops characters XML 1.0 forbids even when escaped, so a captured ANSI escape +or NUL byte in a message or output fragment cannot make the report malformed. +-/ +private def xmlEscape (s : String) : String := + dropXmlForbidden <| + s.replace "&" "&" |>.replace "<" "<" |>.replace ">" ">" |>.replace "\"" """ + +instance : ToJson Location where + toJson l := json%{ + "file": $l.file, + "startLine": $l.startPos.line, + "startColumn": $l.startPos.column, + "endLine": $l.endPos.line, + "endColumn": $l.endPos.column + } + +instance : FromJson Location where + fromJson? j := do + return { + file := ← j.getObjValAs? String "file", + startPos := ⟨← j.getObjValAs? Nat "startLine", ← j.getObjValAs? Nat "startColumn"⟩, + endPos := ⟨← j.getObjValAs? Nat "endLine", ← j.getObjValAs? Nat "endColumn"⟩ + } + +instance : ToJson Output where + toJson + | .stdout s => json%{ "stream": "stdout", "text": $s } + | .stderr s => json%{ "stream": "stderr", "text": $s } + +instance : FromJson Output where + fromJson? j := do + let text ← j.getObjValAs? String "text" + match ← j.getObjValAs? String "stream" with + | "stdout" => return .stdout text + | "stderr" => return .stderr text + | other => .error s!"unknown output stream: {other}" + +instance : ToJson OutputLog where + toJson o := ToJson.toJson o.log + +instance : FromJson OutputLog where + fromJson? j := return { log := ← FromJson.fromJson? j } + +/-- The suite a result belongs to: its module. -/ +private def suiteOf (r : Result) : String := + r.moduleName + +/-- The case name of a result: the test name below the module. -/ +private def caseOf (r : Result) : String := + r.testName + +private def countWhere (results : Array Result) (p : Status → Bool) : Nat := + results.foldl (fun n r => if p r.status then n + 1 else n) 0 + +/-- Groups results by their module in a single pass, keeping each module's first-seen order. -/ +private def byModule (results : Array Result) : Array (String × Array Result) := Id.run do + let mut order : Array String := #[] + let mut groups : Std.HashMap String (Array Result) := {} + for r in results do + let s := suiteOf r + if !groups.contains s then order := order.push s + groups := groups.alter s fun cur => some ((cur.getD #[]).push r) + return order.map fun s => (s, groups.getD s #[]) + +/-- Renders the results as JUnit XML, grouping by the module path. -/ +def junitReport (results : Array Result) : String := Id.run do + let mut out := "\n\n" + for (suite, cases) in byModule results do + let pkg := (cases[0]?.map (·.package)).getD "" + let failures := countWhere cases (fun s => s matches .fail _) + let errors := countWhere cases (fun s => s matches .error _) + let skipped := countWhere cases (fun s => s matches .skip _) + out := out ++ s!" \n" + for r in cases do + let time := toString (Float.ofNat r.durationMs / 1000.0) + let opening := s!" " + match r.status with + | .pass => + out := out ++ opening ++ "\n" + | .fail f => + let loc := match f.location? with | some l => locationText l ++ ": " | none => "" + out := out ++ opening ++ s!"\n \ + {xmlEscape (f.detail?.getD "")}\n \n" + | .error m => + out := out ++ opening ++ s!"\n \n \n" + | .skip reason => + out := out ++ opening ++ s!"\n \n \n" + out := out ++ " \n" + out := out ++ "\n" + return out + +private def statusFields : Status → List (String × Json) + | .pass => [("status", Json.str "pass")] + | .fail f => + [("status", Json.str "fail"), ("message", Json.str f.message)] ++ + (match f.detail? with | some d => [("detail", Json.str d)] | none => []) ++ + (match f.location? with | some l => [("location", ToJson.toJson l)] | none => []) + | .error m => [("status", Json.str "error"), ("message", Json.str m)] + | .skip reason => [("status", Json.str "skip"), ("reason", Json.str reason)] + +instance : ToJson Result where + toJson r := private + Json.mkObj <| + [("package", Json.str r.package), ("module", Json.str r.moduleName), + ("test", Json.str r.test), ("resultPath", ToJson.toJson r.resultPath), + ("durationMs", ToJson.toJson r.durationMs)] ++ + statusFields r.status ++ + (if r.output.isEmpty then [] else [("output", ToJson.toJson r.output)]) ++ + (match r.description? with | some d => [("description", Json.str d)] | none => []) + +/-- Decodes an optional field: absent maps to {lean}`none`. -/ +private def optField [FromJson α] (j : Json) (key : String) : Except String (Option α) := + match j.getObjVal? key with + | .ok v => some <$> FromJson.fromJson? v + | .error _ => pure none + +instance : FromJson Status where + fromJson? j := private do + match ← j.getObjValAs? String "status" with + | "pass" => return .pass + | "error" => return .error (← j.getObjValAs? String "message") + | "skip" => return .skip (← j.getObjValAs? String "reason") + | "fail" => return .fail { + message := ← j.getObjValAs? String "message", + detail? := ← optField j "detail", + location? := ← optField j "location" + } + | other => .error s!"unknown status: {other}" + +instance : FromJson Result where + fromJson? j := private do + return { + package := ← j.getObjValAs? String "package", + moduleName := ← j.getObjValAs? String "module", + test := ← j.getObjValAs? String "test", + resultPath := ← j.getObjValAs? (Array String) "resultPath", + durationMs := ← j.getObjValAs? Nat "durationMs", + status := ← FromJson.fromJson? j, + output := (← optField j "output").getD {}, + description? := ← optField j "description" + } + +/-- Renders the results as a JSON array of objects. -/ +def jsonReport (results : Array Result) : String := (ToJson.toJson results).pretty + +/-- The length of the longest run of consecutive backticks in {name}`s`. -/ +private def longestBacktickRun (s : String) : Nat := + (s.foldl (init := (0, 0)) fun (cur, best) c => + if c == '`' then (cur + 1, Nat.max best (cur + 1)) else (0, best)).2 + +/-- Wraps {name}`body` in a fenced code block whose fence outlasts any backtick run inside it. -/ +private def fencedBlock (body : String) : String := + let fence := String.ofList (List.replicate (Nat.max 3 (longestBacktickRun body + 1)) '`') + s!"{fence}\n{body}\n{fence}" + +/-- +Renders the results as Markdown for a CI job summary: a headline tally, each failure and error in an +open collapsible block with its location and detail, and a per-module table in a closed one. +-/ +def markdownReport (results : Array Result) : String := Id.run do + let passed := countWhere results (· matches .pass) + let failed := countWhere results (· matches .fail _) + let errors := countWhere results (· matches .error _) + let skipped := countWhere results (· matches .skip _) + let icon := if failed + errors == 0 then "✅" else "❌" + let mut out := s!"## {icon} Errata test results\n\n" + out := out ++ + s!"**{passed}** passed · **{failed}** failed · **{errors}** errors · **{skipped}** skipped\n\n" + for r in results do + let render (mark message : String) (detail? : Option String) : String := Id.run do + let mut s := s!"
{mark} {xmlEscape r.moduleTarget} \ + {xmlEscape r.testName}: {xmlEscape message}\n\n" + if let some d := r.description? then s := s ++ s!"{d}\n\n" + if let .fail f := r.status then + if let some l := f.location? then s := s ++ s!"`{locationText l}`\n\n" + if let some d := detail? then s := s ++ s!"{fencedBlock d}\n\n" + unless r.output.isEmpty do + s := s ++ s!"
output\n\n{fencedBlock r.output.all}\n\n
\n\n" + return s ++ "
\n\n" + match r.status with + | .fail f => out := out ++ render "❌" f.message f.detail? + | .error m => out := out ++ render "💥" m none + | _ => pure () + out := out ++ "
Summary by module\n\n" + out := out ++ "| Module | ✅ | ❌ | 💥 | ⏭️ |\n| :-- | --: | --: | --: | --: |\n" + for (m, cs) in byModule results do + out := out ++ s!"| {m} | {countWhere cs (· matches .pass)} | {countWhere cs (· matches .fail _)} \ + | {countWhere cs (· matches .error _)} | {countWhere cs (· matches .skip _)} |\n" + return out ++ "\n
\n" diff --git a/src/errata/Errata/Result.lean b/src/errata/Errata/Result.lean new file mode 100644 index 00000000..963bc37e --- /dev/null +++ b/src/errata/Errata/Result.lean @@ -0,0 +1,186 @@ +/- +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 section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- How much the human-readable report prints. -/ +inductive Verbosity where + /-- Print only failures and errors. -/ + | silent + /-- Also print passes and skips, truncating each test's results after a cap. -/ + | quiet + /-- Print every result. -/ + | verbose + /-- Print every result, and each test's docstring alongside it, not only those that fail. -/ + | superVerbose +deriving Repr, Inhabited, DecidableEq, BEq + +/-- Whether passes and skips are printed at this verbosity. -/ +def Verbosity.showsPasses : Verbosity → Bool + | .silent => false + | .quiet | .verbose | .superVerbose => true + +/-- Whether each test's results are truncated after a cap at this verbosity. -/ +def Verbosity.truncates : Verbosity → Bool + | .quiet => true + | .silent | .verbose | .superVerbose => false + +/-- Whether every result's docstring is shown, not only those of failures and errors. -/ +def Verbosity.showsAllDocstrings : Verbosity → Bool + | .superVerbose => true + | .silent | .quiet | .verbose => false + +/-- The next verbosity up, for an accumulating {lit}`-v` / {lit}`-vv` / {lit}`-vvv`. -/ +def Verbosity.increase : Verbosity → Verbosity + | .silent => .quiet + | .quiet => .verbose + | .verbose | .superVerbose => .superVerbose + +/-- A line and column within a source file, counting from one. -/ +structure Position where + /-- The line, counting from one. -/ + line : Nat + /-- The column, counting from one. -/ + column : Nat +deriving Repr, Inhabited, BEq, DecidableEq + +/-- A source span, used in failure messages and editor integration. -/ +structure Location where + /-- The source file that contains the span. -/ + file : String + /-- The start of the span. -/ + startPos : Position + /-- The end of the span. -/ + endPos : Position +deriving Repr, Inhabited, BEq, DecidableEq + +/-- A test failure, carrying the information needed to explain it. -/ +structure TestFailure where + /-- A short description of what went wrong. -/ + message : String + /-- Supporting detail, such as a diff, a counterexample, or expected and actual values. -/ + detail? : Option String := none + /-- The source location of the failed check, when known. -/ + location? : Option Location := none +deriving Repr, Inhabited, DecidableEq + +/-- The verdict that a test body may return. -/ +inductive TestResult where + /-- The test passed. -/ + | pass + /-- The test failed, with details. -/ + | fail (failure : TestFailure) + /-- The test was skipped, with a reason. -/ + | skip (reason : String) +deriving Repr, Inhabited + +/-- The recorded outcome of a test or a named result. -/ +inductive Status where + /-- The check passed. -/ + | pass + /-- The check failed. -/ + | fail (failure : TestFailure) + /-- An error escaped the check, so it could not produce a verdict. -/ + | error (message : String) + /-- The check was skipped. -/ + | skip (reason : String) +deriving Repr, Inhabited, DecidableEq + +/-- Whether a status counts as success for the exit code. -/ +def Status.isSuccess : Status → Bool + | .pass | .skip _ => true + | .fail _ | .error _ => false + +/-- A fragment of captured output, tagged by the stream it was written to. -/ +inductive Output where + /-- Text written to standard output. -/ + | stdout (text : String) + /-- Text written to standard error. -/ + | stderr (text : String) +deriving Repr, Inhabited, DecidableEq + +/-- The text of an output fragment, regardless of stream. -/ +def Output.text : Output → String + | .stdout s | .stderr s => s + +/-- All captured output, concatenated in order. -/ +def capturedText (output : Array Output) : String := + output.foldl (fun acc o => acc ++ o.text) "" + +/-- Output captured from an action, in order and tagged by stream. -/ +structure OutputLog where + /-- The captured fragments, in order, tagged by stream. -/ + log : Array Output := #[] +deriving Repr, Inhabited, DecidableEq + +namespace OutputLog + +/-- Whether no output was captured. -/ +def isEmpty (o : OutputLog) : Bool := o.log.isEmpty + +/-- The text written to stdout, concatenated in order. -/ +def stdout (o : OutputLog) : String := + o.log.foldl (fun acc out => match out with | .stdout s => acc ++ s | .stderr _ => acc) "" + +/-- The text written to stderr, concatenated in order. -/ +def stderr (o : OutputLog) : String := + o.log.foldl (fun acc out => match out with | .stderr s => acc ++ s | .stdout _ => acc) "" + +/-- The text written to stdout and stderr, concatenated in order. -/ +def all (o : OutputLog) : String := capturedText o.log + +end OutputLog + +/-- One entry collected during a run and rendered by the reporters. -/ +structure Result where + /-- The package that defines the test. -/ + package : String + /-- The module that defines the test, as a dotted name. -/ + moduleName : String + /-- The test declaration's name below its module, as a dotted name. -/ + test : String + /-- The named result below the test; empty for the test's own result. -/ + resultPath : Array String := #[] + /-- The recorded outcome. -/ + status : Status + /-- How long the check took, in milliseconds. -/ + durationMs : Nat := 0 + /-- What the test wrote to stdout and stderr. -/ + output : OutputLog := {} + /-- The test's docstring, rendered as Markdown, when it has one. -/ + description? : Option String := none +deriving Repr, Inhabited, DecidableEq + +/-- The test name below the module: the declaration and any named result, dotted. -/ +def Result.testName (result : Result) : String := + if result.resultPath.isEmpty then result.test + else result.test ++ "." ++ ".".intercalate result.resultPath.toList + +/-- +The module as a Lake target specification ({lit}`package/module`). This is the unit of execution: +passing it to {lit}`lake test` re-runs the module that produced the result. +-/ +def Result.moduleTarget (result : Result) : String := + result.package ++ "/" ++ result.moduleName + +/-- A failed verdict from a compile-time message mismatch, carrying its source span. -/ +def TestResult.mismatch (message detail file : String) + (startLine startCol endLine endCol : Nat) : TestResult := + .fail { + message, + detail? := some detail, + location? := some { + file, + startPos := { line := startLine, column := startCol }, + endPos := { line := endLine, column := endCol } + } + } diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean new file mode 100644 index 00000000..7f4464c3 --- /dev/null +++ b/src/errata/Errata/Runner.lean @@ -0,0 +1,184 @@ +/- +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 Errata.TestM +public import Errata.IsTest +public import Errata.Report + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- A test to run: its identity and the action that produces its results. -/ +structure TestEntry where + /-- The package that defines the test. -/ + package : String + /-- The module that defines the test, as a dotted name. -/ + moduleName : String + /-- The test declaration's name below its module. -/ + test : String + /-- The test's own source range, used as the default failure location. -/ + location : Location + /-- The test's docstring, rendered as Markdown, when it has one. -/ + docstring? : Option String := none + /-- The action to run. -/ + run : TestM Unit + +/-- Builds a test entry from any testable value. -/ +def TestEntry.of {α} [IsTest α] (package moduleName test : String) (location : Location) + (value : α) (docstring? : Option String := none) : TestEntry where + package := package + moduleName := moduleName + test := test + location := location + docstring? := docstring? + run := IsTest.toTest value + +/-- Runs a single test entry, collecting all of its results. -/ +def runEntry (cfg : Context) (entry : TestEntry) : IO (Array Result) := do + let log ← IO.mkRef (#[] : Array Result) + let ctx := { cfg with + package := entry.package, moduleName := entry.moduleName, test := entry.test, + resultPath := #[], location := entry.location, log, description? := entry.docstring? + } + let start ← IO.monoMsNow + let (outcome, output) ← runCapturing ctx entry.run + let stop ← IO.monoMsNow + let dur := stop - start + let logged ← log.get + return match ctx.resultOfOutcome outcome output dur (!logged.isEmpty) with + | some r => logged.push r + | none => logged + +/-- Runs all the test entries and collects their results. -/ +def run (cfg : Context) (entries : Array TestEntry) : IO (Array Result) := do + let mut all : Array Result := #[] + for entry in entries do + all := all ++ (← runEntry cfg entry) + return all + +/-- A base context with the given settings and a fresh, empty log. -/ +def mkContext (verbosity : Verbosity := .silent) (updateGolden : Bool := false) + (options : OptionMap := {}) (seed : Option Nat := none) : IO Context := do + let log ← IO.mkRef (#[] : Array Result) + let usedOptions ← IO.mkRef ({} : Std.HashSet String) + return { verbosity, updateGolden, options, seed, log, usedOptions } + +/-- The settings parsed from the runner's command line. -/ +structure Options where + /-- The reporting verbosity. -/ + verbosity : Verbosity := .silent + /-- Rewrites golden expected files instead of comparing. -/ + updateGolden : Bool := false + /-- The seed for property tests, for reproducing a failure. -/ + seed : Option Nat := none + /-- Writes a JUnit XML report to this path. -/ + junitPath : Option String := none + /-- Writes a JSON report to this path. -/ + jsonPath : Option String := none + /-- Writes a Markdown report to this path. -/ + markdownPath : Option String := none + /-- Project-specific options, as a multi-map so repeated options accumulate. -/ + options : OptionMap := {} + /-- Prints usage information instead of running the tests. -/ + help : Bool := false + +/-- +{given}`name : String, value : String` + +Parses arguments into {lean}`(name, value)` pairs. + +A long option is {lit}`--name`, {lit}`--name=value`, or {lit}`--name value`. The {lit}`--name value` +form takes the next token as the value when that token is an ordinary argument; a token beginning with +{lit}`-` starts the next option instead, so a value beginning with {lit}`-` uses the {lit}`--name=value` +form. Short options bundle: {lit}`-xyz` is equivalent to {lit}`--x --y --z`, and the last may take a +following value. Any other argument is rejected. +-/ +partial def rawOptions : List String → Except String (List (String × String)) + | [] => .ok [] + | arg :: rest => + if let some arg := arg.dropPrefix? "--" then + match arg.copy.splitOn "=" with + | [] => unreachable! -- `splitOn` always returns at least one element + | [name] => + if name.isEmpty then .error s!"unexpected argument: {arg}" + else match rest with + | value :: rest' => + if value.startsWith "-" then (((name, "") :: ·)) <$> rawOptions rest + else (((name, value) :: ·)) <$> rawOptions rest' + | [] => .ok [(name, "")] + | name :: valueParts => + if name.isEmpty then .error s!"unexpected argument: {arg}" + else (((name, "=".intercalate valueParts) :: ·)) <$> rawOptions rest + else if arg.startsWith "-" && arg.length > 1 then + -- Expand bundled short flags: `-xyz` becomes `--x --y --z`. + let expanded := (arg.drop 1).copy.toList.map (fun c => "--" ++ toString c) + rawOptions (expanded ++ rest) + else + .error s!"unexpected argument: {arg}" + +/-- Parses the runner's command-line arguments, peeling off known flags and keeping the rest as +project options. -/ +def parseArgs (args : List String) : Except String Options := do + let raw ← rawOptions args + let mut opts : Options := {} + for (name, value) in raw do + match name with + | "verbose" | "v" => opts := { opts with verbosity := opts.verbosity.increase } + | "update-golden" => opts := { opts with updateGolden := true } + | "seed" => + match value.toNat? with + | some n => opts := { opts with seed := some n } + | none => throw s!"--seed expects a natural number, got '{value}'" + | "junit" => + if value.isEmpty then throw "--junit expects a path" + opts := { opts with junitPath := some value } + | "json" => + if value.isEmpty then throw "--json expects a path" + opts := { opts with jsonPath := some value } + | "markdown" => + if value.isEmpty then throw "--markdown expects a path" + opts := { opts with markdownPath := some value } + | "help" | "h" => opts := { opts with help := true } + | _ => + let prev := opts.options.getD name #[] + opts := { opts with options := opts.options.insert name (prev.push value) } + return opts + +/-- Usage information for the test runner, shown for {lit}`--help`. -/ +def usage : String := include_str "usage.txt" + +/-- The entry point the generated runner calls: parse arguments, run the tests, and report. -/ +def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do + let opts ← + match parseArgs args with + | .ok opts => pure opts + | .error msg => + IO.eprintln s!"error: {msg}" + IO.eprintln usage + return 1 + if opts.help then + IO.println usage + return 0 + let cfg ← mkContext (verbosity := opts.verbosity) (updateGolden := opts.updateGolden) + (options := opts.options) (seed := opts.seed) + let results ← run cfg entries + if let some path := opts.junitPath then IO.FS.writeFile path (junitReport results) + if let some path := opts.jsonPath then IO.FS.writeFile path (jsonReport results) + if let some path := opts.markdownPath then IO.FS.writeFile path (markdownReport results) + let failures ← humanReport opts.verbosity results + -- Warn about options that were supplied but never read by any test (typos, removed flags). + let used ← cfg.usedOptions.get + let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k + unless unused.isEmpty do + IO.eprintln s!"warning: option(s) provided but never read: {", ".intercalate unused}" + -- A process exit status keeps only its low 8 bits, so report a failing run as 1 rather than the + -- count, which a multiple of 256 would otherwise wrap to 0. + return if failures == 0 then 0 else 1 diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean new file mode 100644 index 00000000..e0a227df --- /dev/null +++ b/src/errata/Errata/TestM.lean @@ -0,0 +1,191 @@ +/- +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 Errata.Context +public import Errata.Result +public import Errata.Here + +public section + +set_option linter.missingDocs true +set_option doc.verso true + +namespace Errata + +/-- +The monad in which tests run. + +The reader carries the configuration and the result log; the exception layer carries a structured +failure, which the interpreter distinguishes from an {name}`IO.Error` that escapes. +-/ +abbrev TestM := ReaderT Context (ExceptT TestFailure IO) + +/-- A test: a {name}`TestM` action that succeeds unless it fails an assertion or raises an error. -/ +abbrev Test := TestM Unit + +/-- +Fails at the location recorded in the context. The runner seeds that with the test's own source +range, so a failure with no more specific location still points at the test. This is the primitive +the internal layer uses when no call site is available. +-/ +def failHere (message : String) (detail? : Option String := none) : TestM α := do + throw { message, detail?, location? := some (← read).location } + +/-- +Fails at an explicit source location. The assertion language captures its call site with +{lit}`here%` and reports through this primitive. +-/ +def failAt (loc : Location) (message : String) (detail? : Option String := none) : TestM α := + throw { message, detail?, location? := some loc } + +/-- Fails the current test, or named result, with a message and optional detail. -/ +def fail (message : String) (detail? : Option String := none) + (loc : Location := by exact here%) : TestM α := + failAt loc message detail? + +/-- +{lit}`failure` fails the test at the context's location, and {lit}`<|>` recovers from an assertion +failure by running the alternative. An escaping {name}`IO.Error` still propagates, so {lit}`<|>` does +not mask a broken setup. +-/ +instance : Alternative TestM where + failure := failHere "failure" + orElse x y := tryCatch x fun _ => y () + +/-- +Runs an action with the current failure location set to a call site, which defaults to the caller. +A user-defined assertion helper can wrap its checks in this so their failures report at the helper's +call site rather than inside the helper. +-/ +def withLocation (loc : Location := by exact here%) (act : TestM α) : TestM α := + withReader ({ · with location := loc }) act + +/-- All values supplied for a project option, in order; records that the option was read. -/ +def optionValues (name : String) : TestM (Array String) := do + let ctx ← read + ctx.usedOptions.modify (·.insert name) + return ctx.options.getD name #[] + +/-- The last value supplied for a project option, if any; records that the option was read. -/ +def option? (name : String) : TestM (Option String) := + return (← optionValues name).back? + +/-- Whether a project option is present and not set to an explicit false value; records the read. -/ +def flag (name : String) : TestM Bool := + return match (← optionValues name).back? with + | some v => v != "false" && v != "0" && v != "no" + | none => false + +/-- Builds a result for the current scope with the given status and duration. -/ +def Context.mkResult (ctx : Context) (status : Status) (durationMs : Nat := 0) : Result := { + package := ctx.package, moduleName := ctx.moduleName, test := ctx.test, + resultPath := ctx.resultPath, status, durationMs, description? := ctx.description? +} + +/-- A passing result for the current scope. -/ +def Context.pass (ctx : Context) (durationMs : Nat := 0) : Result := + ctx.mkResult .pass durationMs + +/-- A failed result for the current scope. -/ +def Context.fail (ctx : Context) (failure : TestFailure) (durationMs : Nat := 0) : Result := + ctx.mkResult (.fail failure) durationMs + +/-- A result for the current scope that raised an error. -/ +def Context.error (ctx : Context) (message : String) (durationMs : Nat := 0) : Result := + ctx.mkResult (.error message) durationMs + +/-- A skipped result for the current scope. -/ +def Context.skip (ctx : Context) (reason : String) (durationMs : Nat := 0) : Result := + ctx.mkResult (.skip reason) durationMs + +/-- +The result a captured run contributes beyond any nested results it recorded. + +A raised error or a failed assertion becomes one error or failed result carrying the captured output. +A clean run becomes one passing result with the output when it recorded no nested results; when it did +record some, those results stand for it and it adds nothing of its own. +-/ +def Context.resultOfOutcome (ctx : Context) + (outcome : Except IO.Error (Except TestFailure Unit)) (output : OutputLog) (durationMs : Nat) + (hasNested : Bool) : Option Result := + match outcome with + | .error e => some { ctx.error (toString e) durationMs with output } + | .ok (.error f) => some { ctx.fail f durationMs with output } + | .ok (.ok ()) => if hasNested then none else some { ctx.pass durationMs with output } + +/-- Records a skipped result for the current scope. -/ +def skip (reason : String) : TestM Unit := do + let ctx ← read + ctx.log.modify (·.push (ctx.skip reason)) + +/-- A stream that hands each write to a destination as a fragment tagged by the stream it came from. -/ +private def captureStream (emit : Output → IO Unit) (mk : String → Output) : IO.FS.Stream where + flush := pure () + read _ := pure .empty + write bytes := + match String.fromUTF8? bytes with + | some s => emit (mk s) + | none => throw (.userError "captured test output was not valid UTF-8") + getLine := pure "" + putStr s := emit (mk s) + isTty := pure false + +/-- +Runs a test action with the given context, capturing its outcome as data rather than letting it +propagate. The action's stdout and stderr are recorded, in order and tagged by stream, and returned +alongside the outcome. Each fragment is also handed to the context's output destination as it is +written, so a live runner can stream output while the test runs. +-/ +def runCapturing (ctx : Context) (act : TestM Unit) : + IO (Except IO.Error (Except TestFailure Unit) × OutputLog) := do + let log ← IO.mkRef (#[] : Array Output) + let emit (o : Output) : IO Unit := do log.modify (·.push o); ctx.writeOutput o + let outcome ← IO.withStdout (captureStream emit .stdout) <| + IO.withStderr (captureStream emit .stderr) <| ((act ctx).run).toBaseIO + return (outcome, { log := ← log.get }) + +/-- +Runs an action with stdout and stderr captured into a fresh log, then returns the captured output +in order. The redirection is local to the action, so a test can make assertions about what the +action wrote. +-/ +def captureOutput (act : TestM Unit) : TestM OutputLog := do + let log ← IO.mkRef (#[] : Array Output) + let emit (o : Output) : IO Unit := log.modify (·.push o) + IO.withStdout (captureStream emit .stdout) <| IO.withStderr (captureStream emit .stderr) act + return { log := ← log.get } + +/-- +Runs a named result within the current test. + +Its path extends the current path, and its failure is isolated from sibling results. If the action +records no nested results and completes, it contributes one passing result; if it throws, it +contributes one failed result or one that raised an error. +-/ +def result (name : String) (act : TestM Unit) : TestM Unit := + withReader (fun c => { c with resultPath := c.resultPath.push name }) do + let ctx ← read + let before := (← ctx.log.get).size + let start ← IO.monoMsNow + let (outcome, output) ← runCapturing ctx act + let stop ← IO.monoMsNow + let dur := stop - start + let after := (← ctx.log.get).size + if let some r := ctx.resultOfOutcome outcome output dur (after != before) then + ctx.log.modify (·.push r) + +/-- +Expects the action to fail an assertion. The current scope passes if it does and fails if it +succeeds. An escaping {name}`IO.Error` is not an expected failure: it propagates and is reported as an +error, so broken setup is not mistaken for a passing negative test. +-/ +def expectFail (act : TestM Unit) (loc : Location := by exact here%) : TestM Unit := do + try + act + catch _ => + return + failAt loc "expected the action to fail, but it passed" diff --git a/src/errata/Errata/usage.txt b/src/errata/Errata/usage.txt new file mode 100644 index 00000000..667894a7 --- /dev/null +++ b/src/errata/Errata/usage.txt @@ -0,0 +1,21 @@ +Errata test runner + +Usage: + lake test run every test in the package + lake test -- LIBRARY... run the tests in the given libraries + lake test -- LIBRARY... --test-options OPTION... pass runner options after the marker + +Runner options go after `--test-options`; tokens before it name libraries. A library is a bare +`Library` in this package or a `package/Library` reaching into a dependency. +Runner options: + -v, --verbose Also report passes (truncating each test's results); repeat (-vv) for all, + -vvv to also show every test's docstring, not only those that fail. + --update-golden Rewrite golden expected files instead of comparing. + --seed N Seed property tests with N, to reproduce a failure. + --junit PATH Write a JUnit XML report to PATH. + --json PATH Write a JSON report to PATH. + --markdown PATH Write a Markdown report (for a CI job summary) to PATH. + -h, --help Show this help and exit. + +Any other `--name value` option is passed through to the tests. +Write a value that begins with `-` as `--name=value`. From 2ba4657fd128a7c0b86317688fb2169ec1d1bf01 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 14 Aug 2026 10:52:27 +0200 Subject: [PATCH 02/32] Improve release note and add PR number to it --- doc/UsersGuide/Releases/Entries/TestFramework.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/doc/UsersGuide/Releases/Entries/TestFramework.lean b/doc/UsersGuide/Releases/Entries/TestFramework.lean index 1f0e1794..af731496 100644 --- a/doc/UsersGuide/Releases/Entries/TestFramework.lean +++ b/doc/UsersGuide/Releases/Entries/TestFramework.lean @@ -13,11 +13,16 @@ release_note version := ⟨4, 34, 0⟩ breaking := false tag := "feat-test-framework" - prs := [] + prs := [956] #doc (Manual) "Test Framework" => -Added Errata, a test framework with test discovery, uniform failure reporting, and CI-friendly report formats. +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. From da67637a6e0fd4ce18bc587bf5468b4a48809efe Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 14 Aug 2026 22:31:10 +0200 Subject: [PATCH 03/32] chore: verbosity and Cli Migrate command-line parsing to Cli and improve verbosity settings RE success/failure --- lake-manifest.json | 12 +- lakefile.lean | 14 +-- src/errata-tests/ErrataTests.lean | 50 +++++++- src/errata/Errata/Report.lean | 41 +++---- src/errata/Errata/Runner.lean | 196 ++++++++++++++++-------------- src/errata/Errata/usage.txt | 17 +-- 6 files changed, 195 insertions(+), 135 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b09747fa..729d451b 100644 --- a/lake-manifest.json +++ b/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": "", diff --git a/lakefile.lean b/lakefile.lean index cf9bd1e5..9d77ec9b 100644 --- a/lakefile.lean +++ b/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 := true @@ -148,15 +149,9 @@ lean_exe «verso-tests» where -- discovery runner, and the runner script. namespace Errata -@[default_target] -input_file errataUsageFile where - text := true - path := "src/errata/Errata/usage.txt" - lean_lib Errata where srcDir := "src/errata" roots := #[`Errata] - needs := #[errataUsageFile] -- Tests that exercise Errata using Errata itself. lean_lib ErrataTests where @@ -239,7 +234,7 @@ private def splitArgs (args : List String) : Except String (List String × List e.g. `lake test -- --test-options {opt}`." | none => .ok (names, rest) -/-- Usage information for `lake test`, shared with `Errata.usage` through one text file. -/ +/-- Usage information for `lake test`. -/ private def usage : String := include_str "src/errata/Errata/usage.txt" /-- Every `.lean` file below a directory, recursively. -/ @@ -290,8 +285,9 @@ private def warnUncoveredTestModules (ws : Lake.Workspace) : IO Unit := do script run (args) do let ws ← getWorkspace - -- Answer `--help` before discovering or building anything. - if args.any (fun a => a == "--help" || a == "-h") then + -- 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) ← diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 349a8c7b..88a6f5d3 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -106,6 +106,43 @@ def verbosityLevels : Test := do assertEq Verbosity.superVerbose Verbosity.verbose.increase assertEq Verbosity.superVerbose Verbosity.superVerbose.increase +/-- The runner's command line: the `-v` forms select the verbosity, declared flags parse, and +options for the tests go after `--`. -/ +@[test] +def runnerArgParsing : Test := do + result "default verbosity" do + assertEq (some Verbosity.silent) ((parseOptions []).toOption.map (·.verbosity)) + result "-v" do + assertEq (some Verbosity.quiet) ((parseOptions ["-v"]).toOption.map (·.verbosity)) + result "--verbose" do + assertEq (some Verbosity.quiet) ((parseOptions ["--verbose"]).toOption.map (·.verbosity)) + result "-vv" do + assertEq (some Verbosity.verbose) ((parseOptions ["-vv"]).toOption.map (·.verbosity)) + result "-vvv" do + assertEq (some Verbosity.superVerbose) ((parseOptions ["-vvv"]).toOption.map (·.verbosity)) + result "update-golden" do + assertEq (some true) ((parseOptions ["--update-golden"]).toOption.map (·.updateGolden)) + result "seed" do + assertEq (some (some 42)) ((parseOptions ["--seed", "42"]).toOption.map (·.seed)) + result "non-numeric seed rejected" do + assert ((parseOptions ["--seed", "x"]) matches .error _) + result "junit path" do + assertEq (some (some "r.xml")) ((parseOptions ["--junit", "r.xml"]).toOption.map (·.junitPath)) + result "missing junit path rejected" do + assert ((parseOptions ["--junit"]) matches .error _) + result "test options after --" do + let opts := (parseOptions ["--", "--golden", "on", "--flag=v=1", "--golden", "two"]).toOption + assertEq (some #["on", "two"]) (opts.map (·.options.getD "golden" #[])) + assertEq (some #["v=1"]) (opts.map (·.options.getD "flag" #[])) + result "valueless test option" do + assertEq (some #[""]) ((parseOptions ["--", "--fast"]).toOption.map (·.options.getD "fast" #[])) + result "unknown flag rejected" do + assert ((parseOptions ["--golden", "on"]) matches .error _) + result "misplaced library name diagnosed" do + match parseOptions ["--verbose", "ErrataTests"] with + | .error msg => assertContains "ErrataTests" msg + | .ok _ => assert false "expected an error" + /-- At silent verbosity the report hides passes but shows failures and the summary line. -/ @[test] def reportSilent : Test := do @@ -130,11 +167,22 @@ def reportTruncates : Test := do ({ package := "p", moduleName := "M", test := "many", resultPath := #[s!"case {i}"], status := .pass } : Result) let quiet ← captureOutput do discard <| humanReport .quiet many assertEq 51 (quiet.stdout.splitOn "ok ").length - assertContains "(... and 10 more passed, 0 more failed)" quiet.stdout + assertContains "(... and 10 more passed)" quiet.stdout let verbose ← captureOutput do discard <| humanReport .verbose many assertEq 61 (verbose.stdout.splitOn "ok ").length assertEq 1 (verbose.stdout.splitOn "(... and").length +/-- Truncation never suppresses a failure or error: past the cap they print in full and only the +passes around them are summarized. -/ +@[test] +def reportTruncationShowsFailures : Test := do + let many := (Array.range 60).map fun i => + let status : Status := if i == 55 then .fail { message := "boom" } else .pass + ({ package := "p", moduleName := "M", test := "many", resultPath := #[s!"case {i}"], status } : Result) + let quiet ← captureOutput do discard <| humanReport .quiet many + assertContains "FAIL p/M many.case 55: boom" quiet.stdout + assertContains "(... and 9 more passed)" quiet.stdout + /-- `humanReport` returns the number of failures and errors. -/ @[test] def reportFailureCount : Test := do diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean index e220b50f..63f003e4 100644 --- a/src/errata/Errata/Report.lean +++ b/src/errata/Errata/Report.lean @@ -50,36 +50,32 @@ private def printResult (verbosity : Verbosity) (r : Result) : IO Unit := do printDoc unless r.output.isEmpty do IO.println (indentLines s!"output:\n{r.output.all}") -/-- A running tally of results suppressed by truncation. -/ +/-- A running tally of results suppressed by truncation. Only passes and skips are ever suppressed; +failures and errors always print. -/ private structure Suppressed where passed : Nat := 0 - failed : Nat := 0 - errors : Nat := 0 skipped : Nat := 0 /-- Counts one more suppressed result. -/ private def Suppressed.add (s : Suppressed) : Status → Suppressed - | .pass => { s with passed := s.passed + 1 } - | .fail _ => { s with failed := s.failed + 1 } - | .error _ => { s with errors := s.errors + 1 } | .skip _ => { s with skipped := s.skipped + 1 } + | _ => { s with passed := s.passed + 1 } /-- The number of suppressed results. -/ private def Suppressed.total (s : Suppressed) : Nat := - s.passed + s.failed + s.errors + s.skipped + s.passed + s.skipped /-- Prints the truncation summary for a test whose results were capped, if any were suppressed. -/ private def printSuppressed (s : Suppressed) : IO Unit := do if s.total > 0 then - let parts := #[s!"{s.passed} more passed", s!"{s.failed} more failed"] - ++ (if s.errors > 0 then #[s!"{s.errors} more errors"] else #[]) + let parts := (if s.passed > 0 then #[s!"{s.passed} more passed"] else #[]) ++ (if s.skipped > 0 then #[s!"{s.skipped} more skipped"] else #[]) IO.println s!" (... and {", ".intercalate parts.toList})" /-- -Prints a human-readable report and returns the number of failures. Verbosity 0 shows only failures -and errors; 1 also shows passes and skips but truncates each test's results after a cap, summarizing -the rest; 2 shows everything. +Prints a human-readable report and returns the number of failures. Failures and errors are printed +at every verbosity. Verbosity 0 shows nothing else; 1 also shows passes and skips but truncates each +test's passes and skips after a cap, summarizing the rest; 2 shows everything. -/ def humanReport (verbosity : Verbosity) (results : Array Result) : IO Nat := do let cap := 50 @@ -103,16 +99,17 @@ def humanReport (verbosity : Verbosity) (results : Array Result) : IO Nat := do curKey := some key shown := 0 more := {} - let displayable := - match r.status with - | .pass | .skip _ => verbosity.showsPasses - | .fail _ | .error _ => true - if displayable then - if verbosity.truncates && shown ≥ cap then - more := more.add r.status - else - printResult verbosity r - shown := shown + 1 + match r.status with + | .fail _ | .error _ => + printResult verbosity r + shown := shown + 1 + | .pass | .skip _ => + if verbosity.showsPasses then + if verbosity.truncates && shown ≥ cap then + more := more.add r.status + else + printResult verbosity r + shown := shown + 1 printSuppressed more IO.println s!"{passed} passed, {failed} failed, {errors} errors, {skipped} skipped" return failed + errors diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index 7f4464c3..fa8cb6f4 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -8,6 +8,7 @@ module public import Errata.TestM public import Errata.IsTest public import Errata.Report +public import Cli public section @@ -87,98 +88,115 @@ structure Options where markdownPath : Option String := none /-- Project-specific options, as a multi-map so repeated options accumulate. -/ options : OptionMap := {} - /-- Prints usage information instead of running the tests. -/ - help : Bool := false -/-- -{given}`name : String, value : String` - -Parses arguments into {lean}`(name, value)` pairs. +open Cli in +/-- The runner's command-line interface. The handler receives the parsed arguments. -/ +def runnerCmd (handler : Cli.Parsed → IO UInt32) : Cli.Cmd := + `[Cli| + "errata-runner" VIA handler; + "Runs the discovered Errata tests." + + FLAGS: + v, verbose; "Also report passes and skips, truncating each test's results." + vv, "verbose-all"; "Report every result, without truncation." + vvv, "verbose-docs"; "Report every result and every test's docstring." + "update-golden"; "Rewrite golden expected files instead of comparing." + seed : Nat; "Seed property tests, to reproduce a failure." + junit : String; "Write a JUnit XML report to the given path." + json : String; "Write a JSON report to the given path." + markdown : String; "Write a Markdown report (for a CI job summary) to the given path." + + ARGS: + ...testOption : String; "Options for the tests themselves; see below." + + EXTENSIONS: + longDescription "Options for the tests themselves go after a `--` separator, as \ + `--name value` or `--name=value`. Write a value that begins with `-` as `--name=value`." + ] -A long option is {lit}`--name`, {lit}`--name=value`, or {lit}`--name value`. The {lit}`--name value` -form takes the next token as the value when that token is an ordinary argument; a token beginning with -{lit}`-` starts the next option instead, so a value beginning with {lit}`-` uses the {lit}`--name=value` -form. Short options bundle: {lit}`-xyz` is equivalent to {lit}`--x --y --z`, and the last may take a -following value. Any other argument is rejected. +/-- +Parses the options passed through to the tests: {lit}`--name value` and {lit}`--name=value` pairs, +collected into a multi-map so repeated options accumulate. The {lit}`--name value` form takes the +next token as the value when that token does not begin with {lit}`-`; a value that does uses the +{lit}`--name=value` form. Any other token is rejected. -/ -partial def rawOptions : List String → Except String (List (String × String)) - | [] => .ok [] - | arg :: rest => - if let some arg := arg.dropPrefix? "--" then - match arg.copy.splitOn "=" with - | [] => unreachable! -- `splitOn` always returns at least one element - | [name] => - if name.isEmpty then .error s!"unexpected argument: {arg}" - else match rest with - | value :: rest' => - if value.startsWith "-" then (((name, "") :: ·)) <$> rawOptions rest - else (((name, value) :: ·)) <$> rawOptions rest' - | [] => .ok [(name, "")] - | name :: valueParts => - if name.isEmpty then .error s!"unexpected argument: {arg}" - else (((name, "=".intercalate valueParts) :: ·)) <$> rawOptions rest - else if arg.startsWith "-" && arg.length > 1 then - -- Expand bundled short flags: `-xyz` becomes `--x --y --z`. - let expanded := (arg.drop 1).copy.toList.map (fun c => "--" ++ toString c) - rawOptions (expanded ++ rest) - else - .error s!"unexpected argument: {arg}" - -/-- Parses the runner's command-line arguments, peeling off known flags and keeping the rest as -project options. -/ -def parseArgs (args : List String) : Except String Options := do - let raw ← rawOptions args - let mut opts : Options := {} - for (name, value) in raw do - match name with - | "verbose" | "v" => opts := { opts with verbosity := opts.verbosity.increase } - | "update-golden" => opts := { opts with updateGolden := true } - | "seed" => - match value.toNat? with - | some n => opts := { opts with seed := some n } - | none => throw s!"--seed expects a natural number, got '{value}'" - | "junit" => - if value.isEmpty then throw "--junit expects a path" - opts := { opts with junitPath := some value } - | "json" => - if value.isEmpty then throw "--json expects a path" - opts := { opts with jsonPath := some value } - | "markdown" => - if value.isEmpty then throw "--markdown expects a path" - opts := { opts with markdownPath := some value } - | "help" | "h" => opts := { opts with help := true } - | _ => - let prev := opts.options.getD name #[] - opts := { opts with options := opts.options.insert name (prev.push value) } - return opts - -/-- Usage information for the test runner, shown for {lit}`--help`. -/ -def usage : String := include_str "usage.txt" +partial def projectOptions (tokens : List String) : Except String OptionMap := + go {} tokens +where + push (acc : OptionMap) (name value : String) : OptionMap := + acc.insert name ((acc.getD name #[]).push value) + go (acc : OptionMap) : List String → Except String OptionMap + | [] => .ok acc + | tok :: rest => + match tok.dropPrefix? "--" with + | none => + .error s!"unexpected argument '{tok}': test options are `--name value` or `--name=value`" + | some name => + match name.copy.splitOn "=" with + | [] => unreachable! -- `splitOn` always returns at least one element + | [n] => + if n.isEmpty then .error s!"unexpected argument: {tok}" + else match rest with + | value :: rest' => + if value.startsWith "-" then go (push acc n "") rest + else go (push acc n value) rest' + | [] => .ok (push acc n "") + | n :: valueParts => + if n.isEmpty then .error s!"unexpected argument: {tok}" + else go (push acc n ("=".intercalate valueParts)) rest + +/-- The value of a path-valued flag, when it is present; a present but empty path is an error. -/ +private def pathFlag (p : Cli.Parsed) (name : String) : Except String (Option String) := + match p.flag? name with + | none => .ok none + | some f => if f.value.isEmpty then .error s!"--{name} expects a path" else .ok (some f.value) + +/-- Interprets a parsed command line as runner settings. -/ +def optionsOfParsed (p : Cli.Parsed) : Except String Options := do + let verbosity : Verbosity := + if p.hasFlag "verbose-docs" then .superVerbose + else if p.hasFlag "verbose-all" then .verbose + else if p.hasFlag "verbose" then .quiet + else .silent + return { + verbosity, + updateGolden := p.hasFlag "update-golden", + seed := p.flag? "seed" |>.map (·.as! Nat), + junitPath := ← pathFlag p "junit", + jsonPath := ← pathFlag p "json", + markdownPath := ← pathFlag p "markdown", + options := ← projectOptions (p.variableArgsAs! String).toList + } + +/-- Parses the runner's command line into settings: the declared flags, then any options for the +tests themselves after a {lit}`--` separator. -/ +def parseOptions (args : List String) : Except String Options := + match (runnerCmd fun _ => pure 0).parse args with + | .error e => .error e.kind.msg + | .ok (_, parsed) => optionsOfParsed parsed /-- The entry point the generated runner calls: parse arguments, run the tests, and report. -/ def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do - let opts ← - match parseArgs args with - | .ok opts => pure opts - | .error msg => - IO.eprintln s!"error: {msg}" - IO.eprintln usage - return 1 - if opts.help then - IO.println usage - return 0 - let cfg ← mkContext (verbosity := opts.verbosity) (updateGolden := opts.updateGolden) - (options := opts.options) (seed := opts.seed) - let results ← run cfg entries - if let some path := opts.junitPath then IO.FS.writeFile path (junitReport results) - if let some path := opts.jsonPath then IO.FS.writeFile path (jsonReport results) - if let some path := opts.markdownPath then IO.FS.writeFile path (markdownReport results) - let failures ← humanReport opts.verbosity results - -- Warn about options that were supplied but never read by any test (typos, removed flags). - let used ← cfg.usedOptions.get - let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k - unless unused.isEmpty do - IO.eprintln s!"warning: option(s) provided but never read: {", ".intercalate unused}" - -- A process exit status keeps only its low 8 bits, so report a failing run as 1 rather than the - -- count, which a multiple of 256 would otherwise wrap to 0. - return if failures == 0 then 0 else 1 + let cmd := runnerCmd fun parsed => do + let opts ← + match optionsOfParsed parsed with + | .ok opts => pure opts + | .error msg => + IO.eprintln s!"error: {msg}" + return 1 + let cfg ← mkContext (verbosity := opts.verbosity) (updateGolden := opts.updateGolden) + (options := opts.options) (seed := opts.seed) + let results ← run cfg entries + if let some path := opts.junitPath then IO.FS.writeFile path (junitReport results) + if let some path := opts.jsonPath then IO.FS.writeFile path (jsonReport results) + if let some path := opts.markdownPath then IO.FS.writeFile path (markdownReport results) + let failures ← humanReport opts.verbosity results + -- Warn about options that were supplied but never read by any test (typos, removed flags). + let used ← cfg.usedOptions.get + let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k + unless unused.isEmpty do + IO.eprintln s!"warning: option(s) provided but never read: {", ".intercalate unused}" + -- A process exit status keeps only its low 8 bits, so report a failing run as 1 rather than the + -- count, which a multiple of 256 would otherwise wrap to 0. + return if failures == 0 then 0 else 1 + cmd.validate args diff --git a/src/errata/Errata/usage.txt b/src/errata/Errata/usage.txt index 667894a7..bfaa9344 100644 --- a/src/errata/Errata/usage.txt +++ b/src/errata/Errata/usage.txt @@ -5,17 +5,8 @@ Usage: lake test -- LIBRARY... run the tests in the given libraries lake test -- LIBRARY... --test-options OPTION... pass runner options after the marker -Runner options go after `--test-options`; tokens before it name libraries. A library is a bare -`Library` in this package or a `package/Library` reaching into a dependency. -Runner options: - -v, --verbose Also report passes (truncating each test's results); repeat (-vv) for all, - -vvv to also show every test's docstring, not only those that fail. - --update-golden Rewrite golden expected files instead of comparing. - --seed N Seed property tests with N, to reproduce a failure. - --junit PATH Write a JUnit XML report to PATH. - --json PATH Write a JSON report to PATH. - --markdown PATH Write a Markdown report (for a CI job summary) to PATH. - -h, --help Show this help and exit. +Tokens before `--test-options` name libraries. A library is a bare `Library` in this package or a +`package/Library` reaching into a dependency. Everything after the marker goes to the test runner. -Any other `--name value` option is passed through to the tests. -Write a value that begins with `-` as `--name=value`. +The runner documents its own options, including how to pass options to the tests themselves: + lake test -- --test-options --help From bea35d86a748b698dedb0a759c5be5ba3f52d459 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 14 Aug 2026 22:42:04 +0200 Subject: [PATCH 04/32] fix: run Errata's tests from the Verso test suite --- lakefile.lean | 4 +++- src/errata/Errata/usage.txt | 8 ++++---- src/tests/TestMain.lean | 12 +++++++++++- src/tests/Tests.lean | 1 + src/tests/Tests/ErrataSuite.lean | 12 ++++++++++++ 5 files changed, 31 insertions(+), 6 deletions(-) create mode 100644 src/tests/Tests/ErrataSuite.lean diff --git a/lakefile.lean b/lakefile.lean index 9d77ec9b..0f6b89b7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -149,11 +149,13 @@ lean_exe «verso-tests» where -- 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] @@ -231,7 +233,7 @@ private def splitArgs (args : List String) : Except String (List String × List | 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 test -- --test-options {opt}`." + e.g. `lake run Errata.run --test-options {opt}`." | none => .ok (names, rest) /-- Usage information for `lake test`. -/ diff --git a/src/errata/Errata/usage.txt b/src/errata/Errata/usage.txt index bfaa9344..a9ffa278 100644 --- a/src/errata/Errata/usage.txt +++ b/src/errata/Errata/usage.txt @@ -1,12 +1,12 @@ Errata test runner Usage: - lake test run every test in the package - lake test -- LIBRARY... run the tests in the given libraries - lake test -- LIBRARY... --test-options OPTION... pass runner options after the marker + lake run Errata.run run every test in the package + lake run Errata.run LIBRARY... run the tests in the given libraries + lake run Errata.run LIBRARY... --test-options OPTION... pass runner options after the marker Tokens before `--test-options` name libraries. A library is a bare `Library` in this package or a `package/Library` reaching into a dependency. Everything after the marker goes to the test runner. The runner documents its own options, including how to pass options to the tests themselves: - lake test -- --test-options --help + lake run Errata.run --test-options --help diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 28314873..037cc427 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -357,6 +357,15 @@ def testBuildLog (_ : Config) : IO Unit := do throw <| IO.userError "redirected logging should still accumulate into the logger's buffers" IO.println " All build-log tests passed." +/-- Runs Errata's own tests, reporting them the way the Errata runner does. -/ +def testErrata (config : Config) : IO Unit := do + let verbosity := if config.verbose then Errata.Verbosity.quiet else .silent + let cfg ← Errata.mkContext (verbosity := verbosity) + let results ← Errata.run cfg errataTests + let failures ← Errata.humanReport verbosity results + unless failures == 0 do + throw <| IO.userError s!"{failures} Errata test(s) failed" + open Verso.Integration in def tests := [ testBuildLog, @@ -380,7 +389,8 @@ def tests := [ testLiterateConfig, testLiterateHtml, testLiterateHtmlMultiRoot, - testSetupLiterate + testSetupLiterate, + testErrata ] def getConfig (config : Config) : List String → IO Config diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean index 5bcdd422..52967abf 100644 --- a/src/tests/Tests.lean +++ b/src/tests/Tests.lean @@ -14,6 +14,7 @@ import Tests.DocVisibility import Tests.DocstringMissing import Tests.DocstringMissingLegacy import Tests.HighlightedToTeX +import Tests.ErrataSuite import Tests.ExpanderSignatures import Tests.ExpanderSignaturesLegacy import Tests.Html diff --git a/src/tests/Tests/ErrataSuite.lean b/src/tests/Tests/ErrataSuite.lean new file mode 100644 index 00000000..ae0a5a21 --- /dev/null +++ b/src/tests/Tests/ErrataSuite.lean @@ -0,0 +1,12 @@ +/- +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 Errata +import all ErrataTests + +/-- Errata's own tests, gathered so that a driver outside the module system can run them. -/ +public def errataTests : Array Errata.TestEntry := getAllTests% "verso" ErrataTests From 5a2002def2e80dea578d2d271f1c8e2ba8416b83 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 17 Aug 2026 15:10:16 +0200 Subject: [PATCH 05/32] fix: better warnings for tests that would silently not run --- .github/workflows/ci.yml | 2 +- lakefile.lean | 102 ++++++++++++------------------ src/errata-tests/ErrataTests.lean | 6 ++ src/errata/Errata/Discovery.lean | 4 +- 4 files changed, 49 insertions(+), 65 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f4a8b601..9be07d1f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -74,7 +74,7 @@ jobs: 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)" if [ -n "$(printf '%s' "$out" | tr -d '[:space:]')" ]; then echo "Found orphaned modules:" echo "$out" diff --git a/lakefile.lean b/lakefile.lean index 0f6b89b7..b218a94a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -179,18 +179,6 @@ lean_exe «errata-runner» where supportInterpreter := true needs := #[errataSelection] -/-- -Whether a source file introduces Errata tests, by an `@[test]` attribute (applied inline or with a -separate `attribute [test] …`), a `#test_msgs` command, or a `#test_guard` command. This drives the -glob-coverage check, which reads source files before anything is built; test discovery itself reads -the compiled modules. --/ -private def sourceHasTests (lines : List String) : Bool := - lines.any fun line => - let t := line.trimAsciiStart - t.startsWith "@[test]" || t.startsWith "attribute [test" || - t.startsWith "#test_msgs" || t.startsWith "#test_guard" - /-- 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 @@ -200,6 +188,24 @@ private def moduleInfo (oleanFile : System.FilePath) : IO (Bool × Bool) := do 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 := @@ -239,52 +245,6 @@ private def splitArgs (args : List String) : Except String (List String × List /-- Usage information for `lake test`. -/ private def usage : String := include_str "src/errata/Errata/usage.txt" -/-- Every `.lean` file below a directory, recursively. -/ -private partial def leanFiles (dir : System.FilePath) : IO (Array System.FilePath) := do - unless ← dir.pathExists do return #[] - let mut out := #[] - for entry in ← dir.readDir do - if ← entry.path.isDir then - out := out ++ (← leanFiles entry.path) - else if entry.path.extension == some "lean" then - out := out.push entry.path - return out - -/-- The module name of a `.lean` file relative to a source directory, if it lies within it. -/ -private def moduleOfPath (srcDir path : System.FilePath) : Option Lean.Name := do - guard (path.extension == some "lean") - let stem ← path.fileStem - let parent ← path.parent - guard (srcDir.components.isPrefixOf parent.components) - let comps := parent.components.drop srcDir.components.length ++ [stem] - some (".".intercalate comps).toName - -/-- -Warns about modules that look like they define tests but whose library's globs do not cover them, so -the tests would be silently undiscovered. A module within a library's root that is not matched by the -library's globs, in a file that introduces tests, is the signal. The check reads source text and is a -heuristic, so it warns rather than failing the run. --/ -private def warnUncoveredTestModules (ws : Lake.Workspace) : IO Unit := do - let mut missed : Array Lean.Name := #[] - for lib in ws.root.leanLibs do - if lib.name == `ErrataGenerated then continue - let srcDir := lib.srcDir - for path in ← leanFiles srcDir do - let some mod := moduleOfPath srcDir path | continue - let withinRoot := lib.roots.any (·.isPrefixOf mod) - let globbed := lib.config.globs.any (·.matches mod) - if withinRoot && !globbed && !missed.contains mod then - let lines := (← IO.FS.readFile path).splitOn "\n" - if sourceHasTests lines then - missed := missed.push mod - unless missed.isEmpty do - IO.eprintln "warning: these modules look like they define tests but their library's globs do \ - not cover them, so the tests are not discovered. Widen the library's `globs` \ - (e.g. `globs := #[Glob.andSubmodules `Root]`):" - for mod in missed do - IO.eprintln s!" {mod}" - script run (args) do let ws ← getWorkspace -- Answer the driver's own `--help` before discovering or building anything. A `--help` after the @@ -328,20 +288,19 @@ script run (args) do IO.eprintln s!"error: no library matches '{spec}'" return 1 pure chosen - -- Modules that look like they define tests but escape their library's globs are likely a - -- configuration slip; warn, but run the discovered suite anyway. - warnUncoveredTestModules ws -- Build every module in the selected libraries; their compiled `.olean` headers are authoritative -- on which modules carry tests, so no test is dropped by a source-level heuristic. - let modInfos ← runBuild do + 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 + 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 := #[] @@ -351,6 +310,23 @@ script run (args) do 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. Only libraries that already carry tests are worth + -- checking. 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 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 + IO.eprintln "warning: 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}" -- 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 / ".lake" / "errata-runner" diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 88a6f5d3..f7de846f 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -59,6 +59,12 @@ set_option doc.verso true in #test_msgs in #eval 3 + 4 +/-- +error: Module `NoSuchModule` is not imported, so its tests cannot be reached. Import it, using `import all NoSuchModule` if it belongs to the module system. +-/ +#test_msgs in +example : Array TestEntry := getAllTests% "verso" NoSuchModule + /-- A property test. -/ @[test] def addComm : Test := diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean index e39527ad..cd72f9a6 100644 --- a/src/errata/Errata/Discovery.lean +++ b/src/errata/Errata/Discovery.lean @@ -106,7 +106,9 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do let mut entries : Array Term := #[] for modStx in mods do let moduleName := modStx.getId - let some idx := env.getModuleIdx? moduleName | continue + let some idx := env.getModuleIdx? moduleName + | throwErrorAt modStx "Module `{moduleName}` is not imported, so its tests cannot be \ + reached. Import it, using `import all {moduleName}` if it belongs to the module system." let moduleStr := moduleName.toString for test in testExt.getModuleEntries env idx do let userName := privateToUserName test.name From ee0d6ee1cae6a45eeab7b07412d8308c40f93b0f Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 17 Aug 2026 15:20:39 +0200 Subject: [PATCH 06/32] refactor: use upstream function instead of inlining --- src/errata/Errata/CompileTime.lean | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean index 06c349f7..668cd92f 100644 --- a/src/errata/Errata/CompileTime.lean +++ b/src/errata/Errata/CompileTime.lean @@ -8,6 +8,7 @@ module public import Errata.Result public meta import Errata.CompileTime.Helpers public import Lean.Elab.Command +public import Lean.Elab.GuardMsgs public import Lean.Data.Options open Lean Elab Command Errata.CompileTime @@ -40,16 +41,13 @@ syntax (name := testMsgsCmd) (plainDocComment)? "#test_msgs" "in" command : comm meta def elabTestMsgs : Command.CommandElab | `($[$dc?:docComment]? #test_msgs%$tk in $cmd) => do let expected := ((← dc?.mapM (getDocStringText ·)).getD "").trimAscii.copy - -- Elaborate the command, capturing its messages instead of letting them surface. Both the - -- synchronous log and the asynchronous snapshot tasks are collected, so messages from linters - -- (which run after elaboration) are included, as `#guard_msgs` does. + -- Elaborate the command, capturing its messages instead of letting them surface. Collection + -- covers the asynchronous snapshot tasks as well as the synchronous log, so messages from + -- linters, which run after elaboration, are included. Elaborating the command replaces the + -- message log, so the surrounding one is put back afterwards. let saved := (← get).messages - modify ({ · with messages := {} }) - withReader ({ · with snap? := none }) do - elabCommandTopLevel cmd #[] - let produced := (← get).messages ++ - (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) .empty) .empty - modify ({ · with messages := saved, snapshotTasks := #[] }) + let produced ← Lean.Elab.Tactic.GuardMsgs.runAndCollectMessages cmd + modify ({ · with messages := saved }) let visible := produced.toList.filter (!·.isSilent) let strings ← (visible.mapM formatMessage : IO (List String)) -- Multiple messages are separated by `---`, matching the block `#guard_msgs` compares against. From 970e7ae44d0d7792e093f63b945c5ad79d6f6d9d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 19 Aug 2026 20:47:41 +0200 Subject: [PATCH 07/32] refactor: use assertTrue to avoid do conflict --- src/errata-tests/ErrataTests.lean | 19 +++++++++++++++---- src/errata/Errata/Assertions.lean | 15 ++------------- src/errata/Errata/Discovery.lean | 4 +++- src/errata/Errata/Result.lean | 8 ++++---- 4 files changed, 24 insertions(+), 22 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index f7de846f..43db56ea 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -94,6 +94,17 @@ def goldenRoundTrip : Test := assertFileExists goldenPath goldenFile goldenPath "contents\n" +-- `here%` reports its own position, so the expected column below is the indentation of the line it +-- sits on, and the expected span is the five characters of the token itself. +def indentedHere : Location := + here% + +/-- Source positions follow Lean's convention: lines count from one and columns from zero. -/ +@[test] +def positionConvention : Test := do + assertEq 2 indentedHere.startPos.column + assertEq 5 (indentedHere.endPos.column - indentedHere.startPos.column) + /-- The `Verbosity` predicates and accumulation behave as the report relies on. -/ @[test] def verbosityLevels : Test := do @@ -131,11 +142,11 @@ def runnerArgParsing : Test := do result "seed" do assertEq (some (some 42)) ((parseOptions ["--seed", "42"]).toOption.map (·.seed)) result "non-numeric seed rejected" do - assert ((parseOptions ["--seed", "x"]) matches .error _) + assertTrue ((parseOptions ["--seed", "x"]) matches .error _) result "junit path" do assertEq (some (some "r.xml")) ((parseOptions ["--junit", "r.xml"]).toOption.map (·.junitPath)) result "missing junit path rejected" do - assert ((parseOptions ["--junit"]) matches .error _) + assertTrue ((parseOptions ["--junit"]) matches .error _) result "test options after --" do let opts := (parseOptions ["--", "--golden", "on", "--flag=v=1", "--golden", "two"]).toOption assertEq (some #["on", "two"]) (opts.map (·.options.getD "golden" #[])) @@ -143,11 +154,11 @@ def runnerArgParsing : Test := do result "valueless test option" do assertEq (some #[""]) ((parseOptions ["--", "--fast"]).toOption.map (·.options.getD "fast" #[])) result "unknown flag rejected" do - assert ((parseOptions ["--golden", "on"]) matches .error _) + assertTrue ((parseOptions ["--golden", "on"]) matches .error _) result "misplaced library name diagnosed" do match parseOptions ["--verbose", "ErrataTests"] with | .error msg => assertContains "ErrataTests" msg - | .ok _ => assert false "expected an error" + | .ok _ => assertTrue false "expected an error" /-- At silent verbosity the report hides passes but shows failures and the summary line. -/ @[test] diff --git a/src/errata/Errata/Assertions.lean b/src/errata/Errata/Assertions.lean index ce2d59eb..ac51b72d 100644 --- a/src/errata/Errata/Assertions.lean +++ b/src/errata/Errata/Assertions.lean @@ -15,22 +15,11 @@ set_option doc.verso true namespace Errata -/-- -Asserts that a condition holds. In a {lit}`do` block, {lit}`assert cond` and -{lit}`assert cond msg` invoke this assertion. --/ -def assert (cond : Bool) (message : String := "assertion failed") +/-- Asserts that a condition holds. -/ +def assertTrue (cond : Bool) (message : String := "assertion failed") (loc : Location := by exact here%) : TestM Unit := unless cond do failAt loc message --- The `assert` statement of `do` blocks parses its whole argument list as one term, so an --- application there is the condition followed by the message. -macro_rules - | `(doElem| assert $p:term) => - match p with - | `($cond $message) => `(doElem| Errata.assert $cond $message) - | cond => `(doElem| Errata.assert $cond) - /-- Asserts that the actual value equals the expected value, reporting both when they differ. -/ def assertEq {α} [BEq α] [Repr α] (expected actual : α) (loc : Location := by exact here%) : TestM Unit := diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean index cd72f9a6..d916acad 100644 --- a/src/errata/Errata/Discovery.lean +++ b/src/errata/Errata/Discovery.lean @@ -111,6 +111,8 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do reached. Import it, using `import all {moduleName}` if it belongs to the module system." let moduleStr := moduleName.toString for test in testExt.getModuleEntries env idx do + -- The internal name is used here, because the user-facing name can be ambiguous for private + -- tests let userName := privateToUserName test.name let testName := testNameBelow moduleName userName let range ← findDeclarationRanges? test.name @@ -125,5 +127,5 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do (Errata.Location.mk $(quote test.file) (Errata.Position.mk $(quote pos.line) $(quote pos.column)) (Errata.Position.mk $(quote endPos.line) $(quote endPos.column))) - (@$(mkIdent userName)) (docstring? := $docStx)) + (@$(mkCIdent test.name)) (docstring? := $docStx)) elabTerm (← `(#[$entries,*])) expectedType? diff --git a/src/errata/Errata/Result.lean b/src/errata/Errata/Result.lean index 963bc37e..d3b39bc7 100644 --- a/src/errata/Errata/Result.lean +++ b/src/errata/Errata/Result.lean @@ -45,11 +45,11 @@ def Verbosity.increase : Verbosity → Verbosity | .quiet => .verbose | .verbose | .superVerbose => .superVerbose -/-- A line and column within a source file, counting from one. -/ +/-- A line and column within a source file, following Lean's own source positions. -/ structure Position where /-- The line, counting from one. -/ line : Nat - /-- The column, counting from one. -/ + /-- The column, counting from zero. -/ column : Nat deriving Repr, Inhabited, BEq, DecidableEq @@ -166,8 +166,8 @@ def Result.testName (result : Result) : String := else result.test ++ "." ++ ".".intercalate result.resultPath.toList /-- -The module as a Lake target specification ({lit}`package/module`). This is the unit of execution: -passing it to {lit}`lake test` re-runs the module that produced the result. +The package-qualified module that defines the test ({lit}`package/module`). Reports use it to label +each result and to group the results of one module together. -/ def Result.moduleTarget (result : Result) : String := result.package ++ "/" ++ result.moduleName From e2950bb36334b9a6ccae15745af0356db815355e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 19 Aug 2026 20:56:43 +0200 Subject: [PATCH 08/32] small fixes --- src/errata/Errata/CompileTime.lean | 6 +++--- src/errata/Errata/Golden.lean | 28 ++++++++++++++++++++++++---- src/errata/Errata/Report.lean | 17 ++++++++++------- 3 files changed, 37 insertions(+), 14 deletions(-) diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean index 668cd92f..cd37e4c7 100644 --- a/src/errata/Errata/CompileTime.lean +++ b/src/errata/Errata/CompileTime.lean @@ -60,11 +60,12 @@ meta def elabTestMsgs : Command.CommandElab let endPos := fileMap.toPosition (tk.getTailPos?.getD 0) let declName := `_root_ ++ (← getMainModule) ++ Name.mkSimple s!"errataMsgTest_L{startPos.line}_C{startPos.column}" + let detail := s!"Expected:\n{expected}\n\nActual:\n{actual}" let verdict ← if passed then `(Errata.TestResult.pass) else - `(Errata.TestResult.mismatch "compile-time messages do not match" $(quote actual) + `(Errata.TestResult.mismatch "compile-time messages do not match" $(quote detail) $(quote (← getFileName)) $(quote startPos.line) $(quote startPos.column) $(quote endPos.line) $(quote endPos.column)) @@ -74,8 +75,7 @@ meta def elabTestMsgs : Command.CommandElab let fixRef := (dc?.map (·.raw)).getD tk let hint ← liftCoreM <| MessageData.hint m!"Update the expected output:" #[{ suggestion := suggestedDoc actual }] (ref? := some fixRef) - let body := m!"Errata #test_msgs: the messages do not match.\n\n\ - Expected:\n{expected}\n\nActual:\n{actual}" + let body := m!"Errata #test_msgs: the messages do not match.\n\n{detail}" if (← getOptions).getBool `errata.failOnError false then logErrorAt tk (body ++ hint) else diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean index 5aba57d0..184f339f 100644 --- a/src/errata/Errata/Golden.lean +++ b/src/errata/Errata/Golden.lean @@ -52,6 +52,21 @@ partial def filesUnder (dir : System.FilePath) : IO (Array System.FilePath) := d private def relativeTo (base file : System.FilePath) : String := (file.toString.drop (base.toString.length + 1)).copy +/-- The offset of the first byte at which two contents differ, within the length they share. -/ +private def firstDifference (a b : ByteArray) : Option Nat := Id.run do + for i in [0 : min a.size b.size] do + if a[i]! != b[i]! then return some i + return none + +/-- Describes how two contents differ, for content that is not text. -/ +private def binaryDifference (want got : ByteArray) : String := + let place := + match firstDifference want got with + | some i => s!"binary content differs at byte {i}" + | none => "binary content differs in length" + if want.size == got.size then place + else s!"{place}: expected {want.size} bytes, produced {got.size} bytes" + /-- Compares a produced directory tree against a golden tree, or rewrites it under `--update-golden`. -/ def goldenDir (expected actual : System.FilePath) (loc : Location := by exact here%) : TestM Unit := do @@ -62,7 +77,7 @@ def goldenDir (expected actual : System.FilePath) for file in actualFiles do let dest := expected / relativeTo actual file if let some parent := dest.parent then IO.FS.createDirAll parent - IO.FS.writeFile dest (← IO.FS.readFile file) + IO.FS.writeBinFile dest (← IO.FS.readBinFile file) -- Remove expected files that the produced output no longer contains. if ← expected.pathExists then for file in ← filesUnder expected do @@ -77,10 +92,15 @@ def goldenDir (expected actual : System.FilePath) let want := expected / rel unless ← want.pathExists do failAt loc s!"file not present in the golden directory: {rel}" - let wantContent ← IO.FS.readFile want - let gotContent ← IO.FS.readFile file + let wantContent ← IO.FS.readBinFile want + let gotContent ← IO.FS.readBinFile file unless wantContent == gotContent do - failAt loc s!"golden mismatch for {rel}" (detail? := some (goldenDiff wantContent gotContent)) + -- A diff is only meaningful for text; other content is described by size. + let detail := + match String.fromUTF8? wantContent, String.fromUTF8? gotContent with + | some wantText, some gotText => goldenDiff wantText gotText + | _, _ => binaryDifference wantContent gotContent + failAt loc s!"golden mismatch for {rel}" (detail? := some detail) for file in ← filesUnder expected do let rel := relativeTo expected file unless ← (actual / rel).pathExists do diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean index 63f003e4..1a66cac7 100644 --- a/src/errata/Errata/Report.lean +++ b/src/errata/Errata/Report.lean @@ -73,9 +73,10 @@ private def printSuppressed (s : Suppressed) : IO Unit := do IO.println s!" (... and {", ".intercalate parts.toList})" /-- -Prints a human-readable report and returns the number of failures. Failures and errors are printed -at every verbosity. Verbosity 0 shows nothing else; 1 also shows passes and skips but truncates each -test's passes and skips after a cap, summarizing the rest; 2 shows everything. +Prints a human-readable report and returns the number of failures. Failures and errors are printed at +every verbosity. {name}`Verbosity.quiet` adds passes and skips, truncating each test's after a cap and +summarizing the remainder; {name}`Verbosity.verbose` shows them all; and +{name}`Verbosity.superVerbose` also shows every test's docstring. -/ def humanReport (verbosity : Verbosity) (results : Array Result) : IO Nat := do let cap := 50 @@ -166,9 +167,9 @@ instance : ToJson OutputLog where instance : FromJson OutputLog where fromJson? j := return { log := ← FromJson.fromJson? j } -/-- The suite a result belongs to: its module. -/ +/-- The suite a result belongs to: its package-qualified module. -/ private def suiteOf (r : Result) : String := - r.moduleName + r.moduleTarget /-- The case name of a result: the test name below the module. -/ private def caseOf (r : Result) : String := @@ -177,7 +178,7 @@ private def caseOf (r : Result) : String := private def countWhere (results : Array Result) (p : Status → Bool) : Nat := results.foldl (fun n r => if p r.status then n + 1 else n) 0 -/-- Groups results by their module in a single pass, keeping each module's first-seen order. -/ +/-- Groups results by their package-qualified module in a single pass, keeping first-seen order. -/ private def byModule (results : Array Result) : Array (String × Array Result) := Id.run do let mut order : Array String := #[] let mut groups : Std.HashMap String (Array Result) := {} @@ -190,8 +191,10 @@ private def byModule (results : Array Result) : Array (String × Array Result) : /-- Renders the results as JUnit XML, grouping by the module path. -/ def junitReport (results : Array Result) : String := Id.run do let mut out := "\n\n" - for (suite, cases) in byModule results do + -- Every case in a group shares a package and a module, since the group is keyed by both. + for (_, cases) in byModule results do let pkg := (cases[0]?.map (·.package)).getD "" + let suite := (cases[0]?.map (·.moduleName)).getD "" let failures := countWhere cases (fun s => s matches .fail _) let errors := countWhere cases (fun s => s matches .error _) let skipped := countWhere cases (fun s => s matches .skip _) From 481596ea75b5ec7c17371e492487b345ed9d096e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 19 Aug 2026 21:22:48 +0200 Subject: [PATCH 09/32] name conflict fix --- src/errata/Errata/CompileTime.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean index cd37e4c7..d0b83212 100644 --- a/src/errata/Errata/CompileTime.lean +++ b/src/errata/Errata/CompileTime.lean @@ -123,11 +123,14 @@ meta def elabTestGuard : Command.CommandElab if (lines.drop 1).any (fun l => !l.trimAscii.isEmpty) then firstLine ++ "…" else firstLine let ns ← getCurrNamespace let env ← getEnv + -- Use the module name as part of the test name to avoid conflicts + let modName ← getMainModule + let qualified (n : String) : Name := `_root_ ++ modName ++ ns ++ Name.mkSimple n let mut name := base let mut n := 1 -- In a `module`, the generated definition is private, so probe its mangled name as well. - while env.contains (ns ++ Name.mkSimple name) - || env.contains (mkPrivateName env (ns ++ Name.mkSimple name)) do + while env.contains (qualified name) + || env.contains (mkPrivateName env (qualified name)) do n := n + 1 name := s!"{base} ({n})" let verdict ← @@ -138,7 +141,7 @@ meta def elabTestGuard : Command.CommandElab $(quote (← getFileName)) $(quote startPos.line) $(quote startPos.column) $(quote endPos.line) $(quote endPos.column)) - elabCommand (← `(@[test] def $(mkIdent (Name.mkSimple name)) : Errata.TestResult := $verdict)) + elabCommand (← `(@[test] def $(mkIdent (qualified name)) : Errata.TestResult := $verdict)) -- Report a failure at build time, as `#test_msgs` does. unless passed do let body := m!"Errata #test_guard: the expression did not evaluate to `true`:\n{source}" From bdfc8c632a77806062eaec88351e18c40c092259 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 19 Aug 2026 21:31:51 +0200 Subject: [PATCH 10/32] recording outputs on errors --- src/errata-tests/ErrataTests.lean | 39 +++++++++++++++++++++++++++++++ src/errata/Errata/TestM.lean | 31 ++++++++++++++++++++---- 2 files changed, 66 insertions(+), 4 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 43db56ea..bad409b1 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -94,6 +94,45 @@ def goldenRoundTrip : Test := assertFileExists goldenPath goldenFile goldenPath "contents\n" +/-- Runs one action as a test in a fresh context, returning the results it recorded. -/ +private def resultsOf (act : Test) : TestM (Array Result) := do + let cfg ← mkContext + runEntry cfg <| + TestEntry.of "p" "M" "inner" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } act + +/-- Output written before a failure reaches the enclosing result, where it explains the failure. -/ +@[test] +def captureOutputKeepsOutputOnFailure : Test := do + let results ← resultsOf (discard <| captureOutput (do IO.println "diagnostic"; fail "boom")) + assertEq 1 results.size + let r := results[0]! + assertTrue (r.status matches .fail _) + assertContains "diagnostic" r.output.all + +/-- Output from an action that completes stays with the capture, rather than reaching the result. -/ +@[test] +def captureOutputDivertsOnSuccess : Test := do + let results ← resultsOf do + let captured ← captureOutput (IO.println "quiet") + assertContains "quiet" captured.all + assertEq 1 results.size + assertTrue results[0]!.status.isSuccess + assertTrue results[0]!.output.isEmpty + +/-- A failure that a nested `result` recorded still satisfies `expectFail`. -/ +@[test] +def expectFailSeesNestedResult : Test := do + let results ← resultsOf (expectFail (result "inner" (assertEq 1 2))) + assertEq 1 results.size + assertTrue results[0]!.status.isSuccess + +/-- An error inside `expectFail` is not an expected failure, even when a nested `result` records it. -/ +@[test] +def expectFailRejectsNestedError : Test := do + let results ← resultsOf + (expectFail (result "inner" (show IO Unit from throw (.userError "broken setup")))) + assertTrue (results.any (!·.status.isSuccess)) + -- `here%` reports its own position, so the expected column below is the indentation of the line it -- sits on, and the expected span is the five characters of the token itself. def indentedHere : Location := diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index e0a227df..20f026ee 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -156,7 +156,18 @@ action wrote. def captureOutput (act : TestM Unit) : TestM OutputLog := do let log ← IO.mkRef (#[] : Array Output) let emit (o : Output) : IO Unit := log.modify (·.push o) - IO.withStdout (captureStream emit .stdout) <| IO.withStderr (captureStream emit .stderr) act + let completed ← IO.mkRef false + try + IO.withStdout (captureStream emit .stdout) <| IO.withStderr (captureStream emit .stderr) act + completed.set true + finally + -- An action that does not complete never receives this log, and what it wrote is what explains + -- the failure, so the fragments are handed to the enclosing capture instead. + unless ← completed.get do + for o in ← log.get do + match o with + | .stdout s => IO.print s + | .stderr s => IO.eprint s return { log := ← log.get } /-- @@ -184,8 +195,20 @@ succeeds. An escaping {name}`IO.Error` is not an expected failure: it propagates error, so broken setup is not mistaken for a passing negative test. -/ def expectFail (act : TestM Unit) (loc : Location := by exact here%) : TestM Unit := do - try - act - catch _ => + let ctx ← read + let before := (← ctx.log.get).size + let threw ← + try + act + pure false + catch _ => + pure true + if threw then return + -- A nested `result` records a failure rather than propagating it, so the results it recorded are + -- inspected too. Those results describe the expected failure, so they are dropped along with it. + -- A recorded error is a broken setup rather than an expected failure, and stands. + let logged ← ctx.log.get + if (logged.extract before logged.size).any (·.status matches .fail _) then + ctx.log.set (logged.extract 0 before) return failAt loc "expected the action to fail, but it passed" From 0d55e1044e7a4f9f658aec4b8dfc2f027e6c2029 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 20 Aug 2026 06:36:11 +0200 Subject: [PATCH 11/32] fixes --- src/errata-tests/ErrataTests.lean | 32 ++++++++++++++++++++++++++++-- src/errata/Errata/CompileTime.lean | 8 +++++--- src/errata/Errata/TestM.lean | 16 +++++++-------- 3 files changed, 43 insertions(+), 13 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index bad409b1..e3925e0a 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -129,10 +129,34 @@ def expectFailSeesNestedResult : Test := do /-- An error inside `expectFail` is not an expected failure, even when a nested `result` records it. -/ @[test] def expectFailRejectsNestedError : Test := do - let results ← resultsOf - (expectFail (result "inner" (show IO Unit from throw (.userError "broken setup")))) + let results ← resultsOf <| + expectFail (result "inner" (show IO Unit from throw (.userError "broken setup"))) assertTrue (results.any (!·.status.isSuccess)) +/-- An error inside `expectFail` stands even when a sibling result recorded a failure. -/ +@[test] +def expectFailKeepsErrorBesideFailure : Test := do + let results ← resultsOf <| expectFail do + result "a" <| assertEq 1 2 + result "b" <| show IO Unit from throw (.userError "broken setup") + assertTrue (results.any (·.status matches .error _)) + +/-- A nested failure satisfies `expectFail` whether or not the action goes on to throw. -/ +@[test] +def expectFailAgreesAcrossPaths : Test := do + let thrown ← resultsOf (expectFail (do result "a" (assertEq 1 2); assertEq 3 4)) + let recorded ← resultsOf (expectFail (do result "a" (assertEq 1 2); result "b" (assertEq 3 4))) + result "action throws afterwards" (assertTrue (thrown.all (·.status.isSuccess))) + result "action records only" (assertTrue (recorded.all (·.status.isSuccess))) + +/-- Results other than the expected failure survive `expectFail`. -/ +@[test] +def expectFailKeepsPassingResults : Test := do + let results ← resultsOf <| expectFail do + result "ok" (assertEq 1 1) + result "a" (assertEq 1 2) + assertTrue (results.any (fun r => r.status.isSuccess && r.testName.endsWith "ok")) + -- `here%` reports its own position, so the expected column below is the indentation of the line it -- sits on, and the expected span is the five characters of the token itself. def indentedHere : Location := @@ -266,3 +290,7 @@ def alternativeFailure : Test := expectFail failure /-- `<|>` recovers from an assertion failure by running the alternative. -/ @[test] def alternativeOrElse : Test := failure <|> assertEq 1 1 + +-- Two guards whose first source line is identical must get distinct generated names. +#test_guard 1 + 1 == 2 +#test_guard 1 + 1 == 2 diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean index d0b83212..ebbf3c61 100644 --- a/src/errata/Errata/CompileTime.lean +++ b/src/errata/Errata/CompileTime.lean @@ -125,12 +125,14 @@ meta def elabTestGuard : Command.CommandElab let env ← getEnv -- Use the module name as part of the test name to avoid conflicts let modName ← getMainModule - let qualified (n : String) : Name := `_root_ ++ modName ++ ns ++ Name.mkSimple n + -- `_root_` marks the name as absolute for the declaration, but it's not _really_ part of the name + let declared (n : String) : Name := modName ++ ns ++ Name.mkSimple n + let qualified (n : String) : Name := `_root_ ++ declared n let mut name := base let mut n := 1 -- In a `module`, the generated definition is private, so probe its mangled name as well. - while env.contains (qualified name) - || env.contains (mkPrivateName env (qualified name)) do + while env.contains (declared name) + || env.contains (mkPrivateName env (declared name)) do n := n + 1 name := s!"{base} ({n})" let verdict ← diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 20f026ee..44b4a420 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -203,12 +203,12 @@ def expectFail (act : TestM Unit) (loc : Location := by exact here%) : TestM Uni pure false catch _ => pure true - if threw then return - -- A nested `result` records a failure rather than propagating it, so the results it recorded are - -- inspected too. Those results describe the expected failure, so they are dropped along with it. - -- A recorded error is a broken setup rather than an expected failure, and stands. + -- A nested `result` records a failure rather than propagating it, so the results the action + -- recorded are inspected too. Their failures are the expected failure and are dropped. + -- Everything else is retained because a recorded error is a broken setup rather than a failure. let logged ← ctx.log.get - if (logged.extract before logged.size).any (·.status matches .fail _) then - ctx.log.set (logged.extract 0 before) - return - failAt loc "expected the action to fail, but it passed" + let added := logged.extract before logged.size + let failedInside := added.any (·.status matches .fail _) + ctx.log.set (logged.extract 0 before ++ added.filter (fun r => !(r.status matches .fail _))) + unless threw || failedInside do + failAt loc "expected the action to fail, but it passed" From 2b69e29af9ceb277508afaa12165712937b5dc50 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 20 Aug 2026 09:45:54 +0200 Subject: [PATCH 12/32] output fixes --- lakefile.lean | 2 +- src/errata-tests/ErrataTests.lean | 40 ++++++++++++++++++++++++++++++ src/errata/Errata/CompileTime.lean | 2 +- src/errata/Errata/Golden.lean | 12 ++++++--- src/errata/Errata/Runner.lean | 9 ++++--- src/errata/Errata/TestM.lean | 31 +++++++++++++++++------ src/tests/TestMain.lean | 2 +- 7 files changed, 80 insertions(+), 18 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index b218a94a..0b37148e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -242,7 +242,7 @@ private def splitArgs (args : List String) : Except String (List String × List e.g. `lake run Errata.run --test-options {opt}`." | none => .ok (names, rest) -/-- Usage information for `lake test`. -/ +/-- Usage information for `lake run Errata.run`. -/ private def usage : String := include_str "src/errata/Errata/usage.txt" script run (args) do diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index e3925e0a..2c464c44 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -94,12 +94,52 @@ def goldenRoundTrip : Test := assertFileExists goldenPath goldenFile goldenPath "contents\n" +/-- A golden file is written through directories that do not exist yet. -/ +@[test] +def goldenFileCreatesDirectories : Test := + IO.FS.withTempDir fun dir => + withReader ({ · with updateGolden := true }) do + let goldenPath := dir / "nested" / "deeper" / "expected.txt" + goldenFile goldenPath "contents\n" + assertFileExists goldenPath + /-- Runs one action as a test in a fresh context, returning the results it recorded. -/ private def resultsOf (act : Test) : TestM (Array Result) := do let cfg ← mkContext runEntry cfg <| TestEntry.of "p" "M" "inner" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } act +/-- A missing produced directory is a golden failure at the call site, not a bare error. -/ +@[test] +def goldenDirReportsMissingOutput : Test := do + let results ← IO.FS.withTempDir fun dir => + resultsOf (goldenDir (dir / "expected") (dir / "never-created")) + assertEq 1 results.size + assertTrue (results[0]!.status matches .fail _) + +/-- A produced directory with no files in it can be recorded and then compared. -/ +@[test] +def goldenDirHandlesEmptyOutput : Test := do + let results ← IO.FS.withTempDir fun dir => do + let expected := dir / "expected" + let actual := dir / "actual" + IO.FS.createDirAll actual + resultsOf do + withReader ({ · with updateGolden := true }) (goldenDir expected actual) + goldenDir expected actual + assertEq 1 results.size + assertTrue results[0]!.status.isSuccess + +/-- A file where a directory was expected is a golden failure, not a raw error. -/ +@[test] +def goldenDirRejectsNonDirectory : Test := do + let results ← IO.FS.withTempDir fun dir => do + let actual := dir / "actual" + IO.FS.writeFile actual "not a directory\n" + resultsOf (goldenDir (dir / "expected") actual) + assertEq 1 results.size + assertTrue (results[0]!.status matches .fail _) + /-- Output written before a failure reaches the enclosing result, where it explains the failure. -/ @[test] def captureOutputKeepsOutputOnFailure : Test := do diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean index ebbf3c61..0213a6f0 100644 --- a/src/errata/Errata/CompileTime.lean +++ b/src/errata/Errata/CompileTime.lean @@ -57,7 +57,7 @@ meta def elabTestMsgs : Command.CommandElab -- qualifies it so that two modules with a `#test_msgs` at the same position do not collide. let fileMap ← getFileMap let startPos := fileMap.toPosition (tk.getPos?.getD 0) - let endPos := fileMap.toPosition (tk.getTailPos?.getD 0) + let endPos := fileMap.toPosition (tk.getTailPos?.getD (tk.getPos?.getD 0)) let declName := `_root_ ++ (← getMainModule) ++ Name.mkSimple s!"errataMsgTest_L{startPos.line}_C{startPos.column}" let detail := s!"Expected:\n{expected}\n\nActual:\n{actual}" diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean index 184f339f..75bea8a7 100644 --- a/src/errata/Errata/Golden.lean +++ b/src/errata/Errata/Golden.lean @@ -28,8 +28,7 @@ def goldenFile (expected : System.FilePath) (actual : String) (loc : Location := by exact here%) : TestM Unit := do let ctx ← read if ctx.updateGolden then - if let some parent := expected.parent then IO.FS.createDirAll parent - IO.FS.writeFile expected actual + writeFile expected actual else if ← expected.pathExists then let want ← IO.FS.readFile expected unless want == actual do @@ -71,13 +70,18 @@ private def binaryDifference (want got : ByteArray) : String := def goldenDir (expected actual : System.FilePath) (loc : Location := by exact here%) : TestM Unit := do let ctx ← read + unless ← actual.isDir do + failAt loc s!"missing produced directory {actual}" + (detail? := some "The code under test did not create it as a directory.") let actualFiles ← filesUnder actual if ctx.updateGolden then + -- The golden tree is recorded even when the produced tree holds no files, so that a later run + -- compares against it rather than reporting it as missing. + IO.FS.createDirAll expected let actualRels := actualFiles.map (relativeTo actual) for file in actualFiles do let dest := expected / relativeTo actual file - if let some parent := dest.parent then IO.FS.createDirAll parent - IO.FS.writeBinFile dest (← IO.FS.readBinFile file) + writeBinFile dest (← IO.FS.readBinFile file) -- Remove expected files that the produced output no longer contains. if ← expected.pathExists then for file in ← filesUnder expected do diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index fa8cb6f4..cbba7951 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -187,9 +187,12 @@ def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do let cfg ← mkContext (verbosity := opts.verbosity) (updateGolden := opts.updateGolden) (options := opts.options) (seed := opts.seed) let results ← run cfg entries - if let some path := opts.junitPath then IO.FS.writeFile path (junitReport results) - if let some path := opts.jsonPath then IO.FS.writeFile path (jsonReport results) - if let some path := opts.markdownPath then IO.FS.writeFile path (markdownReport results) + let writeReport (path? : Option String) (render : Array Result → String) : IO Unit := do + if let some path := path? then + writeFile path (render results) + writeReport opts.junitPath junitReport + writeReport opts.jsonPath jsonReport + writeReport opts.markdownPath markdownReport let failures ← humanReport opts.verbosity results -- Warn about options that were supplied but never read by any test (typos, removed flags). let used ← cfg.usedOptions.get diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 44b4a420..3d978b65 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -122,23 +122,38 @@ def skip (reason : String) : TestM Unit := do let ctx ← read ctx.log.modify (·.push (ctx.skip reason)) -/-- A stream that hands each write to a destination as a fragment tagged by the stream it came from. -/ +/-- Writes a file, creating all parent directories if necessary. -/ +def writeFile (path : System.FilePath) (contents : String) : IO Unit := do + if let some parent := path.parent then IO.FS.createDirAll parent + IO.FS.writeFile path contents + +/-- Writes a binary file, creating all parent directories if necessary. -/ +def writeBinFile (path : System.FilePath) (contents : ByteArray) : IO Unit := do + if let some parent := path.parent then IO.FS.createDirAll parent + IO.FS.writeBinFile path contents + +/-- +A stream that hands each write to a destination as a fragment tagged by the stream it came from. + +A write of raw bytes is decoded, and rejected if it is not valid {lit}`UTF-8`. +-/ private def captureStream (emit : Output → IO Unit) (mk : String → Output) : IO.FS.Stream where flush := pure () read _ := pure .empty write bytes := match String.fromUTF8? bytes with | some s => emit (mk s) - | none => throw (.userError "captured test output was not valid UTF-8") + | none => + throw (.userError "a raw byte write to a captured stream was not valid UTF-8") getLine := pure "" putStr s := emit (mk s) isTty := pure false /-- Runs a test action with the given context, capturing its outcome as data rather than letting it -propagate. The action's stdout and stderr are recorded, in order and tagged by stream, and returned -alongside the outcome. Each fragment is also handed to the context's output destination as it is -written, so a live runner can stream output while the test runs. +propagate. The action's stdout and stderr are recorded as text, in order and tagged by stream, and +returned alongside the outcome. Each fragment is also handed to the context's output destination as +it is written, so a live runner can stream output while the test runs. -/ def runCapturing (ctx : Context) (act : TestM Unit) : IO (Except IO.Error (Except TestFailure Unit) × OutputLog) := do @@ -149,9 +164,9 @@ def runCapturing (ctx : Context) (act : TestM Unit) : return (outcome, { log := ← log.get }) /-- -Runs an action with stdout and stderr captured into a fresh log, then returns the captured output -in order. The redirection is local to the action, so a test can make assertions about what the -action wrote. +Runs an action with stdout and stderr captured into a fresh log, then returns the captured text in +order. The redirection is local to the action, so a test can make assertions about what the action +wrote. -/ def captureOutput (act : TestM Unit) : TestM OutputLog := do let log ← IO.mkRef (#[] : Array Output) diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 037cc427..87aa2b5d 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -360,7 +360,7 @@ def testBuildLog (_ : Config) : IO Unit := do /-- Runs Errata's own tests, reporting them the way the Errata runner does. -/ def testErrata (config : Config) : IO Unit := do let verbosity := if config.verbose then Errata.Verbosity.quiet else .silent - let cfg ← Errata.mkContext (verbosity := verbosity) + let cfg ← Errata.mkContext (verbosity := verbosity) (updateGolden := config.updateExpected) let results ← Errata.run cfg errataTests let failures ← Errata.humanReport verbosity results unless failures == 0 do From dedfa17d341d132784123687410a84b54b6df003 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 20 Aug 2026 09:47:02 +0200 Subject: [PATCH 13/32] warn on no tests --- src/errata/Errata/Runner.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index cbba7951..140b659f 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -194,6 +194,8 @@ def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do writeReport opts.jsonPath jsonReport writeReport opts.markdownPath markdownReport let failures ← humanReport opts.verbosity results + if entries.isEmpty then + IO.eprintln "warning: no tests were discovered" -- Warn about options that were supplied but never read by any test (typos, removed flags). let used ← cfg.usedOptions.get let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k From 18c7b15cf34980e2904575b66a1c9515beba1cd5 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 20 Aug 2026 10:51:08 +0200 Subject: [PATCH 14/32] output fixes and docs format --- src/errata-tests/ErrataTests.lean | 64 +++++++++++++++++++++++++++++-- src/errata/Errata/Context.lean | 7 ++++ src/errata/Errata/Report.lean | 6 ++- src/errata/Errata/Runner.lean | 9 +++-- src/errata/Errata/TestM.lean | 14 ++++++- 5 files changed, 90 insertions(+), 10 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 2c464c44..e839451d 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -159,6 +159,52 @@ def captureOutputDivertsOnSuccess : Test := do assertTrue results[0]!.status.isSuccess assertTrue results[0]!.output.isEmpty +/-- +A live output destination writes to the real stdout, so printing from it does not re-enter the +capture. The counter is bounded so that a regression fails this test instead of exhausting the stack. +-/ +@[test] +def writeOutputDoesNotRecurse : Test := do + let depth ← IO.mkRef 0 + let cfg ← mkContext + let ctx := { cfg with + writeOutput := fun o => do + depth.modify (· + 1) + if (← depth.get) < 5 then + match o with + | .stdout s => IO.print s + | .stderr s => IO.eprint s } + discard <| runEntry ctx <| + TestEntry.of "p" "M" "prints" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } + (IO.println "live" : Test) + assertEq 1 (← depth.get) + +/-- +A live output destination that fails does not fail the test that happened to be printing. It is +reported once and then left alone, rather than retried for every fragment. +-/ +@[test] +def writeOutputFailureIsContained : Test := do + let calls ← IO.mkRef 0 + let statuses ← IO.mkRef (#[] : Array Status) + let cfg ← mkContext + let ctx := { cfg with + writeOutput := fun _ => do + calls.modify (· + 1) + throw (.userError "broken pipe") } + let out ← captureOutput do + for name in ["first", "second"] do + let entry := TestEntry.of "p" "M" name + { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } (IO.println "output" : Test) + for r in ← runEntry ctx entry do + statuses.modify (·.push r.status) + result "the printing tests are not blamed" do + assertTrue ((← statuses.get).all (·.isSuccess)) + result "the destination is left alone after it fails" do + assertEq 1 (← calls.get) + result "the failure is reported" do + assertContains "live output destination failed" out.all + /-- A failure that a nested `result` recorded still satisfies `expectFail`. -/ @[test] def expectFailSeesNestedResult : Test := do @@ -226,8 +272,10 @@ def verbosityLevels : Test := do assertEq Verbosity.superVerbose Verbosity.verbose.increase assertEq Verbosity.superVerbose Verbosity.superVerbose.increase -/-- The runner's command line: the `-v` forms select the verbosity, declared flags parse, and -options for the tests go after `--`. -/ +/-- +The runner's command line: the `-v` forms select the verbosity, declared flags parse, and options +for the tests go after `--`. +-/ @[test] def runnerArgParsing : Test := do result "default verbosity" do @@ -263,6 +311,12 @@ def runnerArgParsing : Test := do | .error msg => assertContains "ErrataTests" msg | .ok _ => assertTrue false "expected an error" +/-- A run that discovers nothing says so, rather than reporting success silently. -/ +@[test] +def emptyRunWarns : Test := do + let out ← captureOutput (discard <| runMain #[] []) + assertContains "no tests were discovered" out.all + /-- At silent verbosity the report hides passes but shows failures and the summary line. -/ @[test] def reportSilent : Test := do @@ -292,8 +346,10 @@ def reportTruncates : Test := do assertEq 61 (verbose.stdout.splitOn "ok ").length assertEq 1 (verbose.stdout.splitOn "(... and").length -/-- Truncation never suppresses a failure or error: past the cap they print in full and only the -passes around them are summarized. -/ +/-- +Truncation never suppresses a failure or error: past the cap they print in full and only the passes +around them are summarized. +-/ @[test] def reportTruncationShowsFailures : Test := do let many := (Array.range 60).map fun i => diff --git a/src/errata/Errata/Context.lean b/src/errata/Errata/Context.lean index d72d8060..454cf1a9 100644 --- a/src/errata/Errata/Context.lean +++ b/src/errata/Errata/Context.lean @@ -52,5 +52,12 @@ structure Context where /-- Receives each captured output fragment as it is written, in order. The default discards them; a live runner sets it to stream output as the test produces it. + + It runs with the streams that were in place before the test's output was redirected, so it may + print in case of internal errors. -/ writeOutput : Output → IO Unit := fun _ => pure () + /-- + Whether a write to the output destination has failed. If true, further attempts are suppressed. + -/ + outputFailed : IO.Ref Bool diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean index 1a66cac7..c6cddcbd 100644 --- a/src/errata/Errata/Report.lean +++ b/src/errata/Errata/Report.lean @@ -50,8 +50,10 @@ private def printResult (verbosity : Verbosity) (r : Result) : IO Unit := do printDoc unless r.output.isEmpty do IO.println (indentLines s!"output:\n{r.output.all}") -/-- A running tally of results suppressed by truncation. Only passes and skips are ever suppressed; -failures and errors always print. -/ +/-- +A running tally of results suppressed by truncation. Only passes and skips are ever suppressed; +failures and errors always print. +-/ private structure Suppressed where passed : Nat := 0 skipped : Nat := 0 diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index 140b659f..d8b500d5 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -70,7 +70,8 @@ def mkContext (verbosity : Verbosity := .silent) (updateGolden : Bool := false) (options : OptionMap := {}) (seed : Option Nat := none) : IO Context := do let log ← IO.mkRef (#[] : Array Result) let usedOptions ← IO.mkRef ({} : Std.HashSet String) - return { verbosity, updateGolden, options, seed, log, usedOptions } + let outputFailed ← IO.mkRef false + return { verbosity, updateGolden, options, seed, log, usedOptions, outputFailed } /-- The settings parsed from the runner's command line. -/ structure Options where @@ -168,8 +169,10 @@ def optionsOfParsed (p : Cli.Parsed) : Except String Options := do options := ← projectOptions (p.variableArgsAs! String).toList } -/-- Parses the runner's command line into settings: the declared flags, then any options for the -tests themselves after a {lit}`--` separator. -/ +/-- +Parses the runner's command line into settings: the declared flags, then any options for the tests +themselves after a {lit}`--` separator. +-/ def parseOptions (args : List String) : Except String Options := match (runnerCmd fun _ => pure 0).parse args with | .error e => .error e.kind.msg diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 3d978b65..efba7ed0 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -158,7 +158,19 @@ it is written, so a live runner can stream output while the test runs. def runCapturing (ctx : Context) (act : TestM Unit) : IO (Except IO.Error (Except TestFailure Unit) × OutputLog) := do let log ← IO.mkRef (#[] : Array Output) - let emit (o : Output) : IO Unit := do log.modify (·.push o); ctx.writeOutput o + -- The destination runs with the streams that were in place before the redirection, so writing to + -- stdout from it reaches the runner instead of re-entering this capture. + let realOut ← IO.getStdout + let realErr ← IO.getStderr + let emit (o : Output) : IO Unit := do + log.modify (·.push o) + unless ← ctx.outputFailed.get do + try + IO.withStdout realOut <| IO.withStderr realErr <| ctx.writeOutput o + catch e => + ctx.outputFailed.set true + -- Saying so can fail in turn, when the destination that just failed was stderr itself. + try realErr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure () let outcome ← IO.withStdout (captureStream emit .stdout) <| IO.withStderr (captureStream emit .stderr) <| ((act ctx).run).toBaseIO return (outcome, { log := ← log.get }) From 46d16f934f16e381019aedd76d593dbff3e493b6 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 06:35:38 +0200 Subject: [PATCH 15/32] test fixes --- .github/workflows/ci.yml | 10 ++-- src/errata-tests/ErrataTests.lean | 71 ++++++++++++++++++++++++-- src/errata/Errata/Discovery.lean | 55 +++++++++++--------- src/errata/Errata/Golden.lean | 19 +++---- src/errata/Errata/Report.lean | 8 +-- src/errata/Errata/Runner.lean | 3 +- src/errata/Errata/TestM.lean | 85 +++++++++++++++++++++++++------ 7 files changed, 189 insertions(+), 62 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9be07d1f..9e31734d 100644 --- a/.github/workflows/ci.yml +++ b/.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 Errata:orphanMods)" + VersoLiterateCode:orphanMods Errata:orphanMods ErrataTests:orphanMods)" if [ -n "$(printf '%s' "$out" | tr -d '[:space:]')" ]; then echo "Found orphaned modules:" echo "$out" @@ -149,10 +151,6 @@ jobs: run: | lake test -- --verbose --check-tex - - name: Run Errata's self-tests - run: | - lake run Errata.run ErrataTests --test-options --verbose - - name: Test the dev server run: | ./src/tests/run_serve_test.sh diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index e839451d..fc35269f 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -140,6 +140,30 @@ def goldenDirRejectsNonDirectory : Test := do assertEq 1 results.size assertTrue (results[0]!.status matches .fail _) +/-- A directory standing where the golden tree has a file is a missing file, not a pass. -/ +@[test] +def goldenDirRejectsDirectoryForFile : Test := do + let results ← IO.FS.withTempDir fun dir => do + let expected := dir / "expected" + let actual := dir / "actual" + writeFile (expected / "d") "contents\n" + IO.FS.createDirAll (actual / "d") + resultsOf (goldenDir expected actual) + assertEq 1 results.size + assertTrue (results[0]!.status matches .fail _) + +/-- A file standing where the golden tree has a directory is a golden failure, not a raw error. -/ +@[test] +def goldenDirRejectsFileForDirectory : Test := do + let results ← IO.FS.withTempDir fun dir => do + let expected := dir / "expected" + let actual := dir / "actual" + writeFile (expected / "d" / "inner") "contents\n" + writeFile (actual / "d") "not a directory\n" + resultsOf (goldenDir expected actual) + assertEq 1 results.size + assertTrue (results[0]!.status matches .fail _) + /-- Output written before a failure reaches the enclosing result, where it explains the failure. -/ @[test] def captureOutputKeepsOutputOnFailure : Test := do @@ -159,6 +183,34 @@ def captureOutputDivertsOnSuccess : Test := do assertTrue results[0]!.status.isSuccess assertTrue results[0]!.output.isEmpty +/-- A raw write may end partway through a code point; the write that completes it is joined on. -/ +@[test] +def captureJoinsSplitWrites : Test := do + let bytes := "é".toUTF8 + let captured ← captureOutput do + let out ← IO.getStdout + out.write (bytes.extract 0 1) + out.write (bytes.extract 1 bytes.size) + assertEq "é" captured.stdout + +/-- Bytes whose code point is never completed are an error, not silently dropped. -/ +@[test] +def captureRejectsDanglingBytes : Test := do + let results ← resultsOf do + let out ← IO.getStdout + out.write ("é".toUTF8.extract 0 1) + assertEq 1 results.size + assertTrue (results[0]!.status matches .error _) + +/-- A raw write with no valid decoding is rejected at the write itself. -/ +@[test] +def captureRejectsInvalidBytes : Test := do + let results ← resultsOf do + let out ← IO.getStdout + out.write (ByteArray.mk #[0xFF]) + assertEq 1 results.size + assertTrue (results[0]!.status matches .error _) + /-- A live output destination writes to the real stdout, so printing from it does not re-enter the capture. The counter is bounded so that a regression fails this test instead of exhausting the stack. @@ -311,11 +363,14 @@ def runnerArgParsing : Test := do | .error msg => assertContains "ErrataTests" msg | .ok _ => assertTrue false "expected an error" -/-- A run that discovers nothing says so, rather than reporting success silently. -/ +/-- A run that discovers nothing fails: a test tool with no tests is a broken setup, not a pass. -/ @[test] -def emptyRunWarns : Test := do - let out ← captureOutput (discard <| runMain #[] []) +def emptyRunFails : Test := do + let code ← IO.mkRef (0 : UInt32) + let out ← captureOutput do + code.set (← runMain #[] []) assertContains "no tests were discovered" out.all + assertEq 1 (← code.get).toNat /-- At silent verbosity the report hides passes but shows failures and the summary line. -/ @[test] @@ -334,6 +389,16 @@ def reportVerbose : Test := do let out ← captureOutput do discard <| humanReport .verbose #[pass] assertContains "ok p/M t" out.stdout +/-- Characters XML 1.0 forbids are dropped from the JUnit report rather than emitted. -/ +@[test] +def junitDropsForbiddenChars : Test := do + let bad := (Char.ofNat 0xFFFF).toString ++ (Char.ofNat 0xFFFE).toString ++ (Char.ofNat 0x1).toString + let r : Result := { package := "p", moduleName := "M", test := "t", + status := .fail { message := s!"bad{bad}char" } } + let xml := junitReport #[r] + assertContains "badchar" xml + assertTrue (!xml.contains (Char.ofNat 0xFFFF) && !xml.contains (Char.ofNat 0xFFFE)) + /-- A test's results are truncated after the cap at quiet verbosity, with a summary, but not at verbose. -/ @[test] def reportTruncates : Test := do diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean index d916acad..abb983f5 100644 --- a/src/errata/Errata/Discovery.lean +++ b/src/errata/Errata/Discovery.lean @@ -91,8 +91,9 @@ meta def testNameBelow (moduleName declName : Name) : String := /-- {lit}`getAllTests% "package" Mod.A Mod.B ...` reads the tests recorded by {lit}`@[test]` in the -named modules and expands to the array of {name}`TestEntry` values that run them. Each module must -be imported, with {lit}`import all` for module-system modules, so its tests are reachable. +named modules and every imported module below them, and expands to the array of {name}`TestEntry` +values that run them. Each module must be imported, with {lit}`import all` for module-system +modules, so its tests are reachable. -/ syntax (name := getAllTests) "getAllTests%" str ident* : term @@ -103,29 +104,33 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do | throwUnsupportedSyntax let package := pkg.getString let env ← getEnv + let moduleNames := env.allImportedModuleNames let mut entries : Array Term := #[] for modStx in mods do - let moduleName := modStx.getId - let some idx := env.getModuleIdx? moduleName - | throwErrorAt modStx "Module `{moduleName}` is not imported, so its tests cannot be \ - reached. Import it, using `import all {moduleName}` if it belongs to the module system." - let moduleStr := moduleName.toString - for test in testExt.getModuleEntries env idx do - -- The internal name is used here, because the user-facing name can be ambiguous for private - -- tests - let userName := privateToUserName test.name - let testName := testNameBelow moduleName userName - let range ← findDeclarationRanges? test.name - let pos := (range.map (·.range.pos)).getD ⟨0, 0⟩ - let endPos := (range.map (·.range.endPos)).getD ⟨0, 0⟩ - -- The docstring captured when the attribute was applied, so the report and widget can show it. - let docStx ← match test.docstring? with - | some doc => `(some $(quote doc)) - | none => `((none : Option String)) - entries := entries.push <| ← - `(Errata.TestEntry.of $(quote package) $(quote moduleStr) $(quote testName) - (Errata.Location.mk $(quote test.file) - (Errata.Position.mk $(quote pos.line) $(quote pos.column)) - (Errata.Position.mk $(quote endPos.line) $(quote endPos.column))) - (@$(mkCIdent test.name)) (docstring? := $docStx)) + let rootName := modStx.getId + unless (env.getModuleIdx? rootName).isSome do + throwErrorAt modStx "Module `{rootName}` is not imported, so its tests cannot be \ + reached. Import it, using `import all {rootName}` if it belongs to the module system." + for h : idx in [0 : moduleNames.size] do + let moduleName := moduleNames[idx] + unless rootName.isPrefixOf moduleName do continue + let moduleStr := moduleName.toString + for test in testExt.getModuleEntries env idx do + -- The internal name is used here, because the user-facing name can be ambiguous for private + -- tests + let userName := privateToUserName test.name + let testName := testNameBelow moduleName userName + let range ← findDeclarationRanges? test.name + let pos := (range.map (·.range.pos)).getD ⟨0, 0⟩ + let endPos := (range.map (·.range.endPos)).getD ⟨0, 0⟩ + -- The docstring captured when the attribute was applied, so the report and widget can show it. + let docStx ← match test.docstring? with + | some doc => `(some $(quote doc)) + | none => `((none : Option String)) + entries := entries.push <| ← + `(Errata.TestEntry.of $(quote package) $(quote moduleStr) $(quote testName) + (Errata.Location.mk $(quote test.file) + (Errata.Position.mk $(quote pos.line) $(quote pos.column)) + (Errata.Position.mk $(quote endPos.line) $(quote endPos.column))) + (@$(mkCIdent test.name)) (docstring? := $docStx)) elabTerm (← `(#[$entries,*])) expectedType? diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean index 75bea8a7..e3cea3aa 100644 --- a/src/errata/Errata/Golden.lean +++ b/src/errata/Errata/Golden.lean @@ -91,13 +91,15 @@ def goldenDir (expected actual : System.FilePath) unless ← expected.pathExists do failAt loc s!"missing golden directory {expected}" (detail? := some "Run with --update-golden to create it.") - for file in actualFiles do - let rel := relativeTo actual file - let want := expected / rel - unless ← want.pathExists do + -- Membership is decided against the walked file lists rather than by a filesystem probe, so a + -- directory standing where a file belongs counts as that file being absent. + let expectedRels := (← filesUnder expected).map (relativeTo expected) + let actualRels := actualFiles.map (relativeTo actual) + for rel in actualRels do + unless expectedRels.contains rel do failAt loc s!"file not present in the golden directory: {rel}" - let wantContent ← IO.FS.readBinFile want - let gotContent ← IO.FS.readBinFile file + let wantContent ← IO.FS.readBinFile (expected / rel) + let gotContent ← IO.FS.readBinFile (actual / rel) unless wantContent == gotContent do -- A diff is only meaningful for text; other content is described by size. let detail := @@ -105,7 +107,6 @@ def goldenDir (expected actual : System.FilePath) | some wantText, some gotText => goldenDiff wantText gotText | _, _ => binaryDifference wantContent gotContent failAt loc s!"golden mismatch for {rel}" (detail? := some detail) - for file in ← filesUnder expected do - let rel := relativeTo expected file - unless ← (actual / rel).pathExists do + for rel in expectedRels do + unless actualRels.contains rel do failAt loc s!"file missing from the produced output: {rel}" diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean index c6cddcbd..5f924c1c 100644 --- a/src/errata/Errata/Report.lean +++ b/src/errata/Errata/Report.lean @@ -118,12 +118,14 @@ def humanReport (verbosity : Verbosity) (results : Array Result) : IO Nat := do return failed + errors /-- -Drops the control characters XML 1.0 forbids even when escaped: those below {lit}`U+0020` other than -tab, newline, and carriage return. +Drops the characters XML 1.0 forbids even when escaped: those below {lit}`U+0020` other than tab, +newline, and carriage return, and the noncharacters {lit}`U+FFFE` and {lit}`U+FFFF`. -/ private def dropXmlForbidden (s : String) : String := s.foldl (init := "") fun acc c => - if c == '\t' || c == '\n' || c == '\r' || Nat.ble 0x20 c.toNat then acc.push c else acc + if c == '\uFFFE' || c == '\uFFFF' then acc + else if c == '\t' || c == '\n' || c == '\r' || Nat.ble 0x20 c.toNat then acc.push c + else acc /-- Escapes text for XML and drops characters XML 1.0 forbids even when escaped, so a captured ANSI escape diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index d8b500d5..1a84db77 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -198,7 +198,8 @@ def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do writeReport opts.markdownPath markdownReport let failures ← humanReport opts.verbosity results if entries.isEmpty then - IO.eprintln "warning: no tests were discovered" + IO.eprintln "error: no tests were discovered" + return 1 -- Warn about options that were supplied but never read by any test (typos, removed flags). let used ← cfg.usedOptions.get let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index efba7ed0..310de83d 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -132,22 +132,64 @@ def writeBinFile (path : System.FilePath) (contents : ByteArray) : IO Unit := do if let some parent := path.parent then IO.FS.createDirAll parent IO.FS.writeBinFile path contents +/-- The number of bytes in the {lit}`UTF-8` sequence a lead byte introduces, or {name}`none` for a +continuation or invalid byte. -/ +private def utf8SeqLength (b : UInt8) : Option Nat := + if b &&& 0x80 == 0 then some 1 + else if b &&& 0xE0 == 0xC0 then some 2 + else if b &&& 0xF0 == 0xE0 then some 3 + else if b &&& 0xF8 == 0xF0 then some 4 + else none + +/-- +Splits bytes into a prefix ready to decode and a tail that is the start of an unfinished +{lit}`UTF-8` code point. Bytes that cannot be completed by any continuation go in the prefix, where +decoding reports them as invalid. +-/ +private def splitUtf8Tail (bytes : ByteArray) : ByteArray × ByteArray := Id.run do + for back in [1 : 4] do + if back > bytes.size then break + let i := bytes.size - back + if let some len := utf8SeqLength bytes[i]! then + if i + len > bytes.size then + return (bytes.extract 0 i, bytes.extract i bytes.size) + else + break + return (bytes, .empty) + /-- A stream that hands each write to a destination as a fragment tagged by the stream it came from. -A write of raw bytes is decoded, and rejected if it is not valid {lit}`UTF-8`. +A write of raw bytes may end partway through a {lit}`UTF-8` code point; the trailing bytes wait in a +buffer for the write that completes them. Bytes that decode to nothing valid are rejected. The +returned action ends the capture, rejecting any buffered bytes whose code point never arrived. -/ -private def captureStream (emit : Output → IO Unit) (mk : String → Output) : IO.FS.Stream where - flush := pure () - read _ := pure .empty - write bytes := - match String.fromUTF8? bytes with - | some s => emit (mk s) - | none => - throw (.userError "a raw byte write to a captured stream was not valid UTF-8") - getLine := pure "" - putStr s := emit (mk s) - isTty := pure false +private def captureStream (emit : Output → IO Unit) (mk : String → Output) : + IO (IO.FS.Stream × IO Unit) := do + let pending ← IO.mkRef ByteArray.empty + let invalid : IO.Error := + .userError "a raw byte write to a captured stream was not valid UTF-8" + let stream : IO.FS.Stream := { + flush := pure () + read := fun _ => pure .empty + write := fun bytes => do + let (ready, rest) := splitUtf8Tail ((← pending.get) ++ bytes) + match String.fromUTF8? ready with + | some s => + pending.set rest + unless s.isEmpty do emit (mk s) + | none => + pending.set .empty + throw invalid + getLine := pure "" + putStr := fun s => emit (mk s) + isTty := pure false + } + let close : IO Unit := do + unless (← pending.get).isEmpty do + pending.set .empty + throw invalid + return (stream, close) /-- Runs a test action with the given context, capturing its outcome as data rather than letting it @@ -171,8 +213,16 @@ def runCapturing (ctx : Context) (act : TestM Unit) : ctx.outputFailed.set true -- Saying so can fail in turn, when the destination that just failed was stderr itself. try realErr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure () - let outcome ← IO.withStdout (captureStream emit .stdout) <| - IO.withStderr (captureStream emit .stderr) <| ((act ctx).run).toBaseIO + let (outStream, outClose) ← captureStream emit .stdout + let (errStream, errClose) ← captureStream emit .stderr + -- Closing inside the captured action makes dangling bytes at the end of the test an error of the + -- test itself. + let body : IO (Except TestFailure Unit) := do + let r ← (act ctx).run + outClose + errClose + return r + let outcome ← IO.withStdout outStream <| IO.withStderr errStream <| body.toBaseIO return (outcome, { log := ← log.get }) /-- @@ -184,8 +234,13 @@ def captureOutput (act : TestM Unit) : TestM OutputLog := do let log ← IO.mkRef (#[] : Array Output) let emit (o : Output) : IO Unit := log.modify (·.push o) let completed ← IO.mkRef false + let (outStream, outClose) ← captureStream emit .stdout + let (errStream, errClose) ← captureStream emit .stderr try - IO.withStdout (captureStream emit .stdout) <| IO.withStderr (captureStream emit .stderr) act + IO.withStdout outStream <| IO.withStderr errStream do + act + outClose + errClose completed.set true finally -- An action that does not complete never receives this log, and what it wrote is what explains From 346578b9d034ac935bf137dedd767c10b83db05b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 08:06:41 +0200 Subject: [PATCH 16/32] more warning --- lakefile.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 0b37148e..2d2d467e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -311,12 +311,14 @@ script run (args) do 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. Only libraries that already carry tests are worth - -- checking. That is a configuration slip rather than a test failure, so report it and run anyway. + -- 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 mods.any (testMods.contains ·) then + 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) From 9506b8aecc0c23d2da2fe5fdca860ccc8ce46b52 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 08:25:02 +0200 Subject: [PATCH 17/32] fix: don't double-deliver printed output --- src/errata-tests/ErrataTests.lean | 20 ++++++++++++++++++++ src/errata/Errata/Context.lean | 13 +++++++++++++ src/errata/Errata/TestM.lean | 15 +++++++++------ 3 files changed, 42 insertions(+), 6 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index fc35269f..438d3a58 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -231,6 +231,26 @@ def writeOutputDoesNotRecurse : Test := do (IO.println "live" : Test) assertEq 1 (← depth.get) +/-- +A fragment printed inside a nested result reaches the live output destination exactly once. The +destination is cut off after a few fragments so that a regression fails this test with a short +array instead of flooding it. +-/ +@[test] +def writeOutputDeliversNestedFragmentsOnce : Test := do + let received ← IO.mkRef (#[] : Array String) + let cfg ← mkContext + let ctx := { cfg with + writeOutput := fun o => do + if (← received.get).size < 5 then + match o with + | .stdout s => received.modify (·.push s); IO.print s + | .stderr s => IO.eprint s } + discard <| runEntry ctx <| + TestEntry.of "p" "M" "nested" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } + (result "inner" (IO.println "hi") : Test) + assertEq #["hi\n"] (← received.get) + /-- A live output destination that fails does not fail the test that happened to be printing. It is reported once and then left alone, rather than retried for every fragment. diff --git a/src/errata/Errata/Context.lean b/src/errata/Errata/Context.lean index 454cf1a9..08499a3c 100644 --- a/src/errata/Errata/Context.lean +++ b/src/errata/Errata/Context.lean @@ -20,6 +20,13 @@ open Std (HashMap HashSet) /-- A multi-map from option names to all the values supplied for them. -/ abbrev OptionMap := HashMap String (Array String) +/-- The standard streams from before a test's output was captured. -/ +structure RealStreams where + /-- The stdout from before the capture. -/ + stdout : IO.FS.Stream + /-- The stderr from before the capture. -/ + stderr : IO.FS.Stream + /-- The run-wide configuration and per-test state threaded through every test. -/ structure Context where /-- The reporting verbosity. -/ @@ -61,3 +68,9 @@ structure Context where Whether a write to the output destination has failed. If true, further attempts are suppressed. -/ outputFailed : IO.Ref Bool + /-- + The streams from before the outermost capture, under which the output destination runs. The + outermost capture records them, and a capture nested inside it reuses them, so a {lit}`writeOutput` + handler that prints reaches the runner's own streams from any nesting depth. + -/ + realStreams? : Option RealStreams := none diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 310de83d..174b3b82 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -200,19 +200,22 @@ it is written, so a live runner can stream output while the test runs. def runCapturing (ctx : Context) (act : TestM Unit) : IO (Except IO.Error (Except TestFailure Unit) × OutputLog) := do let log ← IO.mkRef (#[] : Array Output) - -- The destination runs with the streams that were in place before the redirection, so writing to - -- stdout from it reaches the runner instead of re-entering this capture. - let realOut ← IO.getStdout - let realErr ← IO.getStderr + -- The destination runs with the streams from before the outermost capture, so writing to stdout + -- from it reaches the runner instead of re-entering a capture at any level. + let real ← + match ctx.realStreams? with + | some streams => pure streams + | none => do pure { stdout := ← IO.getStdout, stderr := ← IO.getStderr : RealStreams } + let ctx := { ctx with realStreams? := some real } let emit (o : Output) : IO Unit := do log.modify (·.push o) unless ← ctx.outputFailed.get do try - IO.withStdout realOut <| IO.withStderr realErr <| ctx.writeOutput o + IO.withStdout real.stdout <| IO.withStderr real.stderr <| ctx.writeOutput o catch e => ctx.outputFailed.set true -- Saying so can fail in turn, when the destination that just failed was stderr itself. - try realErr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure () + try real.stderr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure () let (outStream, outClose) ← captureStream emit .stdout let (errStream, errClose) ← captureStream emit .stderr -- Closing inside the captured action makes dangling bytes at the end of the test an error of the From 5b4c6112316d410d38346d582524a3d847dcd2c2 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 08:26:59 +0200 Subject: [PATCH 18/32] docstring/comment improvements --- lakefile.lean | 20 +++++++++++++------- src/errata/Errata/Discovery.lean | 6 ++++-- src/errata/Errata/Report.lean | 8 +++++--- src/errata/Errata/TestM.lean | 6 ++++-- 4 files changed, 26 insertions(+), 14 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 2d2d467e..5074b44b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -179,8 +179,10 @@ lean_exe «errata-runner» where 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`). -/ +/-- +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 @@ -206,16 +208,20 @@ private def unreachableModules (lib : Lake.LeanLib) (known : Lean.NameSet) : | 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%`. -/ +/-- +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. -/ +/-- +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 @@ -289,7 +295,7 @@ script run (args) do return 1 pure chosen -- Build every module in the selected libraries; their compiled `.olean` headers are authoritative - -- on which modules carry tests, so no test is dropped by a source-level heuristic. + -- on which modules carry tests. let (modInfos, libMods) ← runBuild do let mut oleanJobs := #[] let mut infos : Array (Lean.Name × System.FilePath) := #[] diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean index abb983f5..c1a89f99 100644 --- a/src/errata/Errata/Discovery.lean +++ b/src/errata/Errata/Discovery.lean @@ -60,9 +60,11 @@ meta initialize testExt : SimplePersistentEnvExtension TestDecl (Array TestDecl) addImportedFn := fun es => es.foldl Array.append #[] } -/-- Records a declaration as a test, capturing the source file that defines it and its docstring. +/-- +Records a declaration as a test, capturing the source file that defines it and its docstring. The docstring is read here, while it is still in the live environment, since a downstream build does -not load the imported docstrings. -/ +not load the imported docstrings. +-/ meta def recordTest (decl : Name) : AttrM Unit := do (checkIsTest decl).run' let docstring? ← findDocString? (← getEnv) decl diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean index 5f924c1c..ca0e1e8d 100644 --- a/src/errata/Errata/Report.lean +++ b/src/errata/Errata/Report.lean @@ -28,9 +28,11 @@ private def indentLines (text : String) : String := private def locationText (l : Location) : String := s!"{l.file}:{l.startPos.line}:{l.startPos.column}" -/-- Prints one result: its status line, its docstring when shown, and for a failure its detail and -captured output. A failure or error shows its docstring; a pass or skip shows it only when the -verbosity does. -/ +/-- +Prints one result: its status line, its docstring when shown, and for a failure its detail and +captured output. A failure or error always shows its docstring; a pass or skip shows it only at a +verbosity that shows all docstrings. +-/ private def printResult (verbosity : Verbosity) (r : Result) : IO Unit := do let name := s!"{r.moduleTarget} {r.testName}" let printDoc : IO Unit := do diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 174b3b82..d2592e5f 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -132,8 +132,10 @@ def writeBinFile (path : System.FilePath) (contents : ByteArray) : IO Unit := do if let some parent := path.parent then IO.FS.createDirAll parent IO.FS.writeBinFile path contents -/-- The number of bytes in the {lit}`UTF-8` sequence a lead byte introduces, or {name}`none` for a -continuation or invalid byte. -/ +/-- +The number of bytes in the {lit}`UTF-8` sequence a lead byte introduces, or {name}`none` for a +continuation or invalid byte. +-/ private def utf8SeqLength (b : UInt8) : Option Nat := if b &&& 0x80 == 0 then some 1 else if b &&& 0xE0 == 0xC0 then some 2 From c0815fd862abdf442bdab4a78d7508f35f21b2d4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 08:36:06 +0200 Subject: [PATCH 19/32] dead code --- src/errata/Errata/Context.lean | 2 -- src/errata/Errata/Runner.lean | 6 +++--- src/tests/TestMain.lean | 2 +- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/errata/Errata/Context.lean b/src/errata/Errata/Context.lean index 08499a3c..bed799c2 100644 --- a/src/errata/Errata/Context.lean +++ b/src/errata/Errata/Context.lean @@ -29,8 +29,6 @@ structure RealStreams where /-- The run-wide configuration and per-test state threaded through every test. -/ structure Context where - /-- The reporting verbosity. -/ - verbosity : Verbosity := .silent /-- Whether golden checks rewrite their expected files instead of comparing. -/ updateGolden : Bool := false /-- Project-specific options, as a multi-map so repeated options accumulate. -/ diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index 1a84db77..cd34192e 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -66,12 +66,12 @@ def run (cfg : Context) (entries : Array TestEntry) : IO (Array Result) := do return all /-- A base context with the given settings and a fresh, empty log. -/ -def mkContext (verbosity : Verbosity := .silent) (updateGolden : Bool := false) +def mkContext (updateGolden : Bool := false) (options : OptionMap := {}) (seed : Option Nat := none) : IO Context := do let log ← IO.mkRef (#[] : Array Result) let usedOptions ← IO.mkRef ({} : Std.HashSet String) let outputFailed ← IO.mkRef false - return { verbosity, updateGolden, options, seed, log, usedOptions, outputFailed } + return { updateGolden, options, seed, log, usedOptions, outputFailed } /-- The settings parsed from the runner's command line. -/ structure Options where @@ -187,7 +187,7 @@ def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do | .error msg => IO.eprintln s!"error: {msg}" return 1 - let cfg ← mkContext (verbosity := opts.verbosity) (updateGolden := opts.updateGolden) + let cfg ← mkContext (updateGolden := opts.updateGolden) (options := opts.options) (seed := opts.seed) let results ← run cfg entries let writeReport (path? : Option String) (render : Array Result → String) : IO Unit := do diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 87aa2b5d..f24dc963 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -360,7 +360,7 @@ def testBuildLog (_ : Config) : IO Unit := do /-- Runs Errata's own tests, reporting them the way the Errata runner does. -/ def testErrata (config : Config) : IO Unit := do let verbosity := if config.verbose then Errata.Verbosity.quiet else .silent - let cfg ← Errata.mkContext (verbosity := verbosity) (updateGolden := config.updateExpected) + let cfg ← Errata.mkContext (updateGolden := config.updateExpected) let results ← Errata.run cfg errataTests let failures ← Errata.humanReport verbosity results unless failures == 0 do From 5e708c9bc794d02877aaf7643dc1f672e9e6a9e3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 08:41:25 +0200 Subject: [PATCH 20/32] dead code --- src/errata-tests/ErrataTests.lean | 6 +----- src/errata/Errata/Result.lean | 6 ------ 2 files changed, 1 insertion(+), 11 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 438d3a58..e39165ae 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -326,7 +326,7 @@ def positionConvention : Test := do assertEq 2 indentedHere.startPos.column assertEq 5 (indentedHere.endPos.column - indentedHere.startPos.column) -/-- The `Verbosity` predicates and accumulation behave as the report relies on. -/ +/-- The `Verbosity` predicates behave as the report relies on. -/ @[test] def verbosityLevels : Test := do assertEq false Verbosity.silent.showsPasses @@ -339,10 +339,6 @@ def verbosityLevels : Test := do assertEq false Verbosity.superVerbose.truncates assertEq false Verbosity.verbose.showsAllDocstrings assertEq true Verbosity.superVerbose.showsAllDocstrings - assertEq Verbosity.quiet Verbosity.silent.increase - assertEq Verbosity.verbose Verbosity.quiet.increase - assertEq Verbosity.superVerbose Verbosity.verbose.increase - assertEq Verbosity.superVerbose Verbosity.superVerbose.increase /-- The runner's command line: the `-v` forms select the verbosity, declared flags parse, and options diff --git a/src/errata/Errata/Result.lean b/src/errata/Errata/Result.lean index d3b39bc7..ec506bdd 100644 --- a/src/errata/Errata/Result.lean +++ b/src/errata/Errata/Result.lean @@ -39,12 +39,6 @@ def Verbosity.showsAllDocstrings : Verbosity → Bool | .superVerbose => true | .silent | .quiet | .verbose => false -/-- The next verbosity up, for an accumulating {lit}`-v` / {lit}`-vv` / {lit}`-vvv`. -/ -def Verbosity.increase : Verbosity → Verbosity - | .silent => .quiet - | .quiet => .verbose - | .verbose | .superVerbose => .superVerbose - /-- A line and column within a source file, following Lean's own source positions. -/ structure Position where /-- The line, counting from one. -/ From c0674a0a064c43761158177a8d282418c9484b66 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 09:57:12 +0200 Subject: [PATCH 21/32] duplicate/redundancy --- src/errata-tests/ErrataTests.lean | 2 +- src/errata/Errata/Discovery.lean | 4 ++-- src/errata/Errata/Golden.lean | 9 +++------ src/errata/Errata/Here.lean | 4 ++-- src/errata/Errata/Report.lean | 6 +----- src/errata/Errata/Result.lean | 18 +++++++---------- src/errata/Errata/TestM.lean | 32 ++++--------------------------- 7 files changed, 20 insertions(+), 55 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index e39165ae..379826b6 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -72,7 +72,7 @@ def addComm : Test := open Lean (toJson fromJson?) -deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Position +deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Lean.Position deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Location deriving instance Plausible.Shrinkable, Plausible.Arbitrary for TestFailure deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Status diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean index c1a89f99..d42a5793 100644 --- a/src/errata/Errata/Discovery.lean +++ b/src/errata/Errata/Discovery.lean @@ -132,7 +132,7 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do entries := entries.push <| ← `(Errata.TestEntry.of $(quote package) $(quote moduleStr) $(quote testName) (Errata.Location.mk $(quote test.file) - (Errata.Position.mk $(quote pos.line) $(quote pos.column)) - (Errata.Position.mk $(quote endPos.line) $(quote endPos.column))) + (Lean.Position.mk $(quote pos.line) $(quote pos.column)) + (Lean.Position.mk $(quote endPos.line) $(quote endPos.column))) (@$(mkCIdent test.name)) (docstring? := $docStx)) elabTerm (← `(#[$entries,*])) expectedType? diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean index e3cea3aa..0e24e53d 100644 --- a/src/errata/Errata/Golden.lean +++ b/src/errata/Errata/Golden.lean @@ -38,13 +38,10 @@ def goldenFile (expected : System.FilePath) (actual : String) (detail? := some "Run with --update-golden to create it.") /-- All files below a directory, recursively, in a deterministic order. -/ -partial def filesUnder (dir : System.FilePath) : IO (Array System.FilePath) := do +def filesUnder (dir : System.FilePath) : IO (Array System.FilePath) := do let mut out : Array System.FilePath := #[] - for entry in ← dir.readDir do - if ← entry.path.isDir then - out := out ++ (← filesUnder entry.path) - else - out := out.push entry.path + for entry in ← dir.walkDir do + unless ← entry.isDir do out := out.push entry return out.qsort (·.toString < ·.toString) /-- The path of a file relative to a base directory. -/ diff --git a/src/errata/Errata/Here.lean b/src/errata/Errata/Here.lean index 5486a74b..ae1ba60c 100644 --- a/src/errata/Errata/Here.lean +++ b/src/errata/Errata/Here.lean @@ -28,5 +28,5 @@ meta def elabHere : TermElab := fun _stx _expectedType? => do let endPos := fileMap.toPosition (ref.getTailPos?.getD (ref.getPos?.getD 0)) let file ← getFileName elabTerm (← `(Errata.Location.mk $(quote file) - (Errata.Position.mk $(quote startPos.line) $(quote startPos.column)) - (Errata.Position.mk $(quote endPos.line) $(quote endPos.column)))) none + (Lean.Position.mk $(quote startPos.line) $(quote startPos.column)) + (Lean.Position.mk $(quote endPos.line) $(quote endPos.column)))) none diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean index ca0e1e8d..e53db16a 100644 --- a/src/errata/Errata/Report.lean +++ b/src/errata/Errata/Report.lean @@ -17,10 +17,6 @@ set_option doc.verso true namespace Errata -/-- The number of results that did not pass. -/ -def failureCount (results : Array Result) : Nat := - results.foldl (fun n r => if r.status.isSuccess then n else n + 1) 0 - private def indentLines (text : String) : String := "\n".intercalate ((text.splitOn "\n").map (fun l => " " ++ l)) @@ -182,7 +178,7 @@ private def caseOf (r : Result) : String := r.testName private def countWhere (results : Array Result) (p : Status → Bool) : Nat := - results.foldl (fun n r => if p r.status then n + 1 else n) 0 + results.countP (p ·.status) /-- Groups results by their package-qualified module in a single pass, keeping first-seen order. -/ private def byModule (results : Array Result) : Array (String × Array Result) := Id.run do diff --git a/src/errata/Errata/Result.lean b/src/errata/Errata/Result.lean index ec506bdd..dee7e100 100644 --- a/src/errata/Errata/Result.lean +++ b/src/errata/Errata/Result.lean @@ -5,6 +5,8 @@ Author: David Thrane Christiansen -/ module +public import Lean.Data.Position + public section set_option linter.missingDocs true @@ -39,22 +41,16 @@ def Verbosity.showsAllDocstrings : Verbosity → Bool | .superVerbose => true | .silent | .quiet | .verbose => false -/-- A line and column within a source file, following Lean's own source positions. -/ -structure Position where - /-- The line, counting from one. -/ - line : Nat - /-- The column, counting from zero. -/ - column : Nat -deriving Repr, Inhabited, BEq, DecidableEq - -/-- A source span, used in failure messages and editor integration. -/ +/-- +A source span, used in failure messages and editor integration. +-/ structure Location where /-- The source file that contains the span. -/ file : String /-- The start of the span. -/ - startPos : Position + startPos : Lean.Position /-- The end of the span. -/ - endPos : Position + endPos : Lean.Position deriving Repr, Inhabited, BEq, DecidableEq /-- A test failure, carrying the information needed to explain it. -/ diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index d2592e5f..270c2fdf 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -56,14 +56,6 @@ instance : Alternative TestM where failure := failHere "failure" orElse x y := tryCatch x fun _ => y () -/-- -Runs an action with the current failure location set to a call site, which defaults to the caller. -A user-defined assertion helper can wrap its checks in this so their failures report at the helper's -call site rather than inside the helper. --/ -def withLocation (loc : Location := by exact here%) (act : TestM α) : TestM α := - withReader ({ · with location := loc }) act - /-- All values supplied for a project option, in order; records that the option was read. -/ def optionValues (name : String) : TestM (Array String) := do let ctx ← read @@ -86,22 +78,6 @@ def Context.mkResult (ctx : Context) (status : Status) (durationMs : Nat := 0) : resultPath := ctx.resultPath, status, durationMs, description? := ctx.description? } -/-- A passing result for the current scope. -/ -def Context.pass (ctx : Context) (durationMs : Nat := 0) : Result := - ctx.mkResult .pass durationMs - -/-- A failed result for the current scope. -/ -def Context.fail (ctx : Context) (failure : TestFailure) (durationMs : Nat := 0) : Result := - ctx.mkResult (.fail failure) durationMs - -/-- A result for the current scope that raised an error. -/ -def Context.error (ctx : Context) (message : String) (durationMs : Nat := 0) : Result := - ctx.mkResult (.error message) durationMs - -/-- A skipped result for the current scope. -/ -def Context.skip (ctx : Context) (reason : String) (durationMs : Nat := 0) : Result := - ctx.mkResult (.skip reason) durationMs - /-- The result a captured run contributes beyond any nested results it recorded. @@ -113,14 +89,14 @@ def Context.resultOfOutcome (ctx : Context) (outcome : Except IO.Error (Except TestFailure Unit)) (output : OutputLog) (durationMs : Nat) (hasNested : Bool) : Option Result := match outcome with - | .error e => some { ctx.error (toString e) durationMs with output } - | .ok (.error f) => some { ctx.fail f durationMs with output } - | .ok (.ok ()) => if hasNested then none else some { ctx.pass durationMs with output } + | .error e => some { ctx.mkResult (.error (toString e)) durationMs with output } + | .ok (.error f) => some { ctx.mkResult (.fail f) durationMs with output } + | .ok (.ok ()) => if hasNested then none else some { ctx.mkResult .pass durationMs with output } /-- Records a skipped result for the current scope. -/ def skip (reason : String) : TestM Unit := do let ctx ← read - ctx.log.modify (·.push (ctx.skip reason)) + ctx.log.modify (·.push (ctx.mkResult (.skip reason))) /-- Writes a file, creating all parent directories if necessary. -/ def writeFile (path : System.FilePath) (contents : String) : IO Unit := do From 224459b1aefaf3cd2781a3be4ffc2338f303b049 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 10:57:31 +0200 Subject: [PATCH 22/32] docstring clarification --- src/errata/Errata/TestM.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 270c2fdf..42a4edc3 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -174,6 +174,8 @@ Runs a test action with the given context, capturing its outcome as data rather propagate. The action's stdout and stderr are recorded as text, in order and tagged by stream, and returned alongside the outcome. Each fragment is also handed to the context's output destination as it is written, so a live runner can stream output while the test runs. + +Output from tasks or subprocesses spawned by the test is not captured. -/ def runCapturing (ctx : Context) (act : TestM Unit) : IO (Except IO.Error (Except TestFailure Unit) × OutputLog) := do From 86ca3e8c95cfe0e5d20ae49c0797f5985f1f1e99 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 11:01:41 +0200 Subject: [PATCH 23/32] output writer as option --- src/errata-tests/ErrataTests.lean | 6 +++--- src/errata/Errata/Context.lean | 6 +++--- src/errata/Errata/TestM.lean | 15 ++++++++------- 3 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 379826b6..c0aa0cda 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -220,7 +220,7 @@ def writeOutputDoesNotRecurse : Test := do let depth ← IO.mkRef 0 let cfg ← mkContext let ctx := { cfg with - writeOutput := fun o => do + writeOutput := some fun o => do depth.modify (· + 1) if (← depth.get) < 5 then match o with @@ -241,7 +241,7 @@ def writeOutputDeliversNestedFragmentsOnce : Test := do let received ← IO.mkRef (#[] : Array String) let cfg ← mkContext let ctx := { cfg with - writeOutput := fun o => do + writeOutput := some fun o => do if (← received.get).size < 5 then match o with | .stdout s => received.modify (·.push s); IO.print s @@ -261,7 +261,7 @@ def writeOutputFailureIsContained : Test := do let statuses ← IO.mkRef (#[] : Array Status) let cfg ← mkContext let ctx := { cfg with - writeOutput := fun _ => do + writeOutput := some fun _ => do calls.modify (· + 1) throw (.userError "broken pipe") } let out ← captureOutput do diff --git a/src/errata/Errata/Context.lean b/src/errata/Errata/Context.lean index bed799c2..155ae9ab 100644 --- a/src/errata/Errata/Context.lean +++ b/src/errata/Errata/Context.lean @@ -55,13 +55,13 @@ structure Context where /-- The option names read during the run, shared across all tests, for reporting unused options. -/ usedOptions : IO.Ref (HashSet String) /-- - Receives each captured output fragment as it is written, in order. The default discards them; a - live runner sets it to stream output as the test produces it. + Receives each captured output fragment as it is written, in order. A live runner sets it to + stream output as the test produces it, and it is {lean}`none` when no runner is listening. It runs with the streams that were in place before the test's output was redirected, so it may print in case of internal errors. -/ - writeOutput : Output → IO Unit := fun _ => pure () + writeOutput : Option (Output → IO Unit) := none /-- Whether a write to the output destination has failed. If true, further attempts are suppressed. -/ diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 42a4edc3..776f74b2 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -189,13 +189,14 @@ def runCapturing (ctx : Context) (act : TestM Unit) : let ctx := { ctx with realStreams? := some real } let emit (o : Output) : IO Unit := do log.modify (·.push o) - unless ← ctx.outputFailed.get do - try - IO.withStdout real.stdout <| IO.withStderr real.stderr <| ctx.writeOutput o - catch e => - ctx.outputFailed.set true - -- Saying so can fail in turn, when the destination that just failed was stderr itself. - try real.stderr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure () + if let some dest := ctx.writeOutput then + unless ← ctx.outputFailed.get do + try + IO.withStdout real.stdout <| IO.withStderr real.stderr <| dest o + catch e => + ctx.outputFailed.set true + -- Saying so can fail in turn, when the destination that just failed was stderr itself. + try real.stderr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure () let (outStream, outClose) ← captureStream emit .stdout let (errStream, errClose) ← captureStream emit .stderr -- Closing inside the captured action makes dangling bytes at the end of the test an error of the From 2c40eb7924d564dd3256e1ce0e6beb61b7552a11 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 11:29:50 +0200 Subject: [PATCH 24/32] single def for errata runner dir --- lakefile.lean | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 5074b44b..6e96f64a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -160,22 +160,26 @@ 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 := ".lake/errata-runner/selection" + path := errataRunnerDir / "selection" -- The generated discovered-tests module (`allTests`), written by the Errata driver. lean_lib ErrataGenerated where - srcDir := ".lake/errata-runner" + 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 := ".lake/errata-runner" + srcDir := errataRunnerDir supportInterpreter := true needs := #[errataSelection] @@ -267,8 +271,9 @@ script run (args) do return 1 -- 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. The generated runner lib has no source until this script writes it, and no tests. - let candidates := ws.root.leanLibs.filter (·.name != `ErrataGenerated) + -- 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 @@ -337,7 +342,7 @@ script run (args) do IO.eprintln s!" {lib.name}: {mod}" -- 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 / ".lake" / "errata-runner" + let dir := ws.root.dir / errataRunnerDir IO.FS.createDirAll dir let selection := "\n".intercalate ((moduleMods ++ nonModuleMods).map (·.toString) |>.qsort (· < ·)).toList for (name, src) in From cf95fd9937125aab385d344780d2943ae3f1442b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:39:46 +0200 Subject: [PATCH 25/32] fix: deduplicate tests when roots are nested --- src/errata-tests/ErrataTests.lean | 9 +++++++++ src/errata-tests/ErrataTests/Fixture.lean | 17 +++++++++++++++++ src/errata-tests/ErrataTests/Fixture/Sub.lean | 17 +++++++++++++++++ src/errata/Errata/Discovery.lean | 10 ++++++++-- 4 files changed, 51 insertions(+), 2 deletions(-) create mode 100644 src/errata-tests/ErrataTests/Fixture.lean create mode 100644 src/errata-tests/ErrataTests/Fixture/Sub.lean diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index c0aa0cda..485412f4 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -9,6 +9,8 @@ module public import Errata public meta import Errata +import all ErrataTests.Fixture +import all ErrataTests.Fixture.Sub open Errata @@ -65,6 +67,13 @@ error: Module `NoSuchModule` is not imported, so its tests cannot be reached. Im #test_msgs in example : Array TestEntry := getAllTests% "verso" NoSuchModule +/-- A module below several named roots contributes its tests once. -/ +@[test] +def discoveryDeduplicates : Test := do + -- `ErrataTests.Fixture.Sub` lies below both roots, so exactly the two fixture tests are found. + let entries := (getAllTests% "verso" ErrataTests.Fixture ErrataTests.Fixture.Sub) + assertEq 2 entries.size + /-- A property test. -/ @[test] def addComm : Test := diff --git a/src/errata-tests/ErrataTests/Fixture.lean b/src/errata-tests/ErrataTests/Fixture.lean new file mode 100644 index 00000000..13e2317c --- /dev/null +++ b/src/errata-tests/ErrataTests/Fixture.lean @@ -0,0 +1,17 @@ +/- +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 + +A module holding a test, for checks of test discovery itself. Its name is a prefix of +`ErrataTests.Fixture.Sub`'s name. +-/ +module + +public import Errata + +open Errata + +/-- A test in the fixture module. -/ +@[test] +def fixtureTest : Bool := true diff --git a/src/errata-tests/ErrataTests/Fixture/Sub.lean b/src/errata-tests/ErrataTests/Fixture/Sub.lean new file mode 100644 index 00000000..9e62f275 --- /dev/null +++ b/src/errata-tests/ErrataTests/Fixture/Sub.lean @@ -0,0 +1,17 @@ +/- +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 + +A module holding a test, for checks of test discovery itself. Its name extends +`ErrataTests.Fixture`'s name, so it lies below that module as well as below itself. +-/ +module + +public import Errata + +open Errata + +/-- A test in the nested fixture module. -/ +@[test] +def subFixtureTest : Bool := true diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean index d42a5793..0ef020b6 100644 --- a/src/errata/Errata/Discovery.lean +++ b/src/errata/Errata/Discovery.lean @@ -94,8 +94,9 @@ meta def testNameBelow (moduleName declName : Name) : String := /-- {lit}`getAllTests% "package" Mod.A Mod.B ...` reads the tests recorded by {lit}`@[test]` in the named modules and every imported module below them, and expands to the array of {name}`TestEntry` -values that run them. Each module must be imported, with {lit}`import all` for module-system -modules, so its tests are reachable. +values that run them. A module that lies below more than one of the named modules contributes its +tests once. Each module must be imported, with {lit}`import all` for module-system modules, so its +tests are reachable. -/ syntax (name := getAllTests) "getAllTests%" str ident* : term @@ -108,6 +109,9 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do let env ← getEnv let moduleNames := env.allImportedModuleNames let mut entries : Array Term := #[] + -- One root's name may extend another's, putting a module below both; each module's tests are + -- gathered once. + let mut seen : NameSet := {} for modStx in mods do let rootName := modStx.getId unless (env.getModuleIdx? rootName).isSome do @@ -116,6 +120,8 @@ meta def elabGetAllTests : TermElab := fun stx expectedType? => do for h : idx in [0 : moduleNames.size] do let moduleName := moduleNames[idx] unless rootName.isPrefixOf moduleName do continue + if seen.contains moduleName then continue + seen := seen.insert moduleName let moduleStr := moduleName.toString for test in testExt.getModuleEntries env idx do -- The internal name is used here, because the user-facing name can be ambiguous for private From cf02476e8d654dc563a77af2669dccddd74ac236 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:40:56 +0200 Subject: [PATCH 26/32] fix: update golden trees across file/directory shape changes The update path replaces the recorded tree wholesale, so a path that changed shape between file and directory no longer makes the update run throw an IO error. --- src/errata-tests/ErrataTests.lean | 22 ++++++++++++++++++++++ src/errata/Errata/Golden.lean | 17 +++++++---------- 2 files changed, 29 insertions(+), 10 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 485412f4..13ccddd1 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -139,6 +139,28 @@ def goldenDirHandlesEmptyOutput : Test := do assertEq 1 results.size assertTrue results[0]!.status.isSuccess +/-- Updating absorbs a path that changed shape between file and directory, in both directions. -/ +@[test] +def goldenDirUpdatesAcrossShapeChanges : Test := do + let results ← IO.FS.withTempDir fun dir => do + let expected := dir / "expected" + let actual := dir / "actual" + IO.FS.createDirAll expected + IO.FS.writeFile (expected / "d") "was a file\n" + IO.FS.createDirAll (actual / "d") + IO.FS.writeFile (actual / "d" / "inner") "now a directory\n" + resultsOf do + -- First update: the golden file `d` becomes a directory holding `inner`. + withReader ({ · with updateGolden := true }) (goldenDir expected actual) + goldenDir expected actual + -- Second update, the other way: the produced `d` is a file again. + IO.FS.removeDirAll (actual / "d") + IO.FS.writeFile (actual / "d") "a file once more\n" + withReader ({ · with updateGolden := true }) (goldenDir expected actual) + goldenDir expected actual + assertEq 1 results.size + assertTrue results[0]!.status.isSuccess + /-- A file where a directory was expected is a golden failure, not a raw error. -/ @[test] def goldenDirRejectsNonDirectory : Test := do diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean index 0e24e53d..69e86cb9 100644 --- a/src/errata/Errata/Golden.lean +++ b/src/errata/Errata/Golden.lean @@ -72,18 +72,15 @@ def goldenDir (expected actual : System.FilePath) (detail? := some "The code under test did not create it as a directory.") let actualFiles ← filesUnder actual if ctx.updateGolden then - -- The golden tree is recorded even when the produced tree holds no files, so that a later run - -- compares against it rather than reporting it as missing. + -- The recorded tree is replaced wholesale, so a path that changed shape between file and + -- directory updates as cleanly as changed content. The golden tree is recorded even when the + -- produced tree holds no files, so that a later run compares against it rather than reporting + -- it as missing. + if ← expected.isDir then IO.FS.removeDirAll expected + else if ← expected.pathExists then IO.FS.removeFile expected IO.FS.createDirAll expected - let actualRels := actualFiles.map (relativeTo actual) for file in actualFiles do - let dest := expected / relativeTo actual file - writeBinFile dest (← IO.FS.readBinFile file) - -- Remove expected files that the produced output no longer contains. - if ← expected.pathExists then - for file in ← filesUnder expected do - unless actualRels.contains (relativeTo expected file) do - IO.FS.removeFile file + writeBinFile (expected / relativeTo actual file) (← IO.FS.readBinFile file) return unless ← expected.pathExists do failAt loc s!"missing golden directory {expected}" From e1c978cbd1bfaec6bf963b8b9edc17097c1b0b8d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:41:51 +0200 Subject: [PATCH 27/32] fix: keep a test's own failure when capture close errors Dangling bytes at the end of a failing test no longer replace the message with one about byte encodings. --- src/errata-tests/ErrataTests.lean | 12 ++++++++++++ src/errata/Errata/TestM.lean | 11 ++++++++--- 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 13ccddd1..664c17fc 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -233,6 +233,18 @@ def captureRejectsDanglingBytes : Test := do assertEq 1 results.size assertTrue (results[0]!.status matches .error _) +/-- Dangling bytes at the end of a failing test do not displace the test's own failure. -/ +@[test] +def danglingBytesKeepFailure : Test := do + let results ← resultsOf do + let out ← IO.getStdout + out.write ("é".toUTF8.extract 0 1) + fail "the real failure" + assertEq 1 results.size + match results[0]!.status with + | .fail f => assertEq "the real failure" f.message + | s => fail s!"expected the assertion failure, got {repr s}" + /-- A raw write with no valid decoding is rejected at the write itself. -/ @[test] def captureRejectsInvalidBytes : Test := do diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index 776f74b2..e5aebc46 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -200,11 +200,16 @@ def runCapturing (ctx : Context) (act : TestM Unit) : let (outStream, outClose) ← captureStream emit .stdout let (errStream, errClose) ← captureStream emit .stderr -- Closing inside the captured action makes dangling bytes at the end of the test an error of the - -- test itself. + -- test itself. When the test already failed, that failure is the report's verdict, and a + -- dangling-byte error at close does not displace it. let body : IO (Except TestFailure Unit) := do let r ← (act ctx).run - outClose - errClose + match r with + | .ok () => + outClose + errClose + | .error _ => + try outClose; errClose catch _ => pure () return r let outcome ← IO.withStdout outStream <| IO.withStderr errStream <| body.toBaseIO return (outcome, { log := ← log.get }) From 1aa39a85a45e286457283c8153d7da95442dc3ca Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:42:57 +0200 Subject: [PATCH 28/32] fix: record mixed putStr and raw writes in production order Text writes go through the same pending-byte pathway as raw writes, so a print no longer overtakes an earlier raw write that is waiting for the rest of its code point. --- src/errata-tests/ErrataTests.lean | 20 ++++++++++++++++++++ src/errata/Errata/TestM.lean | 26 ++++++++++++++++---------- 2 files changed, 36 insertions(+), 10 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 664c17fc..b4afcacb 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -233,6 +233,26 @@ def captureRejectsDanglingBytes : Test := do assertEq 1 results.size assertTrue (results[0]!.status matches .error _) +/-- Output mixed from raw writes and prints is recorded in the order it was produced. -/ +@[test] +def captureOrdersMixedWrites : Test := do + let captured ← captureOutput do + let out ← IO.getStdout + out.write "é".toUTF8 + IO.print "x" + out.write "û".toUTF8 + assertEq "éxû" captured.stdout + +/-- Text printed while a raw code point is unfinished is malformed output, not reordered output. -/ +@[test] +def capturePrintDuringPartialWriteRejected : Test := do + let results ← resultsOf do + let out ← IO.getStdout + out.write ("é".toUTF8.extract 0 1) + IO.print "x" + assertEq 1 results.size + assertTrue (results[0]!.status matches .error _) + /-- Dangling bytes at the end of a failing test do not displace the test's own failure. -/ @[test] def danglingBytesKeepFailure : Test := do diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean index e5aebc46..8c51f4dd 100644 --- a/src/errata/Errata/TestM.lean +++ b/src/errata/Errata/TestM.lean @@ -147,20 +147,26 @@ private def captureStream (emit : Output → IO Unit) (mk : String → Output) : let pending ← IO.mkRef ByteArray.empty let invalid : IO.Error := .userError "a raw byte write to a captured stream was not valid UTF-8" + let write (bytes : ByteArray) : IO Unit := do + let (ready, rest) := splitUtf8Tail ((← pending.get) ++ bytes) + match String.fromUTF8? ready with + | some s => + pending.set rest + unless s.isEmpty do emit (mk s) + | none => + pending.set .empty + throw invalid let stream : IO.FS.Stream := { + -- A flush partway through a code point is not an error: the partial sequence stays buffered + -- for the write that completes it. flush := pure () read := fun _ => pure .empty - write := fun bytes => do - let (ready, rest) := splitUtf8Tail ((← pending.get) ++ bytes) - match String.fromUTF8? ready with - | some s => - pending.set rest - unless s.isEmpty do emit (mk s) - | none => - pending.set .empty - throw invalid + write getLine := pure "" - putStr := fun s => emit (mk s) + -- Text goes through the byte pathway, so output mixed from `putStr` and raw writes is + -- recorded in the order it was produced, and text interrupting an unfinished code point is + -- reported as the malformed stream it is. + putStr := fun s => write s.toUTF8 isTty := pure false } let close : IO Unit := do From d31fac0aca58d7940a9e3631a13fa673c072e68b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:43:52 +0200 Subject: [PATCH 29/32] feat: detail param on assertTrue and an assertThrowsIO assertion assertTrue now takes an optional detail like the other assertions, so predicate checks can attach the value that failed them. assertThrowsIO expects an action to throw an IO.Error, with a predicate picking the subset of acceptable errors. --- src/errata-tests/ErrataTests.lean | 23 +++++++++++++++++++++++ src/errata/Errata/Assertions.lean | 20 +++++++++++++++++--- 2 files changed, 40 insertions(+), 3 deletions(-) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index b4afcacb..85112bfd 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -233,6 +233,29 @@ def captureRejectsDanglingBytes : Test := do assertEq 1 results.size assertTrue (results[0]!.status matches .error _) +/-- The detail given to a true-assertion is attached to its failure. -/ +@[test] +def assertTrueAttachesDetail : Test := do + let results ← resultsOf (assertTrue false "boom" (detail? := some "why")) + assertEq 1 results.size + match results[0]!.status with + | .fail f => assertEq (some "why") f.detail? + | s => fail s!"expected a failure, got {repr s}" + +/-- An expected IO error passes, and the predicate picks which errors are acceptable. -/ +@[test] +def assertThrowsIOAccepts : Test := do + assertThrowsIO (throw (IO.userError "nope") : IO Unit) + assertThrowsIO (throw (IO.userError "nope") : IO Unit) + (acceptable := fun e => e matches .userError _) + +/-- A successful action fails the throw assertion, as does an error the predicate rejects. -/ +@[test] +def assertThrowsIORejects : Test := do + expectFail (assertThrowsIO (pure () : IO Unit)) + expectFail <| + assertThrowsIO (throw (IO.userError "nope") : IO Unit) (acceptable := fun _ => false) + /-- Output mixed from raw writes and prints is recorded in the order it was produced. -/ @[test] def captureOrdersMixedWrites : Test := do diff --git a/src/errata/Errata/Assertions.lean b/src/errata/Errata/Assertions.lean index ac51b72d..91c11b7c 100644 --- a/src/errata/Errata/Assertions.lean +++ b/src/errata/Errata/Assertions.lean @@ -15,10 +15,10 @@ set_option doc.verso true namespace Errata -/-- Asserts that a condition holds. -/ +/-- Asserts that a condition holds, attaching the detail to the failure when given. -/ def assertTrue (cond : Bool) (message : String := "assertion failed") - (loc : Location := by exact here%) : TestM Unit := - unless cond do failAt loc message + (detail? : Option String := none) (loc : Location := by exact here%) : TestM Unit := + unless cond do failAt loc message (detail? := detail?) /-- Asserts that the actual value equals the expected value, reporting both when they differ. -/ def assertEq {α} [BEq α] [Repr α] (expected actual : α) @@ -44,6 +44,20 @@ def assertNotContains (unexpected actual : String) (message : String := "unexpec unless (actual.find? unexpected).isNone do failAt loc message (detail? := some s!"expected not to contain: {unexpected}\nactual: {actual}") +/-- +Asserts that an action throws an {name}`IO.Error`. The predicate picks the subset of acceptable +errors: the assertion fails when the action succeeds, and when it throws an error the predicate +rejects. The name says {lit}`IO` because the expectation is about a thrown {name}`IO.Error`, as +opposed to failure in some other error monad. +-/ +def assertThrowsIO {α} (act : IO α) (acceptable : IO.Error → Bool := fun _ => true) + (loc : Location := by exact here%) : TestM Unit := do + match ← act.toBaseIO with + | .ok _ => failAt loc "expected an IO error, but the action succeeded" + | .error e => + unless acceptable e do + failAt loc "the action threw an unacceptable IO error" (detail? := some (toString e)) + /-- Asserts that a file exists. -/ def assertFileExists (path : System.FilePath) (loc : Location := by exact here%) : TestM Unit := do From 5a0fa94c5f044d146c55ed0e1a06e82033010d03 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:52:40 +0200 Subject: [PATCH 30/32] feat: a --wfail runner flag that fails the run on warnings This allows warnings such as "unused parameter" to fail in CI. --- doc/UsersGuide/Releases/Entries/TestFramework.lean | 2 +- lakefile.lean | 10 +++++++--- src/errata-tests/ErrataTests.lean | 13 +++++++++++++ src/errata/Errata/Runner.lean | 12 ++++++++++-- 4 files changed, 31 insertions(+), 6 deletions(-) diff --git a/doc/UsersGuide/Releases/Entries/TestFramework.lean b/doc/UsersGuide/Releases/Entries/TestFramework.lean index af731496..23b46293 100644 --- a/doc/UsersGuide/Releases/Entries/TestFramework.lean +++ b/doc/UsersGuide/Releases/Entries/TestFramework.lean @@ -26,6 +26,6 @@ In particular, there were no universal conventions about output or failure repor 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, and write JUnit XML, JSON, and Markdown reports. +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. diff --git a/lakefile.lean b/lakefile.lean index 6e96f64a..fe3d377d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -269,6 +269,8 @@ script run (args) do 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 @@ -334,12 +336,14 @@ script run (args) do let missed ← unreachableModules lib known unless missed.isEmpty do unreachable := unreachable.push (lib, missed) unless unreachable.isEmpty do - IO.eprintln "warning: 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]`):" + 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 diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 85112bfd..1a11ce2e 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -233,6 +233,19 @@ def captureRejectsDanglingBytes : Test := do assertEq 1 results.size assertTrue (results[0]!.status matches .error _) +/-- Under --wfail, an option no test read fails the run instead of only warning. -/ +@[test] +def wfailPromotesUnusedOptions : Test := do + let entry := TestEntry.of "p" "M" "t" + { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } (pure () : Test) + let lax ← IO.mkRef (0 : UInt32) + let wfail ← IO.mkRef (0 : UInt32) + discard <| captureOutput do + lax.set (← runMain #[entry] ["--", "--bogus=1"]) + wfail.set (← runMain #[entry] ["--wfail", "--", "--bogus=1"]) + assertEq 0 (← lax.get) + assertEq 1 (← wfail.get) + /-- The detail given to a true-assertion is attached to its failure. -/ @[test] def assertTrueAttachesDetail : Test := do diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index cd34192e..4bce4087 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -87,6 +87,8 @@ structure Options where jsonPath : Option String := none /-- Writes a Markdown report to this path. -/ markdownPath : Option String := none + /-- Fails the run if warnings are logged, as Lake's `--wfail` does for builds. -/ + wfail : Bool := false /-- Project-specific options, as a multi-map so repeated options accumulate. -/ options : OptionMap := {} @@ -106,6 +108,7 @@ def runnerCmd (handler : Cli.Parsed → IO UInt32) : Cli.Cmd := junit : String; "Write a JUnit XML report to the given path." json : String; "Write a JSON report to the given path." markdown : String; "Write a Markdown report (for a CI job summary) to the given path." + wfail; "Fail the run if warnings are logged." ARGS: ...testOption : String; "Options for the tests themselves; see below." @@ -166,6 +169,7 @@ def optionsOfParsed (p : Cli.Parsed) : Except String Options := do junitPath := ← pathFlag p "junit", jsonPath := ← pathFlag p "json", markdownPath := ← pathFlag p "markdown", + wfail := p.hasFlag "wfail", options := ← projectOptions (p.variableArgsAs! String).toList } @@ -201,11 +205,15 @@ def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do IO.eprintln "error: no tests were discovered" return 1 -- Warn about options that were supplied but never read by any test (typos, removed flags). + -- Under `--wfail`, the warning is an error and fails the run. let used ← cfg.usedOptions.get let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k unless unused.isEmpty do - IO.eprintln s!"warning: option(s) provided but never read: {", ".intercalate unused}" + let level := if opts.wfail then "error" else "warning" + IO.eprintln s!"{level}: option(s) provided but never read: {", ".intercalate unused}" -- A process exit status keeps only its low 8 bits, so report a failing run as 1 rather than the -- count, which a multiple of 256 would otherwise wrap to 0. - return if failures == 0 then 0 else 1 + if failures != 0 then return 1 + if opts.wfail && !unused.isEmpty then return 1 + return 0 cmd.validate args From 9e363ec099622b52578cd830af83964bd695a646 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 26 Aug 2026 17:04:03 +0200 Subject: [PATCH 31/32] style: keep the file header comment to the copyright notice Explanatory text moves to a comment of its own below the header. --- src/errata-tests/ErrataTests.lean | 2 ++ src/errata-tests/ErrataTests/Fixture.lean | 2 ++ src/errata-tests/ErrataTests/Fixture/Sub.lean | 2 ++ src/errata/Errata/CompileTime/Helpers.lean | 2 ++ 4 files changed, 8 insertions(+) diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean index 1a11ce2e..d5fce3a9 100644 --- a/src/errata-tests/ErrataTests.lean +++ b/src/errata-tests/ErrataTests.lean @@ -2,7 +2,9 @@ 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 +-/ +/- Tests that exercise Errata using Errata itself. -/ module diff --git a/src/errata-tests/ErrataTests/Fixture.lean b/src/errata-tests/ErrataTests/Fixture.lean index 13e2317c..a41e5e70 100644 --- a/src/errata-tests/ErrataTests/Fixture.lean +++ b/src/errata-tests/ErrataTests/Fixture.lean @@ -2,7 +2,9 @@ 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 +-/ +/- A module holding a test, for checks of test discovery itself. Its name is a prefix of `ErrataTests.Fixture.Sub`'s name. -/ diff --git a/src/errata-tests/ErrataTests/Fixture/Sub.lean b/src/errata-tests/ErrataTests/Fixture/Sub.lean index 9e62f275..98f7cae2 100644 --- a/src/errata-tests/ErrataTests/Fixture/Sub.lean +++ b/src/errata-tests/ErrataTests/Fixture/Sub.lean @@ -2,7 +2,9 @@ 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 +-/ +/- A module holding a test, for checks of test discovery itself. Its name extends `ErrataTests.Fixture`'s name, so it lies below that module as well as below itself. -/ diff --git a/src/errata/Errata/CompileTime/Helpers.lean b/src/errata/Errata/CompileTime/Helpers.lean index 50f58f87..68ae1532 100644 --- a/src/errata/Errata/CompileTime/Helpers.lean +++ b/src/errata/Errata/CompileTime/Helpers.lean @@ -2,7 +2,9 @@ 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 +-/ +/- Non-meta helpers for the `#test_msgs` command, kept separate so the command elaborator is the only meta definition. -/ From d9e48c3752ef952b5eb7b516620814598290ad1e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 27 Aug 2026 15:20:31 +0200 Subject: [PATCH 32/32] fix: make names match --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index fe3d377d..39c16279 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -171,7 +171,7 @@ input_file errataSelection where path := errataRunnerDir / "selection" -- The generated discovered-tests module (`allTests`), written by the Errata driver. -lean_lib ErrataGenerated where +lean_lib ErrataDiscovered where srcDir := errataRunnerDir roots := #[`ErrataDiscovered] needs := #[errataSelection]