From c537caffae0cf005e5aa51014292834b38c98a33 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Wed, 18 Oct 2023 17:44:30 +0200 Subject: [PATCH 1/6] lazily fill exports --- vscode-lean4/src/extension.ts | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index e254000de..07f06ab2c 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -159,12 +159,14 @@ async function activateLean4Features(context: ExtensionContext, installer: LeanI return { clientProvider, infoProvider, projectOperationProvider } } +let extensionExports: Exports + export async function activate(context: ExtensionContext): Promise { await setLeanFeatureSetActive(false) const alwaysEnabledFeatures: AlwaysEnabledFeatures = activateAlwaysEnabledFeatures(context) if (await isLean3Project(alwaysEnabledFeatures.installer)) { - return { + extensionExports = { isLean4Project: false, version: '3', infoProvider: undefined, @@ -174,13 +176,14 @@ export async function activate(context: ExtensionContext): Promise { docView: alwaysEnabledFeatures.docView, projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider } + return extensionExports } activateAbbreviationFeature(context, alwaysEnabledFeatures.docView) if (findOpenLeanDocument()) { const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(context, alwaysEnabledFeatures.installer) - return { + extensionExports = { isLean4Project: true, version: '4', infoProvider: lean4EnabledFeatures.infoProvider, @@ -190,17 +193,21 @@ export async function activate(context: ExtensionContext): Promise { docView: alwaysEnabledFeatures.docView, projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider } + return extensionExports } // No Lean 4 document yet => Load remaining features when one is open const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => { if (isLean(doc.languageId)) { - await activateLean4Features(context, alwaysEnabledFeatures.installer) + const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(context, alwaysEnabledFeatures.installer) + extensionExports.infoProvider = lean4EnabledFeatures.infoProvider + extensionExports.clientProvider = lean4EnabledFeatures.clientProvider + extensionExports.projectOperationProvider = lean4EnabledFeatures.projectOperationProvider disposeActivationListener.dispose() } }, context.subscriptions) - return { + extensionExports = { isLean4Project: true, version: '4', infoProvider: undefined, @@ -210,4 +217,5 @@ export async function activate(context: ExtensionContext): Promise { docView: alwaysEnabledFeatures.docView, projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider } + return extensionExports } From e14d04ba901930aba2ee3d019b60c117001b6d49 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Wed, 18 Oct 2023 18:13:39 +0200 Subject: [PATCH 2/6] test: wait for infoviewprovider --- vscode-lean4/test/suite/utils/helpers.ts | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index 46083a91b..8197dbd02 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -49,6 +49,7 @@ export async function initLean4(fileName: string) : Promise { + logger.log('Waiting for info view provider to be loaded...'); + + let count = 0; + while (!exports.infoProvider) { + count += 1; + if (count >= retries){ + logger.log('Info view provider did not load.') + return false; + } + await sleep(delay); + } + + logger.log('Info view provider loaded.') + return true +} + export async function waitForInfoViewOpen(infoView: InfoProvider, retries=60, delay=1000) : Promise { let count = 0; let opened = false; From 5cab99c6471294e7ebeabe8977d74ef6e42d216a Mon Sep 17 00:00:00 2001 From: mhuisi Date: Wed, 18 Oct 2023 19:21:25 +0200 Subject: [PATCH 3/6] test: don't show modal dialogs in tests --- vscode-lean4/src/utils/clientProvider.ts | 9 +++++++-- vscode-lean4/test/suite/utils/helpers.ts | 2 +- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index e24f81c14..f2d443e25 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -48,7 +48,7 @@ export class LeanClientProvider implements Disposable { this.subscriptions.push( commands.registerCommand('lean4.restartFile', () => this.restartFile()), commands.registerCommand('lean4.refreshFileDependencies', () => this.restartFile()), - commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()), + commands.registerCommand('lean4.restartServer', showDialog => this.restartActiveClient(showDialog ?? true)), commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()) ); @@ -155,7 +155,12 @@ export class LeanClientProvider implements Disposable { } } - private async restartActiveClient() { + private async restartActiveClient(showDialog: boolean = true) { + if (!showDialog) { + void this.activeClient?.restart(); + return + } + const result: string | undefined = await window.showInformationMessage( 'Restart Lean 4 server to re-elaborate all open files?', { modal: true }, diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index 8197dbd02..4ee946f41 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -392,7 +392,7 @@ export async function restartLeanServer(client: LeanClient, retries=60, delay=10 client.restarted(() => { stateChanges.push('restarted'); }); client.serverFailed(() => { stateChanges.push('failed'); }); - await vscode.commands.executeCommand('lean4.restartServer'); + await vscode.commands.executeCommand('lean4.restartServer', false); while (count < retries){ const index = stateChanges.indexOf('restarted'); From 3b205d188d678039aca6d921777ae21814f2ee6c Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 19 Oct 2023 11:00:43 +0200 Subject: [PATCH 4/6] test: add missing message --- vscode-lean4/test/suite/toolchains/toolchain.test.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/vscode-lean4/test/suite/toolchains/toolchain.test.ts b/vscode-lean4/test/suite/toolchains/toolchain.test.ts index 64f5c424b..94228a75b 100644 --- a/vscode-lean4/test/suite/toolchains/toolchain.test.ts +++ b/vscode-lean4/test/suite/toolchains/toolchain.test.ts @@ -13,6 +13,7 @@ suite('Toolchain Test Suite', () => { test('Edit lean-toolchain version', async () => { logger.log('=================== Edit lean-toolchain version ==================='); + void vscode.window.showInformationMessage('Running tests: ' + __dirname); const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple'); From d3f06e451048cb32ec09ce08cae77b5b21969c97 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 19 Oct 2023 11:11:18 +0200 Subject: [PATCH 5/6] test: adjust waiting logic for new activation logic --- vscode-lean4/test/suite/utils/helpers.ts | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index 4ee946f41..b70f8b190 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -38,16 +38,15 @@ export async function initLean4(fileName: string) : Promise Date: Thu, 19 Oct 2023 15:41:19 +0200 Subject: [PATCH 6/6] address unstable test? --- vscode-lean4/package-lock.json | 4 ++-- vscode-lean4/test/suite/restarts/restarts.test.ts | 10 ++++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/vscode-lean4/package-lock.json b/vscode-lean4/package-lock.json index 1ae58c497..ff47451eb 100644 --- a/vscode-lean4/package-lock.json +++ b/vscode-lean4/package-lock.json @@ -1,12 +1,12 @@ { "name": "lean4", - "version": "0.0.115", + "version": "0.0.116", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "lean4", - "version": "0.0.115", + "version": "0.0.116", "license": "Apache-2.0", "dependencies": { "axios": "~0.24.0", diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts index 4e031ab86..da361da20 100644 --- a/vscode-lean4/test/suite/restarts/restarts.test.ts +++ b/vscode-lean4/test/suite/restarts/restarts.test.ts @@ -113,6 +113,16 @@ suite('Lean Server Restart Test Suite', () => { const info = lean.exports.infoProvider; assert(info, 'No InfoProvider export'); + + const activeEditor = vscode.window.activeTextEditor + assert(activeEditor, 'No active text editor') + const evalLine = '#eval main' + const startOffset = activeEditor.document.getText().indexOf(evalLine) + assert(startOffset !== -1, 'Cannot find #eval in Main.lean') + const endOffset = startOffset + evalLine.length + const endPos = activeEditor.document.positionAt(endOffset) + activeEditor.selection = new vscode.Selection(endPos, endPos) + const expectedVersion = 'Hello:'; const html = await waitForInfoviewHtml(info, expectedVersion); const versionString = extractPhrase(html, 'Hello:', '<').trim();