From 5f6de035d272e1938ef02ab77b1c43bb1f7e293e Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Tue, 14 Apr 2026 21:52:49 +0200
Subject: [PATCH] test: disable flaky test

---
 .../test/suite/restarts/restarts.test.ts      | 92 ++++++++++---------
 1 file changed, 47 insertions(+), 45 deletions(-)

diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts
index 7be61a433..cbad4568c 100644
--- a/vscode-lean4/test/suite/restarts/restarts.test.ts
+++ b/vscode-lean4/test/suite/restarts/restarts.test.ts
@@ -69,51 +69,53 @@ suite('Lean Server Restart Test Suite', () => {
         await closeAllEditors()
     }).timeout(120000)
 
-    test('Worker crashed and client running - Restarting File (Refreshing dependencies)', async () => {
-        logger.log(
-            '=================== Test worker crashed and client running (Refreshing dependencies) ===================',
-        )
-        displayNotification('Information', 'Running tests: ' + __dirname)
-
-        // add normal values to initialize lean4 file
-        const hello = 'Hello World'
-        const evalLine = `#eval "${hello}"`
-        const features = await initLean4Untitled(evalLine)
-        const info = features.infoProvider
-        assert(info, 'No InfoProvider export')
-
-        logger.log('make sure language server is up and running.')
-        await assertStringInInfoviewAt('#eval', info, hello)
-
-        const clients = features.clientProvider
-        assert(clients, 'No LeanClientProvider export')
-
-        logger.log('Insert eval that causes crash.')
-        await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
-
-        const expectedMessage = 'The Lean Server has stopped processing this file'
-        await assertStringInInfoview(info, expectedMessage)
-
-        logger.log('restart the server (without modifying the file, so it should crash again)')
-        let client = await waitForActiveClient(clients)
-        await restartFile()
-
-        logger.log('Checking that it crashed again.')
-        await assertStringInInfoview(info, expectedMessage)
-
-        logger.log('deleting the problematic string closing active editors and restarting the server')
-        await deleteAllText()
-        await insertText(`#eval "${hello}"`)
-        logger.log('Now invoke the restart server command')
-        client = await waitForActiveClient(clients)
-        await restartFile()
-
-        logger.log('checking that Hello World comes back after restart')
-        await assertStringInInfoviewAt('#eval', info, hello)
-
-        // make sure test is always run in predictable state, which is no file or folder open
-        await closeAllEditors()
-    }).timeout(120000)
+    // Disabled because the old nightlies that these tests run on have a bug where the language server drops requests
+    // on crash.
+    // test('Worker crashed and client running - Restarting File (Refreshing dependencies)', async () => {
+    //     logger.log(
+    //         '=================== Test worker crashed and client running (Refreshing dependencies) ===================',
+    //     )
+    //     displayNotification('Information', 'Running tests: ' + __dirname)
+
+    //     // add normal values to initialize lean4 file
+    //     const hello = 'Hello World'
+    //     const evalLine = `#eval "${hello}"`
+    //     const features = await initLean4Untitled(evalLine)
+    //     const info = features.infoProvider
+    //     assert(info, 'No InfoProvider export')
+
+    //     logger.log('make sure language server is up and running.')
+    //     await assertStringInInfoviewAt('#eval', info, hello)
+
+    //     const clients = features.clientProvider
+    //     assert(clients, 'No LeanClientProvider export')
+
+    //     logger.log('Insert eval that causes crash.')
+    //     await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
+
+    //     const expectedMessage = 'The Lean Server has stopped processing this file'
+    //     await assertStringInInfoview(info, expectedMessage)
+
+    //     logger.log('restart the server (without modifying the file, so it should crash again)')
+    //     let client = await waitForActiveClient(clients)
+    //     await restartFile()
+
+    //     logger.log('Checking that it crashed again.')
+    //     await assertStringInInfoview(info, expectedMessage)
+
+    //     logger.log('deleting the problematic string closing active editors and restarting the server')
+    //     await deleteAllText()
+    //     await insertText(`#eval "${hello}"`)
+    //     logger.log('Now invoke the restart server command')
+    //     client = await waitForActiveClient(clients)
+    //     await restartFile()
+
+    //     logger.log('checking that Hello World comes back after restart')
+    //     await assertStringInInfoviewAt('#eval', info, hello)
+
+    //     // make sure test is always run in predictable state, which is no file or folder open
+    //     await closeAllEditors()
+    // }).timeout(120000)
 
     test('Restart Server', async () => {
         logger.log('=================== Test Restart Server ===================')