Declarations diff with to_additive

Stream: mathlib4

[Yakov Pechersky]

In #15589, I am "multiplicativizing" Archimedean, which involved creating a new class and shifting lemmas from mentioning nsmul to pow. In the PR summary comment, it says that various declarations are lost -- but they are not, they are generated by to_additive and retain their original name. Is this expected? I could imagine two scenarios

• completely new declaration, tagged with to_additive -- this really added two declarations -- the summary can mention the primary name with a symbol to indicate that it generated an additive version too
• existing declaration is now generated via a to_additive of a new declaration -- the summary should mention the new one but not consider the old one gone

[Ruben Van de Velde]

Yeah, the summary looks only at the actual source code

[Kevin Buzzard]

My understanding is that the tool which is trying to figure out if declarations are lost is not doing anything clever, it's just grepping the source code or something. @Damiano Testa will know better. It works very well in many cases but I'm pretty sure that you've got a case here where the naive approach will fail.

[Ruben Van de Velde]

We're hoping something leaff-based to replace at some point

[Damiano Testa]

Indeed, the current script is intended as a "patch": it is quick, only looks at the source code with no parsing, no namespace, no auto-generated information.

[Damiano Testa]

So, what you describe is expected, not desired, but also not within the scope of the current script.

[Yakov Pechersky]

Makes total sense, thanks. I think my PR description would help explain the "lost declarations" for any reviewer.

[Damiano Testa]

Indeed! I actually am fairly surprised by how effective the script is. I also think that it probably reached the limit of its capabilities, while still being maintainable and simple-minded.