feat: proper test framework by david-christiansen · Pull Request #902 · leanprover/verso

david-christiansen · 2026-07-01T09:30:34Z

This PR rearchitects our test suite into a proper testing framework.

Before, our tests were all essentially ad hoc. Each kind of test would be an IO action that might throw, and there were some rough conventions, but output reporting was inconsistent and sometimes hard to understand. Tests were noisy as well, which made it hard to find reasons for failure at a glance.

Now, there's a test framework called Errata, designed to be something we can extract to its own repo after we get some experience with it here (so it can be used e.g. in verso-slides and lean-sqlite).

In Errata, tests are marked by the @[test] attribute. Their docstring and source range are saved for failure reporting. The value of a test can have any type with an IsTest instance. Some machinery in the Lakefile enumerates all tests, providing them to the runner.

Elaboration-time tests can also be implemented using #test_msgs and #test_guard, which are versions of #guard_msgs and #guard that run the compile-time test but save the result as a test case for reporting together with the rest of the tests.

Errata also supports saving JUnit XML, which various GitHub actions can conveniently display for us.

Tests can additionally be run interactively using a widget.

Also major staging simplification

david-christiansen · 2026-07-01T10:14:23Z

Some examples of the widget:

It also captures output and provides timestamps and indicates whether it was stdout or stderr:

david-christiansen · 2026-07-01T14:40:36Z

@tydeu If you could check out the Lake parts of this and make sure I'm not doing anything that's likely to fail unexpectedly, it'd be appreciated. Thanks!

tydeu

The Lake code looks reasonable to me! The comments I left are just minor suggestions. Very cool tool!

tydeu · 2026-07-01T14:53:17Z

+/--
+Whether a source file introduces Errata tests, by an `@[test]` attribute (applied inline or with a
+separate `attribute [test] …`), a `#test_msgs` command, or a `#test_guard` command. This drives the
+glob-coverage check, which reads source files before anything is built; test discovery itself reads
+the compiled modules.
+-/
+private def errataSourceHasTests (lines : List String) : Bool :=
+  lines.any fun line =>
+    let t := line.trimAsciiStart.copy
+    t.startsWith "@[test]" || t.startsWith "attribute [test" ||
+      t.startsWith "#test_msgs" || t.startsWith "#test_guard"


This seems very fragile. Perhaps one could (also?) mark errata files with a line like --! errata?

Hmm, maybe it'd be better just to delete the warning?

The situation I want to avoid is someone saying "I thought my tests were running!" when they aren't. I think remembering to add --! errata is no more likely than remembering to change the glob value, so I don't think it would catch this kind of thing.

But this is indeed fragile. Probably deleting it is better, and instead warning if the globs setting of a library that contains any test at all is the wrong one, or just documenting the footgun loudly in a README. I'll sleep on it.

tydeu · 2026-07-01T15:19:32Z

+-- The selected test set, written by the driver. The generated targets depend on it, so changing
+-- the selection changes their trace and Lake rebuilds them rather than relinking a stale object.
+input_file errataSelection where
+  text := true
+  path := ".lake/errata-runner/selection"
+
+-- The generated discovered-tests module (`allTests`), written by the Errata driver.
+lean_lib ErrataGenerated where
+  srcDir := ".lake/errata-runner"
+  roots := #[`ErrataDiscovered]
+  needs := #[errataSelection]
+
+-- The generated, discovered test runner. Its source is written by the Errata test driver.
+lean_exe «errata-runner» where
+  root := `ErrataRunnerMain
+  srcDir := ".lake/errata-runner"
  supportInterpreter := true
+  needs := #[errataSelection]


The current workflow is to for these to fail to build until errata-test is run to generate them. I presume the reason for this is that they can change based on the arguments passed to errata-test? Otherwise, I would have suggested to use needs to depend on custom target which generates them. That way, e.g., lake exe errata-runner works even if a errata-test has yet to be called. It may be worth documenting the rationale for the current design in a brief comment.

You understand correctly. I'll do the comment.

robsimmons

Have some minor comments, but ran into two larger comments:

The Assertions module doesn't consistently allow a user defined message, that API feels like it should be uniform
I think we want the Assertions module to consistently define a message that is (Option (Unit -> String)) rather than a string — the user might want to give a computationally-expensive error message and that's waiting to cause us pain with the current API.

I could nitpick the widget to death and would somewhat prefer to ship an MVP without it, but realistically we could switch it out later as long as the RPC protocol is sound.

robsimmons · 2026-07-01T16:42:14Z

+# 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.


Why don't we just delete the required status and then go ahead and delete this file in the PR? Seems preferable and more atomic.

OK. When we decide "merge", I can delete it from the PR and remove it from the required set. Until then, let's keep things passing.

robsimmons · 2026-07-01T16:59:38Z

+Usage:
+  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


Strong request: can we use -lLIBRARY/--lib=LIBRARY so we're not sad when we need to add a second kind of CLI configuration?

Weak request: can we use the more standard -- divider for runner options? --test-options doesn't present itself as being any kind of meta-cli-arg.

The unit of execution here for the runner is a library. This seems a bit like wanting cp --source=a.txt --dest=b.txt instead of cp a.txt b.txt in case cp wants something more.

It had the -- for the second divider before. I found myself repeatedly making the mistake that I'd write something like lake test -- --enable-tex instead of lake text -- -- --enable-tex, and I stopped making that mistake when the second -- became --test-options. This is not a strongly-held preference, but it did arise from working with the thing.

robsimmons · 2026-07-01T17:14:03Z

+def formatMessage (msg : Lean.Message) : IO String := do
+  let mut str ← msg.data.toString
+  unless msg.caption == "" do
+    str := msg.caption ++ ":\n" ++ str
+  -- The severity is followed by a space only when the body stays on the same line, matching the
+  -- rendering that `#guard_msgs` compares against.
+  unless str.startsWith "\n" do str := " " ++ str
+  str :=
+    if msg.isTrace then "trace:" ++ str
+    else match msg.severity with
+      | .information => "info:" ++ str
+      | .warning => "warning:" ++ str
+      | .error => "error:" ++ str
+  unless str.endsWith "\n" do str := str ++ "\n"
+  return str
+
+open Lean.Elab.Tactic.GuardMsgs (WhitespaceMode) in
+/-- Whether the expected and actual message blocks match, normalizing whitespace as `#guard_msgs` does. -/
+def messagesMatch (expected actual : String) : Bool :=
+  let norm := fun s => (WhitespaceMode.normalized.apply s).trimAscii.copy
+  norm expected == norm actual
+
+/-- The doc comment that would make the expected block match the actual output. -/
+def suggestedDoc (actual : String) : String :=
+  if actual.isEmpty then ""
+  else if actual.contains '\n' then s!"/--\n{actual}\n-/\n"
+  else s!"/-- {actual} -/\n"


