Porting between Lean versions

Stream: Machine Learning for Theorem Proving

[Bas Spitters]

This is a topic that has come up before. What is currently the best way to (back)port code between Lean versions?

[Michael Rothgang]

Backporting code is not really supported. For bumping Lean versions, have you trying searching on zulip? What did you try; what did you learn?

[Fabian Glöckle]

currently updating NuminaMath-Lean semimanually to recent mathlib.
https://mathlib-changelog.org/v4 is useful + I made a script based on changelog's github code that generates a replacement dictionary from alias and @[deprecated] in the codebase

semi-manually = find a pattern, run it on all proofs, stop when the marginal payoff gets too small

[Bas Spitters]

There's a tool by @Cyril Cohen @nicolas tabareau that aims to do this automatically in the future. However, I don't think it's been trained on different Lean versions yet.
https://hal.science/hal-05342510/document