Stream: new members
Topic: Lean keeps "Loading..."
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:
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
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
If you're working on a project that depends on mathlib, you should run
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
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):
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
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
Last updated: May 12 2021 at 03:23 UTC