From 2ceeb2ad3f8681d82ab32b327ffc2d78e9391c2f Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Wed, 12 Aug 2026 02:02:56 +0000 Subject: [PATCH] tests: defer tc roundtrip fixtures The pure tc-unit roundtrip fixtures were evaluated while Tests.Main constructed the primary suite registry. As a result, selecting an unrelated ignored runner such as ixvm still spawned the seven anonRoundtrip task batches and printed their progress before the requested suite began. Register each fixture as an LSpec individualIO test and place roundtripAll behind an explicit IO state-token thunk. A plain pure/do wrapper is not sufficient because Lean can evaluate the pure work while constructing the IO value. The explicit thunk keeps the work dormant until LSpec executes tc-unit. This keeps the fixtures in tc-unit and preserves their individual results while removing unrelated work and output from ignored-suite startup. Verified with: - lake test -- tc-unit - lake test -- --ignored no-such-suite (registry selection emits no anonRoundtrip output) --- Tests/Ix/Tc/Roundtrip.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Tests/Ix/Tc/Roundtrip.lean b/Tests/Ix/Tc/Roundtrip.lean index 0e9158ad..390d0a68 100644 --- a/Tests/Ix/Tc/Roundtrip.lean +++ b/Tests/Ix/Tc/Roundtrip.lean @@ -79,11 +79,17 @@ def fixtureTests : TestSeq := Id.run do ("shared subterms", envShare.1), ("mutual defs block", envMutualDefs.1), ("inductive block", envInductive.1) ] + /- Defer a pure computation until the returned IO action is executed. + A plain `pure (f ())` is strict enough for Lean to run `f` while the + surrounding `TestSeq` is constructed. -/ + let deferIO := fun f s => .ok (f ()) s let mut ts : TestSeq := .done for (label, env) in cases do - let (rows, err?) := roundtripAll env - let msg := match err? with | some e => s!" — {e}" | none => "" - ts := ts ++ test s!"roundtrip fixture: {label} ({rows} rows){msg}" err?.isNone + let testIO := deferIO fun () => + let (rows, err?) := roundtripAll env + let msg := err?.map fun e => s!"{rows} rows — {e}" + (err?.isNone, 0, 1, msg) + ts := ts ++ .individualIO s!"roundtrip fixture: {label}" none testIO .done return ts open Tests.Tc.Fixtures in