feat: [lean4web] abstract lean client setup for websocket clients

vscode-lean4/src/extension.ts

@@ -10,6 +10,7 @@ import { PreconditionCheckResult, SetupNotificationOptions } from './diagnostics
 import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports'
 import { InfoProvider } from './infoview'
 import { LeanClient } from './leanclient'
+import { setupClient } from './leanclientsetup'
 import { LoogleView } from './loogleview'
 import { ManualView } from './manualview'
 import { MoogleView } from './moogleview'
@@ -177,7 +178,7 @@ async function activateLean4Features(
     installer: LeanInstaller,
     elanCommandProvider: ElanCommandProvider,
 ): Promise<Lean4EnabledFeatures> {
-    const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel())
+    const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel(), setupClient)
     elanCommandProvider.setClientProvider(clientProvider)
     context.subscriptions.push(clientProvider)
 

vscode-lean4/src/leanclient.ts

@@ -13,16 +13,15 @@ import {
     WorkspaceFolder,
 } from 'vscode'
 import {
+    BaseLanguageClient,
     DiagnosticSeverity,
     DidChangeTextDocumentParams,
     DidCloseTextDocumentParams,
     DocumentFilter,
     InitializeResult,
-    LanguageClient,
     LanguageClientOptions,
     PublishDiagnosticsParams,
     RevealOutputChannelOn,
-    ServerOptions,
     State,
 } from 'vscode-languageclient/node'
 import * as ls from 'vscode-languageserver-protocol'
