[BUG] Completion blocks stepping over proof steps

[PhotonQuantum]

IMPORTANT: Before You Submit This Issue

• I have searched the existing VsRocq issues
• I have reviewed the VsRocq FAQ.md and my issue is not addressed there.

Describe the Bug

With VSRocq 2.4.3, enabling vsrocq.completion.enable can make proof stepping appear to hang for about 5-10 seconds. A textDocument/completion request blocks the server event loop, so a later prover/stepForward notification is not processed until completion returns.

To Reproduce

Steps to reproduce the behavior:

1. Import something huge (From iris.bi Require Import bi.)
2. Define a random theorem, use some tactic and forward to it (Theorem a: 1+1 = 2. Proof. Unfold Nat.add. (cursor here))
3. Move cursor back, insert some new tactic, and step forward (Theorem a: 1+1 = 2. Proof. (cursor here) Unfold Nat.add., Theorem a: 1+1 = 2. Proof. simpl. (cursor here) Unfold Nat.add.)

Expected vs. Actual Behavior

What I expected: Proof steps immediately
What happened: It takes ~5s to step forward

Another interesting behaviour is if you wait for ~5 after writing simpl. and before stepping forward, it steps immediately.

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

Debug Information	Value
Rocq Installation	The Rocq Prover, version 9.0.1 compiled with OCaml 5.3.0
Rocq Path	/Users/lightquantum/.opam/iris/lib/coq
VsRocq Extension Version	2.4.3
VsRocqTop Version	2.4.3
VsRocqTop Path	_opam/bin/vsrocqtop
OS	arm64 darwin
VSCode Version	1.119.0

Rocq Log Output (if applicable)

vsrocq_lsp.log

 [lspManager          , 70102, 1778607063.372850] received: {
   "id": 20,
   "params": {
     "textDocument": {
       "uri": "file:///Users/lightquantum/Projects/vsrocq-completion-reproduce/Test.v"
     },
     "position": { "line": 4, "character": 5 },
     "context": { "triggerKind": 1 }
   },
   "method": "textDocument/completion",
   "jsonrpc": "2.0"
 }
 [lspManager          , 70102, 1778607063.372851] ui request: textDocument/completion
 [lspManager          , 70102, 1778607067.894702] sent: {
   "id": 20,
   "jsonrpc": "2.0",
   "result": {
     "isIncomplete": false,
     "items": [
       {
         "detail": "2 = 2",
         "documentation": "Path: Stdlib.Arith.PeanoNat.Nat.two_succ\nScore: 20.000000, Size: 6.000000, Final Score: -94.000000",
         "filterText": "Nat.two_succ",
         "insertText": "Nat.two_succ",
         "label": "★ Nat.two_succ",
         "sortText": "    0"
       },
 <skip 160000+ lines>
       {
         "detail": "∀ (SI : sidx) (K : Type) (EqDecision0 : EqDecision K) \n  (H : Countable K) (A : cmra.cmra) (m1 m2 : gmap K (cmra.cmra_car A)) \n  (i : K) (x y : cmra.cmra_car A),\n  <[i:=cmra.op x y]> (cmra.op m1 m2) = cmra.op (<[i:=x]> m1) (<[i:=y]> m2)",
         "documentation": "Path: iris.algebra.gmap.insert_op\nScore: 5.000000, Size: 393.000000, Final Score: 368.000000",
         "filterText": "gmap.insert_op",
         "insertText": "gmap.insert_op",
         "label": "gmap.insert_op",
         "sortText": "20927"
       }
     ]
   }
 }
 [top                 , 70102, 1778607068.103039] ==========================================================
 [top                 , 70102, 1778607068.103090] New Todo events: { Sel.Todo.ready = { Sorted.sorted = false; data = [] };
                    system =
                    { Sorted.sorted = false;
                      data =
                      [({ Events.Event.WithAttributes.name = (Some "lsp");
                          priority = { Sorted.user = -6; insertion = 160 };
                          it = ReadInProgress; cancelled = ref (false) },
                        { Sorted.user = -6; insertion = 160 })]
                      };
                    queue =
                    { Sorted.sorted = false;
                      data =
                      [({ Events.Event.WithAttributes.name = (Some "feedback");
                          priority = { Sorted.user = -7; insertion = 12 };
                          it = WaitQueueBatch1; cancelled = ref (false) },
                        { Sorted.user = -7; insertion = 12 });
                        ({ Events.Event.WithAttributes.name = (Some "debug");
                           priority = { Sorted.user = -7; insertion = 3 };
                           it = WaitQueue1; cancelled = ref (false) },
                         { Sorted.user = -7; insertion = 3 })
                        ]
                      };
                    tasks = { Sorted.sorted = true; data = [] } }
 [top                 , 70102, 1778607068.103098] ==========================================================
 
 
 [lspManager          , 70102, 1778607068.103127] UI req ready
 [top                 , 70102, 1778607068.103141] Main loop event ready: Request, 2 events waiting
 <skip 20+ lines>
 [lspManager          , 70102, 1778607068.132614] Received notification: prover/stepForward

[gares]

Thanks for reporting. I think the right fix for this (family of) issues is #1046 that I hope to merge soon. In that branch any completion task is capped to 0.5 seconds (which is already a lot). It could be possibly refined to make parsing/execution events preempt queries. This refinement is implementable once that PR gets in.