chore: delete flaky tests for now#13711
Merged
Merged
Conversation
This PR deletes two tests that sometimes timeout (or crash, unclear without #13710) and I was not able to fix it by EOD.
nomeata
added a commit
that referenced
this pull request
May 12, 2026
This PR restores the `cancellation_empty_by.lean` and `cancellation_par.lean` server-interactive tests that were deleted in #13711 ("delete flaky tests for now"). With #13710 in place, a hung worker now surfaces as a prompt `waitForMessage` abort rather than a 1500s CTest timeout, so the tests are tractable to keep enabled. Trim diagnostic tracing in `cancellation_empty_by.lean` to the minimum that's actually causally ordered against the test's synchronisation points: * `test: imports done` -- synchronous `#eval` at the top of the file, fires once before any async task is spawned. * `tracerSuggestion ready` -- gated to the first `tracerSuggestion` invocation via `mkTestTask`, fires exactly once. * `cancelTokenSet` -- inside the `cancelTk.onSet` callback, fires exactly once when `cancelRec` reaches the snapshot. * `sync received` (x2) -- in `t1`'s body after `wait_for_sync` returns, once per elaboration. Removed traces that were either every-invocation (and therefore raced non-deterministically with the snapshot task's other output) or that fired at command-elab boundaries where their position relative to async stderr buffers was unstable: `tracerSuggestion: entered`, `tracerSuggestion: returning candidate`, `t1: body entered`, `test: before/after empty-by example`, `test: file end`. Also drop the `LEAN_DEBUG_MAX_WORKERS` runtime hack added during investigation: it served its purpose (confirming the wait-pressure-driven worker pool ratchet in `task_manager::wait_for`) but is not appropriate as a long-lived debug knob in the runtime. Stress: 24/24 parallel runs pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
1 participant
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.
This PR deletes two tests that sometimes timeout (or crash, unclear
without #13710) and I was not able to fix it by EOD.