lean-toolchain details

Stream: lean4

[Martin Dvořák]

What does lean-toolchain specify? Does it determine both the version of Lean 4 and the version of all libraries? Can lakefile.lean override the latter? Does lean-toolchain also influence what Lake commands do?

When should I create the file? The command lake new foo math gave me a project without the lean-toolchain file.

[Mauricio Collares]

If you don't get a lean-toolchain file immediately, then lake new foo math is almost certainly using an old version of lake, probably because your default toolchain is either a stable version of Lean 4 or an old nightly. Or maybe you ran lake in a directory affected by a previous elan override command.

[Mauricio Collares]

Try using elan default to configure your default toolchain

[Mauricio Collares]

lean-toolchain does not determine library versions (that's for the lakefile), but it constrains your choice of libraries/library versions to the ones which work with your chosen toolchain. This is probably what you meant, I just wrote it explicitly for clarification purposes.