Feature request: cancel outdated Lean RPC requests

[Vtec234]

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.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 Severe lag: repeated $/lean/rpc/call request storm in <1s #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 $/cancelRequest the corresponding $/lean/rpc/call.