Dealing with breaking changes

Stream: new members

[Kevin Cheung]

After updating Mathlib4 in my project, I realized that a number of imports don't exist anymore. (Also, dsimp and simp have gotten a bit more powerful in some of my proofs, rendering some later steps unnecessary.)

I am wondering if breaking changes like this are to be expected between point releases. And if so, what is the best practice to make sure one doesn't obtain updates that involve breaking changes?

[Ruben Van de Velde]

Yes, this is expected. The only way to avoid them is not updating at all :)

[Ruben Van de Velde]

I guess we need to think about a better experience for removed files

[Kyle Miller]

One tool that's useful is https://mathlib-changelog.org/v4 to see where things went.

Another is to try to update mathlib more frequently, since it's often easier to handle when there are smaller things to fix. That means following the Lean rc releases along with mathlib though.