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