How do I reliably ensure that `lake` uses stable releases?

Stream: new members

[alcuin]

I would like to make a new Lean4 project with lake which reliably uses the stable release of mathlib4 (v4.24.0) but I cannot get lake to reliably start with that.

I've done the following things:

% which elan
/Users/me/.elan/bin/elan

% which lake
/Users/me/.elan/bin/lake

% which lean
/Users/me/.elan/bin/lean

% elan which elan
error: not a file: '/Users/me/.elan/toolchains/leanprover--lean4---v4.24.0/bin/elan'

% elan which lake
/Users/me/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lake

% elan which lean
/Users/me/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean

% lean -v
Lean (version 4.24.0, arm64-apple-darwin23.6.0, commit 797c613eb9b6d4ec95db23e3e00af9ac6657f24b, Release)

% lake --version
Lake version 5.0.0-src+797c613 (Lean version 4.24.0)

% elan -V
elan 4.1.2 (58e8d545e 2025-05-26)

# I've also checked that my ~/.zshrc has the `export PATH="$HOME/.elan/bin:$PATH"` just in case. It has it at the bottom and the top and several times in between over numerous failed attempts.

Now, when I go into a new folder and do this sequence of highly defensive things:

% mkdir my-proj
% cd my-proj
my-proj % elan override set 4.24.0
info: override toolchain for '/Users/me/my-proj' set to 'leanprover/lean4:v4.24.0'
my-proj % lake +4.24.0 init . math.lean
info: downloading mathlib `lean-toolchain` file
info: my-proj: 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 'f1c336fec192caff79da15b1c598ab530902a08f'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8864a73bf79aad549e34eff972c606343935106d'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '451499ea6e97cee4c8979b507a9af5581a849161'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'ca519018e8bdc34d7bb4ecf0c8d39634a8c15300'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '95c2f8afe09d9e49d3cacca667261da04f7f93f7'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'e0442e0a213dfceca01d4c9beac9822be4b04a0a'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '72ae7004d9f0ddb422aec5378204fdd7828c5672'
info: mathlib: running post-update hooks
Not running `lake exe cache get` yet, as the `lake` version does not match the toolchain version in the project.
You should run `lake exe cache get` manually.

I'm already concerned about this "lake version does not match the toolchain version in the project." message but now when I look inside:

% cat lean-toolchain
leanprover/lean4:v4.25.0-rc2

This isn't what I wanted, I didn't want the release-candidate, I wanted the stable release version.
I don't see why it continues to ignore that everything else in the world is 4.24.0 (?)
I think I am kind of out of options, now.

[Ruben Van de Velde]

You definitely don't want to use elan override

[Ruben Van de Velde]

Instead, in your lakefile.toml, add rev = "v4.24.0" (or maybe rev = "stable", but I'm not sure that's well-tested) under the mathlib header

[alcuin]

Ruben Van de Velde said:

Instead, in your lakefile.toml, add rev = "v4.24.0" (or maybe rev = "stable", but I'm not sure that's well-tested) under the mathlib header

Yes; I did see someone on Stack Overflow had a similar issue--

I would have thought it's a bit "chicken and egg" to have lakefile.toml made after I already init the project-- do I feed a lakefile.toml into lake before the init process (at least I did not see that option under 21.1.2.5 on Lean documentation)? Is it different for .toml vs .lean versions of lakefile?

[Ruben Van de Velde]

I'm sure there's a way to do it in lakefile.lean, but don't have the syntax at the top of my head. You should be able to add the revision to the lakefile after lake init and then probably lake update will do the right thing

[alcuin]

I'll try to reinitialize with the lakefile's .toml default version [I was under the impression it's better for futureproofing to go with the .lean version]. What is any particular reason why elan override is the bad choice?

update: I did the following things now. I will see if it works:

• I deleted lake-manifest.json as well as the pre-existing .lake/
• I modified the lakefile.toml and lean-toolchain files to say 4.24.0 instead of 4.25.0-rc2

Currently, my VS Code is attempting to now start the Lean4 server and it seems its downloading mathlib4 but I cannot tell if it is progressing right now [output in the Panel shows the connection to server is erroring. I may now retry.]

[Ruben Van de Velde]

Lean projects explicitly say in the lean-toolchain file what version of lean to use - elan override says "actually, ignore that, and use some other version that almost certainly will not work with the project"