All of these are waiting-to-shoot-us-in-the-foot functions that really ought to be made public and factored out of Lean.Elab.GuardMsgs

robsimmons · 2026-07-01T17:32:58Z

+    "compilerOptions": {
+        "lib": ["ES2024", "DOM", "DOM.Iterable"],
+        "target": "ES2024",
+        "noEmit": true


Suggested change

"noEmit": true

"noEmit": true,

"strict": false

Strict is true by default now (typescript 6) and in recently-updated VSCode versions this will show an error (because VSCode generally uses most-recent typescript) unless we specify strict:false

Should it be false? Or should it be true, and the code improved to match?

robsimmons · 2026-07-01T17:53:07Z

+/--
+When true, a failing Errata compile-time test is an elaboration error rather than a warning.
+-/
+register_option errata.failOnError : Bool := {
+  defValue := false
+  descr := "Make a failing Errata compile-time test an elaboration error rather than a warning."
+}


Not a demand by any means, but I do kind of subscribe to the "don't have warnings" school of thought. Why not just start with failing Errata compile-time tests as elaboration errors? Or is the idea here that the tests are "really" being run separately and the elaboration warnings are just hints... in which case do we really need to start with that configurability knob?

The thing that's funny about Lean testing is that we usually have tests at two separate phases: elaboration-time and run-time. Most languages have only the second.

The goal with this setup is to give a single list of all tests and their results and make the interface as uniform as it can be. If elaboration-time tests block elaboration, then a failing test prevents all downstream test modules from running at all, and there's no way for it to be included in an overall report of passes/fails. So the test library's version of #guard_msgs and friends save their test result in the environment as essentially a constant test, already defined as a pass or a fail, so it can be included in the run-time-phase test execution. This gives uniformity.

It also has the annoying consequence that, while editing the test, useful information is hidden - the fact that it fails! Logging a warning surfaces this so that the author can see to fix it. The idea is that these warnings never get actually committed to main, but they can exist while working on a feature and tracking progress.

I'd be up for deleting this option.

I agree with your rationale for the warning — but I think failOnError is worth deleting unless/until there's a compelling reason for it, and it sounds like maybe you agree.

robsimmons · 2026-07-01T18:30:23Z

+    export function useRpcSession(): {
+        call(method: string, params: any): Promise<any>;
+    };
+}


I'd suggest replacing this whole file with

declare module "@leanprover/infoview";

We're not using TS in a way that gives us effectively any guarantees here, so having an easily-capable-of-drift .d.ts file here is mostly security theater.

Removing the react module would require updating package.json; I can do this in another PR if you prefer but I think it should be the following:

{ "devDependencies": { "@types/react": "^19.2.17", "prettier": "3.9.4", "typescript": "6.0.3" } }

If bumping package.json, you can also add @leanprover/infoview as a dev dependency and remove widget-externals.d.ts altogether.

Would you be up for just making this whole TypeScript situation be actually good for this widget in such a way that users don't need npm if they don't want to replicate what CI is doing? I'm really a n00b here, and I think you could make it excellent in like 5 minutes. If you're up for it, please just push to the branch!

