feat: [lean4web] abstract lean client setup to allow for websocket cl…

…ients
leanprover · Aug 16, 2024 · d3c23f7 · d3c23f7
1 parent 403c539
commit d3c23f7
Show file tree

Hide file tree

Showing 4 changed files with 75 additions and 62 deletions.
diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts
@@ -17,6 +17,7 @@ import { PreconditionCheckResult } from './diagnostics/setupNotifs'
 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 { ProjectInitializationProvider } from './projectinit'
@@ -175,6 +176,7 @@ async function activateLean4Features(
         installer,
         installer.getOutputChannel(),
         checkLean4ProjectPreconditions,
+        setupClient
     )
     context.subscriptions.push(clientProvider)
 

diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
@@ -15,29 +15,21 @@ 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'
 
 import { LeanFileProgressParams, 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 { SemVer } from 'semver'
@@ -49,7 +41,6 @@ import {
     displayErrorWithOutput,
     displayInformationWithOptionalInput,
 } from './utils/notifs'
-import { willUseLakeServer } from './utils/projectInfo'
 import path = require('path')
 
 const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
@@ -58,7 +49,7 @@ 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[] = []
@@ -107,7 +98,16 @@ export class LeanClient implements Disposable {
     private serverFailedEmitter = new EventEmitter<string>()
     serverFailed = this.serverFailedEmitter.event
 
-    constructor(folderUri: ExtUri, outputChannel: OutputChannel, elanDefaultToolchain: string) {
+    constructor(
+        folderUri: ExtUri,
+        outputChannel: OutputChannel,
+        elanDefaultToolchain: string,
+        private setupClient: (
+            clientOptions: LanguageClientOptions,
+            folderUri: ExtUri,
+            elanDefaultToolchain: string,
+        ) => Promise<BaseLanguageClient>,
+    ) {
         this.outputChannel = outputChannel // can be null when opening adhoc files.
         this.folderUri = folderUri
         this.elanDefaultToolchain = elanDefaultToolchain
@@ -189,7 +189,8 @@ export class LeanClient implements Disposable {
 
         const startTime = Date.now()
         progress.report({ increment: 0 })
-        this.client = await this.setupClient()
+        this.client = await this.setupClient(this.obtainClientOptions(), this.folderUri, this.elanDefaultToolchain)
+        patchConverters(this.client.protocol2CodeConverter, this.client.code2ProtocolConverter)
 
         let insideRestart = true
         try {
@@ -431,43 +432,6 @@ export class LeanClient implements Disposable {
         return this.running ? this.client?.initializeResult : undefined
     }
 
-    private async determineServerOptions(): Promise<ServerOptions> {
-        const env = Object.assign({}, process.env)
-        if (serverLoggingEnabled()) {
-            env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
-        }
-
-        const [serverExecutable, options] = await this.determineExecutable()
-
-        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 {
-            // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder
-            // which is not what we want.  For adhoc files we want the (default) toolchain instead.
-            options.unshift('+' + this.elanDefaultToolchain)
-            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',
@@ -596,14 +560,4 @@ export class LeanClient implements Disposable {
             },
         }
     }
-
-    private async setupClient(): Promise<LanguageClient> {
-        const serverOptions: ServerOptions = await this.determineServerOptions()
-        const clientOptions: LanguageClientOptions = this.obtainClientOptions()
-
-        const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
-
-        patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter)
-        return client
-    }
 }
diff --git a/vscode-lean4/src/leanclientsetup.ts b/vscode-lean4/src/leanclientsetup.ts
@@ -0,0 +1,45 @@
+import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node'
+import { serverArgs, serverLoggingEnabled, serverLoggingPath } from './config'
+import { ExtUri } from './utils/exturi'
+import { willUseLakeServer } from './utils/projectInfo'
+
+export async function setupClient(
+    clientOptions: LanguageClientOptions,
+    folderUri: ExtUri,
+    elanDefaultToolchain: string,
+): Promise<LanguageClient> {
+    const env = Object.assign({}, process.env)
+    if (serverLoggingEnabled()) {
+        env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
+    }
+
+    let serverExecutable
+    let options
+    if (await willUseLakeServer(folderUri)) {
+        ;[serverExecutable, options] = ['lake', ['serve', '--']]
+    } else {
+        ;[serverExecutable, options] = ['lean', ['--server']]
+    }
+
+    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 {
+        // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder
+        // which is not what we want.  For adhoc files we want the (default) toolchain instead.
+        options.unshift('+' + elanDefaultToolchain)
+        options.push('untitled')
+    }
+
+    const serverOptions: ServerOptions = {
+        command: serverExecutable,
+        args: options.concat(serverArgs()),
+        options: {
+            cwd,
+            env,
+        },
+    }
+
+    return new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
+}
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
@@ -1,5 +1,12 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
 import { Disposable, EventEmitter, OutputChannel, TextDocument, commands, window, workspace } from 'vscode'
+import { BaseLanguageClient, LanguageClientOptions } from 'vscode-languageclient/node'
+import {
+    checkAll,
+    checkIsLakeInstalledCorrectly,
+    checkIsLeanVersionUpToDate,
+    checkIsValidProjectFolder,
+} from '../diagnostics/setupDiagnostics'
 import { PreconditionCheckResult } from '../diagnostics/setupNotifs'
 import { LeanClient } from '../leanclient'
 import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri, toExtUri } from './exturi'
@@ -38,6 +45,11 @@ export class LeanClientProvider implements Disposable {
             channel: OutputChannel,
             folderUri: ExtUri,
         ) => Promise<PreconditionCheckResult>,
+        private setupClient: (
+            clientOptions: LanguageClientOptions,
+            folderUri: ExtUri,
+            elanDefaultToolchain: string,
+        ) => Promise<BaseLanguageClient>,
     ) {
         this.outputChannel = outputChannel
         this.installer = installer
@@ -231,7 +243,7 @@ export class LeanClientProvider implements Disposable {
         logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString())
         const elanDefaultToolchain = await this.installer.getElanDefaultToolchain(folderUri)
 
-        client = new LeanClient(folderUri, this.outputChannel, elanDefaultToolchain)
+        client = new LeanClient(folderUri, this.outputChannel, elanDefaultToolchain, this.setupClient)
         this.subscriptions.push(client)
         this.clients.set(key, client)