Support for RPC protocol

[gebner]

This is a prototype implementation of the RPC protocol, which uses the getInteractiveTermGoal function to obtain the term goal from the server and renders it as a string.

The protocol is still subject to change, so don't merge this yet.

• The docgen tool seems to have a problem with the Session:call function, not sure what's going on there.
• We now have all the tools necessary to e.g. show implicit arguments, docstrings, types, etc. in the infoview (from the InfoWithCtx object). Is there any obvious way to implement these interactive actions in neovim?
• The vscode version uses a FinalizationRegistration to hook into the javascript GC to detect when remote references can be released. I've tried adding a __gc metatable, but this doesn't seem to have an effect in neovim (even though it works just fine on the command-line lua). So we just store all references in the subsession object, and close the subsession whenever the pin is moved (which releases the references).
• The code still uses buf_request with a bufnr (hardcoded to 0), which will break if there are multiple LSP servers. I should figure out how to get the LSP client object and send requests directly (and only) to the lean server.

[Julian]

We now have all the tools necessary to e.g. show implicit arguments, docstrings, types, etc. in the infoview (from the InfoWithCtx object). Is there any obvious way to implement these interactive actions in neovim?

I am playing with some things here as part of toying with widgets. I don't have concrete ideas yet but maybe they're the same UX problem. Will play around with this branch. Anything special I need other than a recent Lean 4?

The docgen tool seems to have a problem with the Session:call function, not sure what's going on there.

It's cranky occasionally (e.g. I can't get it running locally) :/. But will see if I can tell what's up.

figure out how to get the LSP client object

vim.lsp.buf_get_clients() I think? There's possibly multiple though if someone attaches e.g. our client as well as say a linter one, so you have to postfilter I think.

[gebner]

I am playing with some things here as part of toying with widgets. I don't have concrete ideas yet but maybe they're the same UX problem.

I think the UX problem is the same. If you have a nice way to render Lean 3 widgets and handle keypresses, then the same idea should also work here.

Anything special I need other than a recent Lean 4?

You need this branch here, none of this upstream yet: https://github.com/leanprover/lean4/pull/596

[gebner]

See also #23.

[rish987]

I'm going to be trying this out as well, and will be happy to fix any conflicts related to #113.

I've tried adding a __gc metatable, but this doesn't seem to have an effect in neovim (even though it works just fine on the command-line lua)

This could be a Lua 5.1 vs. Lua 5.2 issue (LuaJIT is frozen at 5.1), have you tried this workaround? Again I'll be looking into this myself and so may give it a shot soon.

[gebner]

This could be a Lua 5.1 vs. Lua 5.2 issue (LuaJIT is frozen at 5.1),

I think you're right! I didn't realize that there are version differences in Lua.

[rish987]

Got __gc working with that userdata workaround. I tried it out for a bit and the refs seem to be getting released at a reasonable rate (though definitely not immediately after moving the pin), but of course I'll leave this to your judgment, feel free to add some collectgarbage() calls if you think it will help.

Going to work for a bit on simulating some kind of HTML-style divs for our Info to use in the Info:render() function so that we can easily map from cursor position in the Info to the relevant objects. I think this should actually be pretty simple to do! Then we should be able to just use keymaps and hover windows in the infoview to get the extra information (though I'm not yet familiar with the syntax for using these refs, so will leave that to you).

[rish987]

Alright @gebner everything seems to be ready for you at this point (ignore broken syntax highlighting):

I've mapped widgets to <localleader><space> for now, right now all that happens is it brings up a hover window showing the current div. The API returns the full div stack so you can traverse up to get more data, e.g. the tag and its ref in the case of text divs. Now what I think you'll want to do is a.void() wrap some code in Info:widget() to actually use the ref to do a particular request and display the result in a hover window. Again I don't yet know how to do this so definitely feel free to have a go at it.

Also @Julian I don't know much about Lean 3 widgets yet, but I believe this is a piece of the puzzle for that? Will work on separating the new div stuff from this PR so we can get Lean 3 widgets working ASAP.

[gebner]

Now what I think you'll want to do is a.void() wrap some code in Info:widget() to actually use the ref to do a particular request and display the result in a hover window. Again I don't yet know how to do this so definitely feel free to have a go at it.

Okay, I've updated this PR to the latest version of the RPC protocol (it's been merged, so you can already try it out in mathlib4). I've also implemented the widget() function to show the type, implicit arguments, and docstring. (Though there's something wrong with the implicit arguments, but that's an upstream issue I guess.)

[gebner]

Closed in favor of #123.