Skip to content

fix: deflake the leanExit exit-code-0 test - #14671

Open
sankalpsthakur wants to merge 1 commit into
leanprover:masterfrom
sankalpsthakur:agent/deflake-leanexit-exit0-race
Open

fix: deflake the leanExit exit-code-0 test#14671
sankalpsthakur wants to merge 1 commit into
leanprover:masterfrom
sankalpsthakur:agent/deflake-leanexit-exit0-race

Conversation

@sankalpsthakur

Copy link
Copy Markdown
Contributor

This PR makes the ErrorExit0 case of the tests/lake/tests/leanExit fixture deterministic.

Since #14629 landed, this test has been coin-flipping in CI on unrelated PRs: the type-error diagnostic is emitted by the CLI driver's asynchronous reporting loop (SnapshotTree.runAndReport), while #eval (IO.Process.exit 0 : IO Unit) terminates the compiler from inside the next command's elaboration task. When the exit wins the race, the Type mismatch diagnostic never reaches Lake's captured output, the first match_text assertion fails, and the build instead reports only the missing .olean. Observed in CI job 91870184702 (on #14649) and job 91869672660 (on #14640) within the last day.

Give the reporting loop a short, bounded head start before exiting. IO.sleep already has precedent for sequencing against concurrent work in tests/lake/tests/lock.

Test plan

tests/lake/tests/leanExit/test.sh exercises the same four exit/diagnostic combinations as before; the ErrorExit0 case no longer depends on thread scheduling.

Follow-up to #14629.

AI assistance

AI tools assisted with root-cause analysis and patch preparation. I reviewed the driver reporting flow in src/Lean/Elab/Frontend.lean and src/Lean/Language/Basic.lean, the lean_io_exit runtime semantics in src/runtime/io.cpp, and the final diff.

The ErrorExit0 fixture was racy: the type-error diagnostic is emitted by
the driver's asynchronous reporting loop (SnapshotTree.runAndReport),
while `#eval (IO.Process.exit 0 : IO Unit)` terminates the compiler from
inside the next command's elaboration task. When the exit won the race,
the `Type mismatch` diagnostic never reached Lake's captured output and
the build instead failed on the missing .olean, coin-flipping CI on
unrelated PRs (e.g. job 91870184702 on leanprover#14649, job 91869672660 on leanprover#14640).

Give the reporting loop a short, bounded head start before exiting.
IO.sleep already has precedent for sequencing against concurrent work in
tests/lake/tests/lock.
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 4, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 110db9cb751afaee8b2ac344887d6c7e632f77b4. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 04:02:09)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-04 04:02:11)

@sankalpsthakur
sankalpsthakur marked this pull request as ready for review August 4, 2026 04:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants