Zulip Chat Archive

Stream: general

Topic: elan downloads only Lean 3, not Lean 4

Ingmar Velien (Apr 17 2022 at 13:44):

Next installation problem: I installed Lean on Windows according to https://leanprover-community.github.io/install/windows.html, but with manually installing elan. But I got Lean version 3.42.1 instead of the curent version 4.0.0. Somewhere is written that Lean 4 doesn't has the mathlib library. Another source writes that Lean 4 doesn't use leanpkg.toml, that would be a Lean 3 thing. But elan works with leanpkg.toml.
1.) Are these information still up to date?
2.) What is the right directory for installing Lean 4.0.0?

Henrik Böving (Apr 17 2022 at 13:49):

The way to install Lean 4 is: https://leanprover.github.io/lean4/doc/setup.html#basic-setup
Lean 4 doesnt have a full port of mathlib but a very minimal subset: https://github.com/leanprover-community/mathlib4 if you are interested in higher level mathematics you wont get happy with this though
We use lake and lakefiles instead of leanpkg.toml

Ingmar Velien (Apr 17 2022 at 13:53):

Thank you for this quick answer. It's valuable also for other new users. Thanks.

Alex J. Best (Apr 17 2022 at 14:08):

Elan can download both lean 3 and lean 4 for you (and any subversion of those also), as there are significant numbers of people using both lean 3 and lean 4 right now this is by design.

Last updated: Dec 20 2023 at 11:08 UTC