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 408a1bdd2..bfc4de653 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/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,15 +46,6 @@ 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, '\\$&') @@ -77,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[] = [] @@ -125,7 +101,15 @@ 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, + folderUri: ExtUri, + clientOptions: LanguageClientOptions, + ) => Promise, + ) { 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 { - 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 { - 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 - } } diff --git a/vscode-lean4/src/leanclientsetup.ts b/vscode-lean4/src/leanclientsetup.ts new file mode 100644 index 000000000..88ac8f787 --- /dev/null +++ b/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 { + 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 { + 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 +} diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index e6426647c..0cf682b9f 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' @@ -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, + ) { 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)