High Latency until Infoview Quiescence

[jcreedcmu]

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 (#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.

[jcreedcmu]

What follows is a hack to monkeypatch JSON.parse/.stringify to intercept lsp websocket traffic.
I pasted this into the browser console, did some interaction which resulted in a several-second delay near the end, and then ran __lsp.download() afterwards to obtain an .ndjson file.

(() => {
  const P = JSON.parse, S = JSON.stringify;
  const L = (window.__lsp = { msgs: [], CAP: 8192 });
  const meth = (s) => (s.slice(0, 400).match(/"method"\s*:\s*"([^"]+)"/) || [])[1];
  const id   = (s) => (s.slice(0, 400).match(/"id"\s*:\s*("?[\w-]+"?)/)   || [])[1];
  JSON.parse = function (s, ...r) {                         // inbound (server -> client)
    if (typeof s === "string" && s.length > 30 && s.includes('"jsonrpc"'))
      L.msgs.push({ t: performance.now(), dir: "in", size: s.length,
        method: meth(s), id: id(s), data: s.length <= L.CAP ? s : s.slice(0, L.CAP) });
    return P.call(this, s, ...r);
  };
  JSON.stringify = function (...a) {                        // outbound (client -> server)
    const out = S.apply(this, a);
    if (typeof out === "string" && out.includes('"jsonrpc"') && (out.includes('"method"') || out.includes('"result"')))
      L.msgs.push({ t: performance.now(), dir: "out", size: out.length,
        method: meth(out), id: id(out), data: out });   // outbound kept in full (small)
    return out;
  };
  L.download = () => {
    const b = new Blob(L.msgs.map((m) => S(m) + "\n"), { type: "application/x-ndjson" });
    const a = document.createElement("a");
    a.href = URL.createObjectURL(b); a.download = `lsp-${Date.now()}.ndjson`; a.click();
  };
  L.summary = () => { const c = {}; for (const m of L.msgs) { const k = `${m.dir} ${m.method || "resp#" + m.id}`; (c[k] ??= { n: 0, bytes: 0 }); c[k].n++; c[k].bytes += m.size; } console.table(c); };
  console.log("[__lsp] hooked; reproduce the edit, then __lsp.summary() / __lsp.download()");
})();

@b-mehta , would you like to try pasting this into console, eliciting the really long pause, and attach the file? Here's my trace:

trace.json.txt

I'm provisionally assuming that high-latency getInteractiveGoals are a sufficient proxy for infoview nonresponsiveness.

[jcreedcmu]

There are some abruptly delayed getInteractiveGoals late in the trace that seem to map onto my user-facing experience of the infoview failing to appear resolved and finished:

...
   405    18923    19033    110ms
   409    18988    19098    110ms
   414    19106    19216    110ms
   418    19198    19309    111ms
   424    19310    19418    108ms
   432    20939    23918   2979ms  <-- SLOW
   437    21056    23918   2862ms  <-- SLOW
   441    21172    23918   2746ms  <-- SLOW
   447    21385    23918   2533ms  <-- SLOW
   454    23981    25343   1362ms  <-- SLOW
   458    24107    25343   1236ms  <-- SLOW
   469    28979    29088    109ms

If this is still head-of-line interference from compressed completions in some way (now only about 3Mb rather than 30Mb) then that might influence the right course of action.

[b-mehta]

lsp-1784664374308.ndjson.txt

[b-mehta]

Here is a video showing the ~60s delay starting at around 1:14: https://www.youtube.com/watch?v=OrKlLNumORM, from two days ago.

[joneugster]

A short analysis now suggested that the server might send much more than even possibly relevant: on

example (P: Prop) : P ∨ ¬ P := by appl

the server sends 227 suggestions, while only 8 of these are displayed to the user. It looks like some filtering is happening frontend-side instead of server-side.

[jcreedcmu]

It looks like when we're specifically completing at tactic position and end up inside tacticCompletion we're returning all tactics regardless of whether they match the query.

I'm actually a little confused about whether this is intended behavior. (It seems relatively benign for the purposes of this issue, just because it's considerably smaller than "most all mathlib constants".)

Evidence for it being intended: this unit test, on zero-indexed line 26 and character 24, tries to complete ski, and in the expected output we see various tactics completing, which I think is all the tactics available in that test context.

Evidence for it being unintended: the comment on that unit test says "Tactic completions matching ski expected".

[joneugster]

Thanks for digging into this! You're right, this seems to be only relevant on tactic completion (which is capped at 227 total items) and not scale to the term completion (which has much more items). So this does indeed not have the impact I suspected it could have (factor 25:1 of junk values vs displayed results looked scary)