(language) server infoview initialization_option

Stream: lean4

[Luke Naylor]

The npm package for the the infoview webapp could in principle be used give a VSCode-like lean4 experience to other editors (afaik the only editor with html widgets?). Very few LSP-enabled editors have both the ability to provide a webview for extensions and suitable extension capabilities.

Having an external infoview could not only would this allow people more choice in editors but also there's a potential for different infoview apps suiting different preferences (full fledged web-based like VSCode, or slimmer text based like vim).

Has there ever been any discussions about having the option (via lsp init options) to decouple the editor from the lean4 language server and have the language server send the relevant RPC requests to an external infoview itself instead of requiring the editor to handle non-standard LSP communications? This could be done either by specifying an executable and arguments to start a process that is communicated with via stdin/stdout, or maybe specify a socket or named pipe and require the infoview process to be started separately?

This could in principle be achieved with a shim acting as both an LSP client and server but ultimately would make more sense in the lean4 language server itself.
I would be keen to hear thoughts and previous relevant discussion.

[Julian Berman]

#Emacs > lean4-minimal-mode is a related discussion. I'm not personally interested in this style of external infoview rather than a fully integrated one which is what we have (lean.nvim supports HTML widgets by essentially... reimplementing them :/ -- I certainly would love to think harder about ways to improve this but it's been quite a journey even already. I'd certainly accept PRs to add support for an external infoview to lean.nvim.) But I do think this area needs more people with ideas even though a lot of super nice things have already been built.

[Luke Naylor]

This would also be targeting editors which don't have a good/easy scripting/extension capability. Zed is an example, sublime may allow extensions to handle LSP commands but it's apparently not been done (a lean4 infoview extension). This suggestion would allow editors (and it's extension) to only be concerned with the LSP spec.

[Julian Berman]

You might also be interested in #general > Lean + Zed integration @ 💬 too then (Marc's on vacation but I'm sure would welcome any thoughts you have. I think @leanprover/infoview is already trying hard to be close to what you're asking for, it's just you can't fit everything into LSP, the protocol has limitations compared to what Lean's interaction model is.)

[Luke Naylor]

Julian Berman said:

You might also be interested in #general > Lean + Zed integration @ 💬 too then (Marc's on vacation but I'm sure would welcome any thoughts you have. I think @leanprover/infoview is already trying hard to be close to what you're asking for, it's just you can't fit everything into LSP, the protocol has limitations compared to what Lean's interaction model is.)

Ok thanks that was interesting, my takeaway is that even if the editor does not have to deal with the infoview, the quality of life is still heavily impacted if an extension does not take ownership of certain LSP messages.