3 ms·

I’ve been very excited by lean, but every time I try to set things up I get riddled with exceptions, errors, library incompatibilities, lean 3/4 problems. Tuts

I’ve been very excited by lean, but every time I try to set things up I get riddled with exceptions, errors, library incompatibilities, lean 3/4 problems. Tuts or documentation that is outdated or just doesn’t work. It has made me wonder, is this just really really alpha software, are they working at a bleeding rate? Idk, but I’ve been enticed multiple times by the promise of lean, maybe I’m just missing some info or should stick it out or just wait until it gets more stable. Anyone have any insight here?

ykonstant 3y ago
Yes, you should expect some frustration, especially if you want to configure things your way. The least painful pipeline should be the following (only follow the instructions at the pages I am listing, as otherwise things may get too confusing): 1) Install lean as a VS Code extension lean4 following : https://leanprover.github.io/lean4/doc/quickstart.html https://leanprover.github.io/lean4/doc/quickstart.html 2) Read about using the build system `lake` here : https://leanprover.github.io/lean4/doc/setup.html https://leanprover.github.io/lean4/doc/setup.html 3) Note that this does not install mathlib4; leave that for later. 4) Start playing around with basic examples in VS Code by reading the beginning sections of https://leanprover.github.io/functional_programming_in_lean/title.html https://leanprover.github.io/functional_programming_in_lean/... 5) If something does not work on break, ask in the Zulip chat; the devs are gathering pain points to improve tooling every day. If this seems too painful, indeed you may want to wait a bit for the tooling to improve.
kmill 3y ago
Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between the two for a little while! The mathlib community has been working on getting the documentation to all refer to Lean 4 -- if you find anything old please point it out on the Zulip. There's usually someone around who can fix it relatively quickly. I think it's better to think of it as bleeding-edge research software rather than alpha software. There might be a little bit of culture shock if you're used to industry-oriented software, but part of this stable version announcement is that there's a new Lean organization that now has resources to improve the experience.

ykonstant 3y ago

Yes, you should expect some frustration, especially if you want to configure things your way. The least painful pipeline should be the following (only follow the instructions at the pages I am listing, as otherwise things may get too confusing): 1) Install lean as a VS Code extension lean4 following : https://leanprover.github.io/lean4/doc/quickstart.html https://leanprover.github.io/lean4/doc/quickstart.html 2) Read about using the build system `lake` here : https://leanprover.github.io/lean4/doc/setup.html https://leanprover.github.io/lean4/doc/setup.html 3) Note that this does not install mathlib4; leave that for later. 4) Start playing around with basic examples in VS Code by reading the beginning sections of https://leanprover.github.io/functional_programming_in_lean/title.html https://leanprover.github.io/functional_programming_in_lean/... 5) If something does not work on break, ask in the Zulip chat; the devs are gathering pain points to improve tooling every day. If this seems too painful, indeed you may want to wait a bit for the tooling to improve.

kmill 3y ago

Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between the two for a little while! The mathlib community has been working on getting the documentation to all refer to Lean 4 -- if you find anything old please point it out on the Zulip. There's usually someone around who can fix it relatively quickly. I think it's better to think of it as bleeding-edge research software rather than alpha software. There might be a little bit of culture shock if you're used to industry-oriented software, but part of this stable version announcement is that there's a new Lean organization that now has resources to improve the experience.