Skip to content

feat: warn on transitive deprecations - #14422

Open
wkrozowski wants to merge 8 commits into
leanprover:masterfrom
wkrozowski:wojciech/transitiveDeprecations
Open

feat: warn on transitive deprecations#14422
wkrozowski wants to merge 8 commits into
leanprover:masterfrom
wkrozowski:wojciech/transitiveDeprecations

Conversation

@wkrozowski

@wkrozowski wkrozowski commented Jul 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds a warning when registering a deprecation to a definition that is itself deprecated. The PR relies on #14344 that splits registerParametricAttribute into extension registration and attribute registration.

Waiting until #14600 gets merged first.

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label Jul 16, 2026
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Jul 16, 2026
@leanprover-bot leanprover-bot added the breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. label Jul 16, 2026
@leanprover-bot

leanprover-bot commented Jul 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jul 16, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 16, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
061bd76
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
b804031
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 20, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14422
7f84f4f
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
22de0ae
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 20, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
0d9e1bd
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 20, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14422
752db42
@leanprover-bot leanprover-bot added builds-manual CI has verified that the Lean Language Reference builds against this PR and removed breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. labels Jul 20, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 21, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
c267790
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 21, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
02e31f1
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 21, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14422
6943862
@wkrozowski
wkrozowski marked this pull request as ready for review July 22, 2026 11:22
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 22, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
bc76e90
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 22, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14422
faf5e9a
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 22, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14422
6c5d05d
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR labels Jul 22, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@wkrozowski @leanprover-bot