Has Lean 4 gotten slower?

Stream: lean4

[Gabriel Ebner]

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.

[Sebastian Ullrich]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

Yeah, we should definitely give a lower delay a try

[Sebastian Ullrich]

As well as actually cancelling elaboration tasks

[Gabriel Ebner]

In lean 3 we use 100ms.

[Gabriel Ebner]

(And 200ms for the orange progress bars.)

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

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

[Bryan Gin-ge Chen]

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

[Sebastian Ullrich]

Probably, yes

[Wojciech Nawrocki]

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.

[Huỳnh Trần Khanh]

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

[François G. Dorais]

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

[Joe Hendrix]

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.

[Joe Hendrix]

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

[Sebastian Ullrich]

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.

[Gabriel Ebner]

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

[Gabriel Ebner]

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.

[Johan Commelin]

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

[Gabriel Ebner]

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

[Johan Commelin]

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

[Wojciech Nawrocki]

Bryan Gin-ge Chen: Is it worth making this time configurable via an editor setting?

This should now be possible in the next (current) vscode-lean4 release.