@@ -31,9 +30,6 @@ import { LeanFileProgressParams, LeanFileProgressProcessingInfo, ServerStoppedRe
 import {
     getElaborationDelay,
     getFallBackToStringOccurrenceHighlighting,
-    serverArgs,
-    serverLoggingEnabled,
-    serverLoggingPath,
     shouldAutofocusOutput,
 } from './config'
 import { logger } from './utils/logger'
@@ -50,15 +46,14 @@ import {
     displayNotificationWithOptionalInput,
     displayNotificationWithOutput,
 } from './utils/notifs'
-import { willUseLakeServer } from './utils/projectInfo'
 
 const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
 
 export type ServerProgress = Map<ExtUri, LeanFileProgressProcessingInfo[]>
 
 export class LeanClient implements Disposable {
     running: boolean
-    private client: LanguageClient | undefined
+    private client: BaseLanguageClient | undefined
     private outputChannel: OutputChannel
     folderUri: ExtUri
     private subscriptions: Disposable[] = []
@@ -106,7 +101,13 @@ export class LeanClient implements Disposable {
     private serverFailedEmitter = new EventEmitter<string>()
     serverFailed = this.serverFailedEmitter.event
 
-    constructor(folderUri: ExtUri, outputChannel: OutputChannel) {
+    constructor(folderUri: ExtUri, outputChannel: OutputChannel,
+        private setupClient: (
+            toolchainOverride: string | undefined,
+            clientOptions: LanguageClientOptions,
+            folderUri: ExtUri,
+        ) => Promise<BaseLanguageClient>,
+    ) {
         this.outputChannel = outputChannel
         this.folderUri = folderUri
         this.subscriptions.push(new Disposable(() => this.staleDepNotifier?.dispose()))
@@ -253,7 +254,7 @@ export class LeanClient implements Disposable {
         const toolchainOverride: string | undefined =
             toolchainOverrideResult.kind === 'Override' ? toolchainOverrideResult.toolchain : undefined
 
-        this.client = await this.setupClient(toolchainOverride)
+        this.client = await this.setupClient(toolchainOverride, this.obtainClientOptions(), this.folderUri)
 
         let insideRestart = true
         try {
@@ -502,43 +503,6 @@ export class LeanClient implements Disposable {
         return this.running ? this.client?.initializeResult : undefined
     }
 
-    private async determineServerOptions(toolchainOverride: string | undefined): Promise<ServerOptions> {
-        const env = Object.assign({}, process.env)
-        if (serverLoggingEnabled()) {
-            env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
-        }
-
-        const [serverExecutable, options] = await this.determineExecutable()
-        if (toolchainOverride) {
-            options.unshift('+' + toolchainOverride)
-        }
-
-        const cwd = this.folderUri.scheme === 'file' ? this.folderUri.fsPath : undefined
-        if (cwd) {
-            // Add folder name to command-line so that it shows up in `ps aux`.
-            options.push(cwd)
-        } else {
-            options.push('untitled')
-        }
-
-        return {
-            command: serverExecutable,
-            args: options.concat(serverArgs()),
-            options: {
-                cwd,
-                env,
-            },
-        }
-    }
-
-    private async determineExecutable(): Promise<[string, string[]]> {
-        if (await willUseLakeServer(this.folderUri)) {
-            return ['lake', ['serve', '--']]
-        } else {
-            return ['lean', ['--server']]
-        }
-    }
-
     private obtainClientOptions(): LanguageClientOptions {
         const documentSelector: DocumentFilter = {
             language: 'lean4',
@@ -667,14 +631,4 @@ export class LeanClient implements Disposable {
             },
         }
     }
-
-    private async setupClient(toolchainOverride: string | undefined): Promise<LanguageClient> {
-        const serverOptions: ServerOptions = await this.determineServerOptions(toolchainOverride)
-        const clientOptions: LanguageClientOptions = this.obtainClientOptions()
-
-        const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
-
-        patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter)
-        return client
-    }
 }

vscode-lean4/src/leanclientsetup.ts

@@ -0,0 +1,55 @@
+import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node'
+import { serverArgs, serverLoggingEnabled, serverLoggingPath } from './config'
+import { ExtUri } from './utils/exturi'
+import { willUseLakeServer } from './utils/projectInfo'
+import { c2pConverter, p2cConverter, patchConverters, setDependencyBuildMode } from './utils/converters'
+
+async function determineExecutable(folderUri: ExtUri): Promise<[string, string[]]> {
+    if (await willUseLakeServer(folderUri)) {
+        return ['lake', ['serve', '--']]
+    } else {
+        return ['lean', ['--server']]
+    }
+}
+
+async function determineServerOptions(toolchainOverride: string | undefined, folderUri: ExtUri): Promise<ServerOptions> {
+    const env = Object.assign({}, process.env)
+    if (serverLoggingEnabled()) {
+        env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
+    }
+
+    const [serverExecutable, options] = await determineExecutable(folderUri)
+    if (toolchainOverride) {
+        options.unshift('+' + toolchainOverride)
+    }
+
+    const cwd = this.folderUri.scheme === 'file' ? this.folderUri.fsPath : undefined
+    if (cwd) {
+        // Add folder name to command-line so that it shows up in `ps aux`.
+        options.push(cwd)
+    } else {
+        options.push('untitled')
+    }
+
+    return {
+        command: serverExecutable,
+        args: options.concat(serverArgs()),
+        options: {
+            cwd,
+            env,
+        },
+    }
+}
+
+export async function setupClient(
+    toolchainOverride: string | undefined,
+    clientOptions: LanguageClientOptions,
+    folderUri: ExtUri,
+): Promise<LanguageClient> {
+    const serverOptions: ServerOptions = await this.determineServerOptions(toolchainOverride, folderUri)
+
+    const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
+
+    patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter)
+    return client
+}

vscode-lean4/src/utils/clientProvider.ts

@@ -1,6 +1,7 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
 import path from 'path'
 import { Disposable, EventEmitter, OutputChannel, commands, workspace } from 'vscode'
+import { BaseLanguageClient, LanguageClientOptions } from 'vscode-languageclient/node'
 import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics'
 import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs'
 import { LeanClient } from '../leanclient'
@@ -58,7 +59,15 @@ export class LeanClientProvider implements Disposable {
     private clientStoppedEmitter = new EventEmitter<[LeanClient, boolean, ServerStoppedReason]>()
     clientStopped = this.clientStoppedEmitter.event
 
-    constructor(installer: LeanInstaller, outputChannel: OutputChannel) {
+    constructor(
+        installer: LeanInstaller,
+        outputChannel: OutputChannel,
+        private setupClient: (
+            toolchainOverride: string | undefined,
+            clientOptions: LanguageClientOptions,
+            folderUri: ExtUri,
+        ) => Promise<BaseLanguageClient>,
+    ) {
         this.outputChannel = outputChannel
         this.installer = installer
 
@@ -269,7 +278,7 @@ export class LeanClientProvider implements Disposable {
         }
 
         logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString())
-        client = new LeanClient(folderUri, this.outputChannel)
+        client = new LeanClient(folderUri, this.outputChannel, this.setupClient)
         this.subscriptions.push(client)
         this.clients.set(key, client)