Lake new with version number inconsistent with Mathlib
Open
@tydeu is already working on this.
Since May 1, 2025.
Lake
P-medium
- Dominant language
- Lean
- Stars
- 9.2k
- Forks
- 990
- Avg merge
- 1d 17h
- Merged PRs (30d)
- 175
Description
When I run lake new with a version number with and without the mathlib template, I get the following results
> lake +leanprover/lean4:v4.18.0 new WithMathlibFourEighteen
> cat WithMathlibFourEighteen/lean-toolchain
leanprover/lean4:v4.18.0
> rm -rf WithMathlibFourEighteen
> lake +leanprover/lean4:v4.18.0 new WithMathlibFourEighteen math
info: downloading mathlib `lean-toolchain` file
> cat WithMathlibFourEighteen/lean-toolchain
leanprover/lean4:v4.19.0-rc3
I feel that, rather than silently providing a toolchain that is different from what I requested, lake should either:
- (ideally) Give me the
most recenttagged version of mathlib that is consistent with the toolchain. - (at a minimum) error/warn me that the toolchain it is providing is different from the one I requested.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.