Can VSCode show earlier that Lean is doing something?

Stream: lean4

[Floris van Doorn]

When opening a Lean file, it can take a while for Lean to start up and have executed the import commands so that it can start compiling the file. This is especially the case when the computer is slow and/or you import a lot of files (from Mathlib).

I believe a large part of this time is spent on importing files. During this time, the user gets a signal at one moment that something is happening, which is that the yellow bars show up. Would it be possible to show a message importing files... or even better a semi-regularly updating message imported xxx/yyyy files that keeps track of the progress?

This could have one added advantage. After changing the import commands or adding an import, Lean often takes multiple seconds importing files. It would be useful if during that time, the error message before that change is not shown anymore (and instead it says imported xxx/yyyy files). It is confusing for users to see something like unknown package 'Mathli' when Lean is still executing the import Mathlib command.

[Sebastian Ullrich]

We should clearly distinguish between building dependencies and importing already-built dependencies. Currently we report progress for the latter. Could you give me a better idea of how expensive importing is on the machine in question, e.g. with lake env time lean Mathlib.lean?

[Floris van Doorn]

I agree we should clearly distinguish between the two. In VSCode there is now a significant difference since the extension will prompt before rebuilding any files. But it would be bad if the new message causes confusion and makes people think "blue squiggle under import means that something is going wrong".

This is after a freshly-downloaded lake exe cache get. This is on a pretty powerful laptop (Windows), some students have way older laptops. The first time is much slower for some reason.

Floris@Dell-E MINGW64 ~/projects/mathlib ((afce5534b...))
$ time lake env lean Mathlib.lean

real    0m14.745s
user    0m0.000s
sys     0m0.000s

Floris@Dell-E MINGW64 ~/projects/mathlib ((afce5534b...))
$ time lake env lean Mathlib.lean

real    0m3.803s
user    0m0.000s
sys     0m0.000s

Floris@Dell-E MINGW64 ~/projects/mathlib ((afce5534b...))
$ time lake env lean Mathlib.lean

real    0m3.839s
user    0m0.000s
sys     0m0.015s

[Sebastian Ullrich]

Yes, the filesystem cache greatly helps with subsequent invocations

[Sebastian Ullrich]

Sebastian Ullrich said:

We should clearly distinguish between building dependencies and importing already-built dependencies

Sorry for being unclear here, what I meant by that is that when reloading a file after editing a dependency as you described, it should be building and not importing that takes most of the time (at least, importing should not be any slower from the change). In which case it should already be the case that any previous errors are replaced with the build progress.

[Floris van Doorn]

Executing the import statements takes multiple seconds (when importing a big chunk of mathlib), so editing them is a reliable way for the server to not update for multiple seconds. This is the case even if all imported files are already built.

[Sebastian Ullrich]

Ah, understood. You're talking about changing the import statement itself, not the file behind it.

[Floris van Doorn]

correct (edit: clarified in original message)

[Sebastian Ullrich]

#8199 would reduce this server startup time in/below mathlib by 20%