diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 0e78e0193..eb0f86098 100644 --- 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 index ff6e815da..fe74cadb2 100644 --- 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 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() 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, + ) { 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 { - 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 { - 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 new file mode 100644 index 000000000..8ea982b92 --- /dev/null +++ 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 { + 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 index cb3159c31..d7cd04663 100644 --- 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, + private setupClient: ( + clientOptions: LanguageClientOptions, + folderUri: ExtUri, + elanDefaultToolchain: string, + ) => Promise, ) { 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)