`lake new foo math` can cause a mismatch in Lean4 versions.

[adamtopaz]

lake new foo math creates a folder foo with a lean-toolchain file based on the version of Lean used to invoke lake, while also adding mathlib4 as a dependency. The issue is that the Lean version required by mathlib4 need not match the version in the folder foo, which can lead to build errors.

Relevant zulip discussion

[tydeu]

This is unfortunately a difficult problem to solve because lake new/init is not designed to connect to the internet and download packages, and without downloading mathlib it seems impossible to know what is the proper version to write to lean-toolchain.

[adamtopaz]

One potential solution is to add tags to mathlib4 associated to the relevant versions, and add mathlib4 as a dependency pointing to the specific tag. That would push some responsibility to the mathlib4 maintainers, but maybe that's okay?

[tydeu]

@adamtopaz I assume you mean have mathlib have a tag/branch per supported Lean version and then have Lake fix mathlib in its template to said branch corresponding to the toolchain version of Lake. That seems like it could work. Feel free to purpose the idea on the mathlib issues board or on the Zulip.

[arthurpaulino]

I think we can close this one

[tydeu]

@arthurpaulino Yeah. #152 has sufficiently addressed this.