deprecations and namespaces

Stream: mathlib4

[Kevin Buzzard]

For the second time when bumping FLT I have run into an issue where a declaration has been removed without deprecation, and after some detective work I've found that a deprecation attempt has actually been made (and has passed review) but there has been a namespace issue: the code

namespace Foo

<stuff>

lemma bar : blah = blah := ...

end Foo

becomes

<stuff>

end Foo

lemma bar_with_new_name : blah = blah := ...

@[deprecated (since := "2025-12-11")]
alias bar := bar_with_new_name

...

with the consequence that mathlib now has a new deprecated definition bar in the root namespace, and code which calls bar with Foo open will typically flag the deprecation but code which calls Foo.bar e.g. via dot notation will simply result in an error because Foo.bar is now gone. I am also getting confusing output from https://mathlib-changelog.org/ about this; I don't know enough about how that website works to say any more though.

Is there a way of linting against this in CI? I don't know too much about linting but this sounds like a complex problem because one has to compare before and after mathlibs. Right now my understanding is that we're using a python script to do a best approximation of this, but the python script does not catch the phenomenon above and in both cases which affected FLT it has been expert users who have made the deprecation error; if it can happen to them, it can happen to all of us.

[Vlad Tsyrklevich]

Are you saying that the change did not show up in the 'declarations diff' section of PR summary? Given your description of the issue I would have expected it to show up there (and perhaps it should be surfaced better to reviewers, but I think it's good to first establish whether it could have been spotted there.)

[Ruben Van de Velde]

The declarations diff is text-based, so does not take namespace into account. We need to replace it with something that uses the actual resolved names, but nobody's taken up the task yet

[Kevin Buzzard]

So my questions are basically what something which did the job more accurately would look like, and how much work it would be.

[Chris Henson]

The last time this came up (and briefly discussing in person with @Damiano Testa) there were questions about replacing the current implementation that stalled things a bit. If you wait for oleans for the PR, it is straightforward to diff declarations. The pending question was if this was a significant enough regression from the current quick feedback that we should still start with a text-based diff that is updated after the build is done.

[Kevin Buzzard]

If the text-based diff is cheap then I don't see why we shouldn't keep it. I see that radar is making a preliminary post and then editing it later on (e.g. pinging people when it terminates).

[Ruben Van de Velde]

It seems confusing to post "this is fine!" "actually it's not"

[Kevin Buzzard]

Hmm maybe. It could be two tests, or one could simply argue that if a test is strictly better than another test then the weaker test can just be dropped.

[Damiano Testa]

Maybe we should just go ahead with the diff computed using the oleans and forget about the text-based one.

[Damiano Testa]

It is always easy to resurrect the old one, in case it is missed.

[Damiano Testa]

Now might also be a good time to figure out whether we want to be stricter about declarations that disappear, and maybe add a flag for those, e.g. a label that the script applies.

[Jireh Loreaux]

Of course, it would still be nice to have something with the comprehensivebess of Leaff, but I'm not sure how viable it is to resurrect that. Obviously the maintenance on that would be much higher too.

[Snir Broshi]

I'd love to see a diff of binder info if there is one- if any variables changed from explicit to implicit, or changed their name. I think it's helpful to both the author and reviewers, the author might have not intended to change something but a variable command sneaked the change into more theorems than expected.