feat: proper test framework

.github/workflows/ci.yml

@@ -13,6 +13,9 @@ jobs:
     build:
         name: Build and test
         runs-on: nscloud-ubuntu-22.04-amd64-8x16
+        permissions:
+            contents: read
+            checks: write
         env:
             # Used for browser tests. Placing them here allows caching to work right.
             PLAYWRIGHT_BROWSERS_PATH: ${{ github.workspace }}/.playwright-browsers
@@ -90,7 +93,31 @@ jobs:
 
             - name: Run tests
               run: |
-                  lake test -- --verbose --check-tex
+                  lake test -- --test-options --verbose --check-tex --junit=errata-report.xml --markdown=errata-summary.md
+
+            - name: Add test results to the job summary
+              if: always()
+              run: |
+                  if [ -f errata-summary.md ]; then cat errata-summary.md >> "$GITHUB_STEP_SUMMARY"; fi
+
+            - name: Publish the JUnit test report
+              if: always()
+              uses: dorny/test-reporter@v1
+              with:
+                  name: Errata tests
+                  path: errata-report.xml
+                  reporter: java-junit
+                  fail-on-error: false
+
+            - name: Upload the raw test reports
+              if: always()
+              uses: actions/upload-artifact@v4
+              with:
+                  name: errata-test-reports
+                  path: |
+                      errata-report.xml
+                      errata-summary.md
+                  if-no-files-found: ignore
 
             - name: Generate the test website
               run: |
@@ -147,6 +174,12 @@ jobs:
                   npx tsc --noEmit -p jsconfig.json
                   popd
 
+            - name: Type check the run-test widget JS code
+              run: |
+                  pushd src/errata/Errata/widget
+                  npx tsc --noEmit -p jsconfig.json
+                  popd
+
             - name: Check the ToC width storage key stays in sync
               run: |
                   # toc-resize.js and toc-resize-preload.js must agree on the localStorage

.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:"

.github/workflows/test-imports.yml

@@ -1,3 +1,8 @@
+# This check is retained only to satisfy the required "Check all test modules are imported" status
+# check on the protected branch. It is a no-op on this layout: test modules now live under
+# src/tests/VersoTests and are discovered by globbing, and src/tests/Tests no longer exists, so the
+# scan below finds nothing. Coverage is instead enforced by `errataWarnUncoveredTestModules` during
+# `lake test`. Remove this workflow (and drop the required check) once merged.
 name: All test modules imported
 
 on: [pull_request, merge_group]

.github/workflows/update-subverso.yml

@@ -84,7 +84,7 @@ jobs:
             - name: Run tests
               if: steps.check-changes.outputs.changed == 'true'
               run: |
-                  lake test -- --verbose --check-tex
+                  lake test -- --test-options --verbose --check-tex
 
             - name: Create branch and open PR
               if: steps.check-changes.outputs.changed == 'true'

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f3f26cc72646205ca167117487c008ee1dafe816",
+   "rev": "f3c7bd5061bd81b4480295c524d4f245c8b7e4e2",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -124,15 +124,256 @@ lean_exe «verso-literate-plan» where
   srcDir := "src/verso-literate-plan"
   supportInterpreter := true
 
+-- All test code: Errata test modules, compile-time tests, fixtures, and generators. Submodules are
+-- globbed so each is built and every `@[test]` module is discoverable.
 @[default_target]
-lean_lib Tests where
+lean_lib VersoTests where
   srcDir := "src/tests"
+  roots := #[`VersoTests]
+  globs := #[Glob.andSubmodules `VersoTests]
 
-@[test_driver]
-lean_exe «verso-tests» where
-  root := `TestMain
-  srcDir := "src/tests"
+-- Everything below is Errata's own implementation: its library, the single-test runner and widget
+-- support exe, its self-tests, the generated discovery runner, and the `lake test` driver.
+section Errata
+
+@[default_target]
+input_file errataUsageFile where
+  text := true
+  path := "src/errata/Errata/usage.txt"
+
+input_file errataRunTestWidgetJs where
+  text := true
+  path := "src/errata/Errata/widget/run_test_widget.js"
+
+lean_lib Errata where
+  srcDir := "src/errata"
+  roots := #[`Errata]
+  needs := #[errataUsageFile, errataRunTestWidgetJs]
+
+-- Runs one test in a fresh process so the widget can stream its output and kill it on cancel.
+@[default_target]
+lean_exe «errata-run-one» where
+  srcDir := "src/errata"
+  root := `ErrataRunOne
+  supportInterpreter := true
+
+-- 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 errataSourceHasTests (lines : List String) : Bool :=
+  lines.any fun line =>
+    let t := line.trimAsciiStart.copy
+    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 errataModuleInfo (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 errataDiscoveredSource (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 errataMainSource (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 errataSplitArgs (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 errataUsage : String := include_str "src/errata/Errata/usage.txt"
+
+/-- Every `.lean` file below a directory, recursively. -/
+private partial def errataLeanFiles (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 ++ (← errataLeanFiles 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 errataModuleOfPath (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 errataWarnUncoveredTestModules (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 ← errataLeanFiles srcDir do
+      let some mod := errataModuleOfPath 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 errataSourceHasTests 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}"
+
+@[test_driver]
+script «errata-test» (args) do
+  let ws ← getWorkspace
+  -- Answer `--help` before discovering or building anything.
+  if args.any (fun a => a == "--help" || a == "-h") then
+    IO.println errataUsage
+    return 0
+  let (libNames, runnerArgs) ←
+    match errataSplitArgs args with
+    | .ok result => pure result
+    | .error msg =>
+      IO.eprintln s!"error: {msg}"
+      IO.eprintln errataUsage
+      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.
+  errataWarnUncoveredTestModules 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)
+    let _ ← (Job.collectArray oleanJobs).await
+    pure (Job.pure 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) ← errataModuleInfo 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", errataDiscoveredSource ws.root.prettyName moduleMods),
+       ("ErrataRunnerMain.lean", errataMainSource 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 some exe := ws.findLeanExe? `«errata-runner»
+    | IO.eprintln "errata-runner executable is not configured"; return 1
+  let exePath ← runBuild exe.fetch
+  let child ← IO.Process.spawn { cmd := exePath.toString, args := runnerArgs.toArray }
+  child.wait
+
+end Errata
 
 lean_lib UsersGuide where
   srcDir := "doc"