feat: run Errata tests interactively in a widget

.github/workflows/ci.yml

@@ -242,6 +242,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

doc/UsersGuide/Releases/Entries/TestFramework.lean

@@ -13,7 +13,7 @@ release_note
   version := ⟨4, 34, 0⟩
   breaking := false
   tag := "feat-test-framework"
-  prs := [956, 957]
+  prs := [956, 957, 959]
 
 #doc (Manual) "Test Framework" =>
 
@@ -31,3 +31,5 @@ The test runner discovers every test in the package; it can restrict the run to
 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

@@ -143,14 +143,26 @@ lean_lib VersoTests where
   roots := #[`VersoTests]
   globs := #[Glob.andSubmodules `VersoTests]
 
--- Everything below is Errata's own implementation: its library, its self-tests, the generated
--- discovery runner, and the `lake test` driver.
+-- 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
 
+input_file errataRunTestWidgetJs where
+  text := true
+  path := "src/errata/Errata/widget/run_test_widget.js"
+
 @[default_target]
 lean_lib Errata where
   srcDir := "src/errata"
   roots := #[`Errata]
+  needs := #[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.
 @[default_target]

src/errata-tests/ErrataTests.lean

@@ -561,6 +561,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
 
@@ -70,6 +72,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 {
@@ -82,6 +148,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`"

src/errata/Errata/RunOne.lean

@@ -0,0 +1,123 @@
+/-
+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 Lean.Data.Json
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- A run of captured output from a single stream, used to render output with the streams distinct. -/
+structure OutputChunk where
+  /-- The stream the text was written to: {lit}`"stdout"` or {lit}`"stderr"`. -/
+  stream : String
+  /-- The text written to that stream. -/
+  text : String
+  /-- When the chunk was received, in milliseconds since the Unix epoch; set by the runner. -/
+  time : Nat := 0
+deriving Lean.FromJson, Lean.ToJson, Repr, Inhabited, DecidableEq
+
+/-- The chunk for a single captured output fragment, tagged by its stream. -/
+def OutputChunk.ofOutput : Output → OutputChunk
+  | .stdout s => { stream := "stdout", text := s }
+  | .stderr s => { stream := "stderr", text := s }
+
+/--
+The outcome of running a single test, in a form the InfoView widget renders. The status is one of
+{lit}`"passed"`, {lit}`"failed"`, {lit}`"error"`, or {lit}`"skipped"`.
+-/
+structure RunOutcome where
+  /-- The overall verdict: {lit}`"passed"`, {lit}`"failed"`, {lit}`"error"`, or {lit}`"skipped"`. -/
+  status : String
+  /-- How long the run took, in milliseconds. -/
+  durationMs : Nat
+  /-- The failure or skip message, when the test did not pass. -/
+  message? : Option String := none
+  /-- Supporting detail for a failure, such as a diff or counterexample. -/
+  detail? : Option String := none
+  /-- The captured output, in order, with each chunk tagged by the stream it was written to. -/
+  output : Array OutputChunk := #[]
+  /-- The test's docstring, rendered as Markdown, when it has one. -/
+  description? : Option String := none
+deriving Lean.FromJson, Lean.ToJson, Repr, Inhabited
+
+/-- The status name a single result contributes. -/
+private def statusName : Status → String
+  | .pass => "passed"
+  | .fail _ => "failed"
+  | .error _ => "error"
+  | .skip _ => "skipped"
+
+/-- The message a status carries, when it did not pass. -/
+private def statusMessage : Status → Option String
+  | .pass => none
+  | .fail f => some f.message
+  | .error m => some m
+  | .skip r => some r
+
+/-- Appends one output fragment, merging it into the previous chunk when it is from the same stream. -/
+private def pushFragment (chunks : Array OutputChunk) (o : Output) : Array OutputChunk :=
+  let stream := match o with | .stdout _ => "stdout" | .stderr _ => "stderr"
+  match chunks.back? with
+  | some last => if last.stream == stream
+      then chunks.pop.push { last with text := last.text ++ o.text }
+      else chunks.push { stream, text := o.text }
+  | none => chunks.push { stream, text := o.text }
+
+/--
+Condenses the results of one test run into a single outcome. The verdict is the most severe status
+present (error over failed over skipped over passed), the message and detail come from the first
+result with that status, and the output is every result's captured fragments in order, each tagged by
+its stream.
+-/
+def summarizeResults (results : Array Result) : RunOutcome := Id.run do
+  let rank : Status → Nat
+    | .error _ => 3
+    | .fail _ => 2
+    | .skip _ => 1
+    | .pass => 0
+  let worst := results.foldl (fun acc r => if rank r.status > rank acc then r.status else acc) .pass
+  let duration := results.foldl (fun acc r => acc + r.durationMs) 0
+  let output := results.foldl (fun acc r => r.output.log.foldl pushFragment acc) #[]
+  return {
+    status := statusName worst
+    durationMs := duration
+    message? := statusMessage worst
+    detail? := match worst with | .fail f => f.detail? | _ => none
+    output
+  }
+
+/--
+Runs one testable value to completion and condenses its results into a {name}`RunOutcome`. Captured
+output is kept on a passing result too, since the widget shows it on demand rather than only on
+failure.
+-/
+def runValue {α} [IsTest α] (location : Location) (value : α)
+    (sink : Output → IO Unit := fun _ => pure ()) : IO RunOutcome := do
+  let log ← IO.mkRef (#[] : Array Result)
+  let usedOptions ← IO.mkRef ∅
+  let outputFailed ← IO.mkRef false
+  let cfg : Context := { log, usedOptions, outputFailed, location, writeOutput := sink }
+  let start ← IO.monoMsNow
+  let (outcome, output) ← runCapturing cfg (IsTest.toTest value)
+  let dur := (← IO.monoMsNow) - start
+  let logged ← log.get
+  let results :=
+    match cfg.resultOfOutcome outcome output dur (!logged.isEmpty) with
+    | some r => logged.push r
+    | none =>
+      -- A passing test with named results: the results stand for it, but keep the test's own
+      -- top-level output (written outside any result block) so the widget still shows it.
+      if output.log.isEmpty then logged else logged.push { cfg.mkResult .pass with output }
+  return summarizeResults results
+
+/-- Runs one testable value with a default failure location, for callers without a source range. -/
+def runValueDefault {α} [IsTest α] (value : α) : IO RunOutcome := runValue default value