Experimental Attribute

Stream: mathlib4

[Tristan Figueroa-Reid]

As discussed in #mathlib4 > Grammars downstream of Mathlib. Discussion started here.

[Eric Wieser]

I think with the very narrow interpretation of "no deprecation is required here" this could make sense, but I think mathlib is already fairly willing to waive deprecation requirements with reasonable justification (e.g. "you deprecated Foo to Bar, I won't make you deprecate the 100 lemmas about Foo if dot notation still works" or "this lemma only landed last week and there's a typo in its name")

[Yury G. Kudryashov]

I would deprecate 100 lemmas in case 1.

[Eric Wieser]

I don't think we did that with the Is* renames

[Kevin Buzzard]

The full story of the TopologicalRing -> IsTopologicalRing rename is that in my machine-generated PR #21472 which did the renaming, I totally forgot to deprecate anything and no reviewers mentioned this. Then two people independently, on the same day, pointed out to me that bumping their projects was more painful than expected because there was a host of errors instead of warnings, so I spent a couple of hours manually going through the 187 files changed in the renaming PR, and then made this commit which deprecated every result which had been explicitly renamed in the original PR. However it perhaps did not quite do the "100 lemma" approach which Yury suggested; to do this would involve not just looking at the changes made by the PR but at all of the 187 changed files, to find everything in the changed namespaces. However my reasoning was that anyone using TopologicalRing would now discover very quickly that it had changed to IsTopologicalRing because of the deprecation warning, and then it would be pretty obvious that if they actually had any open TopologicalRings in their code then it would be pretty clear that they should be changing them to open IsTopologicalRing anyway. The idea of deprecations is to make it easier for the user to bump; our setup isn't going to change open TopologicalRingto open IsTopologicalRing anyway. In fact mathlib tended not to open TopologicalRing anyway, so in fact perhaps that commit I linked to is a good approximation to what Yury was suggesting.

Ironically, the commit was then reviewed and I was told that most of the deprecating I'd done was deprecation of instances which is apparently not policy, so i had to make this commit undeprecating all the instance names anyway!