Zulip Chat Archive

Stream: new members

Topic: Lean keeps "Loading..."


view this post on Zulip 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?

view this post on Zulip 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")

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 04:42):

Yeah, that means that Lean is compiling mathlib.

view this post on Zulip 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.

view this post on Zulip Chris M (Jul 19 2020 at 04:45):

ok, thanks, I'll try this.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 04:59):

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

view this post on Zulip Chris M (Jul 19 2020 at 04:59):

yeah it seems to work, thanks :)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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