Feature request: cancel outdated Lean RPC requests
- Dominant language
- Lua
- Stars
- 581
- Forks
- 60
- Avg merge
- 4d 12h
- Merged PRs (30d)
- 2
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](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#cancelRequest).
- 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.nvim` also makes some Lean-specific RPC calls such as `Lean.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](https://react.dev/reference/react/useEffect#useeffect) cleanup function.
- Implementation-wise, one needs to `$/cancelRequest` the corresponding `$/lean/rpc/call`.
Contributor guide
Assessment
This issue has not been assessed yet.