Zulip Chat Archive

Stream: new members

Topic: lake binary missing

Jesse Slater (Dec 29 2022 at 03:55):

I am trying to follow the lean4 installation process from the lean manual. I installed elam, which seemed to work, and set it to use the stable release. That seemed to work, but now when I try to use lake, it gives this error: image.png

Reid Barton (Dec 29 2022 at 07:30):

leanprover/lean:nightly is Lean 3. However you set that, you should go and insert a 4 after lean.

Reid Barton (Dec 29 2022 at 07:30):

(And lake didn't exist in Lean 3.)

Last updated: Dec 20 2023 at 11:08 UTC