High Latency until Infoview Quiescence

To reproduce: put

import Mathlib

theorem foo (a b : ℕ) : a + b = b+a
  := by omega

into https://live.lean-lang.org and rapidly delete and retype the a of b+a.

Observe: sometimes (perhaps on the order of 1/5-1/10 of attempts consisting of deleting/retyping about 10 times and then waiting) the infoview becomes unresponsive for an atypically long period of time, in the sense of the project filename (e.g. MathlibDemo.lean) in the infoview being colored yellow and a spinner remaining. For me, I've been able to see as much as 5s, but @b-mehta reports as much as 60s or more.

It was conjectured this was due to large (~20-40Mb) completion messages blocking other messages (e.g. responses for $/rpc/getInteractiveGoals) due to websocket head-of-line behavior, but enabling compression (https://github.com/leanprover-community/lean4web/pull/133) did not seem to alleviate the problem.

It seems that somehow the problem is likely involves something peculiar to lean4web or the production circumstances of live.lean-lang.org, since the problem has not been observed in vscode.

Start by reproducing the issue in https://live.lean-lang.org with the provided Mathlib example, then inspect lean4web’s handling of completion messages and $/rpc/getInteractiveGoals over the websocket. Compare the behavior with VS Code and verify that rapid edits no longer leave the Infoview spinner and filename yellow for an atypically long period.