Skip to content

Commit 4bcb6fb

Browse files
mhuisiclaude
andcommitted
test: stabilize flaky restart test by waiting for fresh client
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>
1 parent 988871a commit 4bcb6fb

File tree

1 file changed

+9
-6
lines changed

1 file changed

+9
-6
lines changed

vscode-lean4/test/suite/utils/helpers.ts

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,9 @@ export async function initLean4Untitled(contents: string): Promise<EnabledFeatur
135135
// If info view opens too quickly there is no LeanClient ready yet and
136136
// it's initialization gets messed up.
137137
assertAndLog(await waitForInfoViewOpen(info, 60), 'Info view did not open after 60 seconds')
138+
// Reusing the Untitled-1 URI across tests can leave the InfoProvider bound to a stale
139+
// client; wait until a fresh client for this document is running before returning.
140+
await waitForActiveClientRunning(features.clientProvider)
138141
return features
139142
}
140143

@@ -445,19 +448,18 @@ export async function findWord(
445448
retries = 60,
446449
delay = 1000,
447450
): Promise<vscode.Range> {
448-
let count = 0
451+
const totalRetries = retries
449452
while (retries > 0) {
450453
const text = editor.document.getText()
451454
const pos = text.indexOf(word)
452-
if (pos < 0) {
453-
await sleep(delay)
454-
count += 1
455-
} else {
455+
if (pos >= 0) {
456456
return new vscode.Range(editor.document.positionAt(pos), editor.document.positionAt(pos + word.length))
457457
}
458+
await sleep(delay)
459+
retries -= 1
458460
}
459461

460-
const timeout = (retries * delay) / 1000
462+
const timeout = (totalRetries * delay) / 1000
461463
assertAndLog(false, `word ${word} not found in editor after ${timeout} seconds`)
462464
}
463465

@@ -541,6 +543,7 @@ export async function clickInfoViewButton(info: InfoProvider, name: string): Pro
541543
try {
542544
const cmd = `document.querySelector(\'[data-id*="${name}"]\').click()`
543545
await info.runTestScript(cmd)
546+
return
544547
} catch (err) {
545548
logger.log(`### runTestScript failed: ${err.message}`)
546549
if (retries === 0) {

0 commit comments

Comments
 (0)