feat: run Errata tests interactively in a widget

.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
@@ -147,11 +150,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: Run Errata's self-tests
+            - name: Add test results to the job summary
+              if: always()
               run: |
-                  lake run Errata.run ErrataTests --test-options --verbose
+                  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: Test the dev server
               run: |
@@ -212,6 +235,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/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'

doc/UsersGuide/Releases/Entries/TestFramework.lean

@@ -29,3 +29,7 @@ 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.
+
+Verso's own test suite runs on Errata: `lake test` discovers and runs every test in the package, and CI publishes the resulting reports.
+
+Tests can also be run interactively from the editor: a panel widget shown on a test's declaration runs it in a separate process, streaming its output as it is produced.

lakefile.lean

@@ -134,29 +134,38 @@ 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"
-  supportInterpreter := true
-
--- Everything below is Errata's own implementation: its library, its self-tests, the generated
--- discovery runner, and the runner script.
+-- 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.
 namespace 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]
+  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
@@ -288,6 +297,7 @@ private def warnUncoveredTestModules (ws : Lake.Workspace) : IO Unit := do
     for mod in missed do
       IO.eprintln s!"  {mod}"
 
+@[test_driver]
 script run (args) do
   let ws ← getWorkspace
   -- Answer `--help` before discovering or building anything.

src/errata-tests/ErrataTests.lean

@@ -155,6 +155,62 @@ def reportMarkdown : Test := do
   assertContains "expected 1\nactual 2" md
   assertContains "Summary by module" md
 
+/-- `runValue` reports a passing value as passed. -/
+@[test]
+def runOnePasses : Test := do
+  let o ← runValue default (pure () : Test)
+  assertEq "passed" o.status
+
+/-- `runValue` reports a failing value as failed and carries its message. -/
+@[test]
+def runOneFails : Test := do
+  let o ← runValue default (TestResult.fail { message := "boom" })
+  assertEq "failed" o.status
+  assertEq (some "boom") o.message?
+
+/-- `runValue` reports a skipped value as skipped. -/
+@[test]
+def runOneSkips : Test := do
+  let o ← runValue default (TestResult.skip "later")
+  assertEq "skipped" o.status
+
+/-- A failing run surfaces its captured output in the outcome. -/
+@[test]
+def runOneCapturesOutput : Test := do
+  let o ← runValue default (do IO.println "trace line"; failHere "nope" : Test)
+  assertEq "failed" o.status
+  assertEq 1 o.output.size
+  assertEq "stdout" o.output[0]!.stream
+  assertContains "trace line" o.output[0]!.text
+
+/-- An outcome takes the most severe verdict among several named results. -/
+@[test]
+def runOneAggregates : Test := do
+  let o ← runValue default (do result "a" (pure ()); result "b" (failHere "bad") : Test)
+  assertEq "failed" o.status
+
+/-- A passing run still surfaces its captured output. -/
+@[test]
+def runOnePassOutput : Test := do
+  let o ← runValue default (do IO.println "printed"; return true : IO Bool)
+  assertEq "passed" o.status
+  assertEq 1 o.output.size
+  assertEq "stdout" o.output[0]!.stream
+  assertContains "printed" o.output[0]!.text
+
+/-- Captured output keeps stdout and stderr distinct and interleaved in order. -/
+@[test]
+def runOneStreams : Test := do
+  let o ← runValue default (do
+    IO.println "out one"
+    IO.eprintln "err one"
+    IO.println "out two"
+    return true : IO Bool)
+  assertEq "passed" o.status
+  assertEq 3 o.output.size
+  assertEq "stdout" o.output[0]!.stream
+  assertEq "stderr" o.output[1]!.stream
+  assertEq "stdout" o.output[2]!.stream
 /-- `failure` from the `Alternative` instance fails a test. -/
 @[test]
 def alternativeFailure : Test := expectFail failure

src/errata/Errata.lean

@@ -15,6 +15,8 @@ public import Errata.Process
 public import Errata.Golden
 public import Errata.Report
 public import Errata.Runner
+public import Errata.NameJson
+public import Errata.RunOne
 public import Errata.Discovery
 public import Errata.CompileTime
 public import Errata.Property

src/errata/Errata/Discovery.lean

@@ -9,6 +9,8 @@ public import Errata.IsTest
 public import Errata.Runner
 public import Lean
 public meta import Lean
+public meta import Errata.NameJson
+public meta import Errata.Widget
 
 open Lean Meta Elab Term
 
@@ -68,6 +70,70 @@ meta def recordTest (decl : Name) : AttrM Unit := do
   let docstring? ← findDocString? (← getEnv) decl
   modifyEnv (testExt.addEntry · { name := decl, file := ← getFileName, docstring? })
 
