katex

Stream: general

[Kevin Buzzard]

For me shaking on the goal is fine, but if I start shaking over the entire local context then I get problems

[Alex Peattie]

Ah OK I see the problem (although not new as far as I can see). It's to do with how handle_widget_event handles multithreading/receiving requests faster than the Lean server can handle - which it looks like you flagged already @Edward Ayers : https://github.com/leanprover-community/lean/blob/v3.19.0/src/shell/server.cpp#L630-L632 . It seems that for complicated tactic states, the onMouseEnter/onMouseLeave events start taking a while and they start "stacking up" quite quickly.

[Alex Peattie]

I guess there are a few ways to handle this - one would be changing the behaviour of handle_widget_event on the server-side. We could also have VSCode be smarter about how it dispatches widget events. E.g. if it's waiting for a widget rerender from the server, instead of dispatching another widget event request right away, enqueue it in memory. Then once the widget's rerendered, prune the queue to get rid of duplicate onMouseEnter events etc. :thinking:

[Edward Ayers]

I can't get this lagginess to happen on Scott's file. :/

[Edward Ayers]

I agree that indenting is a huge issue

[Edward Ayers]

But the lagging thing is certainly caused by a queue of events. So the fix is to have lean only keep the latest widget_event in the queue. Maybe @Gabriel Ebner will know how difficult that is. But it still doesn't explain why the issues would have started over the last few days.

[Alex Peattie]

Not to complicate things further, but I was thinking about it and I actually wonder if keeping only the latest widget_event will cause strange behaviour. Like if you hovered and quickly clicked an expression, Lean might throw away either the onMouseEnter or the onClick event, and so the UI only registers either the hover or the click (but not both)...

[Alex Peattie]

Ideally maybe Lean should keep only the latest of each kind of widget_event?

[Edward Ayers]

Yeah that's a good idea

[Edward Ayers]

Indenting fix is on the way thanks to CSS wizardry of @Daniel Fabian and @Gabriel Ebner #3764

[Edward Ayers]

Patrick Massot said:

Wouldn't be easier to work on "jump to definition" in the info view?

#3982

[Kevin Buzzard]

As I've been using widgets more and more I've been realising I'm missing this.

[Scott Morrison]

I don't think it's (laggy highlighting) started in the last few days; I think I've had it all along.

[Patrick Massot]

I'd love to have this merged! I'll give a propaganda talk tomorrow morning, I could certainly use it.

[Gabriel Ebner]

Re: lagging and event queue. Maybe it would help to handle some events directly in the info view instead of sending them back to Lean? For example, we could offload the highlighting like here: https://gebner.github.io/mathlib_docs/geometry/euclidean/circumcenter.html#euclidean_geometry.exists_unique_dist_eq_of_insert

[Patrick Massot]

Oh, is this new?

[Gabriel Ebner]

The flashy highlighting? I've been toying around with the idea for a while, but this is not the official documentation page.

[Patrick Massot]

Yes, the flashy highlighting. Maybe the color gradient is a bit too much, but some highlighting is nice.

[Edward Ayers]

I love the gradient

[Rob Lewis]

I forgot about @Gabriel Ebner 's highlighting to the docs, sorry! Do people feel like it's too much? I like it and it adds functionality.

[Rob Lewis]

(https://github.com/leanprover-community/doc-gen/pull/59)

[Sebastien Gouezel]

I like the idea of highlighting a lot. If we have to choose between the two color schemes, I prefer the first one (one color, with a gradient) over the second one (random rainbow colors, too much "flower power" for my taste)

[Rob Lewis]

But how else will we capture Lean's hippie spirit? :peace:

[Rob Lewis]

It matches Kevin's pants!

[Johan Commelin]

I can totally see a footnote at the bottom of the docs page

UI design by Kevin's pants, Inc.

[Rob Lewis]

Here's an alternative color scheme: https://github.com/leanprover-community/doc-gen/pull/73