Zulip Chat Archive

Stream: lean4

Topic: Has Lean 4 gotten slower?


view this post on Zulip Gabriel Ebner (Jan 29 2021 at 13:46):

I remember being positively surprised by how snappy the language server was in 4.0.0-M1.
But now there seems to be a one second delay before you get any response from lean.

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 13:49):

That would most likely be https://github.com/leanprover/lean4/pull/285 :)
We haven't fine-tuned the delay yet, and it also feels much longer than that sometimes, not sure about that yet

view this post on Zulip Gabriel Ebner (Jan 29 2021 at 14:00):

I believe Lean waits until you haven't typed anything for a second. So the delay can even be infinitely long.

view this post on Zulip Mario Carneiro (Jan 29 2021 at 14:03):

I think something more like 200ms is appropriate - slow enough that if you are in the middle of typing it doesn't try to elaborate all the time but picking up as soon as you stop or slow down

view this post on Zulip Mario Carneiro (Jan 29 2021 at 14:04):

100ms would be great since that's about when people notice a delay but that's too fast for typing so you probably won't get much benefit from a delay that shourt

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 14:04):

Yeah, we should definitely give a lower delay a try

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 14:05):

As well as actually cancelling elaboration tasks

view this post on Zulip Gabriel Ebner (Jan 29 2021 at 14:06):

In lean 3 we use 100ms.

view this post on Zulip Gabriel Ebner (Jan 29 2021 at 14:06):

(And 200ms for the orange progress bars.)

view this post on Zulip Gabriel Ebner (Jan 29 2021 at 14:07):

The lean 3 delay is actually just for the error messages. Processing starts immediately after each keystroke.

view this post on Zulip Mario Carneiro (Jan 29 2021 at 14:08):

yeah, rather than delaying the processing you can just cancel the previous elaboration, although that causes issues if the processing delay is long because then the user doesn't get any response until they stop and wait

view this post on Zulip Mario Carneiro (Jan 29 2021 at 14:10):

I haven't tried having a bounded number of in-flight requests (greater than one), that might work to get the best of both worlds

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 14:12):

We do allow parallel requests up to the hardware thread count. There's nothing easy about (timely) cancelling elaboration tasks though.

view this post on Zulip Bryan Gin-ge Chen (Jan 29 2021 at 16:44):

Is it worth making this time configurable via an editor setting?

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 16:50):

Probably, yes

view this post on Zulip Wojciech Nawrocki (Jan 29 2021 at 18:31):

Yeah, the plan is to make it an editor option. Users should also be able to set it to 0 in which case elaboration is launched immediately, but beware that this will absolutely eat up your CPU. Personally I don't find it useful to see diagnostics for every half-typed word, so I would use at least 200ms.

view this post on Zulip Huỳnh Trần Khanh (Jan 31 2021 at 01:51):

There is a post on Stack Exchange that I think might be helpful https://ux.stackexchange.com/a/110444

view this post on Zulip François G. Dorais (Jan 31 2021 at 05:38):

And the Doherty Threshold article linked there suggests < 400ms is necessary to make Lean "addictive"... I am very far from an expert on this but 500ms seems like a very long default value from my recent experience.

Huỳnh Trần Khanh said:

There is a post on Stack Exchange that I think might be helpful https://ux.stackexchange.com/a/110444

view this post on Zulip Joe Hendrix (Feb 04 2021 at 03:22):

Would it be at all feasible to maybe prioritize elaboration? e.g., You may want the current declaration and visible declarations to be elaborated quickly, but happy to queue up inferring effects on other definitions until more time has passed.

view this post on Zulip Joe Hendrix (Feb 04 2021 at 03:24):

I've been thinking about exploring this in a vscode plugin I'm working on for another language.

view this post on Zulip Sebastian Ullrich (Feb 04 2021 at 08:54):

It wasn't prioritization per se, but in Lean 3 we have a mode to elaborate only on-screen content. Bringing that to Lean 4 would necessitate extending the LSP.

view this post on Zulip Gabriel Ebner (Feb 04 2021 at 09:00):

Lean 3 both prioritizes visible declarations (by default), and has a mode to only elaborate on-screen content (you can click on the "(checking visible files)" in the status bar and change it to "visible lines", or "visible lines and above", or a few other options).

view this post on Zulip Gabriel Ebner (Feb 04 2021 at 09:02):

Unfortunately this is less useful than it could be, because Lean 3 can't lower the priority of a task again. So once something has been on screen, Lean will prioritize it even if you switch to another file. I was really happy to see this in Lean 4: files just stop elaborating when you switch to another file, and then continue when you switch back.

view this post on Zulip Johan Commelin (Feb 04 2021 at 09:04):

@Gabriel Ebner in Lean 3, if you close a tab in VScode, is it still high prio? (And once you reopen it?)

view this post on Zulip Gabriel Ebner (Feb 04 2021 at 09:11):

I don't remember precisely, but I think it remains high prio.

view this post on Zulip Johan Commelin (Feb 04 2021 at 09:13):

aha, that might explain some crazy experiences I had, that were only fixed by restarting the server.


Last updated: May 07 2021 at 13:21 UTC