Errors in tutorial setup

Stream: new members

[Gunnar Þór Magnússon]

Hello,

I'm trying to follow along the Lean tutorial here: https://github.com/leanprover-community/tutorials

I've installed Lean 3.5.1, and ran "leanproject get tutorials" to fetch the tutorial setup (with leanproject version 1.0.0). When I try to run the "lean" command on anything inside the directory I get (which has a leanpkg.path to point lean to the vendored mathlib), it runs for a few minutes, consumes a few CPUs, and writes a continuous stream of errors like:

tutorials/_target/deps/mathlib/src/tactic/interactive_expr.lean:265:0: error: unknown identifier 'tc.stateless'

Am I doing something obviously wrong here?

[Patrick Massot]

I don't know those errors, but why are you running lean on anything?

[Patrick Massot]

Where did you see that in the README?

[Bryan Gin-ge Chen]

Lean 3.5.1 is horribly old and the tutorials require Lean 3.23.0. Did you install elan and leanproject following the appropriate "Regular Install" instructions here: #install ?

[Patrick Massot]

Oh, I didn't even read that part!

[Gunnar Þór Magnússon]

No, I trusted my OS to have up-to-date packages. I'll follow those instructions. Thanks.

[Alex J. Best]

Which OS/package manager?