test: make tests more stable (#601)

mhuisi · web-flow · commit 389bb4d444bb · 2025-04-08T15:47:42.000+02:00
This PR adjusts tests that check the contents of 'All Messages' to check
the content of 'Messages' instead, which (when initializing the InfoView
for the first time) is sometimes subject to a race condition that makes
it not display any messages. This is a known, albeit minor, issue.
diff --git a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts
@@ -10,7 +10,7 @@ import {
     initLean4Untitled,
     waitForActiveClient,
     waitForActiveClientRunning,
-    waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
 } from '../utils/helpers'
 
 suite('Lean4 Bootstrap Test Suite', () => {
@@ -32,20 +32,7 @@ suite('Lean4 Bootstrap Test Suite', () => {
         await waitForActiveClient(features.clientProvider, 120)
         await waitForActiveClientRunning(features.clientProvider, 300)
 
-        const hackNeeded = false
-        if (hackNeeded) {
-            // this is a hack we can do if it turns out this bootstrap test is unreliable.
-            // The hack would be covering a product bug, which is why we'd prefer not to use it.
-            // if it times out at 600 seconds then waitForInfoviewHtml prints the contents of the InfoView so we can see what happened.
-            // await waitForInfoviewHtml(info, expected, 10, 60000, true, async () => {
-            //     // 60 seconds elapsed, and infoview is not updating, try and re-edit
-            //     // the file to force the LSP to update.
-            //     await deleteAllText();
-            //     await insertText('#eval Lean.versionString');
-            // });
-        } else {
-            await waitForInfoviewHtml(info, expected, 600)
-        }
+        await waitForInfoviewHtmlAt('#eval', info, expected, 600)
 
         logger.log('Lean installation is complete.')
 
@@ -74,7 +61,7 @@ suite('Lean4 Bootstrap Test Suite', () => {
         assert(info, 'No InfoProvider export')
 
         logger.log('Wait for Lean nightly build server to start...')
-        await waitForInfoviewHtml(info, '4.0.0-nightly-', 120)
+        await waitForInfoviewHtmlAt('#eval', info, '4.0.0-nightly-', 120)
         logger.log('Lean nightly build server is running.')
 
         // make sure test is always run in predictable state, which is no file or folder open
diff --git a/vscode-lean4/test/suite/info/info.test.ts b/vscode-lean4/test/suite/info/info.test.ts
@@ -4,6 +4,7 @@ import * as vscode from 'vscode'
 import { logger } from '../../../src/utils/logger'
 import {
     assertStringInInfoview,
+    assertStringInInfoviewAt,
     clickInfoViewButton,
     closeActiveEditor,
     closeAllEditors,
@@ -12,8 +13,10 @@ import {
     gotoPosition,
     initLean4Untitled,
     insertText,
+    insertTextAfter,
     waitForActiveEditor,
     waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
     waitForInfoviewNotHtml,
 } from '../utils/helpers'
 
@@ -29,7 +32,7 @@ suite('InfoView Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
-        await assertStringInInfoview(info, expectedEval1)
+        await assertStringInInfoviewAt('#eval', info, expectedEval1)
 
         logger.log('Clicking copyToComment button in InfoView')
         await clickInfoViewButton(info, 'copy-to-comment')
@@ -50,7 +53,8 @@ suite('InfoView Test Suite', () => {
         const c = 77
         const d = 7
 
-        const features = await initLean4Untitled(`#eval ${a}*${b}`)
+        const evalLine1 = `#eval ${a}*${b}`
+        const features = await initLean4Untitled(evalLine1)
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
@@ -61,11 +65,12 @@ suite('InfoView Test Suite', () => {
         await clickInfoViewButton(info, 'toggle-pinned')
 
         logger.log('Insert another couple lines and another eval')
-        await insertText(`\n\n/- add another unpinned eval -/\n#eval ${c}*${d}`)
+        const evalLine2 = `#eval ${c}*${d}`
+        await insertTextAfter(evalLine1, `\n\n/- add another unpinned eval -/\n${evalLine2}`)
 
         logger.log('wait for the new expression to appear')
         const expectedEval2 = (c * d).toString()
-        await assertStringInInfoview(info, expectedEval2)
+        await assertStringInInfoviewAt(evalLine2, info, expectedEval2)
 
         logger.log('make sure pinned expression is still there')
         await assertStringInInfoview(info, expectedEval1)
@@ -75,7 +80,7 @@ suite('InfoView Test Suite', () => {
 
         logger.log('Make sure pinned eval is gone, but unpinned eval remains')
         await waitForInfoviewNotHtml(info, expectedEval1)
-        await assertStringInInfoview(info, expectedEval2)
+        await assertStringInInfoviewAt(evalLine2, info, expectedEval2)
 
         await closeAllEditors()
     }).timeout(60000)
@@ -92,7 +97,7 @@ suite('InfoView Test Suite', () => {
 
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
-        await waitForInfoviewHtml(info, expectedEval, 30, 1000, false)
+        await waitForInfoviewHtmlAt('#eval', info, expectedEval, 30, 1000, false)
 
         logger.log('Pin this info')
         await clickInfoViewButton(info, 'toggle-pinned')
@@ -106,7 +111,7 @@ suite('InfoView Test Suite', () => {
 
         logger.log('wait for the new expression to appear')
         const expectedEval2 = '[4, 1, 2, 3]'
-        await waitForInfoviewHtml(info, expectedEval2, 30, 1000, false)
+        await waitForInfoviewHtmlAt('#eval', info, expectedEval2, 30, 1000, false)
 
         logger.log('make sure pinned expression is not showing an error')
         await waitForInfoviewNotHtml(info, 'Incorrect position')
@@ -116,7 +121,7 @@ suite('InfoView Test Suite', () => {
         editor.selection = new vscode.Selection(newLastLine.start, newLastLine.start)
 
         logger.log('make sure pinned value reverts after an undo')
-        await waitForInfoviewHtml(info, expectedEval, 30, 1000, false)
+        await waitForInfoviewHtmlAt('#eval', info, expectedEval, 30, 1000, false)
 
         await closeAllEditors()
     }).timeout(60000)
@@ -128,21 +133,22 @@ suite('InfoView Test Suite', () => {
         const b = 95
         const prefix = 'Lean version is:'
 
-        const features = await initLean4Untitled(`#eval ${a}*${b}`)
+        const evalLine = `#eval ${a}*${b}`
+        const features = await initLean4Untitled(evalLine)
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
         const expectedEval = (a * b).toString()
-        await assertStringInInfoview(info, expectedEval)
+        await assertStringInInfoviewAt('#eval', info, expectedEval)
 
         logger.log('Pin this info')
         await clickInfoViewButton(info, 'toggle-pinned')
 
         logger.log('Insert another eval')
-        await insertText('\n\n#eval s!"' + prefix + ': {Lean.versionString}"')
+        await insertTextAfter(evalLine, '\n\n#eval s!"' + prefix + ': {Lean.versionString}"')
 
         logger.log('make sure output of versionString is also there')
-        await assertStringInInfoview(info, prefix)
+        await assertStringInInfoviewAt('#eval s!', info, prefix)
 
         logger.log('make sure pinned expression is not showing an error')
         await waitForInfoviewNotHtml(info, 'Incorrect position')
@@ -177,7 +183,7 @@ suite('InfoView Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
-        gotoPosition(0, text.indexOf('by'))
+        gotoPosition('by')
         await assertStringInInfoview(info, 'issue461')
 
         logger.log('Opening tooltip for goal type')
diff --git a/vscode-lean4/test/suite/multi/multi.test.ts b/vscode-lean4/test/suite/multi/multi.test.ts
@@ -4,7 +4,7 @@ import * as path from 'path'
 import * as vscode from 'vscode'
 import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
-import { assertStringInInfoview, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers'
+import { assertStringInInfoviewAt, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers'
 
 suite('Multi-Folder Test Suite', () => {
     test('Load a multi-project workspace', async () => {
@@ -19,7 +19,7 @@ suite('Multi-Folder Test Suite', () => {
         // verify we have a nightly build running in this folder.
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
-        await assertStringInInfoview(info, '4.0.0-nightly-')
+        await assertStringInInfoviewAt('#eval Lean.versionString', info, '4.0.0-nightly-')
 
         // Now open a file from the other project
         const doc2 = await vscode.workspace.openTextDocument(path.join(multiRoot, 'foo', 'Foo.lean'))
@@ -28,7 +28,7 @@ suite('Multi-Folder Test Suite', () => {
         await vscode.window.showTextDocument(doc2, options)
 
         logger.log(`wait for version ${version} to load...`)
-        await assertStringInInfoview(info, version)
+        await assertStringInInfoviewAt('#eval', info, version)
 
         // Now verify we have 2 LeanClients running.
         const clients = features.clientProvider
diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts
@@ -7,12 +7,14 @@ import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
 import {
     assertStringInInfoview,
+    assertStringInInfoviewAt,
     closeAllEditors,
     deleteAllText,
     extractPhrase,
     initLean4,
     initLean4Untitled,
     insertText,
+    insertTextAfter,
     restartFile,
     restartLeanServer,
     waitForActiveClient,
@@ -29,18 +31,19 @@ suite('Lean Server Restart Test Suite', () => {
 
         // add normal values to initialize lean4 file
         const hello = 'Hello World'
-        const features = await initLean4Untitled(`#eval "${hello}"`)
+        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 assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         const clients = features.clientProvider
         assert(clients, 'No LeanClientProvider export')
 
         logger.log('Insert eval that causes crash.')
-        await insertText('\n\n#eval (unsafeCast 0 : String)')
+        await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
 
         const expectedMessage = 'The Lean Server has stopped processing this file'
         await assertStringInInfoview(info, expectedMessage)
@@ -60,7 +63,7 @@ suite('Lean Server Restart Test Suite', () => {
         await restartLeanServer(client)
 
         logger.log('checking that Hello World comes back after restart')
-        await assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
@@ -74,18 +77,19 @@ suite('Lean Server Restart Test Suite', () => {
 
         // add normal values to initialize lean4 file
         const hello = 'Hello World'
-        const features = await initLean4Untitled(`#eval "${hello}"`)
+        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 assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         const clients = features.clientProvider
         assert(clients, 'No LeanClientProvider export')
 
         logger.log('Insert eval that causes crash.')
-        await insertText('\n\n#eval (unsafeCast 0 : String)')
+        await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
 
         const expectedMessage = 'The Lean Server has stopped processing this file'
         await assertStringInInfoview(info, expectedMessage)
@@ -105,7 +109,7 @@ suite('Lean Server Restart Test Suite', () => {
         await restartFile()
 
         logger.log('checking that Hello World comes back after restart')
-        await assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts
@@ -6,14 +6,15 @@ import { elanInstalledToolchains } from '../../../src/utils/elan'
 import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
 import {
-    assertStringInInfoview,
+    assertStringInInfoviewAt,
     closeAllEditors,
     extractPhrase,
     gotoDefinition,
     initLean4,
     initLean4Untitled,
     waitForActiveEditor,
     waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
 } from '../utils/helpers'
 
 suite('Lean4 Basics Test Suite', () => {
@@ -25,7 +26,7 @@ suite('Lean4 Basics Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
-        await assertStringInInfoview(info, '4.0.0-nightly-')
+        await assertStringInInfoviewAt('#eval', info, '4.0.0-nightly-')
 
         // test goto definition to lean toolchain works
         await waitForActiveEditor()
@@ -60,7 +61,7 @@ suite('Lean4 Basics Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
         const expectedVersion = '5040' // the factorial function works.
-        const html = await waitForInfoviewHtml(info, expectedVersion)
+        const html = await waitForInfoviewHtmlAt('#eval factorial 7', info, expectedVersion)
 
         const installer = features.installer
         assert(installer, 'No LeanInstaller export')
@@ -73,7 +74,7 @@ suite('Lean4 Basics Test Suite', () => {
             defaultToolchain = defaultToolchain.replace('/', '--')
             defaultToolchain = defaultToolchain.replace(':', '---')
             // make sure this string exists in the info view.
-            await waitForInfoviewHtml(info, defaultToolchain)
+            await waitForInfoviewHtmlAt('#eval IO.appPath', info, defaultToolchain)
         }
 
         // make sure test is always run in predictable state, which is no file or folder open
@@ -97,7 +98,7 @@ suite('Lean4 Basics Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
         let expectedVersion = 'Hello:'
-        let html = await waitForInfoviewHtml(info, expectedVersion)
+        let html = await waitForInfoviewHtmlAt('#eval main', info, expectedVersion)
         const versionString = extractPhrase(html, 'Hello:', '<').trim()
         logger.log(`>>> Found "${versionString}" in infoview`)
 
diff --git a/vscode-lean4/test/suite/toolchains/toolchain.test.ts b/vscode-lean4/test/suite/toolchains/toolchain.test.ts
@@ -5,12 +5,12 @@ import * as path from 'path'
 import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
 import {
-    assertStringInInfoview,
+    assertStringInInfoviewAt,
     closeAllEditors,
     extractPhrase,
     getAltBuildVersion,
     initLean4,
-    waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
 } from '../utils/helpers'
 
 // Expects to be launched with folder: ${workspaceFolder}/vscode-lean4/test/suite/simple
@@ -30,11 +30,11 @@ suite('Toolchain Test Suite', () => {
         assert(installer, 'No LeanInstaller export')
 
         // wait for info view to show up.
-        await assertStringInInfoview(info, 'Hello')
+        await assertStringInInfoviewAt('#eval main', info, 'Hello')
 
         // verify we have a nightly build running in this folder.
         const expectedVersion = '4.0.0-nightly-'
-        const html = await waitForInfoviewHtml(info, expectedVersion)
+        const html = await waitForInfoviewHtmlAt('#eval main', info, expectedVersion)
         const foundVersion = extractPhrase(html, expectedVersion, '\n')
 
         // Now edit the lean-toolchain file.
@@ -48,7 +48,7 @@ suite('Toolchain Test Suite', () => {
 
         try {
             logger.log(`verify that we switched to alt version ${version}`)
-            const html = await assertStringInInfoview(info, version)
+            const html = await assertStringInInfoviewAt('#eval main', info, version)
 
             // check the path to lean.exe from the `eval IO.appPath`
             const leanPath = extractPhrase(html, 'FilePath.mk', '<').trim()
@@ -61,7 +61,7 @@ suite('Toolchain Test Suite', () => {
         }
 
         logger.log(`Wait for version to appear, it should be ${foundVersion}`)
-        await assertStringInInfoview(info, foundVersion)
+        await assertStringInInfoviewAt('#eval main', info, foundVersion)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts
