## Stream: new members

#### Chris M (Jul 19 2020 at 04:35):

I just opened VScode today, and instead of doing the usual thing of compiling the code and producing errors, it just says:

Loading...


Here is an image: https://gyazo.com/3362aa391e110124e2e516325c02e1ea.

I've waited for a long time now (15 minutes). What could be the cause of this?
Is Lean actually having to connect to a remote server for me to compile the code? Or is Lean doing this locally?

#### Bryan Gin-ge Chen (Jul 19 2020 at 04:36):

It's all local. Try restarting Lean? (ctrl+p, and then search for "Lean: restart")

#### Bryan Gin-ge Chen (Jul 19 2020 at 04:37):

It's possible that Lean is compiling mathlib, in which case you might have to run leanproject get-mathlib-cache.

#### Chris M (Jul 19 2020 at 04:39):

Interesting, this message just popped up: https://gyazo.com/fc23974c42edc84fe3732978805ff74d

And looking at the task manager, Lean is consuming 4 GB of RAM

#### Chris M (Jul 19 2020 at 04:40):

Is that a normal amount of RAM usage? If so, I'll just have to close other programs.

#### Bryan Gin-ge Chen (Jul 19 2020 at 04:42):

Yeah, that means that Lean is compiling mathlib.

#### Bryan Gin-ge Chen (Jul 19 2020 at 04:44):

Generally you don't want to be doing that from within VS Code. So I would close VS Code first.

If you're working on a branch of mathlib, you should run leanproject get-cache.

If you're working on a project that depends on mathlib, you should run leanproject get-mathlib-cache.

#### Chris M (Jul 19 2020 at 04:45):

ok, thanks, I'll try this.

#### Chris M (Jul 19 2020 at 04:57):

leanproject get-mathlib-cache gives me

Looking for local mathlib oleans
Found local mathlib oleans


while  leanproject get-cache gives me

Failed to fetch mathlib oleans


I presume this means that my project merely depends on mathlib, but is not a branch of mathlib.

#### Bryan Gin-ge Chen (Jul 19 2020 at 04:58):

If your src/ directory has a bunch of files you wrote, then it's a project that depends on mathlib. If the src/ directory looks like this then you're working on mathlib.

#### Bryan Gin-ge Chen (Jul 19 2020 at 04:59):

Anyways, try launching VS Code now, it should hopefully work.

#### Chris M (Jul 19 2020 at 04:59):

yeah it seems to work, thanks :)

#### Chris M (Jul 30 2020 at 18:34):

I'm getting a strange error when trying to upgrade mathlib cache:

\$ leanproject get-mathlib-cache
Looking for local mathlib oleans
Found local mathlib oleans
[Errno 22] Invalid argument: 'C:\\Users\\chris\\dropbox\\programming\\lean\\math_in_lean_cvm\\_target\\deps\\mathlib\\src\\order\\filter\\indicator_function.olean'


Btw, I'm doing this because it's again taking a long time for VSCode to show anything. Is it normal for this to happen often, and for me to have to call leanproject get-mathlib-cache often? And do I still need to call it after calling leanproject up?

#### Kevin Buzzard (Jul 30 2020 at 23:29):

If you don't ever type leanproject up and if you're the only one ever bumping the version of mathlib then you shouldn't ever need to type leanproject anything

#### Utensil Song (Jul 31 2020 at 10:13):

If I'm not using leanproject get xxx_repo, I always do leanpkg configure then leanproject get-mathlib-cache followed by a restart of Lean in VSCode. If anything goes wrong, could try delete _target and do that again, or sometimes leanproject delete_zombies.

Last updated: May 12 2021 at 03:23 UTC