How can I fix Lean version for a lake project?

Stream: new members

[Youngju Song]

I have set it via lean-toolchain, but it gets overwritten by lake build or lake update.
What would be the right way to fix Lean version for a like project?

I tried

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

following some answer in Stackoverflow, but it looks very hacky and it did not work.

[Youngju Song]

fyi, my full lakefile.toml is:

"lean-my-project"
version = "0.1.0"
defaultTargets = ["lean-my-project"]

[[lean_lib]]
name = "LeanMyProject"

[[lean_exe]]
name = "lean-my-project"
root = "Main"

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

and my lean-toolchain is

leanprover/lean4:v4.25.1

and when I type lake build or lake update, it gets overwritten to

leanprover/lean4:v4.26.0-rc2

Doing rm -rf .lake and starting over again does not help here.

[Ruben Van de Velde]

Youngju Song said:

I have set it via lean-toolchain, but it gets overwritten by lake build or lake update.
What would be the right way to fix Lean version for a like project?

I tried

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

following some answer in Stackoverflow, but it looks very hacky and it did not work.

This is the right way and should work. I suggest you try this again and tell us what goes wrong

[Ruben Van de Velde]

(I find it very impossible that lake build would change the lean-toolchain file)