(Bug?) Lean stuck on the last few files when restarting file

Stream: general

[Weiyi Wang]

Screencast from 2025-08-11 14-34-53.webm
Uploaded a video that records this behavior^

Working in mathlib, sometimes when I switch branch and the file needs a restart because the base branch was different, I think "I'll just restart the file and let my beefy computer rebuild all the dependencies. No need to bother downloading the cache". After clicking "Restart File" and go through all the files to rebuild, the progress often gets stuck at the last two or three files (doesn't seem to be the same file each time). Weirdly enough, the orange bar clears itself as if the rebuilding has completed, but the file doesn't provides linting or updates infoview. When it is in this state, restarting files or changing files are also unresponsive.

Restarting vscode / downloading cache / waiting for 5 more minutes can often clear the problem.

I remember also seeing this behavior in a standalone project with mathlib dependency, but I haven't tried it for a while

Is this a known behavior?

[Marc Huisinga]

I've never seen this issue before. What's your VS Code extension version and Lean version?

[Weiyi Wang]

You reminded me my vscode might be out of date for a month.
vscode : 1.102.3
lean: v4.22.0-rc4

[Marc Huisinga]

What about the extension version? You can check it by using the "Show Setup Information" command.

[Weiyi Wang]

Operating system: Linux (release: 6.8.0-71-generic)
CPU architecture: x64
CPU model: 16 x 11th Gen Intel(R) Core(TM) i7-11700 @ 2.50GHz
Available RAM: 16.64 GB

VS Code version: Reasonably up-to-date (version: 1.103.0)
Lean 4 extension version: 0.0.209
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 4.1.2)
Lean: Reasonably up-to-date (version: 4.21.0)
Project: No open project
Active Lean version: leanprover/lean4:stable (default Lean version)
Installed Lean versions: leanprover/lean4:v4.21.0, leanprover/lean4:v4.22.0-rc2, leanprover/lean4:v4.22.0-rc3, leanprover/lean4:v4.22.0-rc4

(I have just updated vscode after posting the previous message)

[Marc Huisinga]

Thanks, so everything is up-to-date. I'll try to see if I can somehow reproduce this myself. Opening a bug report in the Lean repository would also be helpful; perhaps somebody else will come across this as well.

[Weiyi Wang]

I'll do after collecting some more info. I think it is more likely to reproduce when one changes mathlib versions (= a lot of diff) and lets it build for restarting one file without downloading the cache

[Marc Huisinga]

While I haven't been able to reproduce this, one bug that may have been related to this issue and was fixed recently is lean4#10052, so I would be very curious if this issue still occurs on v4.24.0-rc1.

[Jasper Mulder-Sohn]

While I can't be sure, I remember having similar issues in the past. Mostly I just restarted VS Code and the issues resolved themselves.
Concretely I recognise all of this:

Weirdly enough, the orange bar clears itself as if the rebuilding has completed, but the file doesn't provides linting or updates infoview. When it is in this state, restarting files or changing files are also unresponsive.