Skip to content

Commit f9e346d

Browse files
joneugsterjoneugster
committed
feat: abstract lean client setup for websocket clients
1 parent fd8ad21 commit f9e346d

File tree

4 files changed

+111
-92
lines changed

4 files changed

+111
-92
lines changed

‎vscode-lean4/src/extension.ts‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import { PreconditionCheckResult, SetupNotificationOptions } from './diagnostics
1010
import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports'
1111
import { InfoProvider } from './infoview'
1212
import { LeanClient } from './leanclient'
13+
import { setupClient } from './leanclientsetup'
1314
import { LoogleView } from './loogleview'
1415
import { ManualView } from './manualview'
1516
import { MoogleView } from './moogleview'
@@ -177,7 +178,7 @@ async function activateLean4Features(
177178
installer: LeanInstaller,
178179
elanCommandProvider: ElanCommandProvider,
179180
): Promise<Lean4EnabledFeatures> {
180-
const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel())
181+
const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel(), setupClient)
181182
elanCommandProvider.setClientProvider(clientProvider)
182183
context.subscriptions.push(clientProvider)
183184

‎vscode-lean4/src/leanclient.ts‎

Lines changed: 15 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -13,18 +13,15 @@ import {
1313
WorkspaceFolder,
1414
} from 'vscode'
1515
import {
16-
ClientCapabilities,
16+
BaseLanguageClient,
1717
DiagnosticSeverity,
1818
DidChangeTextDocumentParams,
1919
DidCloseTextDocumentParams,
2020
DocumentFilter,
2121
InitializeResult,
22-
LanguageClient,
2322
LanguageClientOptions,
2423
RevealOutputChannelOn,
25-
ServerOptions,
2624
State,
27-
StaticFeature,
2825
} from 'vscode-languageclient/node'
2926

