Skip to content

feat: warn on inexact deprecations - #14600

Open
TwoFX wants to merge 6 commits into
leanprover:masterfrom
TwoFX:julia/inexact-2
Open

feat: warn on inexact deprecations#14600
TwoFX wants to merge 6 commits into
leanprover:masterfrom
TwoFX:julia/inexact-2

Conversation

@TwoFX

@TwoFX TwoFX commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR adds a warning when deprecating a declaration in favor of another declaration that is not reducibly defeq.

Here is the warning in full:

deprecated.lean:20:2-20:43: warning: The updated constant has a different type:
  Nat
instead of
  Nat → Nat

This suggests that addressing the deprecation might be more involved than simply replacing the old name with the new name. This is often excepected, but sometimes it indicates that the deprecation is in favor of the wrong declaration, or that there is a mistake in one of the statements.

If the type difference is intentional, use `+typeChanged` to silence this warning.

Hint: Add `+typeChanged`:
  [apply] +typeChanged

The majority of the diff is removing deprecated declarations which would have triggered this warning but are overdue for removal anyway.

@TwoFX TwoFX added changelog-language Language features and metaprograms downstream Request a downstream-lean4 adaptation PR. labels Jul 30, 2026
@downstream-lean4

downstream-lean4 Bot commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown

The adaptation PR for this PR is leanprover/downstream-lean4#21.

@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 30, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 30, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 06:17:59)

@downstream-lean4 downstream-lean4 Bot mentioned this pull request Jul 30, 2026
Open
@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 30, 2026
@leanprover-bot

leanprover-bot commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 30, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14600
409bbfb
@TwoFX
TwoFX marked this pull request as ready for review July 30, 2026 14:21
@TwoFX

TwoFX commented Jul 30, 2026

Copy link
Copy Markdown
Member Author

@wkrozowski If you have a minute, I'd appreciate your review on the meta code.

wkrozowski
wkrozowski reviewed Jul 30, 2026
View reviewed changes
Comment thread src/Lean/Linter/Deprecated.lean
private def areTypesReduciblyDefEq (decl₁ decl₂ : ConstantInfo) : MetaM Bool := do
if decl₁.numLevelParams != decl₂.numLevelParams then
return false
let levels := decl₁.levelParams.mapIdx fun i _ => mkLevelParam <| Name.num `_deprecated i

@wkrozowski wkrozowski Jul 30, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How do we deal with permuted universe parameters?

For example:
myDef.{u,v} : Type u -> Type v -> Prop
myDef.{v,u} : Type v -> Type u -> Prop

Also, if we have the same level params, why are we substituting them?

@TwoFX TwoFX Jul 30, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the level parameters are permuted, then we consider the type changed.

Also, if we have the same level params, why are we substituting them?

Not sure if I'm following your question here. The problem this is solving is that

theorem foo (a : Type u) : 1 = 1 := rfl

theorem bar (a : Type v) : 1 = 1 := rfl

were considered to have different types and this caused a decent number of false positives.

@wkrozowski wkrozowski Jul 30, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, that makes sense. I was a bit confused, as this reminded me of the related problems I had when adding a hint/code action to deprecated linter, and had to make sure that the replacement would be sound.

For the second one, this also makes sense to me.

@wkrozowski wkrozowski Jul 30, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I genuinely do think that I should wait for this PR to be merged, until I finish #14525, as I could use the information about the preservation of types there.

wkrozowski
wkrozowski reviewed Jul 30, 2026
View reviewed changes
Comment thread src/Lean/Linter/Deprecated.lean
Comment on lines +68 to +77
let hint ← if let some insertPos := insertPos? then
MessageData.hint "Add `+typeChanged`:" #[{
suggestion := " +typeChanged"
messageData? := some "+typeChanged"
span? := Syntax.ofRange ⟨insertPos, insertPos⟩
diffGranularity := .none
toCodeActionTitle? := some fun _ => "Try this: +typeChanged"
}]
else
pure <| MessageData.hint' "Add `+typeChanged` to silence this warning."

@wkrozowski wkrozowski Jul 30, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you check if this correctly displays a code action by the way? (assuming it is branched off from master, when code actions PR was merged)

@TwoFX TwoFX Jul 30, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I have already used the code action many times :)

This was referenced Jul 31, 2026
Closed
Open
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@wkrozowski wkrozowski wkrozowski left review comments
@datokrat datokrat Awaiting requested review from datokrat datokrat is a code owner
@sgraf812 sgraf812 Awaiting requested review from sgraf812 sgraf812 is a code owner
@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner
@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner
@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner
@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. changelog-language Language features and metaprograms downstream Request a downstream-lean4 adaptation PR. 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.

3 participants

@TwoFX @leanprover-bot @wkrozowski