extension performance

Stream: general

[Patrick Massot]

Is anyone else trying to use the latest version of mathlib? Here it's extremely slow. Moving the cursor in a proof makes VSCode consuming 100% CPU and not responding for seconds.

[Patrick Massot]

vscode100.gif

[Patrick Massot]

Of course ffmpeg is working on the capture, but you can also see bursts of code

[Patrick Massot]

I'm very glad this didn't happen during my talk this morning.

[Gabriel Ebner]

What version did you have in the morning? Already master with the sheaves merged?

[Gabriel Ebner]

I'm afraid #3764 might be responsible.

[Patrick Massot]

861f182160b900e97013df7e8fa992d386e1556d

[Patrick Massot]

Which seems to come after

[Patrick Massot]

I wanted the jump to definition in widgets.

[Patrick Massot]

But maybe I was very lucky.

[Patrick Massot]

It appears to be very random. Right now I don't see any issue.

[Gabriel Ebner]

#mwe

import tactic.interactive_expr

example :
0+1+2+3+4+5+6+7+8+9 +
0+1+2+3+4+5+6+7+8+9 =
0+1+2+3+4+5+6+7+8+9 :=
by skip

[Patrick Massot]

Sorry, I don't understand your message. Do you say you can reproduce the problem with this example?

[Scott Morrison]

That does nothing for me.

[Gabriel Ebner]

Yes. Unfortunately I have no idea what the problem is. This is an infinite loop in javascript in the infoview, and I can't figure out how to debug that. @Edward Ayers

[Patrick Massot]

Currently it causes no issue here, but I guess that half an hour ago it would have been hell.

[Patrick Massot]

It looks like I was very lucky this morning.

[Gabriel Ebner]

(deleted)

[Patrick Massot]

Random bugs are the best ones! Fighting bugs is too easy if they are deterministic.

[Gabriel Ebner]

You need to import tactic.interactive_expr first. (We have two files with the same name.)

[Johan Commelin]

Patrick Massot said:

Random bugs are the best ones! Fighting bugs is too easy if they are deterministic.

