Should start a fresh server per folder about vscode-lean4

[gebner]

There is one advantage of doing it in the editor: we could run a different Lean version in every directory.

You also need to write extra code for neovim if you want multiple servers. The manual even includes a nice two-page code snippet for it: https://neovim.io/doc/user/lsp.html (And yes, you need to forward the goal command to the right server yourself.)

[mhuisi]

Seriously, what is the point of the watchdog architecture then?

The worker processes also need to be restarted when the header changes.

[gebner]

Technically, it seems to be possible to start a different server for each folder. Apparently the LSP library for vscode allows you to restrict a server to a subdirectory. We'd just need to start a server for each workspace folder, and stop them when the folder is removed, etc. We'd also need to aggregate the responses from the different servers for the info view, etc. :-/

But if we implement support for multiple servers, we could also cut out the middle management and execute the workers directly.

Seriously, what is the point of the watchdog architecture then? Apparently emacs would also need extra code to manage multiple servers, if I read the linked issue correctly. IMHO this should be handled in the Lean server once and for all and not in every editor (in potentially different and incompatible ways).

cc @Vtec234

[Kha]

I only know the VS Code API from hearsay, but the watchdog architecture was created under the impression that it was not possible to start a server per file. For Emacs at least this is true, lsp-mode will start one server per workspace and has no idea about multi-folder workspaces. So there is nothing to do on the Emacs side.

[Kha]

We'd also need to aggregate the responses from the different servers for the info view, etc. :-/

I had no idea the info view will show messages from multiple folders (though I guess it naturally follows from the current setup)
. Is that even desirable?

[Kha]

And then of course there is the actual watchdog part, where we might want to be even more careful about restarting workers than we already are given the recent bug reports. I wouldn't want to put that into every client.

[gebner]

I had no idea the info view will show messages from multiple folders (though I guess it naturally follows from the current setup). Is that even desirable?

Oh no, it won't. But it will communicate with the server, e.g. to request the goal state. So we need some abstraction to send these requests to the correct server.

[Kha]

I had no idea the info view will show messages from multiple folders (though I guess it naturally follows from the current setup). Is that even desirable?

Oh no, it won't. But it will communicate with the server, e.g. to request the goal state. So we need some abstraction to send these requests to the correct server.

I see. But so does VS Code for every built-in requests, can we reuse that?

[gebner]

I see. But so does VS Code for every built-in requests, can we reuse that?

Not really. The LSP library registers itself as e.g. a definition provider for the specified subdirectory, and then it will get the go-to definition requests for that subdirectory.

But aside from that there's no support for running multiple servers. You literally need to start them yourself for every directory, keep track of them, etc. And if you have custom commands, you need to redirect them yourself.

[gebner]

For Emacs at least this is true, lsp-mode will start one server per workspace and has no idea about multi-folder workspaces.

So how does this work with emacs? Do you need to run a separate emacs instance for every lean project? Does it matter which directory you start emacs from?

[gebner]

The worker processes also need to be restarted when the header changes.

Ah, so interfacing with the workers directly is not an option then.

[Kha]

For Emacs at least this is true, lsp-mode will start one server per workspace and has no idea about multi-folder workspaces.

So how does this work with emacs? Do you need to run a separate emacs instance for every lean project? Does it matter which directory you start emacs from?

No, you can open multiple workspaces in a single Emacs instance. Each server is started in the workspace root dir. But it looks like lsp-mode also supports multi-root workspaces and will start a single server for them if you set multi-root when calling make-lsp-client. In either case, lsp-mode completely takes care of managing the processes. This is confusing...

[Kha]

So, I'm not opposed to making the server folder-aware, which is probably the right choice in the long term. Coming from lsp-mode and the server code it just seemed easier to tell VS Code to behave like Emacs since that was explicitly listed as an option in their documentation.

[lovettchris]

https://github.com/microsoft/vscode/wiki/Adopting-Multi-Root-Workspace-APIs

[Kha]

Yes, we're aware. leanprover/lean4#300 (comment)

[lovettchris]

I was just adding that link for my own benefit, I'm working on this in PR# #104