[BUG] Vscode edits slow on big Imports

[miriampolzer]

Describe the Bug

Whenever I work on files within fiat crypto that have a large set of imports (with in turn slow proofs - not sure if relevant), I need to wait for a while when editing during interactive proof mode. E.g. if I am in a proof, and I change a tactic one line above the currently interpreted line, I need to wait for a few seconds, sometimes minutes for the proof state to be ready to interpret the change.

When trying to reproduce it, we noticed that simply importing the files suffices. I am attaching two runs of the same thing, once in rocqide where it is fast and once in vscode with a visible slowdown.

To Reproduce

Steps to reproduce the behavior:

1. Clone fiat crypto and run make.
2. Open src/Bedrock/P256/PrecomputedMultiples.v
3. Interpret until the end of all imports.
4. Change a line above the current interpretation point and wait for the proof to be responsive again.

Expected vs. Actual Behavior

Expected: Snap back before the edited line and be able to continue stepping through the proof immediately (what we see in rocqide)
Actual: Takes a few seconds to adjust (and even longer when deeper in some files/proofs)

Environment (paste the result of Rocq: Troubleshooting: Show Setup):

Debug Information	Value
Rocq Installation	The Rocq Prover, version 9.2 compiled with OCaml 5.4.1
Rocq Path	/usr/local/google/home/mpolzer/.opam/default/lib/coq
VsRocq Extension Version	2.4.3
VsRocqTop Version	2.4.3
VsRocqTop Path	/usr/local/google/home/mpolzer/.opam/default/bin/vsrocqtop
OS	x64 linux
VSCode Version	1.125.1

Rocq Log Output (if applicable)

If the issue involves a server crash or unexpected Rocq behavior, please provide logs from the "Rocq Language Server" output channel in VS Code.
To get detailed logs:

1. Open your VS Code settings.json.
2. Add/modify the vsrocq.args setting:

   "vsrocq.args": [
       "-bt",
       "-vsrocq-d",
       "all"
   ]

3. Reproduce the bug and copy the relevant output from the "Rocq Language Server" channel here.
   It's a bit big. Attaching as file.

https://github.com/user-attachments/assets/2f6cf50c-d28c-4209-b65e-59306862ab82
https://github.com/user-attachments/assets/e2e2fc17-2f3c-412a-a2b7-3e05e123ccf5

Rocq Language Server.log

[MrQubo]

I had the same problem. vsrocq got very slow when I imported MetaRocq. Waiting few seconds for each tactic makes it hardly usable in practice, I had to switch to Emacs.

Debug Information	Value
Rocq Installation	The Rocq Prover, version 9.1.1 compiled with OCaml 5.2.1
Rocq Path	/home/nix/tmp/rocq/_opam/lib/coq
VsRocq Extension Version	2.4.3
VsRocqTop Version	2.4.3
VsRocqTop Path	/home/nix/tmp/rocq/_opam/bin/vsrocqtop
OS	x64 linux
VSCode Version	1.127.0

[TDiazT]

From the logs it looks like you have the completion setting on, and there is a request taking ~6-7 seconds after the edit, with no other request being processed by the server (other didChange calls only appear after). Ranking up the completion results from a big library (fiat) is probably taking a long time, and the suggester's timeout is probably not kicking in.
Can you try disabling completions and see if the sluggishness continues? It might not explain the minutes-long wait... but it might help a bit.

[gares]

In master completion is capped by a timeout, so the problem should go with the next release