The lovely Heisenbyg (-;

[Patrick Massot]

Oh yes of course!

[Patrick Massot]

With the import I see the issue.

[Patrick Massot]

I see you cheated and just added the import to your mwe :spy:

[Patrick Massot]

Thank you very much for minimizing this.

[Patrick Massot]

And this is persistent, I closed the mwe file and spend 15 minutes talking to a colleague and my VSCode was still frozen

[Edward Ayers]

It's deffo something to do with the blocks

[Alex Peattie]

Mm yeah I think #3764 is causing it... it looks like this gets thrown before everything breaks:

[Alex Peattie]

https://github.com/leanprover-community/lean/blob/v3.19.0/src/frontends/lean/interactive.cpp#L125

[Alex Peattie]

image.png

(Edit: I think this error is unrelated actually)

[Edward Ayers]

I think it's a javascript thing

[Edward Ayers]

In view in interactive_expr.lean, I get

| ca (sf.block i a) := do
  inner ← view ca a,
  -- doesn't break also setting to a different classname is fine
  -- pure $ h "span" [] inner
  -- breaks:
  pure $ h "span" [cn "dib"] inner

[Patrick Massot]

javascript...

[Edward Ayers]

Starting to wonder whether it is a chrome rendering bug...

[Gabriel Ebner]

:+1:

[Gabriel Ebner]

Open the following file using HTML preview:

<link rel="stylesheet" href="https://unpkg.com/tachyons@4.12.0/css/tachyons.min.css"/>
<div  class="fr"><label >filter: </label><select  value="0" key="0"><option  value="0">no filter</option><option  value="1">no instances</option><option  value="2">only props</option></select></div><ul  class="list pl0"><li  class="lh-copy mt2" key="0"><strong  class="goal-goals">1 goal</strong></li><li  class="lh-copy mt2" key="1"><ul  key="1107090674" class="list pl0 font-code"><li  key="_mlocal._fresh.180.1093"><span  class="goal-vdash b">⊢ </span><span  class="expr" key="933652813"><span  class="expr-boundary" key="[]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  key="0">0</span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="1">1</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="2">2</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="3">3</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="4">4</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="5">5</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="6">6</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="7">7</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="8">8</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="9">9</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="0">0</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="1">1</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="2">2</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="3">3</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="4">4</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="5">5</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="6">6</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="7">7</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="8">8</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="9">9</span></span></span></span><span  key=" = "> = </span><span  class="expr-boundary" key="[app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  class="dib" style="padding-left: 1ch; text-indent: -1ch; white-space: pre-wrap; vertical-align: top; "><span  class="expr-boundary" key="[app_fn, app_arg]"><span  key="0">0</span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="1">1</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="2">2</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="3">3</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="4">4</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="5">5</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="6">6</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="7">7</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="8">8</span></span></span></span><span  key=" + "> + </span><span  class="expr-boundary" key="[app_arg]"><span  key="9">9</span></span></span></span></span></span></span></li></ul></li></ul>

[Gabriel Ebner]

Generated using:

import tactic.interactive_expr

namespace widget

meta mutual def component.to_html, html.to_html, attr.to_html
with component.to_html : ∀ {Action Props}, Props → component Props Action → list (html empty)
| _ _ p (component.pure view) := do c ← view p, c.to_html
| _ _ p (component.filter_map_action _ c) := c.to_html p
| _ _ p (component.map_props f c) := c.to_html (f p)
| _ _ p (component.with_should_update _ c) := c.to_html p
| _ _ p (component.with_state _ _ init _ _ c) := c.to_html (init p, p)
| _ _ p (component.with_effects emit c) := c.to_html p
with html.to_html : ∀ {Action}, html Action → list (html empty)
| _ (html.element n as cs) := html.element n (as.bind attr.to_html) (cs.bind html.to_html)
| _ (html.of_string s) := [html.of_string s]
| _ (html.of_component p c) := c.to_html p
with attr.to_html : ∀ {Action}, attr Action → list (attr empty)
| _ (attr.style s) := [attr.style s]
| _ (attr.val k v) := [attr.val k v]
| _ (attr.tooltip t) := [attr.tooltip $ html.element "div" [] t.to_html]
| _ _ := []

meta mutual def html.fmt_html, attr.fmt_html
with html.fmt_html : html empty → format
| (html.element n as cs) :=
  let as := (format.join (do a ← as, [format.space ++ a.fmt_html])) in
  (format!"<{n} {as}>{format.join $ cs.map html.fmt_html}</{n}>")
| (html.of_string s) := s
| (html.of_component _ _) := ""
with attr.fmt_html : ∀ {A}, attr A → format
| _ (attr.style s) :=
  let s := string.join (do (k, v) ← s, [sformat!"{k}: {v}; "]) in
  (attr.val "style" s : attr empty).fmt_html
| _ (attr.val "className" v) := format!"class=\"{v}\""
| _ (attr.val k v) := format!"{k}=\"{v}\""
| _ (attr.tooltip t) := ""
| _ _ := ""

end widget

open widget widget_override tactic expr

example : true := by do
g ← mk_meta_var `(0+1+2+3+4+5+6+7+8+9 +
  0+1+2+3+4+5+6+7+8+9 =
  0+1+2+3+4+5+6+7+8+9),
set_goals [g],
s ← read,
trace $ to_fmt "<link rel=\"stylesheet\" href=\"https://unpkg.com/tachyons@4.12.0/css/tachyons.min.css\"/>\n"
  ++ format.join ((widget_override.tactic_state_widget.to_html s).map html.fmt_html)

[Edward Ayers]

If I open that html snippet in chrome it is fine

[Edward Ayers]

Gabriel can you get it to break from the pure html?

[Gabriel Ebner]

Only in vscode (using the HTML preview extension).

[Edward Ayers]

Does it need tachyons style sheet loaded?

[Edward Ayers]

Nevermind you do that

[Edward Ayers]

I don't think it's tachyons because it breaks if you set the style to inline-block directly

[Alex Peattie]

Yep that crashes HTML preview for me too... I think VSCode's webview uses this: https://docs.microsoft.com/en-us/microsoft-edge/webview2/

[Edward Ayers]

Ok well that's annoying. What's the plan now?

[Gabriel Ebner]

I think part of the issue is that we have too many spans. Could we maybe collapse the expr-boundary span and the inline-block span?

[Gabriel Ebner]

(The error goes away if I comment out the expr-boundary span.)

[Edward Ayers]

Ok, I'm a little worried the error will just come back if we make the mwe longer

[Edward Ayers]

Should we flag an issue on vscode somewhere?

[Edward Ayers]

If noone has already done it I will make a PR with the fix

[Edward Ayers]

#3997

[Patrick Massot]

Thanks a lot! Let's hope it works.

[Edward Ayers]

Ok it's in the merge queue. Please post if anything stops working again!

[Patrick Massot]

I really like Ed's triumph message: "Ok I can't find any awful new bugs."

[Bryan Gin-ge Chen]

I don't see it on bors yet, but maybe github actions is just being slow.

[Patrick Massot]

It's still in CI

[Patrick Massot]

But it's also true that bors didn't acknowledge anything here

[Rob Lewis]

Bors seems a little delayed today, it took its time with #3993 too

[Rob Lewis]

Ah, yeah, there are webhook issues on GitHub today.

[Bryan Gin-ge Chen]

Might be the ongoing "API requests" degradation that just popped up there actually.

[Alex Peattie]

I've dug a bit more into the underlying VSCode issue, and it seems like it locks up when it has to render lots of nested elements with display: inline-block or display: inline-table set. So changing "dib" here to something else like "di" or "inline-flex" brings rendering back to full speed, although obviously that breaks the way indenting works currently :crying_cat: