lsp getInteractiveGoals and subexprPos?

Stream: new members

[Shanghe Chen]

Hi what's the field subexprPos in the method Lean.Widget.getInteractiveGoals of lsp request $/lean/rpc/callused for? I am trying to do some basic funtionality of Lean4 in Intellij Idea and now reach a status that I want to extract the current expression when the cursor hovering in the infoview:
image.png
image.png
image.png

[Shanghe Chen]

I think I must convert the response to some tree-like structure for getting the start and end position for the current hovering position. Is it used for this? I am already deserialized it in some form but not sure how to use it:
image.png

[Julian Berman]

(You're probably better done asking this in #lean4)
I don't recall what that field does, but I can tell you lean.nvim doesn't use it for anything from a quick grep.

[Julian Berman]

(And we support that functionality, IIRC the places to hover come straight from the widgets RPC calls, not from there)

[Julian Berman]

So yeah I'd: 1) ask in #lean4 where Marc may see it and jump in and/or 2) check the Lean server source code (the files have moved around a bit recently so probably just grep for that) and/or 3) grep the VSCode extension to see if it uses it for anything ,as I say lean.nvim doesn't, but maybe we're missing something.

[Julian Berman]

(https://github.com/Julian/lean.nvim/blob/03f743773b684ab4db63c4224dcef06588c1a6f7/lua/lean/infoview/components.lua#L87 in case that helps as well, though probably we ported that directly from the VSCode extension)

[Shanghe Chen]

Yeah thanks it helps a lot! I will check the lua code. A first glance it seems the popup information is loaded eagerly rather than after hovering. I will try to follow nvim's impl too!

[Shanghe Chen]

Btw I cannot move this thread. I will link this for next post in #lean4 :wink:

[Julian Berman]

I don't think I can either, and yeah not a big deal, just might assume the people who know the answers may not necessarily pay attention to this stream.

[Marc Huisinga]

You might find these files to be helpful:
Root for InfoView-related widget requests
Language server request handling
InteractiveGoal type declaration
CodeWithInfos type declaration
TaggedText type declaration
InfoWithCtx type declaration
Lean.SubExpr.Pos type declaration

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

As per the doc linked by Marc, subexprPos is the address of a subexpression within a parent expression. For a simple example, y might have address 2/1 in f x (g y) because it's the first argument to the second argument (NB: it won't actually have that address in Lean, this is just to illustrate the idea).

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

@Shanghe Chen does Idea support browser-based webviews? If it does, you could embed the full infoview as sketched here and wouldn't have to work on reimplementing its functionality.

[Shanghe Chen]

Ah thanks! Yeah it has things like JCEF (Java Chromium Embedded Framework) and I did a basic setup for external infoview with infoview-app here too. I am not planing to reimplement the whole functionality of current infoview-app. Maybe something like popup document and types of current expression should be enough for basic usage.