diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 6f1b0a3b6..fa1b34bdd 100644 --- a/vscode-lean4/src/extension.ts +++ b/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 { - const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel()) + const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel(), setupClient) elanCommandProvider.setClientProvider(clientProvider) context.subscriptions.push(clientProvider) diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index 439447733..9da3ad547 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/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,7 +46,6 @@ import { displayNotificationWithOptionalInput, displayNotificationWithOutput, } from './utils/notifs' -import { willUseLakeServer } from './utils/projectInfo' const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&') @@ -58,7 +53,7 @@ export type ServerProgress = Map 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() serverFailed = this.serverFailedEmitter.event - constructor(folderUri: ExtUri, outputChannel: OutputChannel) { + constructor(folderUri: ExtUri, outputChannel: OutputChannel, + private setupClient: ( + toolchainOverride: string | undefined, + clientOptions: LanguageClientOptions, + folderUri: ExtUri, + ) => Promise, + ) { 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 { - 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 { - 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 - } } diff --git a/vscode-lean4/src/leanclientsetup.ts b/vscode-lean4/src/leanclientsetup.ts new file mode 100644 index 000000000..1efde43f0 --- /dev/null +++ b/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 { + 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 { + const serverOptions: ServerOptions = await this.determineServerOptions(toolchainOverride, folderUri) + + const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions) + + patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter) + return client +} diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index f0ac3f1fd..de9103a2e 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/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, + ) { 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)