chore: adjust tests for adjusted activation logic

vscode-lean4/src/exports.ts

@@ -19,6 +19,19 @@ export interface Lean4EnabledFeatures {
     projectOperationProvider: ProjectOperationProvider
 }
 
-export interface Exports extends AlwaysEnabledFeatures {
-    activatedLean4Features: Thenable<Lean4EnabledFeatures>
+export interface EnabledFeatures extends AlwaysEnabledFeatures, Lean4EnabledFeatures {}
+
+export class Exports {
+    alwaysEnabledFeatures: AlwaysEnabledFeatures
+    lean4EnabledFeatures: Promise<Lean4EnabledFeatures>
+
+    constructor(alwaysEnabledFeatures: AlwaysEnabledFeatures, lean4EnabledFeatures: Promise<Lean4EnabledFeatures>) {
+        this.alwaysEnabledFeatures = alwaysEnabledFeatures
+        this.lean4EnabledFeatures = lean4EnabledFeatures
+    }
+
+    async allFeatures(): Promise<EnabledFeatures> {
+        const lean4EnabledFeatures = await this.lean4EnabledFeatures
+        return { ...this.alwaysEnabledFeatures, ...lean4EnabledFeatures }
+    }
 }

vscode-lean4/src/extension.ts

@@ -155,29 +155,28 @@ export async function activate(context: ExtensionContext): Promise<Exports> {
     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<Lean4EnabledFeatures> = 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)
 }

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...')

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)

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.

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,25 +31,25 @@ export function assertAndLog(value: unknown, message: string): asserts value {
     assert(value, message)
 }
 
-export async function initLean4(fileName: string): Promise<vscode.Extension<Exports>> {
+export async function initLean4(fileName: string): Promise<EnabledFeatures> {
     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}`)
 
     const doc = await vscode.workspace.openTextDocument(fileName)
     await vscode.window.showTextDocument(doc, options)
 
     await waitForActiveEditor(basename(fileName))
-    assertAndLog(await waitForActiveInfoProvider(lean.exports), 'Info view provider did not load after 60 seconds')
-    const info = lean.exports.infoProvider
+    const features = await waitForLean4FeatureActivation(lean.exports)
+    assertAndLog(await waitForActiveInfoProvider(features), 'Info view provider did not load after 60 seconds')
+    const info = features.infoProvider
     assertAndLog(info, 'No InfoProvider export')
     assertAndLog(await waitForInfoViewOpen(info, 60), 'Info view did not open after 20 seconds')
-    return lean
+    return features
 }
 
 export async function insertText(text: string): Promise<void> {
@@ -77,7 +77,7 @@ export async function deleteAllText(): Promise<void> {
     })
 }
 
-export async function initLean4Untitled(contents: string): Promise<vscode.Extension<Exports>> {
+export async function initLean4Untitled(contents: string): Promise<EnabledFeatures> {
     // 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<vscode.Extens
     const lean = await waitForActiveExtension('leanprover.lean4', 60)
     assertAndLog(lean, 'Lean extension not loaded')
     logger.log(`Found lean package version: ${lean.packageJSON.version}`)
-    const info = lean.exports.infoProvider
+    const features = await waitForLean4FeatureActivation(lean.exports)
+    const info = features.infoProvider
     assertAndLog(info, 'No InfoProvider export')
 
     // If info view opens too quickly there is no LeanClient ready yet and
     // it's initialization gets messed up.
     assertAndLog(await waitForInfoViewOpen(info, 60), 'Info view did not open after 60 seconds')
-    return lean
+    return features
 }
 
 export async function waitForActiveClientRunning(
@@ -190,6 +191,17 @@ export async function waitForActiveExtension(
     return lean
 }
 
+export async function waitForLean4FeatureActivation(exports: Exports, timeout = 60000): Promise<EnabledFeatures> {
+    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 waitForActiveEditor(filename = '', retries = 60, delay = 1000): Promise<vscode.TextEditor> {
     let count = 0
     while (!vscode.window.activeTextEditor && count < retries) {
@@ -221,11 +233,15 @@ export async function waitForActiveEditor(filename = '', retries = 60, delay = 1
     return editor
 }
 
-export async function waitForActiveInfoProvider(exports: Exports, retries = 60, delay = 1000): Promise<boolean> {
+export async function waitForActiveInfoProvider(
+    features: EnabledFeatures,
+    retries = 60,
+    delay = 1000,
+): Promise<boolean> {
     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.')