|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author: David Thrane Christiansen |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Errata.IsTest |
| 9 | +public import Lean.Data.Json |
| 10 | + |
| 11 | +public section |
| 12 | + |
| 13 | +set_option linter.missingDocs true |
| 14 | +set_option doc.verso true |
| 15 | + |
| 16 | +namespace Errata |
| 17 | + |
| 18 | +/-- A run of captured output from a single stream, used to render output with the streams distinct. -/ |
| 19 | +structure OutputChunk where |
| 20 | + /-- The stream the text was written to: {lit}`"stdout"` or {lit}`"stderr"`. -/ |
| 21 | + stream : String |
| 22 | + /-- The text written to that stream. -/ |
| 23 | + text : String |
| 24 | + /-- When the chunk was received, in milliseconds since the Unix epoch; set by the runner. -/ |
| 25 | + time : Nat := 0 |
| 26 | +deriving Lean.FromJson, Lean.ToJson, Repr, Inhabited, DecidableEq |
| 27 | + |
| 28 | +/-- The chunk for a single captured output fragment, tagged by its stream. -/ |
| 29 | +def OutputChunk.ofOutput : Output → OutputChunk |
| 30 | + | .stdout s => { stream := "stdout", text := s } |
| 31 | + | .stderr s => { stream := "stderr", text := s } |
| 32 | + |
| 33 | +/-- |
| 34 | +The outcome of running a single test, in a form the InfoView widget renders. The status is one of |
| 35 | +{lit}`"passed"`, {lit}`"failed"`, {lit}`"error"`, or {lit}`"skipped"`. |
| 36 | +-/ |
| 37 | +structure RunOutcome where |
| 38 | + /-- The overall verdict: {lit}`"passed"`, {lit}`"failed"`, {lit}`"error"`, or {lit}`"skipped"`. -/ |
| 39 | + status : String |
| 40 | + /-- How long the run took, in milliseconds. -/ |
| 41 | + durationMs : Nat |
| 42 | + /-- The failure or skip message, when the test did not pass. -/ |
| 43 | + message? : Option String := none |
| 44 | + /-- Supporting detail for a failure, such as a diff or counterexample. -/ |
| 45 | + detail? : Option String := none |
| 46 | + /-- The captured output, in order, with each chunk tagged by the stream it was written to. -/ |
| 47 | + output : Array OutputChunk := #[] |
| 48 | + /-- The test's docstring, rendered as Markdown, when it has one. -/ |
| 49 | + description? : Option String := none |
| 50 | +deriving Lean.FromJson, Lean.ToJson, Repr, Inhabited |
| 51 | + |
| 52 | +/-- The status name a single result contributes. -/ |
| 53 | +private def statusName : Status → String |
| 54 | + | .pass => "passed" |
| 55 | + | .fail _ => "failed" |
| 56 | + | .error _ => "error" |
| 57 | + | .skip _ => "skipped" |
| 58 | + |
| 59 | +/-- The message a status carries, when it did not pass. -/ |
| 60 | +private def statusMessage : Status → Option String |
| 61 | + | .pass => none |
| 62 | + | .fail f => some f.message |
| 63 | + | .error m => some m |
| 64 | + | .skip r => some r |
| 65 | + |
| 66 | +/-- Appends one output fragment, merging it into the previous chunk when it is from the same stream. -/ |
| 67 | +private def pushFragment (chunks : Array OutputChunk) (o : Output) : Array OutputChunk := |
| 68 | + let stream := match o with | .stdout _ => "stdout" | .stderr _ => "stderr" |
| 69 | + match chunks.back? with |
| 70 | + | some last => if last.stream == stream |
| 71 | + then chunks.pop.push { last with text := last.text ++ o.text } |
| 72 | + else chunks.push { stream, text := o.text } |
| 73 | + | none => chunks.push { stream, text := o.text } |
| 74 | + |
| 75 | +/-- |
| 76 | +Condenses the results of one test run into a single outcome. The verdict is the most severe status |
| 77 | +present (error over failed over skipped over passed), the message and detail come from the first |
| 78 | +result with that status, and the output is every result's captured fragments in order, each tagged by |
| 79 | +its stream. |
| 80 | +-/ |
| 81 | +def summarizeResults (results : Array Result) : RunOutcome := Id.run do |
| 82 | + let rank : Status → Nat |
| 83 | + | .error _ => 3 |
| 84 | + | .fail _ => 2 |
| 85 | + | .skip _ => 1 |
| 86 | + | .pass => 0 |
| 87 | + let worst := results.foldl (fun acc r => if rank r.status > rank acc then r.status else acc) .pass |
| 88 | + let duration := results.foldl (fun acc r => acc + r.durationMs) 0 |
| 89 | + let output := results.foldl (fun acc r => r.output.log.foldl pushFragment acc) #[] |
| 90 | + return { |
| 91 | + status := statusName worst |
| 92 | + durationMs := duration |
| 93 | + message? := statusMessage worst |
| 94 | + detail? := match worst with | .fail f => f.detail? | _ => none |
| 95 | + output |
| 96 | + } |
| 97 | + |
| 98 | +/-- |
| 99 | +Runs one testable value to completion and condenses its results into a {name}`RunOutcome`. Captured |
| 100 | +output is kept on a passing result too, since the widget shows it on demand rather than only on |
| 101 | +failure. |
| 102 | +-/ |
| 103 | +def runValue {α} [IsTest α] (location : Location) (value : α) |
| 104 | + (sink : Output → IO Unit := fun _ => pure ()) : IO RunOutcome := do |
| 105 | + let log ← IO.mkRef (#[] : Array Result) |
| 106 | + let usedOptions ← IO.mkRef ∅ |
| 107 | + let cfg : Context := { log, usedOptions, location, writeOutput := sink } |
| 108 | + let start ← IO.monoMsNow |
| 109 | + let (outcome, output) ← runCapturing cfg (IsTest.toTest value) |
| 110 | + let dur := (← IO.monoMsNow) - start |
| 111 | + let logged ← log.get |
| 112 | + let results := |
| 113 | + match cfg.resultOfOutcome outcome output dur (!logged.isEmpty) with |
| 114 | + | some r => logged.push r |
| 115 | + | none => |
| 116 | + -- A passing test with named results: the results stand for it, but keep the test's own |
| 117 | + -- top-level output (written outside any result block) so the widget still shows it. |
| 118 | + if output.log.isEmpty then logged else logged.push { cfg.pass 0 with output } |
| 119 | + return summarizeResults results |
| 120 | + |
| 121 | +/-- Runs one testable value with a default failure location, for callers without a source range. -/ |
| 122 | +def runValueDefault {α} [IsTest α] (value : α) : IO RunOutcome := runValue default value |
0 commit comments