startup time in VS Code

Stream: general

[Kevin Buzzard]

Here's something I don't understand. When doing experiments (e.g. answering user questions on Zulip) I often type import Mathlib in a scratch file in my local copy of the mathlib repo (on the master branch). Now say I want to update mathlib. I exit VS Code (just for safety's sake), type git pull then lake exe cache get then lake build just to check everything worked, and it's always the case that lake build terminates successfully in a couple of seconds. I then open VS Code again, and it opens at the file which begins import Mathlib and after a few seconds the orange bars appear, and then I have to wait for 10 seconds and my memory fills up and the fan comes on and my swap fills up and I get a warning saying "Zulip has become unresponsive", and then the orange bars disappear and I dismiss the Zulip warning and I'm back to a slick experience.

Is this expected or am I missing a trick? Or is the trick to click "buy" on this new laptop?

[Damiano Testa]

I very rarely use import Mathlib on my computer: I only use it in the online playground.

[Marc Huisinga]

For me, on a fairly recent Framework laptop (i.e. not some super powerful desktop machine or Mac, but a fairly recent AMD laptop CPU with an SSD), the orange bars appear almost immediately, and then it takes roughly 2-3s for them to disappear. After that, Lean is still busy for another 6s or so. In total, it takes roughly 10s until Lean has settled entirely, and 4-5s until the orange bars disappear.

The sequence of events is roughly as follows:

1. You launch VS Code. VS Code starts initializing itself.
2. VS Code starts initializing the Lean 4 VS Code extension "some time after" VS Code has finished initializing. Since all extensions share the extension host process, this is likely done in sequence, so having other extensions installed might delay the initialization of the Lean 4 VS Code extension.
3. The Lean 4 VS Code extension detects an open Lean tab and starts initializing a language client (provided by VS Code) for the Lake project that the corresponding Lean file belongs to. This involves launching the language server process and performing the LSP initialization dance. If this process takes longer than 250ms, the Lean 4 VS Code extension starts displaying a progress bar in the bottom right.
4. Once the language server process has launched and has been informed about the open Lean file by the language client, it launches another process (the so-called "file worker") that elaborates the file.
5. Additionally, once the language server process has launched, it starts loading the .ilean files of the whole project. This only needs to be done once for the whole project, and it is done in parallel with the rest of the server operations, so except for consuming CPU usage of one of your cores and putting some pressure on your storage medium, it should not interfere with the latency of other server operations. This is the part that causes Lean to be busy for another 6s or so on my laptop.
6. Once the file worker process has launched, it starts displaying orange progress bars for the file. The orange bars for the import section of the file remain until we have heard back from Lake about the current status of the imports and until all .olean files from the import section of the file have been loaded into the file worker process. For import Mathlib, this includes all .olean data for all of Mathlib.
7. Once all .olean data has been imported, the file worker process starts processing the file beyond the set of imports, and the orange progress bars move down in the file.

VS Code startup

[Johan Commelin]

Do (5)-(7) also happen when you type lake build on the command line? Or is there less work involved?

[Marc Huisinga]

If there is nothing to build, then there is definitely less work involved.

[Marc Huisinga]

One thing that is perhaps also worth pointing out is that if you launch VS Code with lots of open tabs, then the Lean 4 VS Code extension will initialize separate language clients (i.e. everything from step 3 onwards) for every single project in your tabs, and VS Code's language client library will also inform the language server about every open file in your tabs (i.e. everything from step 4 onwards for every single open Lean file). So if you have lots of open tabs, this can definitely exhaust your CPU resources and slow down the whole process for every individual file.

This is unfortunately just how VS Code's language client library works at the moment, and there is currently no good way to disambiguate visible tabs from invisible tabs on either the VS Code side or the language server side.

[Kevin Buzzard]

Oh many thanks Marc! I habitually have ten or more tabs open in VS Code so this is my mistake! I had no idea this made a difference, I am completely clueless about what's going on under the hood (or at least I was before your very informative messages). I can easily change this part of my workflow.

@Damiano Testa I have been burnt too often by importing "the right amount" and then exact? failing because it turns out that I had only imported the right amount to make the statements compile. With this new trend of having many Defs.lean files in mathlib this was happening more and more often to me, so I've switched to always importing everything.

[Kevin Buzzard]

If there was a version of exact? which would find declarations which I hadn't imported then this would be another viable solution for me but right now I'm just super excited to learn that closing all but one of my tabs will make my life a lot better.

[Kevin Buzzard]

PS :-/

code.png

[Marc Huisinga]

Kevin Buzzard said:

I'm just super excited to learn that closing all but one of my tabs will make my life a lot better.

To be clear, this should only matter when booting up VS Code. In general, while there will be active file worker processes for tabs that aren't visible, these invisible files shouldn't consume much CPU and should mostly be idle. It's only when you start or restart the language server that all open tabs are elaborated, which is expensive.

[Shanghe Chen]

Marc Huisinga said:

This is unfortunately just how VS Code's language client library works at the moment, and there is currently no good way to disambiguate visible tabs from invisible tabs on either the VS Code side or the language server side.

Currently the lean language server starts the file worker child progress once it receives the corresponding didOpen request. Would it be better decoupling it to a dedictated rpc method for starting the file worker?

[Marc Huisinga]

Shanghe Chen said:

Marc Huisinga said:

This is unfortunately just how VS Code's language client library works at the moment, and there is currently no good way to disambiguate visible tabs from invisible tabs on either the VS Code side or the language server side.

Currently the lean language server starts the file worker child progress once it receives the corresponding didOpen request. Would it be better decoupling it to a dedictated rpc method for starting the file worker?

Unfortunately no. We used to do something along these lines in the past (namely, we used a language client middleware to filter certain didOpen notifications to the server for files that weren't in the set of tabs at all, as VS Code sometimes spuriously emits didOpen for those kinds of files as well), but it caused all kinds of race conditions that were very difficult to track down with VS Code's language client library itself, some of which are mentioned in the linked thread.
Put simply, the language client library expects didOpen notifications to be emitted at the exact point where it emits them, and if you change anything about when or whether didOpen notifications are emitted, you will run into all kinds of problems.

The only good solution for this problem that doesn't have any major drawbacks is for the language client library to implement this feature itself and ensure that it doesn't race with any of its other features by design. Fortunately, in the linked thread, we were eventually able to convince the LSP maintainer that this is a needed feature, and they implemented it afterwards. On the other hand, unfortunately, Microsoft appears to have de-prioritized all work on LSP immediately after that, so this feature hasn't been released in a stable version yet and the LSP maintainer still appears to be busy working on other VS Code topics.

[Kevin Buzzard]

Marc Huisinga said:

Kevin Buzzard said:

I'm just super excited to learn that closing all but one of my tabs will make my life a lot better.

To be clear, this should only matter when booting up VS Code. In general, while there will be active file worker processes for tabs that aren't visible, these invisible files shouldn't consume much CPU and should mostly be idle. It's only when you start or restart the language server that all open tabs are elaborated, which is expensive.

Oh I often restart the language server if I change imports and get the "imports out of date" error. I click the button, wait for a while, and then restart the server if I get bored waiting for it to finish on the basis that for all I know it might make things faster. Can you clarify the difference between "Restart file" and "Restart server"? To me these are just synonymous, I don't even know what a server is, they just both mean "start again after a pause" as far as I am concerned.

[Marc Huisinga]

'Restart file' rebuilds the imports if necessary and starts re-elaborating the file from the top. 'Restart server' restarts the full language server, which is something that you should only need to do when Lean has somehow started breaking.
See also the corresponding extension manual section.

[Marc Huisinga]

'Restart server' also doesn't rebuild the imports of any file, it really just restarts the language server process in case something went wrong.