lsp fileProgress and gerInteractiveGoals

Stream: lean4

[Shanghe Chen]

Hi I am stills working on the basic support Lean in IntelliJ Idea. While handling caret update , should I wait till fileProgress finished and then invoke the rpc call getInteractiveGoals or just calling getInteractiveGoals even the current file is progressing?

[Shanghe Chen]

Now I am waiting the fileProgress notification finished. I dont know if it’s necessary or not. It seems necessary? While the current file is progressing by the lsp server, getting goals seems no result?

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

The point of the file progress notification, iirc, is to inform the user which postfix of the file is still being processed by the server. In vscode this shows up as orange bars in the left side gutter. You do NOT have to wait for the entire file to finish processing before requesting the goal state at a position: just that part of the file has to have finished processing. This is important for fast interactive feedback. Your code shouldn't have to handle this in any special way: the server will reply to getInteractiveGoals as soon as it can. You just have to wait for that reply asynchronously.

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

Note that the server currently processes files top-to-bottom, linearized. This might change in the future.

[Shanghe Chen]

Thanks! Yeah decoupling the file progressing events and caret/mouse movement events eases the client impl some level. But maybe some debouncing is still necessary for reduce the pressure for the lsp server? I seems saw it in lean.nvim but cannot find it now

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

Hmm, afair there is no code to do that in the vscode extension. Progress notifications are saved in order to display the orange bars, and also to add some visual information in the infoview when the cursor is at a position that is still loading (cf. leanprover/vscode-lean4#470), but it's not used otherwise.

[Shanghe Chen]

Yeah I get it now. Thanks for the help!