Lean becomes unresponsive due to many concurrent getSnapshotData requests

[Aaron1011]

Currently, paperproof calls the getSnapshotData lean function every time the cursor is moved:

paperproof/extension/src/actions/sendPosition/services/fetchLeanData.ts

Line 8 in c3c14d4

const proofTreeResponse = await vscodeRequest(log, "getSnapshotData", client, uri, tdp, { pos: tdp.position });

For large theorems, this can be very expensive (~5 seconds on my machine). However, paperproof never cancels inflight requests ($/cancelRequest), which means that quickly switching between lines can cause a large number of concurrent getSnapshotData requests. When viewing a complex theorem, this can easily lead to ~90% cpu usage, while also preventing other requests from being serviced (e.g. vscode-lean updating the infoview)

[lakesare]

I can reproduce this.
This also happens with the paperproof panel closed, the only way to make the InfoView fast again is to disable the Paperproof extension.

Thanks for the analysis of the problem, I think you're spot on, and this should certainly be fixed.

TODOs:

• don't send the fetchLeanData() request at all when the Paperproof panel is closed (shared.webviewPanel === null)
  [easy fix that at least makes paperproof not interfere with the InfoView speed when the Paperproof panel is closed]
• send the RPC call cancellation request ($/cancelRequest) whenever token.isCancellationRequested is true

[lakesare]

I deployed the fix for the first task, now Paperproof won't affect the InfoView performance when the Paperproof panel is closed.

As per the second task - I understood there is no need to perform the expensive getSnapshotData() operation at all (and therefore no need to cancel it), it only needs to be called once per theorem, and reiterated if the user changed something in the theorem.