High CPU usage and no goal windows in VSCode

Stream: new members

[Eric Wieser]

I'm finding that after running the "lean restart" command, lean.exe is consuming a lot of CPU, and my VScode goal window remains empty. How can I work out what it's doing and why it's taking so long?

[Eric Wieser]

(could it be rebuilding mathlib behind the scenes?)

[Patrick Stevens]

Very possibly - if you close down Lean, do leanproject get-cache, and start Lean up again, is everything fixed?

[Patrick Stevens]

(i.e. ask leanproject to get the compiled .olean files from the Internet and replace your local ones with them)

[Kevin Buzzard]

or leanproject get-mathlib-cache if mathlib is a dependency of your project

[Utensil Song]

Did you updated mathlib without using leanproject up? Then it must be fixed by leanproject get-mathlib-cache or the orange bar will be there like forever.

[Utensil Song]

And I did leanproject up on the master. So you might need to run leanpkg configure and leanproject get-mathlib-cache after pulling.

[Eric Wieser]

I think I accidentally modified a file in mathlib while reading through it, and lean decided to rebuild the universe. Updating mathlib fixed that.

[Utensil Song]

Yes it could happen if the file is at the very bottom of the import graph.

[Utensil Song]

I don't know if this is addressed by Lean 4

[Utensil Song]

There seems to be a completely different import mechanism and compilation model (don't know if it supports incremental or not) in Lean 4.