chore: migrate the test suite to Errata

.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
@@ -149,7 +152,34 @@ jobs:
 
             - name: Run tests
               run: |
-                  lake test -- --verbose --check-tex
+                  lake test -- --test-options --verbose --wfail --junit=errata-report.xml --markdown=errata-summary.md -- --check-tex
+
+            - 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
+
+            # Publishing a check run needs a token with `checks: write`, which pull requests from
+            # forks never receive; those runs get their results from the job summary and the
+            # uploaded artifact instead.
+            - name: Publish the JUnit test report
+              if: always() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
+              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: Test the dev server
               run: |

.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 the test driver's unreachable-modules
+# warning 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 --wfail -- --check-tex
 
             - name: Create branch and open PR
               if: steps.check-changes.outputs.changed == 'true'

doc/UsersGuide/Releases/Entries/TestFramework.lean

@@ -29,3 +29,5 @@ Each test's docstring and source range are saved for failure reporting.
 The test runner discovers every test in the package; it can restrict the run to named libraries, rerun property tests with a fixed seed, update golden files, fail the run on warnings with `--wfail`, and write JUnit XML, JSON, and Markdown reports.
 
 Elaboration-time tests can be written with `#test_msgs` and `#test_guard`, variants of `#guard_msgs` and `#guard` that run their check at compile time and record the outcome as a test case, reported together with the rest of the suite.
+
+Verso's own test suite runs on Errata: `lake test` discovers and runs every test in the package, and CI publishes the resulting reports.

lakefile.lean

@@ -135,18 +135,16 @@ 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"
-
-@[test_driver]
-lean_exe «verso-tests» where
-  root := `TestMain
-  srcDir := "src/tests"
-  supportInterpreter := true
+  roots := #[`VersoTests]
+  globs := #[Glob.andSubmodules `VersoTests]
 
 -- Everything below is Errata's own implementation: its library, its self-tests, the generated
--- discovery runner, and the runner script.
+-- discovery runner, and the `lake test` driver.
 namespace Errata
 
 @[default_target]
@@ -249,12 +247,13 @@ 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 run Errata.run --test-options {opt}`."
+      e.g. `lake test -- --test-options {opt}`."
   | none => .ok (names, rest)
 
-/-- Usage information for `lake run Errata.run`. -/
+/-- Usage information for `lake test`. -/
 private def usage : String := include_str "src/errata/Errata/usage.txt"
 
+@[test_driver]
 script run (args) do
   let ws ← getWorkspace
   -- Answer the driver's own `--help` before discovering or building anything. A `--help` after the

src/errata/Errata/usage.txt

@@ -1,12 +1,12 @@
 Errata test runner
 
 Usage:
-  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
+  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
 
 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 run Errata.run --test-options --help
+  lake test -- --test-options --help