InfoView in a Web Browser?

Stream: general

[Harry Goldstein]

Has anyone set up a way to render the info view in an external web browser (i.e., outside of VSCode)? I see that editors without web rendering (like neovim and zed) roll their own alternatives to the info view, but it seems like it should be pretty straightforward to just set up a local server that serves the info view so you can connect to it in a separate browser.

To be clear, I'm not asking anyone here to support this, and I do think it's probably easiest for the Lean community to just rally around a small subset of editors instead of trying to support everything. I'm just curious if that code is already out there somewhere, because I haven't been able to find it if it is.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Perhaps here?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

IIRC that implementation launches the infoview through Emacs. One could also consider a generic, editor-independent wrapper around the Lean server that launches an infoview browser.

[Jon Eugster]

The version we are currently using for our browser based projects has been extracted as a NPM package:

github.com/hhu-adam/lean4monaco
npmjs.com/package/lean4monaco

It's a bit a hack, mainly because the Infoview/the Lean4-VSCode extension don't really have the capacity to improve usability in this use case, but I'd hope you'd find it instructive :)

[Castedo Ellerman]

For anybody attempting to render infoview in an external web browser, I've coded an extremely minimal example static web app rendering/hosting infoview: https://gitlab.com/castedo/sideinfoview I did this learning from the lean4monaco (and lean4web) respositories.

However, in its current form, it is too minimal to be useful (apart from being instructive). The API interfaces into infoview need to be hooked up to something real that does not exist in any minimal form (that I know of). But one can imagine hooking these interfaces up to a localhost websocket and then having a separate local application connecting the websocket to a locally running editor and Lean LSP server.

This does not seem straightforward to me, but I'm new to the Lean codebase. The details are much messier and trickier than they initially sounded to me. I currently do not have any concrete plans to tackle these messy tricky details any time soon.