can't install a specific version

Stream: new members

[sho]

hey all. grad student from India. i am trying to setup lean + mathlib with 4.15.0. First I am installing elan, setting default version to 4.15.0 then setting up a new project using lake +/leanprover:v4.15.0 new <name> math and then lake update lake build.

Lake update always changes the version number to 4.17 but without that mathlib doesn't import

[Julian Berman]

What's in your lakefile.toml -- you sohuld be pinning Mathlib via a git tag basically

[Kevin Buzzard]

Why do you want an old version of lean+mathlib by the way? Whenever I make a new project I just use today's version

[sho]

It's for a project. We all have to have the same setup and everything.

[Kevin Buzzard]

git ensures that you all have the same setup and everything with my collaborators.