elan downloads only Lean 3, not Lean 4

Stream: general

[Ingmar Velien]

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]

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]

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

[Alex J. Best]

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.