(here "you" was meant to be @robsimmons but @Vtec234 is also very welcome to do it)

I'm afraid that without npm there's just no way for typescript to get the types for react or infoview or etc. I can experiment with whether vscode currently is able to figure them out without an npm install, but I'm not optimistic.

I think it's totally fine to run npm in CI, and as an option for local use when actually working on the code so you don't have to wait for CI. I just don't want our users to need it in order to use the widget or run tests - hence "TypeScript in comments" instead of proper TypeScript.

Vtec234 · 2026-07-01T19:24:41Z

+  -- and prints the exe's absolute path on stdout; progress and errors go to stderr.
+  let build ← IO.Process.spawn {
+    stdin := .null, stdout := .piped, stderr := .piped
+    cmd := "lake", args := #["query", "errata-run-one", module]


I don't understand the setup but this looks sus; we are already in the language server, why are we running Lake instead of getting the test IR from the environment and interpreting it?

It's because we don't really have a way to kill a task in Lean. Tasks need to check for cancellation requests, and arbitrary tests don't typically do that. The fear is someone clicking "run" then "stop" then "run" then "stop" then ..., and ending up starving the language server's thread pool.

Running a process, on the other hand, gives us a way to kill it.

Vtec234 · 2026-07-01T20:00:17Z

+    const version = props.version || "";
+    const cacheKey = JSON.stringify(props.decl) + "@" + version;
+
+    const [outcome, setOutcome] = React.useState(() => resultCache.get(cacheKey) || null);


I usually prefer using state machines that disallow nonsense states; a long sequence of useStates means that we can simultaneously have a successful outcome and error !== null, etc. Downstream from that, some of the effects mutate part of the run state incorrectly, e.g. startedAt.current is reset to Date.now if you click off and back into a test while it's still running. But maybe we're happy with something that works well enough 🤷

I'd like it to be actually good!

Co-authored-by: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>

Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>

Co-authored-by: Mac Malone <tydeu@hatpress.net>

david-christiansen · 2026-07-01T20:13:01Z

The Assertions module doesn't consistently allow a user defined message, that API feels like it should be uniform

I agree and will fix.

I think we want the Assertions module to consistently define a message that is (Option (Unit -> String)) rather than a string — the user might want to give a computationally-expensive error message and that's waiting to cause us pain with the current API.

That's true, but also annoying!

What about something like:

structure AssertionMessage where
  text : Unit -> String
deriving blah blah blah

instance : Coe String AssertionMessage where
  coe str := { text := fun () => str }

I think that lets you write the string literal that is wanted in almost all cases, and also delays it. Or maybe have a sum type with an immediate case and a closure case with strings coercing to the immediate one, if we're worried about too many closures.

david-christiansen added 17 commits June 24, 2026 13:23

feat: add a proper test framework

f8f6e2f

chore: migrate BuildLog tests

805a924

glob warning

e5887d3

Stemmer and zip tests

2618c96

Blog and serialization tests

1ab9a41

Also major staging simplification

Migrate the rest

5501fcd

Really the rest

a8cb3f0

Show on GH

bcf4d0d

invalidation

fb450c7

review

34fe6f6

review

dce73e5

stx and exit

ceaa78e

widget better

db8432d

docstring and widget improvements

8c0875e

separate Lakefile contents

a91db5d

Merge remote-tracking branch 'upstream/main' into test-framework

815caca

migrate test post-merge

e66a331

david-christiansen requested review from Vtec234, ejgallego, jcreedcmu and robsimmons July 1, 2026 09:31

david-christiansen added 2 commits July 1, 2026 11:58

Shake Errata

cbe0cbf

cleanup

0734cc8

david-christiansen added 2 commits July 1, 2026 12:14

migrate

c34a7a4

restore removed mandatory check

76edbb8

david-christiansen requested a review from tydeu July 1, 2026 14:37

tydeu reviewed Jul 1, 2026

View reviewed changes

robsimmons requested changes Jul 1, 2026

View reviewed changes

Vtec234 reviewed Jul 1, 2026

View reviewed changes

Comment thread src/errata/Errata/Widget.lean Outdated

Vtec234 reviewed Jul 1, 2026

View reviewed changes

david-christiansen and others added 4 commits July 1, 2026 22:05

Update src/errata/Errata/Widget.lean

6cca9ab

Co-authored-by: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>

Update src/errata/Errata/widget/run_test_widget.js

e5693e5

Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>

Update lakefile.lean

2e270ca

Co-authored-by: Mac Malone <tydeu@hatpress.net>

Update lakefile.lean

b0180d9

Co-authored-by: Mac Malone <tydeu@hatpress.net>

cleanups

6029b67

Uh oh!

Conversation

david-christiansen commented Jul 1, 2026

Uh oh!

david-christiansen commented Jul 1, 2026

Uh oh!

david-christiansen commented Jul 1, 2026

Uh oh!

tydeu left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robsimmons left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

robsimmons Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

david-christiansen commented Jul 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

robsimmons Jul 1, 2026 •

edited

Loading