Zulip Chat Archive

Stream: new members

Topic: Linux setups

antonio (Dec 17 2021 at 23:25):

I have just installed Lean 4 in my Arch Linux with:

yay -Syu elan-lean
elan default leanprover/lean4:stable

I also installed lean4-mode for Emacs.

Now, to create my first project, should I install and use leanproject or leanpkg?

Adam Topaz (Dec 17 2021 at 23:29):

For lean4, if I understand correctly, one should use lake new

Adam Topaz (Dec 17 2021 at 23:30):

It's good to know that elan is in the AUR btw.

Adam Topaz (Dec 17 2021 at 23:31):

I'm not sure if lake comes with lean4:stable... You may have to switch to the nightly release

antonio (Dec 17 2021 at 23:38):

I can't find it, now I install a nightly release

antonio (Dec 17 2021 at 23:45):

@Adam Topaz, after: 

elan default leanprover/lean4:nightly

lake is still not available

Adam Topaz (Dec 17 2021 at 23:45):

What does lean --version give?

antonio (Dec 17 2021 at 23:47):

Lean (version 4.0.0-nightly-2021-12-17, commit e65f3fe81032, Release)

Adam Topaz (Dec 17 2021 at 23:48):

And I suppose which lake gives nothing?

antonio (Dec 17 2021 at 23:48):

lake not found

Adam Topaz (Dec 17 2021 at 23:49):

this might be an issue with the fact that you installed elan though aur.

Adam Topaz (Dec 17 2021 at 23:49):

I think it's worthwhile asking in the #lean4 stream.

antonio (Dec 17 2021 at 23:50):

thanks

Last updated: Dec 20 2023 at 11:08 UTC