Zulip Chat Archive

Stream: new members

Topic: Failed to load

Alex Zhang (Jun 14 2021 at 15:23):

My Lean keeps loading when importing anything. I don't know how to fix this issue. Could anyone please give me a help?
image.png

Adam Topaz (Jun 14 2021 at 15:26):

Are you using leanpkg? You probably need to fetch the olean files

Bryan Gin-ge Chen (Jun 14 2021 at 15:27):

Did you get Mathematics in Lean by running leanproject get mathematics_in_lean? Were there any error messages when you ran that command?

Alex Zhang (Jun 14 2021 at 15:27):

No. There isn't any error message. Just endless loading...

Alex Zhang (Jun 14 2021 at 15:28):

What is leanpkg?

Kevin Buzzard (Jun 14 2021 at 15:28):

something you don't need to know about

Bryan Gin-ge Chen (Jun 14 2021 at 15:28):

The endless loading is because VS Code can't find compiled olean files for mathlib and is trying to build it from scratch.

You should download the necessary files by using leanproject.

Alex Zhang (Jun 14 2021 at 15:30):

How should I exactly do this?

Kevin Buzzard (Jun 14 2021 at 15:30):

Did you follow the instructions here? https://leanprover-community.github.io/get_started.html

Kevin Buzzard (Jun 14 2021 at 15:31):

If so then you can install Lean projects by following the instructions here https://leanprover-community.github.io/install/project.html

Alex Zhang (Jun 14 2021 at 15:33):

Yes, I installed those already. My Lean worked normally before a crash of my laptop today. Then I restarted my laptop and the issue arose.

Alex Zhang (Jun 14 2021 at 15:38):

too weird...

Bryan Gin-ge Chen (Jun 14 2021 at 15:42):

You could try running leanproject get-mathlib-cache from the mathematics_in_lean directory; that should re-download the files that are needed.

Alex Zhang (Jun 14 2021 at 16:40):

Bryan Gin-ge Chen said:

You could try running leanproject get-mathlib-cache from the mathematics_in_lean directory; that should re-download the files that are needed.

Unfortunately, this didn't work..

Bryan Gin-ge Chen (Jun 14 2021 at 16:40):

What was the output of leanproject get-mathlib-cache?

Alex Zhang (Jun 14 2021 at 16:41):

@Bryan Gin-ge Chen 

DELL@DESKTOP-NRHI2C3 MINGW64 ~/tutorials/mathematics_in_lean (master)
$ leanproject get-mathlib-cache
Looking for local mathlib oleans
Found local mathlib oleans

Bryan Gin-ge Chen (Jun 14 2021 at 16:42):

Ah, I see. In your screenshot it looks like you opened the directory "tutorials" which contains both lftcm2020 and mathematics_in_lean. Try opening just the subdirectory mathematics_in_lean in VS Code.

Bryan Gin-ge Chen (Jun 14 2021 at 16:43):

I don't think the VS Code extension currently supports opening directories containing multiple Lean projects.

Alex Zhang (Jun 14 2021 at 16:47):

Aha, it seems that if I open a single project, then this endless loading problem disappears. (I am not a CS or engineering person, such issues at times confuse me...)

Bryan Gin-ge Chen (Jun 14 2021 at 16:49):

We could probably clarify the wording somewhere to make this more clear. Do you have a suggestion for a place where a warning would have helped you avoid this?

Alex Zhang (Jun 14 2021 at 16:51):

Not really sure now. I will propose if I get any.
Thanks a lot for your help!

Last updated: Dec 20 2023 at 11:08 UTC