test: stabilize flaky restart test by waiting for fresh client#766
Merged
mhuisi merged 1 commit intoleanprover:masterfrom Apr 14, 2026
Merged
test: stabilize flaky restart test by waiting for fresh client#766mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi merged 1 commit intoleanprover:masterfrom
Conversation
The "Worker crashed and client running - Restarting File (Refreshing dependencies)" test reused the `untitled:Untitled-1` URI from the preceding test. `initLean4Untitled` returned as soon as the InfoView was open, before a fresh `LeanClient` for the new document was wired up to the InfoProvider. When the server crashed, infoview RPCs hung against the stale client instead of failing with `WorkerCrashed`, so the "stopped processing" message never appeared and the assertion timed out after 60s. Observed on both Windows and Linux. `initLean4Untitled` now waits for the active client to reach the running state before returning. Also fixes two latent bugs in the test helpers: - `clickInfoViewButton` missed a `return` on success, re-clicking the target up to 5 times and toggling UI state. - `findWord` never decremented `retries`, so a missing word hung until the mocha suite timeout rather than failing with a clear assertion. Co-Authored-By: Claude Opus 4.6 <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.
Summary
The
Worker crashed and client running - Restarting File (Refreshing dependencies)test inrestarts.test.tshas been flaking on Windows (and occasionally Linux) with:Root cause: the test reuses the
untitled:Untitled-1URI from the preceding sibling test.initLean4Untitledreturned as soon as the InfoView was open, before a freshLeanClientfor the new document had been wired up to theInfoProvider. When the server then crashed, infoview RPCs hung against the stale client instead of failing withWorkerCrashed, so the "stopped processing" message — which is only emitted as a side effect of that RPC failure (src/infoview.ts:215-223) — never appeared and the 60s assertion timed out.initLean4Untitlednow waits for the active client to reach the running state before returning.While investigating Claude also fixed two latent bugs in the test helpers:
clickInfoViewButtonhad noreturnon success, re-clicking the target up to 5 times and toggling UI state.findWordnever decrementedretries, so a missing word hung until the mocha suite timeout instead of failing with a clear assertion.Test plan
🤖 Generated with Claude Code