Commit 2025-10-21 16:00 a1948635

CI: remove deprecations automatically (#30070) This workflow automates the removal of deprecated declarations. The action is currently configured to run once a week to automatically remove all deprecations older than 6 months. This is managed by the remove_deprecated_decls action and depends on the two files Mathlib/Tactic/Linter/CommandRanges.lean and Mathlib/Tactic/Linter/FindDeprecations.lean. The action can be manually triggered and there is the option of passing two dates in YYYY-MM-DD format or also the more human "3 months ago", as long as it is a valid input for date -d. The lean files take care of identifying the declarations with the deprecated attribute whose since field is between the given ranges. Those declarations then get automatically removed and, if there are no errors, the bot creates a PR with the changes. These PRs then go, naturally, through CI, where issues related to having removed the deprecated declarations will be picked up. The bot also posts a comment on Zulip mentioning when the PR has been opened. Zulip thread: #mathlib reviewers > auto-removing oudated deprecations (in reviewers channel)