Zulip Chat Archive

Stream: general

Topic: katex


view this post on Zulip Kevin Buzzard (Aug 29 2020 at 18:43):

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

view this post on Zulip Alex Peattie (Aug 30 2020 at 08:40):

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.

view this post on Zulip Alex Peattie (Aug 30 2020 at 08:40):

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:

view this post on Zulip Edward Ayers (Aug 30 2020 at 08:52):

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

view this post on Zulip Edward Ayers (Aug 30 2020 at 08:52):

I agree that indenting is a huge issue

view this post on Zulip Edward Ayers (Aug 30 2020 at 08:57):

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.

view this post on Zulip Alex Peattie (Aug 30 2020 at 09:01):

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)...

view this post on Zulip Alex Peattie (Aug 30 2020 at 09:02):

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

view this post on Zulip Edward Ayers (Aug 30 2020 at 09:02):

Yeah that's a good idea

view this post on Zulip Edward Ayers (Aug 30 2020 at 11:26):

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

view this post on Zulip Edward Ayers (Aug 30 2020 at 12:07):

Patrick Massot said:

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

#3982

view this post on Zulip Kevin Buzzard (Aug 30 2020 at 12:26):

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

view this post on Zulip Scott Morrison (Aug 30 2020 at 12:57):

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

view this post on Zulip Patrick Massot (Aug 30 2020 at 14:45):

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

view this post on Zulip Gabriel Ebner (Aug 30 2020 at 15:00):

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

view this post on Zulip Patrick Massot (Aug 30 2020 at 15:02):

Oh, is this new?

view this post on Zulip Gabriel Ebner (Aug 30 2020 at 15:04):

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

view this post on Zulip Patrick Massot (Aug 30 2020 at 15:04):

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

view this post on Zulip Edward Ayers (Aug 30 2020 at 16:38):

I love the gradient

view this post on Zulip Rob Lewis (Sep 24 2020 at 08:33):

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.

view this post on Zulip Rob Lewis (Sep 24 2020 at 08:33):

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

view this post on Zulip Sebastien Gouezel (Sep 24 2020 at 08:44):

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)

view this post on Zulip Rob Lewis (Sep 24 2020 at 08:45):

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

view this post on Zulip Rob Lewis (Sep 24 2020 at 08:46):

It matches Kevin's pants!

view this post on Zulip Johan Commelin (Sep 24 2020 at 09:02):

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

UI design by Kevin's pants, Inc.

view this post on Zulip Rob Lewis (Sep 24 2020 at 09:32):

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


Last updated: May 09 2021 at 19:11 UTC