Zulip Chat Archive

Stream: mathlib4

Topic: intermediate versions

Scott Morrison (Dec 02 2022 at 23:53):

A public service announcement about Lean 4 versions.

You may see in mathlib4 master (and some branches), lean-toolchain points to semorrison/lean4:fix-1907 right now. We have not forked Lean 4! :-)

The lean4-nightly repository generates releases ... nightly! When we have a critical fix to Lean 4 that affects mathlib4, it is easy for us to generate an unofficial release. All you do is clone the lean4 repo, create a tag (e.g. git tag ABC) and then push it to some fork of the repo (git push fork ABC). CI will then automatically kick in, and produce a release that elan knows how to handle simply by putting the repo and tag in lean-toolchain as above.

One gotcha is that elan/github seems unhappy if the tag name is numeric (it prepends a v when looking for a file, and fails).

It's completely fine to bump Lean 4 back to a nightly version as long as a day has passed and the tagged commit has been incorporated in a lean4-nightly release. Hopefully this will be the exceptional case, and this won't come up very often.

If it would make people happier we could do this at a leanprover-community fork, rather than an individual's; but as this is intended as a very temporary measure hopefully this is fine. (And makes clear we are not forking!!! :-)

Arien Malec (Dec 02 2022 at 23:58):

rn I'm getting the error error: toolchain 'semorrison/lean4:fix-1907' does not have the binary /Users/arienmalec/.elan/toolchains/semorrison--lean4---fix-1907/bin/lake`