## Stream: new members

### Topic: High CPU usage and no goal windows in VSCode

#### Eric Wieser (Jul 02 2020 at 17:54):

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 (Jul 02 2020 at 17:54):

(could it be rebuilding mathlib behind the scenes?)

#### Patrick Stevens (Jul 02 2020 at 20:59):

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

#### Patrick Stevens (Jul 02 2020 at 20:59):

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

#### Kevin Buzzard (Jul 02 2020 at 21:29):

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

#### Utensil Song (Jul 03 2020 at 06:46):

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 (Jul 03 2020 at 06:48):

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 (Jul 03 2020 at 13:53):

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 (Jul 03 2020 at 14:04):

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

#### Utensil Song (Jul 03 2020 at 14:04):

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

#### Utensil Song (Jul 03 2020 at 14:05):

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

Last updated: May 12 2021 at 04:19 UTC