Lake with lean version and math

Stream: general

[Bolton Bailey]

When I run

> lake +leanprover/lean4:v4.18.0 new WithMathlibFourEighteen math

I get a repo with toolchain leanprover/lean4:v4.19.0-rc3

Is this right? Is there a way to install a mathlib 4.18 from lake new?

[Kevin Buzzard]

My understanding is that that is indeed "right" in the sense that the +leanprover/lean4:v4.18.0 is used to decide which version of Lean is being run by Lake when it's being run to make the project, but then math decides that you must mean "give me bleeding edge mathlib in my project" and so it makes the project with bleeding edge lean.

[Bolton Bailey]

Ok, makes sense, still worth fixing IMHO. I opened lean4#8123. (Notice that it gives the intended toolchain if math isn't provided)

[Kevin Buzzard]

FWIW I think the trick to sort your project out is

 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
+rev = "v4.18.0"

(i.e. add rev = ... in your lakefile.toml) and then lake update mathlib

[Kevin Buzzard]

oh no that's not right, looks like you also have to manually edit lean-toolchain to leanprover/lean4:v4.18.0 before lake update mathlib will work

[Kevin Buzzard]

I've tried it and indeed it looks like the project now has mathlib on tag v4.18.0 (from 1st April)