Emacs infoview

Stream: lean4

[Lucas Viana]

Wojciech Nawrocki said:

Andrés Goens said:

is there any hope whatsoever for this to work in emacs?

A while ago I conjectured a concrete plan for how that could work, but so far no one has attempted an implementation, as far as I know. One disadvantage of the plan is that it's quite specific to the emacs GUI, requires native, platform-specific code for emacs-webkit, and emacs-webkit itself has not received maintenance since 2021. A potential alternative, which would even work with terminal-based emacs when the terminal emulator is running in an otherwise graphical environment, would be to spawn a separate browser window (probably electron or something like it) and orchestrate its behavior from within emacs.

I'm contemplating writing this integration for emacs, and my inital idea is to just use a http server and websockets (via simple-httpd and websocket). This way it would in a browser but also inside emacs built with xwidgets or webkit. Do you think this could work? I'm comfortable with elisp but I have basically zero experience with React, typescript and LSP.

Also, reading the EditorApi interface in infoviewApi.ts I wonder if it would be possible or better to have the infoview be served in a localhost port by the lean server itself. This way it would have direct access to all those methods in the EditorApi interface and would basically not require writing integrations for new editors, right?

[Wojciech Nawrocki]

Woo, it would be awesome if someone finally implements this :) Do I understand it correctly that your intention is to build a infoview-server which serves the infoview as a webpage so that it can be opened either from a separate browser, or inside emacs using one of the many browser plugins?

wonder if it would be possible or better to have the infoview be served in a localhost port by the lean server itself.

Do you mean that it would be better for the Lean server to respond to HTTP requests in a manner similar to the proposed infoview-server?

[Lucas Viana]

Do you mean that it would be better for the Lean server to respond to HTTP requests in a manner similar to the proposed infoview-server?

Yes, I wonder if there is something specific to the infoview that requires it to communicate with the editor directly, something that the server itself couldn't do. If the LSP server can handle all the required commands and communicate with the editor then it could also serve a http page with the infoview, right? And communicate with it somehow (websockets for instance).

[Wojciech Nawrocki]

I think the reason for 'why is it like this' is that 'it was implemented that way' :) I don't believe we really ever considered your proposed architecture. I could see it having some advantages; notably, the editor would no longer have to proxy LSP messages between the infoview and the server, so support for sendClient*/(un)subscribeServer*/(un)subscribe* (infoviewApi.ts) would be put in once, in the Lean server, rather than in every editor. I think create/closeRpcSession might be unavoidably editor-bound by virtue of the fact that we need something on the clientside to keep the RPC session alive. Other functionality such as inserting text or copying to clipboard can be implemented via LSP server->client messages, possibly custom ones if the LSP standard doesn't support something.

Having said all that, writing an HTTP server that can reliably host the infoview and linking it into the Lean server, and handle websocket communication with the infoview, would be a serious undertaking. Is it really worth it? The API surface of EditorApi is not that huge. In vscode-lean4 the entire implementation is about 150 lines. The server rewrite would be orders of magnitude more work than writing 150 lines.

[Lucas Viana]

Oh, I guess I was a bit confused with React. I was assuming the infoview could be served like a static web page (with the React app running as JS), that's why I was talking about serving it from emacs or the lean server via HTTP.

[Lucas Viana]

Sorry, I think this means I would have to write a wrapper to serve it via something like node, and I'm very unfamiliar with js development. If someone wants to do that perhaps I can help on the emacs side, but I will leave this project aside for now...

[Wojciech Nawrocki]

No, it totally can be served as a static webpage. There is no server-side rendering. But even just serving a static webpage properly is non-trivial if you want it work across different environments, browsers, with HTTPS, etc. VSCode does this for us with its webview infrastructure. Also, we have to serve a few additional files that the infoview loads (the JS), so the HTTP server has to read those in somehow.