3027
import {
@@ -33,25 +30,13 @@ import {
3330
LeanFileProgressProcessingInfo,
3431
ServerStoppedReason,
3532
} from '@leanprover/infoview-api'
36-
import {
37-
getElaborationDelay,
38-
getFallBackToStringOccurrenceHighlighting,
39-
serverArgs,
40-
serverLoggingEnabled,
41-
serverLoggingPath,
42-
shouldAutofocusOutput,
43-
} from './config'
33+
import { getElaborationDelay, getFallBackToStringOccurrenceHighlighting, shouldAutofocusOutput } from './config'
4434
import { logger } from './utils/logger'
4535
// @ts-ignore
4636
import path from 'path'
4737
import { SemVer } from 'semver'
48-
import {
49-
c2pConverter,
50-
LeanPublishDiagnosticsParams,
51-
p2cConverter,
52-
patchConverters,
53-
setDependencyBuildMode,
54-
} from './utils/converters'
38+
import { setupClient } from './leanclientsetup'
39+
import { c2pConverter, LeanPublishDiagnosticsParams, p2cConverter, setDependencyBuildMode } from './utils/converters'
5540
import { elanInstalledToolchains } from './utils/elan'
5641
import { ExtUri, parseExtUri, toExtUri } from './utils/exturi'
5742
import { leanRunner } from './utils/leanCmdRunner'
@@ -61,23 +46,14 @@ import {
6146
displayNotificationWithOptionalInput,
6247
displayNotificationWithOutput,
6348
} from './utils/notifs'
64-
import { willUseLakeServer } from './utils/projectInfo'
65-
66-
interface LeanClientCapabilties {
67-
silentDiagnosticSupport?: boolean | undefined
68-
}
69-
70-
const leanClientCapabilities: LeanClientCapabilties = {
71-
silentDiagnosticSupport: true,
72-
}
7349

7450
const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
7551

7652
export type ServerProgress = Map<ExtUri, LeanFileProgressProcessingInfo[]>
7753

7854
export class LeanClient implements Disposable {
7955
running: boolean
80-
private client: LanguageClient | undefined
56+
private client: BaseLanguageClient | undefined
8157
private outputChannel: OutputChannel
8258
folderUri: ExtUri
8359
private subscriptions: Disposable[] = []
@@ -125,7 +101,15 @@ export class LeanClient implements Disposable {
125101
private serverFailedEmitter = new EventEmitter<string>()
126102
serverFailed = this.serverFailedEmitter.event
127103

128-
constructor(folderUri: ExtUri, outputChannel: OutputChannel) {
104+
constructor(
105+
folderUri: ExtUri,
106+
outputChannel: OutputChannel,
107+
private setupClient: (
108+
toolchainOverride: string | undefined,
109+
folderUri: ExtUri,
110+
clientOptions: LanguageClientOptions,
111+
) => Promise<BaseLanguageClient>,
112+
) {
129113
this.outputChannel = outputChannel
130114
this.folderUri = folderUri
131115
this.subscriptions.push(new Disposable(() => this.staleDepNotifier?.dispose()))
@@ -272,7 +256,7 @@ export class LeanClient implements Disposable {
272256
const toolchainOverride: string | undefined =
273257
toolchainOverrideResult.kind === 'Override' ? toolchainOverrideResult.toolchain : undefined
274258

275-
this.client = await this.setupClient(toolchainOverride)
259+
this.client = await setupClient(toolchainOverride, this.folderUri, this.obtainClientOptions())
276260

277261
let insideRestart = true
278262
try {
@@ -521,43 +505,6 @@ export class LeanClient implements Disposable {
521505
return this.running ? this.client?.initializeResult : undefined
522506
}
523507

524-
private async determineServerOptions(toolchainOverride: string | undefined): Promise<ServerOptions> {
525-
const env = Object.assign({}, process.env)
526-
if (serverLoggingEnabled()) {
527-
env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
528-
}
529-
530-
const [serverExecutable, options] = await this.determineExecutable()
531-
if (toolchainOverride) {
532-
options.unshift('+' + toolchainOverride)
533-
}
534-
535-
const cwd = this.folderUri.scheme === 'file' ? this.folderUri.fsPath : undefined
536-
if (cwd) {
537-
// Add folder name to command-line so that it shows up in `ps aux`.
538-
options.push(cwd)
539-
} else {
540-
options.push('untitled')
541-
}
542-
543-
return {
544-
command: serverExecutable,
545-
args: options.concat(serverArgs()),
546-
options: {
547-
cwd,
548-
env,
549-
},
550-
}
551-
}
552-
553-
private async determineExecutable(): Promise<[string, string[]]> {
554-
if (await willUseLakeServer(this.folderUri)) {
555-
return ['lake', ['serve', '--']]
556-
} else {
557-
return ['lean', ['--server']]
558-
}
559-
}
560-
561508
private obtainClientOptions(): LanguageClientOptions {
562509
const documentSelector: DocumentFilter = {
563510
language: 'lean4',
@@ -688,25 +635,4 @@ export class LeanClient implements Disposable {
688635
},
689636
}
690637
}
691-
692-
private async setupClient(toolchainOverride: string | undefined): Promise<LanguageClient> {
693-
const serverOptions: ServerOptions = await this.determineServerOptions(toolchainOverride)
694-
const clientOptions: LanguageClientOptions = this.obtainClientOptions()
695-
696-
const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
697-
const leanCapabilityFeature: StaticFeature = {
698-
initialize(_1, _2) {},
699-
getState() {
700-
return { kind: 'static' }
701-
},
702-
fillClientCapabilities(capabilities: ClientCapabilities & { lean?: LeanClientCapabilties | undefined }) {
703-
capabilities.lean = leanClientCapabilities
704-
},
705-
dispose() {},
706-
}
707-
client.registerFeature(leanCapabilityFeature)
708-
709-
patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter)
710-
return client
711-
}
712638
}

‎vscode-lean4/src/leanclientsetup.ts‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
import {
2+
ClientCapabilities,
3+
LanguageClient,
4+
LanguageClientOptions,
5+
ServerOptions,
6+
StaticFeature,
7+
} from 'vscode-languageclient/node'
8+
import { serverArgs, serverLoggingEnabled, serverLoggingPath } from './config'
9+
import { patchConverters } from './utils/converters'
10+
import { ExtUri } from './utils/exturi'
11+
import { willUseLakeServer } from './utils/projectInfo'
12+
13+
interface LeanClientCapabilties {
14+
silentDiagnosticSupport?: boolean | undefined
15+
}
16+
17+
const leanClientCapabilities: LeanClientCapabilties = {
18+
silentDiagnosticSupport: true,
19+
}
20+
21+
async function determineExecutable(folderUri: ExtUri): Promise<[string, string[]]> {
22+
if (await willUseLakeServer(folderUri)) {
23+
return ['lake', ['serve', '--']]
24+
} else {
25+
return ['lean', ['--server']]
26+
}
27+
}
28+
29+
async function determineServerOptions(
30+
toolchainOverride: string | undefined,
31+
folderUri: ExtUri,
32+
): Promise<ServerOptions> {
33+
const env = Object.assign({}, process.env)
34+
if (serverLoggingEnabled()) {
35+
env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
36+
}
37+
38+
const [serverExecutable, options] = await determineExecutable(folderUri)
39+
if (toolchainOverride) {
40+
options.unshift('+' + toolchainOverride)
41+
}
42+
43+
const cwd = folderUri.scheme === 'file' ? folderUri.fsPath : undefined
44+
if (cwd) {
45+
// Add folder name to command-line so that it shows up in `ps aux`.
46+
options.push(cwd)
47+
} else {
48+
options.push('untitled')
49+
}
50+
51+
return {
52+
command: serverExecutable,
53+
args: options.concat(serverArgs()),
54+
options: {
55+
cwd,
56+
env,
57+
},
58+
}
59+
}
60+
61+
export async function setupClient(
62+
toolchainOverride: string | undefined,
63+
folderUri: ExtUri,
64+
clientOptions: LanguageClientOptions,
65+
): Promise<LanguageClient> {
66+
const serverOptions: ServerOptions = await determineServerOptions(toolchainOverride, folderUri)
67+
68+
const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
69+
const leanCapabilityFeature: StaticFeature = {
70+
initialize(_1, _2) {},
71+
getState() {
72+
return { kind: 'static' }
73+
},
74+
fillClientCapabilities(capabilities: ClientCapabilities & { lean?: LeanClientCapabilties | undefined }) {
75+
capabilities.lean = leanClientCapabilities
76+
},
77+
dispose() {},
78+
}
79+
client.registerFeature(leanCapabilityFeature)
80+
81+
patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter)
82+
return client
83+
}

‎vscode-lean4/src/utils/clientProvider.ts‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
22
import path from 'path'
33
import { Disposable, EventEmitter, OutputChannel, commands, workspace } from 'vscode'
4+
import { BaseLanguageClient, LanguageClientOptions } from 'vscode-languageclient/node'
45
import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics'
56
import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs'
67
import { LeanClient } from '../leanclient'
@@ -62,7 +63,15 @@ export class LeanClientProvider implements Disposable {
6263
private clientStoppedEmitter = new EventEmitter<[LeanClient, boolean, ServerStoppedReason]>()
6364
clientStopped = this.clientStoppedEmitter.event
6465

65-
constructor(installer: LeanInstaller, outputChannel: OutputChannel) {
66+
constructor(
67+
installer: LeanInstaller,
68+
outputChannel: OutputChannel,
69+
private setupClient: (
70+
toolchainOverride: string | undefined,
71+
folderUri: ExtUri,
72+
clientOptions: LanguageClientOptions,
73+
) => Promise<BaseLanguageClient>,
74+
) {
6675
this.outputChannel = outputChannel
6776
this.installer = installer
6877

@@ -273,7 +282,7 @@ export class LeanClientProvider implements Disposable {
273282
}
274283

275284
logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString())
276-
client = new LeanClient(folderUri, this.outputChannel)
285+
client = new LeanClient(folderUri, this.outputChannel, this.setupClient)
277286
this.subscriptions.push(client)
278287
this.clients.set(key, client)
279288

0 commit comments

Comments
 (0)
⚡