Slow startup time

Stream: lean4

[Floris van Doorn]

Lean is very slow to start, I believe especially on Windows.

I just timed it and it can take 49 seconds to start Lean in a file with no imports (after 48 seconds the "yellow bars" appear).
After Lean is running, it can take 97 seconds to import Mathlib.
As an example, I recorded a low-quality video of me waiting for Lean and the import on my laptop (there's nothing to see other than me waiting).
2024-03-01-19-25-21.mkv

On some students' laptops the performance is worse, and it's quite frustrating.
It would be great if the startup time of Lean can be improved.

[Patrick Massot]

There is a known regression in Lean 4.6.0 that is meant to be fixed in the next version.

[Patrick Massot]

See https://github.com/leanprover/lean4/pull/3552

[Patrick Massot]

But the timing you report are a lot more extreme than what I saw. On my computer I got 15 seconds before the yellow bars.

[Patrick Massot]

Could you try with the fix?

[Patrick Massot]

@Sebastian Ullrich if this commit indeed fixes the issue, do you think we should have a version 4.6.1?

[Floris van Doorn]

Yes, loading Lean on 4.7.0-nightly-2024-03-01 is about 3x as fast for me. That is a huge improvement! Great!

I hope that more improvements can be found though, since the issue of Lean starting slow for me and my students has already existed for many months.

[Patrick Massot]

Yes this is clearly a regression compared to Lean 3. It doesn’t matter too much when expert users use Lean on brand new machines that were bought for that specific purpose. But students tend to have really crappy machines (unsurprisingly).

[Marc Huisinga]

Floris van Doorn said:

Yes, loading Lean on 4.7.0-nightly-2024-03-01 is about 3x as fast for me. That is a huge improvement! Great!

I hope that more improvements can be found though, since the issue of Lean starting slow for me and my students has already existed for many months.

The fix above is not in nightly-2024-03-01 because it landed today.

[Floris van Doorn]

Interesting. I did notice that there was a huge variance in the starting time of Lean, I didn't guess it was this big :-)

[Sebastian Ullrich]

The OS filesystem cache likely plays a huge role when it comes to reading many small files like this

[David Renshaw]

For me, startup time is on the order of 10 seconds for the first file that I open in emacs. I'm puzzled as to why I don't observe a similar startup time when I do lake build from the command line.

[Marc Huisinga]

David Renshaw said:

For me, startup time is on the order of 10 seconds for the first file that I open in emacs. I'm puzzled as to why I don't observe a similar startup time when I do lake build from the command line.

Which Lean 4 version are you using?

[David Renshaw]

v4.6.0

[David Renshaw]

on Linux

[Marc Huisinga]

Try nightly-2024-03-02.

[David Renshaw]

ah, right. OK, I suppose I should wait for that to arrive.

[David Renshaw]

But even if it's a 3x improvement as reported above, I'm curious about what work lake serve is doing that lake build is not.

[David Renshaw]

is it just the infotrees?

[David Renshaw]

Ah, reading https://github.com/leanprover/lean4/pull/3552 now...

[Marc Huisinga]

As described above, Floris didn't actually test the fix.

[David Renshaw]

Oh, I missed that. And mathlib4#11070 is still on nightly-2024-02-29.

[Richard Copley]

@David Renshaw: If you don't already have these customizations, they might help.

 '(lsp-enable-file-watchers nil)
 '(lsp-enable-imenu nil)

[Floris van Doorn]

Now on 4.7.0-nightly-2024-03-02. The yellow bars in VSCode appear near-instantaneously! A file without imports is ready in ~1 second! This is amazing!

[Floris van Doorn]

I tried it a few times just to be sure.