lake new project with specified lean version?

Stream: new members

[Shanghe Chen]

Hi is there an option for lake new <ProjectName> with specified lean version? Currently it seems always the stable version

[Wang Jingting]

One possible way I've used before is to manually modify the lakefile. For example, if you're using a lakefile.toml, then you can probably change the corresponding section to
[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.15.0"

[Shanghe Chen]

Yeah currently I find only the manual way too

[Sebastian Ullrich]

In combination with elan, you can use e.g. lake +4.15.0 new ..., though that does not (currently) affect the Mathlib version used by the math template

[Sebastian Ullrich]

@Mac Malone Might be a good idea to point out this elan feature in lake new --help

[Shanghe Chen]

wow awesome! Yeah lake new -h doesn’t show this

[Mac Malone]

@Sebastian Ullrich This was a small change, so a PR with is up at lean4#7024.

[Shanghe Chen]

Mac Malone said:

Sebastian Ullrich This was a small change, so a PR with is up at lean4#7024.

Hi I saw that the PR also change the doc for default configuration from lean to toml. Which version is it switched?

[Mauricio Collares]

4.13.0 (lean4#5504)

[Shanghe Chen]

Mauricio Collares said:

4.13.0

Thanks!

[Alexandre Rademaker]

This is not working for me. In MacOS, lake is ignoring the flag for version v4.15.0

% lake +v4.15.0 new test math
% cd test
% cat lean-toolchain
leanprover/lean4:v4.18.0-rc1

[Alexandre Rademaker]

It is even worst. I executed

% lake +v4.15.0 init test math

It ignored me but I edited the lean-toolchain changing to version v4.15.0. But when I build:

% lake build
info: test: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision '7590675dfaa93de9844d39fe9c13106c327456e0'
info: updating toolchain to 'leanprover/lean4:v4.18.0-rc1'
info: restarting Lake via Elan
...

[Sebastian Ullrich]

I said it doesn't currently work for math so I don't know why you expect the opposite. @Wang Jingting gave the correct answer for it.

[Ruben Van de Velde]

You cannot use an arbitrary version of mathlib with your chosen version of lean. You need to pick the version of mathlib that matches, like Wang Jingting says

[Alexandre Rademaker]

I am sorry @Sebastian Ullrich, I didn't pay attention to the @Wang Jingting 's message. I missed the rev key.