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 :)