From e73a0e79fa01d62abaae2cf991231d63527be06a Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 29 Apr 2024 16:16:35 +0200 Subject: [PATCH] chore: adjust tests for adjusted activation logic --- vscode-lean4/src/exports.ts | 17 ++++++- vscode-lean4/src/extension.ts | 49 +++++++++---------- .../test/suite/bootstrap/bootstrap.test.ts | 12 ++--- .../test/suite/docview/docview.test.ts | 6 +-- vscode-lean4/test/suite/info/info.test.ts | 16 +++--- vscode-lean4/test/suite/lean3/lean3.test.ts | 9 +++- vscode-lean4/test/suite/multi/multi.test.ts | 6 +-- .../test/suite/pre-bootstrap/user.test.ts | 7 ++- .../test/suite/restarts/restarts.test.ts | 18 +++---- vscode-lean4/test/suite/simple/simple.test.ts | 14 +++--- .../test/suite/toolchains/toolchain.test.ts | 6 +-- vscode-lean4/test/suite/utils/helpers.ts | 48 +++++++++++++----- 12 files changed, 125 insertions(+), 83 deletions(-) diff --git a/vscode-lean4/src/exports.ts b/vscode-lean4/src/exports.ts index 51ea997c7..de41c6498 100644 --- a/vscode-lean4/src/exports.ts +++ b/vscode-lean4/src/exports.ts @@ -19,6 +19,19 @@ export interface Lean4EnabledFeatures { projectOperationProvider: ProjectOperationProvider } -export interface Exports extends AlwaysEnabledFeatures { - activatedLean4Features: Thenable +export interface EnabledFeatures extends AlwaysEnabledFeatures, Lean4EnabledFeatures {} + +export class Exports { + alwaysEnabledFeatures: AlwaysEnabledFeatures + lean4EnabledFeatures: Promise + + constructor(alwaysEnabledFeatures: AlwaysEnabledFeatures, lean4EnabledFeatures: Promise) { + this.alwaysEnabledFeatures = alwaysEnabledFeatures + this.lean4EnabledFeatures = lean4EnabledFeatures + } + + async allFeatures(): Promise { + const lean4EnabledFeatures = await this.lean4EnabledFeatures + return { ...this.alwaysEnabledFeatures, ...lean4EnabledFeatures } + } } diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index f46af7990..ddfe013ca 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -155,29 +155,28 @@ export async function activate(context: ExtensionContext): Promise { const alwaysEnabledFeatures: AlwaysEnabledFeatures = activateAlwaysEnabledFeatures(context) activateAbbreviationFeature(context, alwaysEnabledFeatures.docView) - return { - ...alwaysEnabledFeatures, - activatedLean4Features: new Promise(async (resolve, _) => { - const doc: TextDocument | undefined = findOpenLeanDocument() - if (doc) { - const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features( - context, - alwaysEnabledFeatures.installer, - ) - resolve(lean4EnabledFeatures) - } else { - // No Lean 4 document yet => Load remaining features when one is open - const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => { - if (isLean4Document(doc)) { - const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features( - context, - alwaysEnabledFeatures.installer, - ) - resolve(lean4EnabledFeatures) - disposeActivationListener.dispose() - } - }, context.subscriptions) - } - }), - } + const lean4EnabledFeatures: Promise = new Promise(async (resolve, _) => { + const doc: TextDocument | undefined = findOpenLeanDocument() + if (doc) { + const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features( + context, + alwaysEnabledFeatures.installer, + ) + resolve(lean4EnabledFeatures) + } else { + // No Lean 4 document yet => Load remaining features when one is open + const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => { + if (isLean4Document(doc)) { + const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features( + context, + alwaysEnabledFeatures.installer, + ) + resolve(lean4EnabledFeatures) + disposeActivationListener.dispose() + } + }, context.subscriptions) + } + }) + + return new Exports(alwaysEnabledFeatures, lean4EnabledFeatures) } diff --git a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts index cbe4bfd6a..d85357fcc 100644 --- a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts +++ b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts @@ -22,15 +22,15 @@ suite('Lean4 Bootstrap Test Suite', () => { // this will wait up to 60 seconds to do full elan lean install, so test machines better // be able to do that. - const lean = await initLean4Untitled('#eval Lean.versionString') - const info = lean.exports.infoProvider + const features = await initLean4Untitled('#eval Lean.versionString') + const info = features.infoProvider const expected = '4.0.0-nightly-' assert(info, 'No InfoProvider export') // give it a extra long timeout in case test machine is really slow. logger.log('Wait for elan install of Lean nightly build...') - await waitForActiveClient(lean.exports.clientProvider, 120) - await waitForActiveClientRunning(lean.exports.clientProvider, 300) + await waitForActiveClient(features.clientProvider, 120) + await waitForActiveClientRunning(features.clientProvider, 300) const hackNeeded = false if (hackNeeded) { @@ -69,8 +69,8 @@ suite('Lean4 Bootstrap Test Suite', () => { void vscode.window.showInformationMessage('Running tests: ' + __dirname) // Lean is already installed so this should be quick. - const lean = await initLean4Untitled('#eval Lean.versionString') - const info = lean.exports.infoProvider + const features = await initLean4Untitled('#eval Lean.versionString') + const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('Wait for Lean nightly build server to start...') diff --git a/vscode-lean4/test/suite/docview/docview.test.ts b/vscode-lean4/test/suite/docview/docview.test.ts index 5d3f29d28..b65789b42 100644 --- a/vscode-lean4/test/suite/docview/docview.test.ts +++ b/vscode-lean4/test/suite/docview/docview.test.ts @@ -26,8 +26,8 @@ suite('Documentation View Test Suite', () => { void vscode.window.showInformationMessage('Running tests: ' + __dirname) const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') const mainFile = path.join(testsRoot, 'Main.lean') - const lean = await initLean4(mainFile) - const info = lean.exports.infoProvider + const features = await initLean4(mainFile) + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedVersion = 'Hello:' let html = await waitForInfoviewHtml(info, expectedVersion) @@ -36,7 +36,7 @@ suite('Documentation View Test Suite', () => { await vscode.commands.executeCommand('lean4.docView.open') - const docView = lean.exports.docView + const docView = features.docView assert(docView, 'No docView export') const expectedMenuItem = 'Abbreviations Cheatsheet' html = await waitForDocViewHtml(docView, expectedMenuItem) diff --git a/vscode-lean4/test/suite/info/info.test.ts b/vscode-lean4/test/suite/info/info.test.ts index c27d0cb39..72f0df9e7 100644 --- a/vscode-lean4/test/suite/info/info.test.ts +++ b/vscode-lean4/test/suite/info/info.test.ts @@ -24,8 +24,8 @@ suite('InfoView Test Suite', () => { const b = 22 const expectedEval1 = (a * b).toString() - const lean = await initLean4Untitled(`#eval ${a}*${b}`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval ${a}*${b}`) + const info = features.infoProvider assert(info, 'No InfoProvider export') await assertStringInInfoview(info, expectedEval1) @@ -49,8 +49,8 @@ suite('InfoView Test Suite', () => { const c = 77 const d = 7 - const lean = await initLean4Untitled(`#eval ${a}*${b}`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval ${a}*${b}`) + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedEval1 = (a * b).toString() @@ -84,12 +84,12 @@ suite('InfoView Test Suite', () => { const expectedEval = '[1, 2, 3]' - const lean = await initLean4Untitled('#eval [1, 1+1, 1+1+1] \n') + const features = await initLean4Untitled('#eval [1, 1+1, 1+1+1] \n') const editor = await waitForActiveEditor() const firstLine = editor.document.lineAt(0).range editor.selection = new vscode.Selection(firstLine.end, firstLine.end) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') await waitForInfoviewHtml(info, expectedEval, 30, 1000, false) @@ -127,8 +127,8 @@ suite('InfoView Test Suite', () => { const b = 95 const prefix = 'Lean version is:' - const lean = await initLean4Untitled(`#eval ${a}*${b}`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval ${a}*${b}`) + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedEval = (a * b).toString() diff --git a/vscode-lean4/test/suite/lean3/lean3.test.ts b/vscode-lean4/test/suite/lean3/lean3.test.ts index e46b746f9..31924fd54 100644 --- a/vscode-lean4/test/suite/lean3/lean3.test.ts +++ b/vscode-lean4/test/suite/lean3/lean3.test.ts @@ -3,7 +3,12 @@ import { suite } from 'mocha' import * as path from 'path' import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' -import { closeAllEditors, waitForActiveEditor, waitForActiveExtension } from '../utils/helpers' +import { + assertLean4FeaturesNotLoaded, + closeAllEditors, + waitForActiveEditor, + waitForActiveExtension, +} from '../utils/helpers' suite('Lean3 Compatibility Test Suite', () => { test('Lean3 project', async () => { @@ -21,7 +26,7 @@ suite('Lean3 Compatibility Test Suite', () => { const lean = await waitForActiveExtension('leanprover.lean4') assert(lean, 'Lean extension not loaded') - assert(!lean.exports.isLean4Project, 'Lean4 extension should not be running!') + await assertLean4FeaturesNotLoaded(lean.exports) logger.log('Checking vscode commands...') const cmds = await vscode.commands.getCommands(true) diff --git a/vscode-lean4/test/suite/multi/multi.test.ts b/vscode-lean4/test/suite/multi/multi.test.ts index 3c34bac53..db47563cc 100644 --- a/vscode-lean4/test/suite/multi/multi.test.ts +++ b/vscode-lean4/test/suite/multi/multi.test.ts @@ -13,10 +13,10 @@ suite('Multi-Folder Test Suite', () => { void vscode.window.showInformationMessage('Running tests: ' + __dirname) const multiRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'multi') - const lean = await initLean4(path.join(multiRoot, 'test', 'Main.lean')) + const features = await initLean4(path.join(multiRoot, 'test', 'Main.lean')) // verify we have a nightly build running in this folder. - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') await assertStringInInfoview(info, '4.0.0-nightly-') @@ -30,7 +30,7 @@ suite('Multi-Folder Test Suite', () => { await assertStringInInfoview(info, version) // Now verify we have 2 LeanClients running. - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') const actual = clients.getClients().length assert(actual === 2, 'Expected 2 LeanClients to be running, but found ' + actual) diff --git a/vscode-lean4/test/suite/pre-bootstrap/user.test.ts b/vscode-lean4/test/suite/pre-bootstrap/user.test.ts index 53993bdae..0c0a8a131 100644 --- a/vscode-lean4/test/suite/pre-bootstrap/user.test.ts +++ b/vscode-lean4/test/suite/pre-bootstrap/user.test.ts @@ -14,10 +14,9 @@ suite('Lean4 Pre-bootstrap Test Suite', () => { // this will wait up to 60 seconds to do full elan lean install, so test machines better // be able to do that. - const promptUser = true const projectRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') - const lean = await initLean4(path.join(projectRoot, 'Main.lean')) - const info = lean.exports.infoProvider + const features = await initLean4(path.join(projectRoot, 'Main.lean')) + const info = features.infoProvider const expected1 = 'Waiting for Lean server to start...' const expected2 = 'nightly' // lean was already installed before this test started! assert(info, 'No InfoProvider export') @@ -33,7 +32,7 @@ suite('Lean4 Pre-bootstrap Test Suite', () => { let retries = 10 while (html.indexOf(expected1) > 0) { - const installer = lean.exports.installer + const installer = features.installer if (!installer?.isPromptVisible()) { html = await waitForInfoviewLambda(info, lambda, 10) retries-- diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts index 634b66553..fca7a8c4b 100644 --- a/vscode-lean4/test/suite/restarts/restarts.test.ts +++ b/vscode-lean4/test/suite/restarts/restarts.test.ts @@ -28,14 +28,14 @@ suite('Lean Server Restart Test Suite', () => { // add normal values to initialize lean4 file const hello = 'Hello World' - const lean = await initLean4Untitled(`#eval "${hello}"`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval "${hello}"`) + const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('make sure language server is up and running.') await assertStringInInfoview(info, hello) - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') logger.log('Insert eval that causes crash.') @@ -73,14 +73,14 @@ suite('Lean Server Restart Test Suite', () => { // add normal values to initialize lean4 file const hello = 'Hello World' - const lean = await initLean4Untitled(`#eval "${hello}"`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval "${hello}"`) + const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('make sure language server is up and running.') await assertStringInInfoview(info, hello) - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') logger.log('Insert eval that causes crash.') @@ -119,9 +119,9 @@ suite('Lean Server Restart Test Suite', () => { // run this code twice to ensure that it still works after a Restart Server for (let i = 0; i < 2; i++) { - const lean = await initLean4(path.join(simpleRoot, 'Main.lean')) + const features = await initLean4(path.join(simpleRoot, 'Main.lean')) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') const activeEditor = vscode.window.activeTextEditor @@ -139,7 +139,7 @@ suite('Lean Server Restart Test Suite', () => { logger.log(`>>> Found "${versionString}" in infoview`) logger.log('Now invoke the restart server command') - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') const client = clients.getClientForFolder(new FileUri(simpleRoot)) if (client) { diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts index 574b79966..4f0591dda 100644 --- a/vscode-lean4/test/suite/simple/simple.test.ts +++ b/vscode-lean4/test/suite/simple/simple.test.ts @@ -29,8 +29,8 @@ suite('Lean4 Basics Test Suite', () => { logger.log(`=================== Untitled Lean File ${getElanMode()} ===================`) void vscode.window.showInformationMessage('Running tests: ' + __dirname) - const lean = await initLean4Untitled('#eval Lean.versionString') - const info = lean.exports.infoProvider + const features = await initLean4Untitled('#eval Lean.versionString') + const info = features.infoProvider assert(info, 'No InfoProvider export') await assertStringInInfoview(info, '4.0.0-nightly-') @@ -63,14 +63,14 @@ suite('Lean4 Basics Test Suite', () => { void vscode.window.showInformationMessage('Running tests: ' + __dirname) const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'orphan') - const lean = await initLean4(path.join(testsRoot, 'factorial.lean')) + const features = await initLean4(path.join(testsRoot, 'factorial.lean')) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedVersion = '5040' // the factorial function works. const html = await waitForInfoviewHtml(info, expectedVersion) - const installer = lean.exports.installer + const installer = features.installer assert(installer, 'No LeanInstaller export') const toolChains = await installer.elanListToolChains(new UntitledUri()) let defaultToolChain = toolChains.find(tc => tc.indexOf('default') > 0) @@ -101,9 +101,9 @@ suite('Lean4 Basics Test Suite', () => { // and again using "open folder" mode. const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') - const lean = await initLean4(path.join(testsRoot, 'Main.lean')) + const features = await initLean4(path.join(testsRoot, 'Main.lean')) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') let expectedVersion = 'Hello:' let html = await waitForInfoviewHtml(info, expectedVersion) diff --git a/vscode-lean4/test/suite/toolchains/toolchain.test.ts b/vscode-lean4/test/suite/toolchains/toolchain.test.ts index a83cc4bec..4a1c86094 100644 --- a/vscode-lean4/test/suite/toolchains/toolchain.test.ts +++ b/vscode-lean4/test/suite/toolchains/toolchain.test.ts @@ -21,12 +21,12 @@ suite('Toolchain Test Suite', () => { const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') - const lean = await initLean4(path.join(testsRoot, 'Main.lean')) + const features = await initLean4(path.join(testsRoot, 'Main.lean')) // turn off the user prompts so restart of lean server happens automatically. - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') - const installer = lean.exports.installer + const installer = features.installer assert(installer, 'No LeanInstaller export') // wait for info view to show up. diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index aff2950cd..5e85931a8 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -4,7 +4,7 @@ import * as os from 'os' import { basename, join } from 'path' import * as vscode from 'vscode' import { DocViewProvider } from '../../../src/docview' -import { Exports } from '../../../src/exports' +import { EnabledFeatures, Exports } from '../../../src/exports' import { InfoProvider } from '../../../src/infoview' import { LeanClient } from '../../../src/leanclient' import { LeanClientProvider } from '../../../src/utils/clientProvider' @@ -31,13 +31,12 @@ export function assertAndLog(value: unknown, message: string): asserts value { assert(value, message) } -export async function initLean4(fileName: string): Promise> { +export async function initLean4(fileName: string): Promise { await closeAllEditors() const options: vscode.TextDocumentShowOptions = { preview: false } const lean = await waitForActiveExtension('leanprover.lean4', 60) assertAndLog(lean, 'Lean extension not loaded') - assertAndLog(lean.exports.isLean4Project, 'Lean extension is not a lean4 project') assertAndLog(lean.isActive, 'Lean extension is not active') logger.log(`Found lean package version: ${lean.packageJSON.version}`) @@ -45,11 +44,12 @@ export async function initLean4(fileName: string): Promise { @@ -77,7 +77,7 @@ export async function deleteAllText(): Promise { }) } -export async function initLean4Untitled(contents: string): Promise> { +export async function initLean4Untitled(contents: string): Promise { // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() @@ -95,13 +95,14 @@ export async function initLean4Untitled(contents: string): Promise { + logger.log('Waiting for Lean 4 feature exports of extension to be loaded...') + const allFeatures: EnabledFeatures | undefined = await new Promise(async (resolve, _) => { + setTimeout(() => resolve(undefined), timeout) + await exports.allFeatures() + }) + assertAndLog(allFeatures, 'Lean 4 features did not activate.') + logger.log('Lean 4 feature exports loaded.') + return allFeatures +} + +export async function assertLean4FeaturesNotLoaded(exports: Exports) { + logger.log('Waiting for Lean 4 feature exports of extension to be loaded...') + const allFeatures: EnabledFeatures | undefined = await new Promise(async (resolve, _) => { + setTimeout(() => resolve(undefined), 5000) + await exports.allFeatures() + }) + assertAndLog(!allFeatures, 'Lean 4 features activated when they should not have been activated.') + logger.log('Lean 4 features correctly did not load.') +} + export async function waitForActiveEditor(filename = '', retries = 60, delay = 1000): Promise { let count = 0 while (!vscode.window.activeTextEditor && count < retries) { @@ -221,11 +243,15 @@ export async function waitForActiveEditor(filename = '', retries = 60, delay = 1 return editor } -export async function waitForActiveInfoProvider(exports: Exports, retries = 60, delay = 1000): Promise { +export async function waitForActiveInfoProvider( + features: EnabledFeatures, + retries = 60, + delay = 1000, +): Promise { logger.log('Waiting for info view provider to be loaded...') let count = 0 - while (!exports.infoProvider) { + while (!features.infoProvider) { count += 1 if (count >= retries) { logger.log('Info view provider did not load.')