fix: error when installing elan while running server

vscode-lean4/src/extension.ts

@@ -208,6 +208,7 @@ async function activateLean4Features(
 ): Promise<Lean4EnabledFeatures> {
     const clientProvider = new LeanClientProvider(installer.getOutputChannel())
     elanCommandProvider.setClientProvider(clientProvider)
+    installer.setClientProvider(clientProvider)
     context.subscriptions.push(clientProvider)
 
     const infoProvider = new InfoProvider(clientProvider, context)

vscode-lean4/src/leanclient.ts

@@ -584,23 +584,24 @@ export class LeanClient implements Disposable {
         ])
     }
 
-    async withStoppedClient(action: () => Promise<void>): Promise<'Success' | 'IsRestarting'> {
+    async withStoppedClient<T>(
+        action: () => Promise<T>,
+    ): Promise<{ kind: 'Success'; result: T } | { kind: 'IsRestarting' }> {
         if (this.isRestarting) {
-            return 'IsRestarting'
+            return { kind: 'IsRestarting' }
         }
         this.isRestarting = true // Ensure that client cannot be restarted in the mean-time
+        let result: T
         try {
             if (this.isStarted()) {
                 await this.stop()
             }
-
-            await action()
+            result = await action()
         } finally {
             this.isRestarting = false
         }
-
         await this.restart()
-        return 'Success'
+        return { kind: 'Success', result }
     }
 
     isInFolderManagedByThisClient(uri: ExtUri): boolean {

vscode-lean4/src/projectoperations.ts

@@ -378,8 +378,8 @@ export class ProjectOperationProvider implements Disposable {
                 toolchainUpdateMode: 'DoNotUpdate',
             })
 
-            const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner))
-            if (result === 'IsRestarting') {
+            const result = await activeClient.withStoppedClient(() => command(lakeRunner))
+            if (result.kind === 'IsRestarting') {
                 displayNotification('Error', 'Cannot run project action while restarting the server.')
             }
         } finally {

vscode-lean4/src/utils/clientProvider.ts

@@ -227,6 +227,26 @@ export class LeanClientProvider implements Disposable {
         return Array.from(this.clients.values())
     }
 
+    withStoppedClients<T>(
+        action: () => Promise<T>,
+    ): Promise<{ kind: 'Success'; result: T } | { kind: 'IsRestarting' }> {
+        let combinedAction: () => Promise<{ kind: 'Success'; result: T } | { kind: 'IsRestarting' }> = async () => ({
+            kind: 'Success',
+            result: await action(),
+        })
+        for (const c of this.clients.values()) {
+            const previousCombinedAction = combinedAction
+            combinedAction = async () => {
+                const r = await c.withStoppedClient(previousCombinedAction)
+                if (r.kind === 'IsRestarting' || r.result.kind === 'IsRestarting') {
+                    return { kind: 'IsRestarting' }
+                }
+                return { kind: 'Success', result: r.result.result }
+            }
+        }
+        return combinedAction()
+    }
+
     getClientForFolder(folder: ExtUri): LeanClient | undefined {
         return this.clients.get(folder.toString())
     }

vscode-lean4/src/utils/leanInstaller.ts

@@ -8,6 +8,7 @@ import {
     displayModalResultError,
     displayResultError,
 } from './batch'
+import { LeanClientProvider } from './clientProvider'
 import { elanSelfUninstall, elanSelfUpdate, elanStableChannel, elanVersion, isElanEagerResolutionVersion } from './elan'
 import {
     NotificationSeverity,
@@ -64,6 +65,7 @@ export type ElanInstallationResult =
 
 export class LeanInstaller implements Disposable {
     private outputChannel: OutputChannel
+    private clientProvider: LeanClientProvider | undefined
     private pendingOperation: 'Install' | 'Update' | 'Uninstall' | undefined
 
     private subscriptions: Disposable[] = []
@@ -80,6 +82,10 @@ export class LeanInstaller implements Disposable {
         )
     }
 
+    setClientProvider(clientProvider: LeanClientProvider) {
+        this.clientProvider = clientProvider
+    }
+
     // Installation
 
     async displayInstallElanPrompt(severity: NotificationSeverity, reason: string | undefined): Promise<boolean> {
@@ -406,7 +412,15 @@ export class LeanInstaller implements Disposable {
             case undefined:
                 this.pendingOperation = kind
                 try {
-                    return await op()
+                    if (this.clientProvider === undefined) {
+                        return await op()
+                    }
+                    const r = await this.clientProvider.withStoppedClients(op)
+                    if (r.kind === 'IsRestarting') {
+                        displayNotification('Error', 'Cannot re-install Elan while a server is being restarted.')
+                        return 'PendingOperation'
+                    }
+                    return r.result
                 } finally {
                     this.pendingOperation = undefined
                 }