Skip to content

Commit 5f6de03

Browse files
committed
test: disable flaky test
1 parent f97799f commit 5f6de03

File tree

1 file changed

+47
-45
lines changed

1 file changed

+47
-45
lines changed

vscode-lean4/test/suite/restarts/restarts.test.ts

Lines changed: 47 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -69,51 +69,53 @@ suite('Lean Server Restart Test Suite', () => {
6969
await closeAllEditors()
7070
}).timeout(120000)
7171

72-
test('Worker crashed and client running - Restarting File (Refreshing dependencies)', async () => {
73-
logger.log(
74-
'=================== Test worker crashed and client running (Refreshing dependencies) ===================',
75-
)
76-
displayNotification('Information', 'Running tests: ' + __dirname)
77-
78-
// add normal values to initialize lean4 file
79-
const hello = 'Hello World'
80-
const evalLine = `#eval "${hello}"`
81-
const features = await initLean4Untitled(evalLine)
82-
const info = features.infoProvider
83-
assert(info, 'No InfoProvider export')
84-
85-
logger.log('make sure language server is up and running.')
86-
await assertStringInInfoviewAt('#eval', info, hello)
87-
88-
const clients = features.clientProvider
89-
assert(clients, 'No LeanClientProvider export')
90-
91-
logger.log('Insert eval that causes crash.')
92-
await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
93-
94-
const expectedMessage = 'The Lean Server has stopped processing this file'
95-
await assertStringInInfoview(info, expectedMessage)
96-
97-
logger.log('restart the server (without modifying the file, so it should crash again)')
98-
let client = await waitForActiveClient(clients)
99-
await restartFile()
100-
101-
logger.log('Checking that it crashed again.')
102-
await assertStringInInfoview(info, expectedMessage)
103-
104-
logger.log('deleting the problematic string closing active editors and restarting the server')
105-
await deleteAllText()
106-
await insertText(`#eval "${hello}"`)
107-
logger.log('Now invoke the restart server command')
108-
client = await waitForActiveClient(clients)
109-
await restartFile()
110-
111-
logger.log('checking that Hello World comes back after restart')
112-
await assertStringInInfoviewAt('#eval', info, hello)
113-
114-
// make sure test is always run in predictable state, which is no file or folder open
115-
await closeAllEditors()
116-
}).timeout(120000)
72+
// Disabled because the old nightlies that these tests run on have a bug where the language server drops requests
73+
// on crash.
74+
// test('Worker crashed and client running - Restarting File (Refreshing dependencies)', async () => {
75+
// logger.log(
76+
// '=================== Test worker crashed and client running (Refreshing dependencies) ===================',
77+
// )
78+
// displayNotification('Information', 'Running tests: ' + __dirname)
79+
80+
// // add normal values to initialize lean4 file
81+
// const hello = 'Hello World'
82+
// const evalLine = `#eval "${hello}"`
83+
// const features = await initLean4Untitled(evalLine)
84+
// const info = features.infoProvider
85+
// assert(info, 'No InfoProvider export')
86+
87+
// logger.log('make sure language server is up and running.')
88+
// await assertStringInInfoviewAt('#eval', info, hello)
89+
90+
// const clients = features.clientProvider
91+
// assert(clients, 'No LeanClientProvider export')
92+
93+
// logger.log('Insert eval that causes crash.')
94+
// await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
95+
96+
// const expectedMessage = 'The Lean Server has stopped processing this file'
97+
// await assertStringInInfoview(info, expectedMessage)
98+
99+
// logger.log('restart the server (without modifying the file, so it should crash again)')
100+
// let client = await waitForActiveClient(clients)
101+
// await restartFile()
102+
103+
// logger.log('Checking that it crashed again.')
104+
// await assertStringInInfoview(info, expectedMessage)
105+
106+
// logger.log('deleting the problematic string closing active editors and restarting the server')
107+
// await deleteAllText()
108+
// await insertText(`#eval "${hello}"`)
109+
// logger.log('Now invoke the restart server command')
110+
// client = await waitForActiveClient(clients)
111+
// await restartFile()
112+
113+
// logger.log('checking that Hello World comes back after restart')
114+
// await assertStringInInfoviewAt('#eval', info, hello)
115+
116+
// // make sure test is always run in predictable state, which is no file or folder open
117+
// await closeAllEditors()
118+
// }).timeout(120000)
117119

118120
test('Restart Server', async () => {
119121
logger.log('=================== Test Restart Server ===================')

0 commit comments

Comments
 (0)