Zulip Chat Archive

Stream: new members

Topic: Errors in tutorial setup


view this post on Zulip Gunnar Þór Magnússon (Jan 09 2021 at 20:50):

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?

view this post on Zulip Patrick Massot (Jan 09 2021 at 20:54):

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

view this post on Zulip Patrick Massot (Jan 09 2021 at 20:55):

Where did you see that in the README?

view this post on Zulip 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 elan and leanproject following the appropriate "Regular Install" instructions here: #install ?

view this post on Zulip Patrick Massot (Jan 09 2021 at 21:02):

Oh, I didn't even read that part!

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Jan 10 2021 at 00:55):

Which OS/package manager?


Last updated: May 11 2021 at 00:31 UTC