Feature request: cancel outdated Lean RPC requests
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
Research direction
Start by tracing the Lean.Widget.getInteractiveGoals calls and the handling of the corresponding $/lean/rpc/call requests. Check how UI destruction and redraws are represented, then investigate how $/cancelRequest can cancel those calls; done means outdated requests are cancelled in the relevant lifecycle cases without disrupting current results.
Written by the indexing model from the issue text.
Description
Feature request
Lean RPC calls should be cancelled by lean.nvim when their results are no longer needed.
Background
- The base LSP protocol offers support for cancellation.
- I am hoping (but haven't confirmed) that the Neovim LSP client already cancels requests that become redundant before a response comes back, e.g. when the user discards a hover popup before its contents have arrived from the server.
lean.nvimalso makes some Lean-specific RPC calls such asLean.Widget.getInteractiveGoals. But pretty-printing large goals and computing goal diffs can be expensive. Such computations can consume a lot of resources if many of these requests are in-flight. It would be better to cancel these requests so that the Lean server can stop their processing threads early.- The cost of these requests is exacerbated when they are made too many times, as in #442.
- There are various possible strategies for when to cancel. The most general one may be to do it when a) the relevant UI is being destroyed and b) when it is being redrawn with new parameters; basically a useEffect cleanup function.
- Implementation-wise, one needs to
$/cancelRequestthe corresponding$/lean/rpc/call.
- Dominant language
- Lua
- Stars
- 601
- Forks
- 61
- Avg merge
- 3d 22h
- Merged PRs (30d)
- 8
Getting set up
- No Dockerfile or Docker Compose file
- No pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from Julian/lean.nvim
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 3/5 1-2 days Newbie friendliness 58/100
-
Difficulty 3/5 1-2 days Newbie friendliness 68/100
-
Difficulty 3/5 1-2 days Newbie friendliness 48/100
All issues in Julian/lean.nvim
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 62/100
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
Maintainers usually reply within 3 days
-
feature
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
-
tests/control, tests/cli: the up-front cleanup removes an ANOTHER or SHIM the environment carriesOpenseverity: low
Difficulty 2/5 1-3 hours Newbie friendliness 80/100
luainkernel/lunatik#1796 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
brndnmtthws/conky#2486 ·
Maintainers usually reply within 1 day