search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

RFC: do not use `_serverProcess` in leanclient. #487

Open joneugster opened 3 months ago

joneugster commented 3 months ago

Consider the following lines of code:

https://github.com/leanprover/vscode-lean4/blob/cee53169b58d31a03a60c4769ee827a3cabffd7c/vscode-lean4/src/leanclient.ts#L264C1-L274C11

;(this.client as any)._serverProcess.stderr.on('data', async (chunk: Buffer) => {
  ...
})

When adapting the extension to monaco, we are replacing vscode's LanguageClient (link to source) with the MonacoLanguageClient (link to source) which does not have _serverProcess, so we basically delete the marked code snippet.

As (this.client as any)._serverProcess seems like quite a hack already (i.e. _serverProcess is marked private), I thought I'd mark this here. Maybe there is a better way to do this that would work in both cases?

abentkamp commented 3 months ago

I don't think this is easy to change since the Lean server would need to be modified for this, too.

How about just adding a few question marks?

;(this.client as any)._serverProcess?.stderr?.on('data', async (chunk: Buffer) => {
  ...
})