using lean4-infoview alone inside an external browser

Stream: general

[Shanghe Chen]

Hi in the repo vscode-lean4 the directory lean4-infoview says that it's possible hosting the infoview in an external browser although it's not tested outside vscode. Could there be a startup demo for how to do this? maybe something like a project starter. I am not familar with react development and the doc says invoking loadRenderInfoview from a react project requires some extra effort. Thanks in advance! :blush:

[Jon Eugster]

we're currently trying to update and cleanup lean4web which can then essentially function as such an example, but the current code suffers from exactly this "some extra effort" mentioned...

[Shanghe Chen]

Ah I see. Thanks! The problem seems coming from that widgets requiring dynamically loaded. Maybe I should just use it statically as a normal package first

[Shanghe Chen]

(deleted)

[Shanghe Chen]

Hi I got a first step via invoking renderInfoview and it results in displaying Waiting for Lean server to start... in Chrome as said in the source I think now I should implement the EditorApi and InfoviewApi But I am not sure the implement for the infoview updating automatically, is it some websocket request or some loop XHR request?

[Shanghe Chen]

btw https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/package.json#L12 seems exporting ".": "./dist/index.development.js", should it be dist/index.production.min.js? I have to change it like this for importing renderInforview

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

Shanghe Chen said:

Hi I got a first step via invoking renderInfoview and it results in displaying Waiting for Lean server to start... in Chrome as said in the source I think now I should implement the EditorApi and InfoviewApi But I am not sure the implement for the infoview updating automatically, is it some websocket request or some loop XHR request?

Maybe this will answer your question: you can think of the infoview as a functional reactive program that will display new contents whenever you invoke one of the event methods in InfoviewApi. So the updating automatically part just amounts to you calling, say, changedCursorLocation, whenever the cursor in your editor has moved.

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

And to get rid of the "Waiting for Lean server to start.." message, you call serverRestarted iirc.

[Shanghe Chen]

Wojciech Nawrocki said:

Shanghe Chen said:

Hi I got a first step via invoking renderInfoview and it results in displaying Waiting for Lean server to start... in Chrome as said in the source I think now I should implement the EditorApi and InfoviewApi But I am not sure the implement for the infoview updating automatically, is it some websocket request or some loop XHR request?

Maybe this will answer your question: you can think of the infoview as a functional reactive program that will display new contents whenever you invoke one of the event methods in InfoviewApi. So the updating automatically part just amounts to you calling, say, changedCursorLocation, whenever the cursor in your editor has moved.

Ah thanks! I may get it now. So my editor is Intellij Idea and connecting to the Lean lsp server. I am also trying to start a web program with the frontend being the infoview in Chrome. Yeah I will see if setting up some websocket connection possible and forward it to the InfoviewApi