Assorted test fixes

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<Exports> {
     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<Exports> {
             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<Exports> {
             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<Exports> {
         docView: alwaysEnabledFeatures.docView,
         projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider
     }
+    return extensionExports
 }

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 },

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();

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

vscode-lean4/test/suite/utils/helpers.ts

@@ -38,17 +38,17 @@ export async function initLean4(fileName: string) : Promise<vscode.Extension<Exp
     await closeAllEditors();
     const options : vscode.TextDocumentShowOptions = { preview: false };
 
-    const doc = await vscode.workspace.openTextDocument(fileName);
-    await vscode.window.showTextDocument(doc, options);
-
     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;
 	assertAndLog(info, 'No InfoProvider export');
     assertAndLog(await waitForInfoViewOpen(info, 60),
@@ -202,6 +202,23 @@ export async function waitForActiveEditor(filename='', retries=60, delay=1000) :
     return editor;
 }
 
+export async function waitForActiveInfoProvider(exports: Exports, retries=60, delay=1000) : Promise<boolean> {
+    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<boolean> {
     let count = 0;
     let opened = false;
@@ -374,7 +391,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');