Lean keeps "Loading..."

Stream: new members

[Chris M]

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]

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

[Bryan Gin-ge Chen]

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

[Chris M]

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]

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

[Bryan Gin-ge Chen]

Yeah, that means that Lean is compiling mathlib.

[Bryan Gin-ge Chen]

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]

ok, thanks, I'll try this.

[Chris M]

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]

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]

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

[Chris M]

yeah it seems to work, thanks :)

[Chris M]

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]

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]

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.