Maintainability tips

Stream: general

[Weiyi Wang]

I learned from https://leanprover-community.github.io/extras/simp.html that non-terminal simps are at risk of breaking when updating libraries. Are there similar pitfalls for other tactics? For example, how likely ring can break after updating dependencies?

[Floris van Doorn]

ring shouldn't break between versions (unless previous tactic produced a different goal state). The reason that simp likely breaks is that it is an extendible tactics: we regularly add more @[simp]-lemmas so that simp can simplify more.
Something similar happens with gcongr, although this breaks proofs less frequently.

[Floris van Doorn]

Most other extendible tactics are finishing tactics (positivity, fun_prop, measurability, etc.), so it doesn't matter if they start doing more.

[Weiyi Wang]

That's good to know, and thanks for the mentioning gcongr because I also used it.