Error requiring MathLib in lake

Stream: new members

[Trevor Hyde]

Very new to Lean. I have downloaded other people's projects and successfully tinkered with them, but now I'm trying to create my own new project. I want to be able to use MathLib, so I am trying to update my lake file.
Screenshot 2025-01-13 at 3.40.47 PM.png
Everything in the lake file updates fine until I added the line starting "require". When I try to update I then get this error:
Screenshot 2025-01-13 at 3.41.58 PM.png
I can't figure out the issue. This lake file is copied nearly directly from another one in a project that works (with the name of the project updated.) Help?

[Ruben Van de Velde]

What I think happens is that the version of lean and lake you're using is too old to understand the lakefile in mathlib

[Ruben Van de Velde]

What's in your lean-toolchain file?

[Trevor Hyde]

It only contains the line:
leanprover/lean4:stable

[Trevor Hyde]

Here are my lean and lake versions
Lean (version 4.8.0, aarch64-apple-darwin, commit df668f00e6c0, Release)
Lake version 5.0.0-df668f0 (Lean version 4.8.0)

[Ruben Van de Velde]

That's much too old to work with a recent version of mathlib

[Julian Berman]

Change therequire line to say: require "leanprover-community" / "mathlib4" @ git "v4.15.0" -- does it work then?

[Julian Berman]

(Remove both lines 13 and 14)

[Ruben Van de Velde]

You can update it to leanprover/lean4:v4.15.0 and... yeah, that

[Mauricio Collares]

To (arguably) clarify Ruben's message, "update it to leanprover/lean4:v4.15.0" means replacing the contents of the lean-toolchain file with leanprover/lean4:v4.15.0. There are elan commands to update the stable version, but this way's easier.

[Trevor Hyde]

Screenshot 2025-01-13 at 3.57.09 PM.png
Thanks for the quick help! Updating lean fixed most of the errors, but now I'm getting this one which I don't understand.

Also, for future reference, what is the command for keeping both lean and lake up to date?

[Julian Berman]

Thanks for the quick help! Updating lean fixed most of the errors, but now I'm getting this one which I don't understand.

Uh, I guess the right line to have given you was require "leanprover-community" / "mathlib" @ git "v4.15.0" (with no 4), which I always forget.

[Julian Berman]

(So change to that.)

[Ruben Van de Velde]

Oh wow, for real. I learned something new today

[Julian Berman]

Yes because it's not a repo name it's a reservoir scope thingy I think when you use that syntax.

[Julian Berman]

("Package" it looks like is the verbiage lake uses. I like "thingy".)

[Trevor Hyde]

It's working--thanks everyone :pray: