Stream: new members
Topic: Errors in tutorial setup
Gunnar Þór Magnússon (Jan 09 2021 at 20:50):
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 (Jan 09 2021 at 20:54):
I don't know those errors, but why are you running
lean on anything?
Patrick Massot (Jan 09 2021 at 20:55):
Where did you see that in the README?
Bryan Gin-ge Chen (Jan 09 2021 at 21:01):
Lean 3.5.1 is horribly old and the tutorials require Lean 3.23.0. Did you install
leanproject following the appropriate "Regular Install" instructions here: #install ?
Patrick Massot (Jan 09 2021 at 21:02):
Oh, I didn't even read that part!
Gunnar Þór Magnússon (Jan 09 2021 at 21:10):
No, I trusted my OS to have up-to-date packages. I'll follow those instructions. Thanks.
Alex J. Best (Jan 10 2021 at 00:55):
Which OS/package manager?
Last updated: May 11 2021 at 00:31 UTC