feat: run Errata tests interactively in a widget - #959
Open
david-christiansen wants to merge 21 commits into
Open
david-christiansen wants to merge 21 commits into
david-christiansen wants to merge 21 commits into
Conversation
david-christiansen
force-pushed
the
test-framework-3
branch
from
August 14, 2026 08:53
02199cd to
2f66877
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
August 26, 2026 10:34
2f66877 to
da8905d
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
August 26, 2026 14:22
6b55385 to
233980c
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
2 times, most recently
from
August 26, 2026 15:10
2defc44 to
ab8f221
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
August 27, 2026 13:03
ab8f221 to
181545b
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
August 27, 2026 13:29
181545b to
eff0700
Compare
Vtec234
self-requested a review
August 27, 2026 14:06
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 8, 2026 13:14
eff0700 to
6399495
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 8, 2026 13:25
6399495 to
4e848d4
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 9, 2026 13:48
4e848d4 to
d18727d
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 9, 2026 14:17
d18727d to
fff228b
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
2 times, most recently
from
September 10, 2026 16:08
28946cb to
2647d9e
Compare
Vtec234
reviewed
Sep 14, 2026
| 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 } {} |
Member
There was a problem hiding this comment.
Re-parsing is a bit of waste - AttrM really should have easier access to the syntax of the marked declaration; but that's a core change AFAICT. There's an attribute with the same issue in verso-blueprint.
Tests can additionally be run interactively using a widget. When the text cursor is on a test's source span, the InfoView offers a "run" button that runs the test in a separate process, streaming its output as it is produced and killing the process if the run is cancelled.
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 15, 2026 08:50
051d006 to
108e8a5
Compare
The run's lifecycle is one reducer over idle/running/done/cancelled/ failed states, each carrying only its own data, so a verdict cannot coexist with an error or a spinner. Timings come from the server's per-run record, so revisiting a test mid-run keeps its true elapsed time instead of restarting the clock.
The runner evaluates the action that `@[test]` compiled beside a test instead of synthesizing its instance again, and takes its context from `mkContext`, which draws the seed the context now requires.
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 15, 2026 08:52
108e8a5 to
7fdcd72
Compare
david-christiansen
force-pushed
the
test-framework-3
branch
from
September 15, 2026 09:14
71b59a2 to
adaf944
Compare
Vtec234
approved these changes
Sep 15, 2026
Vtec234
left a comment
Vtec234
left a comment
Member
There was a problem hiding this comment.
One confusing behavior I found: nested stdout/err boxes do not have a copy button, whereas the copy button on the top box actually copies all the output including nested outputs. Since the boxes are visually separated, this feels surprising.
83C535FF-7F4E-44F9-B75E-821B1E937E9A.mov
Member
|
I am also wondering, should |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Tests can additionally be run interactively using a widget. When the text cursor is on a test's source span, the InfoView offers a "run" button that runs the test in a separate process, streaming its output as it is produced and killing the process if the run is cancelled.