integrating infoview app

Stream: lean4

[Shanghe Chen]

Hi continuing the thread I am trying to integrate the infoview app with intelij idea. I got the basic functionality work but sometimes when there is no goal I got stuck for providing maybe a wrong default value like:

export class DummyEditorApi implements EditorApi {
    async sendClientRequest(uri: string, method: string, params: any): Promise<any> {
        console.log(`Sending client request: ${method} for URI: ${uri}`);
        const res = await fetch('/api/sendClientRequest', {
                method: "POST",
                headers: {
                    "Content-Type": "application/json"
                },
                body: JSON.stringify(params)
            }
        );
        if (!res.ok) {
            throw new Error('Network response was not ok');
        }
        const result = await res.json();
        if (Object.keys(result).length == 0) {
            if (params.method == "Lean.Widget.getInteractiveGoals") {
                return {
                    goals: []
                }
            }
            if (params.method == "Lean.Widget.getInteractiveTermGoal") {
                return {
                    goals: [],
                    hyps: []
                }
            }
            return []
        }
        return result;
    }

it seems that for the no goal case I am providing a wrong default value and get error in here (lean4-infoview/src/infoview/interactiveCode.tsx:36) with fmt undefined:

/**
 * Core loop to display {@link TaggedText} objects. Invokes `InnerTagUi` on `tag` nodes in order to support
 * various embedded information, for example subexpression information stored in {@link CodeWithInfos}.
 * */
export function InteractiveTaggedText<T>({ fmt, InnerTagUi }: InteractiveTaggedTextProps<T>) {
    if ('text' in fmt) return <>{fmt.text}</>
    else if ('append' in fmt)
        return (
            <>
                {fmt.append.map((a, i) => (
                    <InteractiveTaggedText key={i} fmt={a} InnerTagUi={InnerTagUi} />
                ))}
            </>
        )
    else if ('tag' in fmt) return <InnerTagUi fmt={fmt.tag[1]} tag={fmt.tag[0]} />
    else throw new Error(`malformed 'TaggedText': '${fmt}'`)
}

[Shanghe Chen]

any idea for this? It seems kind of fuzzy and I got a screenshot for the error. It seems I didn't provide the correct default value to infoview-app but I cannot find it after some tries
infoview_app3.mp4

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

Hm, a few questions:

• The two fallback cases you have under Object.keys(result).length == 0 are supposed to happen when method === '$/lean/rpc/call', right? It might be clearer to check for that.
• But then still, what are these fallback cases for? Are they necessary? The RPC calls try to handle various errors, so it might be okay to simply throw an error. In that case the infoview should show the error message.
• As to your specific question, I _think_ that the returned data in interactiveTermGoal has the wrong shape. The type it should have is specified here. As you can see, it has no goals field, and you're missing the type field. But instead of being an object, the whole thing can be undefined, so just return undefined might work.

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

Oh, and congrats on getting the infoview working as far as you already did! It would be great to support multiple editors and not just VSCode.

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

Also, I'm not sure how exactly your infoview<->editor communication works (looks like it's using HTTP requests?), but as per the API I linked above, the result of getInteractiveTermGoal can be undefined, and this is a valid value. It simply means that there is no term goal at that specific position. On the other hand, it looks like your code assumes that result is an object (as Object.keys(undefined) throws an error). You may have to fix something internally to handle the case when result === undefined correctly.

[Shanghe Chen]

Thanks! Yeah I changed the default value to undefined for the method Lean.Widget.getInteractiveTermGoal and it works for all case now! But It seems that the default value for method Lean.Widget.getInteractiveGoals cannot be undefined and must be {"goals":[]}

[Shanghe Chen]

Wojciech Nawrocki 发言道：

Also, I'm not sure how exactly your infoview<->editor communication works (looks like it's using HTTP requests?)

Yeah the editor is as a rest service backend and the infoview is the frontend. For EditorApi I sent HTTP requests and using server-sent events for bridging infoview api. Maybe for crossing the http protocol that's why I had to handle these fallback cases.

[Shanghe Chen]

Btw any recommend way to handle outdated RPC session? I am thinking create a new session in the editor end or should I tell infoview to get a new session. And it seems kind of weird it's outdated since I sent $/lean/rpc/keepAlive each 9 seconds periodly though

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

Does it help to look at the implementation here?

[Shanghe Chen]

Yeah thanks! I will check the impl in vscode-lean4

[Shanghe Chen]

Wojciech Nawrocki 发言道：

Does it help to look at the implementation here?

Hi I found that for integrating infoview app inside a web browser, for showing "All Messages" it seems relying on earlier textDocument/publishDiagnostics server notifications. May I ask what 's the designing way for showing up all messages in the infoview? Currently I am caching all server notifications and replaying them if there is a new client connection. But I am afraiding the cache may grow too big though.

[Shanghe Chen]

I saw here that there is some logic for determing maxLine for the All Messages tab but still not quite getting it

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

Here is how it works. The infoview listens on textDocument/publishDiagnostics LSP notifications here. Recall that notifications should be passed to the infoview by the editor in the editor API. The latest set of diagnostics for any given file is persisted in the infoview as part of a React context. Unfortunately, base LSP diagnostics do not contain interactive content, so the infoview must make a getInteractiveDiagnostics call whenever the base diagnostics have changed in order to fetch their 'interactive' versions. This is done just below the line you linked, here.

As far as the editor side is concerned, you shouldn't need to cache anything. It suffices to implement the editor API correctly, in that whenever the LSP server sends a notification that has been subscribed, you pass it through with gotServerNotification. The infoview will cache them as needed. You also need to implement the RPC passthrough correctly for getInteractiveDiagnostics to work.

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

Hope this helps @Shanghe Chen

[Shanghe Chen]

Thanks! I just saw this. It helps a lot!