Zulip Chat Archive

I was just wondering if there already existed good tooling to bump old Lean4 versions to the current one. A lot of the simple deprecations and errors can be simply replaced, but for harder theorems you have to update more, so I'm not surprised that there's not much online. Does anyone know of any good tooling for it though?

Kim Morrison (Sep 02 2025 at 22:42):

Unfortunately no, there is no automatic tooling. I find it vey helpful to only bump one version at a time, which helps localize problems. (e.g. prepare the PR updating the toolchain as a succession of commits, each advancing the toolchain and dependencies by one Lean version).

There are some ideas about making this easier, but not yet in the form of tools.

Oscar Matemb ⚛️ (Sep 02 2025 at 22:44):

honestly I only know how to do it manually.

check the latest lean version (not necessary) with elan show then update elan elan update then you update your lake toolchain file lake update and that's about it.

Kim Morrison (Sep 02 2025 at 22:46):

More precisely, I recommend:

advance lean-toolchain to the next version
check in your lakefile.lean and lakefile.toml to make sure all dependencies are "pinned" to a commit or tag that is compatible with that toolchain (for Mathlib, Batteries, Aesop, etc, there is always a tag called e.g. v4.22.0, which is guaranteed to be compatible with that toolchain version)
run lake update
run lake build && lake test to fix any errors and warnings
commit, and proceed to the next version.

Oscar Matemb ⚛️ (Sep 02 2025 at 22:51):

@Kim Morrison is it advisable to this oftenly for every local or remote mathlib project? Also, pinning dependencies to the toolchain for that version to keep it safe from getting lost?

Kim Morrison (Sep 02 2025 at 23:55):

Yes. I would suggest that if you ever intend to run lake update in your project (and you should!) then you should always be using "pinned" dependencies (i.e. pointing to a particular tag, rather than a branch).

Eric Wieser (Sep 03 2025 at 00:42):

Are there plans to make deprecations auto-replacing like the simp [unused] linter is?

Kim Morrison (Sep 03 2025 at 00:44):

I don't think it's currently on anyone's TODO list. A PR from a contributor, or an issue explaining what is blocking implementation, would be much appreciated.