Deprecating deprecated declarations

Stream: lean4

[Damiano Testa]

@Bryan Gin-ge Chen and I are working on automating the removal of deprecated declarations. While doing this, the following issue came up:

theorem new : True := trivial

@[deprecated new (since := "yesterday")]
theorem X : True := trivial

-- Could this one raise a deprecation warning on `X`?
@[deprecated X (since := "today")]
theorem Y : True := trivial

As you can see, the suggested replacement for Y is the deprecated declaration X. However, there is no warning that X is deprecated.

This means that when the deprecations from yesterday get removed, the declaration X disappears and the command defining Y now raises an error that X does not exist and it may take some effort to figure out what the suggested replacement is.

[Damiano Testa]

So, would it be possible to get a deprecation warning on X in @[deprecated X (since := "today")]?

[Damiano Testa]

Note that this is similar to #lean4 > No warning on deprecated local instances which also comes up when removing deprecated declarations.

[Damiano Testa]

You can see in #30057 the cases of this that were uncovered by the automated removal of deprecations.

[Mac Malone]

According tp the since statements in this example Y was depreacted after X, so why does Y suggest an already deprecated replacement? That is, the evolution of the code suggested by the since statements is:

Initial

theorem X : True := trivial

Yesterday

theorem new : True := trivial

@[deprecated new (since := "yesterday")]
theorem X : True := trivial

Today

theorem new : True := trivial

@[deprecated new (since := "yesterday")]
theorem X : True := trivial

-- Why is this not suggesting `new`?
@[deprecated X (since := "today")]
theorem Y : True := trivial

I imagine these may be a product of some odd merge order on the PRs. For example, the Y was deprecated by X today, but a in-progress PR deprecated X by new yesterday, and they were then merged in reverse order. However, that seems to suggest the correct solution is to possible error (or linter) if deprecation suggests another deprecated method.

[Damiano Testa]

I have not investigated how those deprecations arose, but you can see them in the linked PR. In all cases, the commands are all next to each other.

[Damiano Testa]

What could have happened is that the deprecation dates are usually set when the PRs is opened, not when it is merged. So there can be some strange entanglements there.

[Damiano Testa]

In any case, if the deprecation warning could flag also those uses, that would be great!