Skip to content

test: disable flaky test #768

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mhuisi merged 1 commit into from
Apr 14, 2026
Merged

test: disable flaky test #768

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 47 additions & 45 deletions vscode-lean4/test/suite/restarts/restarts.test.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ===================')
Expand Down
Loading