Mathlib `remove outdated deprecated declarations`

Stream: nightly-testing

[github mathlib4 bot]

Here''Please review #29972, which removes deprecated declarations older than to date not set.''

[Damiano Testa]

This was a test and it was mostly successful!

[Damiano Testa]

There may be some more messaging here, as I test more features.

[github mathlib4 bot]

'Please review #29973, which removes deprecated declarations older than to date not set.'

[github mathlib4 bot]

Please review #29974, which removes deprecated declarations older than to date not set.

[Damiano Testa]

The PR is now up for review at #30070.

[Damiano Testa]

There are several earlier attempts at removing deprecated declarations, the latest one being #30068.

[Damiano Testa]

These count as tests for the action, in case you want to see it working!

[Damiano Testa]

Note that the tests deliberately used large ranges for removing old deprecations, so that they would test removing "complicated" declarations, as well as simple.

[github mathlib4 bot]

Please review #30082, which removes deprecated declarations between 2025-05-23 and 2025-05-23. Pay special attention to whether there are stray comments that can also be deleted.

[github mathlib4 bot]

Please review #30098, which removes deprecated declarations between 2025-01-01 and 2025-03-30.
Pay special attention to whether there are stray comments that can also be deleted.

[Ruben Van de Velde]

I was reviewing, but it was closed?

[Bryan Gin-ge Chen]

Sorry, this is still in the process of testing!

[Bryan Gin-ge Chen]

I should have edited the Zulip message, apologies. There should be one more testing PR soon; please ignore that one as well.

[github mathlib4 bot]

Please review #30099, which removes deprecated declarations between 2025-01-01 and 2025-03-30.
Pay special attention to whether there are stray comments that can also be deleted.

[Bryan Gin-ge Chen]

I'll try to remember to apply the comments from your review myself when this comes for real (probably after #30070 is merged)

[github mathlib4 bot]

Please review #30759, which removes deprecated declarations between 2020-10-21 and 2025-04-21.
Pay special attention to whether there are stray comments that can also be deleted.

[Bryan Gin-ge Chen]

As promised above, I will apply Ruben's suggestions from #30098 to #30759.

edit: done, thanks @Ruben Van de Velde and sorry again for the confusion above!

[Damiano Testa]

... and, importantly, the removal seems to have worked "automatically"!

[Bryan Gin-ge Chen]

#30759 is now green; there are a few comments I'd like some 2nd opinions on, but otherwise it should be ready to go.

[Bryan Gin-ge Chen]

A few updates on #30759:

• I made a separate review thread at #PR reviews > #30759 remove declarations deprecated before 2025-04-21 .
• I realized it probably won't be merged before the next automated run occurs, and then remembered that the action we're using in the workflow will force-push over the branch we're using, so I manually disabled it and opened #30901 to prevent this. I also changed the schedule to monthly since it seems weekly is too ambitious at the moment.

[github mathlib4 bot]

remove outdated deprecated declarations workflow run failed

triggered by: schedule

[Damiano Testa]

Oh, this is probably because the script is using the branch from which the PR was made, but now that the PR has been merged, the branch no longer exists!

[Bryan Gin-ge Chen]

Fixed in #31647

[github mathlib4 bot]

Please review #33988, which removes deprecated declarations between 2021-01-15 and 2025-07-15.
Pay special attention to whether there are stray comments that can also be deleted.

[Ruben Van de Velde]

I reviewed, but also it doesn't build

[Damiano Testa]

I remember that Bryan and I had thought about automatically removing (at least some) commands that reference deprecated declarations. For instance, if X is deprecated and there is an attribute [simp] X, then both should be removed.

[Damiano Testa]

I wonder if this only stayed in a wishful thinking world, or whether we actually implemented it (and it has bugs).

[Damiano Testa]

I went over the PR and it looks good to me.

[Damiano Testa]

The only non-automated replacements have been

• the removal of pairs of open/closed namespaces, with not intervening commands;
• the removal of a declaration that referenced a deprecated (and removed) declaration;
• the removal of a term elaborator for syntax that was deprecated and removed.

You can look at the two very small commits on top of the automated one for these changes.

[Damiano Testa]

While trying to get automation to help with the finishing touches for the removal of old deprecations, here is an interesting file: file#Mathlib/Data/Tree/RBMap.

[Damiano Testa]

Or https://github.com/leanprover-community/mathlib4/blob/3de2350c1fcee0565164fde61903f3d33d3acd64/Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean#L274-L282 in file#Mathlib/RingTheory/NonUnitalSubsemiring/Defs.

[Damiano Testa]

#34021

[github mathlib4 bot]

remove outdated deprecated declarations workflow run failed

triggered by: schedule

[Bryan Gin-ge Chen]

We hadn't updated the branch protection rule to let the app token push a new branch to mathlib yet. Fixed now.

[github mathlib4 bot]

remove outdated deprecated declarations workflow run failed

triggered by: schedule

[Bryan Gin-ge Chen]

(I forgot to hit save... :man_facepalming: should work this time)

[github mathlib4 bot]

Please review #35335, which removes deprecated declarations between 2021-02-15 and 2025-08-15.
Pay special attention to whether there are stray comments that can also be deleted.

[Bryan Gin-ge Chen]

Ready for review (or I might just merge it myself tomorrow)

[Bryan Gin-ge Chen]

One more issue with overview.yaml fixed. Does someone want to look into seeing if we can make check-yaml complain if an entry is deprecated?

edit: posted separately at #mathlib4 > check_yaml @ 💬