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,18 +13,15 @@ import {
     WorkspaceFolder,
 } from 'vscode'
 import {
-    ClientCapabilities,
+    BaseLanguageClient,
     DiagnosticSeverity,
     DidChangeTextDocumentParams,
     DidCloseTextDocumentParams,
     DocumentFilter,
     InitializeResult,
-    LanguageClient,
     LanguageClientOptions,
     RevealOutputChannelOn,
-    ServerOptions,
     State,
-    StaticFeature,
 } from 'vscode-languageclient/node'
 
 import {
@@ -33,25 +30,13 @@ import {
     LeanFileProgressProcessingInfo,
     ServerStoppedReason,
 } from '@leanprover/infoview-api'
-import {
-    getElaborationDelay,
-    getFallBackToStringOccurrenceHighlighting,
-    serverArgs,
-    serverLoggingEnabled,
-    serverLoggingPath,
-    shouldAutofocusOutput,
-} from './config'
+import { getElaborationDelay, getFallBackToStringOccurrenceHighlighting, shouldAutofocusOutput } from './config'
 import { logger } from './utils/logger'
 // @ts-ignore
 import path from 'path'
 import { SemVer } from 'semver'
-import {
-    c2pConverter,
-    LeanPublishDiagnosticsParams,
-    p2cConverter,
-    patchConverters,
-    setDependencyBuildMode,
-} from './utils/converters'
+import { setupClient } from './leanclientsetup'
+import { c2pConverter, LeanPublishDiagnosticsParams, p2cConverter, setDependencyBuildMode } from './utils/converters'
 import { elanInstalledToolchains } from './utils/elan'
 import { ExtUri, parseExtUri, toExtUri } from './utils/exturi'
 import { leanRunner } from './utils/leanCmdRunner'
@@ -61,23 +46,14 @@ import {
     displayNotificationWithOptionalInput,
     displayNotificationWithOutput,
 } from './utils/notifs'
-import { willUseLakeServer } from './utils/projectInfo'
-
-interface LeanClientCapabilties {
-    silentDiagnosticSupport?: boolean | undefined
-}
-
-const leanClientCapabilities: LeanClientCapabilties = {
-    silentDiagnosticSupport: true,
-}
 
 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[] = []
@@ -125,7 +101,15 @@ 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,
+            folderUri: ExtUri,
+            clientOptions: LanguageClientOptions,
+        ) => Promise<BaseLanguageClient>,
+    ) {
         this.outputChannel = outputChannel
         this.folderUri = folderUri
         this.subscriptions.push(new Disposable(() => this.staleDepNotifier?.dispose()))
@@ -272,7 +256,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 setupClient(toolchainOverride, this.folderUri, this.obtainClientOptions())
 
         let insideRestart = true
         try {
@@ -521,43 +505,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',
@@ -688,25 +635,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)
-        const leanCapabilityFeature: StaticFeature = {
-            initialize(_1, _2) {},
-            getState() {
-                return { kind: 'static' }
-            },
-            fillClientCapabilities(capabilities: ClientCapabilities & { lean?: LeanClientCapabilties | undefined }) {
-                capabilities.lean = leanClientCapabilities
-            },
-            dispose() {},
-        }
-        client.registerFeature(leanCapabilityFeature)
-
-        patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter)
-        return client
-    }
 }

vscode-lean4/src/leanclientsetup.ts

@@ -0,0 +1,83 @@
+import {
+    ClientCapabilities,
+    LanguageClient,
+    LanguageClientOptions,
+    ServerOptions,
+    StaticFeature,
+} from 'vscode-languageclient/node'
+import { serverArgs, serverLoggingEnabled, serverLoggingPath } from './config'
+import { patchConverters } from './utils/converters'
+import { ExtUri } from './utils/exturi'
+import { willUseLakeServer } from './utils/projectInfo'
+
+interface LeanClientCapabilties {
+    silentDiagnosticSupport?: boolean | undefined
+}
+
+const leanClientCapabilities: LeanClientCapabilties = {
+    silentDiagnosticSupport: true,
+}
+
+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 = folderUri.scheme === 'file' ? 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,
+    folderUri: ExtUri,
+    clientOptions: LanguageClientOptions,
+): Promise<LanguageClient> {
+    const serverOptions: ServerOptions = await determineServerOptions(toolchainOverride, folderUri)
+
+    const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
+    const leanCapabilityFeature: StaticFeature = {
+        initialize(_1, _2) {},
+        getState() {
+            return { kind: 'static' }
+        },
+        fillClientCapabilities(capabilities: ClientCapabilities & { lean?: LeanClientCapabilties | undefined }) {
+            capabilities.lean = leanClientCapabilities
+        },
+        dispose() {},
+    }
+    client.registerFeature(leanCapabilityFeature)
+
+    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'
@@ -62,7 +63,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,
+            folderUri: ExtUri,
+            clientOptions: LanguageClientOptions,
+        ) => Promise<BaseLanguageClient>,
+    ) {
         this.outputChannel = outputChannel
         this.installer = installer
 
@@ -273,7 +282,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)