Why lake go wrong?

Stream: new members

[Takuya]

Hi folks, I was just installing lean and want to go through the MIL tutorial. Here is what I did

1. installed elan
2. cloned the MIL repo

3. lake exe cache get
   I waited, but there is no output or action. Then I tried:

4. lake build
   Again, it just hangs there. I tried lake clean, also hangs.
   I also tried using vscode, either it is always waiting for Lean server to start, or the goal panel appears, but says "message loading" forever. Please help.

[Kevin Buzzard]

how long did you wait for lake exe cache get? Unfortuantely right now when it is cloning mathlib there is no visible indication that anything is happening.

[Robin Arnez]

Yeah in my experience you'll sometimes need to wait a few minutes until it is done

[Robin Arnez]

(or well until it starts to print something)

[Takuya]

Today I tried lake build then it works. I remembered lake exe cache get is faster, so I stopped the process and ran that successfully. Then I was able to see the goal panel in vscode. However yesterday I must have waited for longer but nothing happened. I guess sometimes it really comes down to turn it off and on again, hehe

[Takuya]

Thanks for the help~

[Henrik Böving]

Kevin Buzzard said:

how long did you wait for lake exe cache get? Unfortuantely right now when it is cloning mathlib there is no visible indication that anything is happening.

https://github.com/leanprover/lean4/pull/9332 there will be next rc