From 4bcb6fb821befb346f55574b01ee12af62fd0f76 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Tue, 14 Apr 2026 20:29:17 +0200
Subject: [PATCH] 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>
---
 vscode-lean4/test/suite/utils/helpers.ts | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts
index 4a6f7547..c3354aad 100644
--- a/vscode-lean4/test/suite/utils/helpers.ts
+++ b/vscode-lean4/test/suite/utils/helpers.ts
@@ -135,6 +135,9 @@ export async function initLean4Untitled(contents: string): Promise<EnabledFeatur
     // If info view opens too quickly there is no LeanClient ready yet and
     // it's initialization gets messed up.
     assertAndLog(await waitForInfoViewOpen(info, 60), 'Info view did not open after 60 seconds')
+    // Reusing the Untitled-1 URI across tests can leave the InfoProvider bound to a stale
+    // client; wait until a fresh client for this document is running before returning.
+    await waitForActiveClientRunning(features.clientProvider)
     return features
 }
 
@@ -445,19 +448,18 @@ export async function findWord(
     retries = 60,
     delay = 1000,
 ): Promise<vscode.Range> {
-    let count = 0
+    const totalRetries = retries
     while (retries > 0) {
         const text = editor.document.getText()
         const pos = text.indexOf(word)
-        if (pos < 0) {
-            await sleep(delay)
-            count += 1
-        } else {
+        if (pos >= 0) {
             return new vscode.Range(editor.document.positionAt(pos), editor.document.positionAt(pos + word.length))
         }
+        await sleep(delay)
+        retries -= 1
     }
 
-    const timeout = (retries * delay) / 1000
+    const timeout = (totalRetries * delay) / 1000
     assertAndLog(false, `word ${word} not found in editor after ${timeout} seconds`)
 }
 
@@ -541,6 +543,7 @@ export async function clickInfoViewButton(info: InfoProvider, name: string): Pro
         try {
             const cmd = `document.querySelector(\'[data-id*="${name}"]\').click()`
             await info.runTestScript(cmd)
+            return
         } catch (err) {
             logger.log(`### runTestScript failed: ${err.message}`)
             if (retries === 0) {