+/-- A synthetic syntax carrying the given source range, used to position the widget. -/
+meta def rangeSyntax [Monad m] [MonadFileMap m]
+    (startPos stopPos : String.Pos.Raw) : m Syntax := do
+  let str := (← getFileMap).source
+  let leading : Substring.Raw := { str, startPos, stopPos := startPos }
+  let trailing : Substring.Raw := { str, startPos := stopPos, stopPos }
+  return Syntax.atom (.original leading startPos trailing stopPos) ""
+
+/-- The text of line {lean}`i`, trimmed of surrounding whitespace. -/
+private meta def lineText (lines : Array String) (i : Nat) : String :=
+  ((lines[i]?).getD "").trimAscii.copy
+
+/-- The first non-blank line at or above {lean}`i`, or {lean}`none` if all are blank up to the top. -/
+private meta partial def firstNonBlankUp (lines : Array String) (i : Nat) : Option Nat :=
+  if (lineText lines i).isEmpty then
+    if i == 0 then none else firstNonBlankUp lines (i - 1)
+  else some i
+
+/-- Scanning up from {lean}`i`, the line that opens a doc comment, stopping at a non-comment line. -/
+private meta partial def docOpenLine (lines : Array String) (i : Nat) : Option Nat :=
+  if (lineText lines i).startsWith "/--" then some i
+  else if (lineText lines i).startsWith "/-" then none
+  else if i == 0 then none
+  else docOpenLine lines (i - 1)
+
+/--
+The 0-based start line of a doc comment immediately above {lean}`markerLineIdx`, if any. To avoid
+mistaking an unrelated trailing comment for one, the comment must be a single-line doc comment or
+have its closing delimiter on its own line opened by a doc-comment line.
+-/
+private meta def docStartLine? (lines : Array String) (markerLineIdx : Nat) : Option Nat := do
+  guard (markerLineIdx > 0)
+  let endLine ← firstNonBlankUp lines (markerLineIdx - 1)
+  let t := lineText lines endLine
+  if t.startsWith "/--" && t.endsWith "-/" then return endLine
+  guard (t == "-/" && endLine > 0)
+  docOpenLine lines (endLine - 1)
+
+/--
+The source range to show the test's widget over: the whole declaration, including a doc comment above
+it. The recorded declaration range is used when available; otherwise the command is re-parsed from the
+start of the marker's line, extending up over an immediately preceding doc comment. Falls back to the
+marker itself.
+-/
+meta def widgetRangeSyntax (decl : Name) (attrStx : Syntax) : AttrM Syntax := do
+  let fileMap ← getFileMap
+  if let some ranges ← findDeclarationRanges? decl then
+    let stx ← rangeSyntax (fileMap.ofPosition ranges.range.pos) (fileMap.ofPosition ranges.range.endPos)
+    return stx
+  let some attrPos := attrStx.getPos? | return attrStx
+  let lineStart := fileMap.ofPosition ⟨(fileMap.toPosition attrPos).line, 0⟩
+  let inputCtx := Parser.mkInputContext fileMap.source (← getFileName)
+  let pmctx : Parser.ParserModuleContext := { env := ← getEnv, options := ← getOptions }
+  let (cmdStx, _, _) := Parser.parseCommand inputCtx pmctx { pos := lineStart } {}
+  match cmdStx.getRange? with
+  | some range =>
+    -- Extend the span up over a doc comment immediately above the marker, when there is one.
+    let lines := (fileMap.source.splitOn "\n").toArray
+    let startPos := match docStartLine? lines ((fileMap.toPosition attrPos).line - 1) with
+      | some docIdx => fileMap.ofPosition ⟨docIdx + 1, 0⟩
+      | none => range.start
+    rangeSyntax startPos range.stop
+  | none => return attrStx
+
 /-- Marks a definition as a test, discovered and run by the Errata test runner. -/
 meta initialize
   registerBuiltinAttribute {
@@ -80,6 +146,22 @@ meta initialize
       Attribute.Builtin.ensureNoArgs stx
       unless kind == AttributeKind.global do throwAttrMustBeGlobal `test kind
       recordTest decl
+      -- Show the widget when the cursor is anywhere on the declaration, not just on the marker.
+      let widgetStx ← widgetRangeSyntax decl stx
+      -- A hash of the test's source, so a run is invalidated when the test is edited.
+      let source := (← getFileMap).source
+      let version := match widgetStx.getRange? with
+        | some range =>
+          let sub : Substring.Raw := { str := source, startPos := range.start, stopPos := range.stop }
+          toString sub.toString.hash
+        | none => ""
+      let props := pure <| json% {
+        decl: $(Errata.nameToJson decl),
+        module: $(toString (← getMainModule)),
+        name: $(toString (privateToUserName decl)),
+        version: $version
+      }
+      Lean.Widget.savePanelWidgetInfo Errata.Widget.runTestWidget.javascriptHash.val props widgetStx
   }
 
 /-- The test's name below its module: the declaration's components past the module prefix, dotted. -/

src/errata/Errata/NameJson.lean

@@ -0,0 +1,38 @@
+/-
+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 Lean.Data.Json
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+open Lean
+
+/--
+Encodes a {name}`Lean.Name` structurally, preserving the numeric and hygienic components that the
+standard string form does not round-trip. The widget and the single-test runner exchange test names
+this way.
+-/
+def nameToJson : Name → Json
+  | .anonymous => .null
+  | .str p s => Json.mkObj [("str", .arr #[nameToJson p, .str s])]
+  | .num p n => Json.mkObj [("num", .arr #[nameToJson p, .num n])]
+
+/-- Decodes a {name}`Lean.Name` written by {name}`nameToJson`. -/
+partial def nameOfJson? (j : Json) : Except String Name := do
+  if j.isNull then return .anonymous
+  if let .ok arr := j.getObjVal? "str" then
+    let #[p, s] := (← fromJson? arr : Array Json) | .error "malformed name component"
+    return .str (← nameOfJson? p) (← fromJson? s)
+  if let .ok arr := j.getObjVal? "num" then
+    let #[p, n] := (← fromJson? arr : Array Json) | .error "malformed name component"
+    return .num (← nameOfJson? p) (← fromJson? n)
+  .error "expected an encoded `Name`"