to_additive instance priority

Stream: mathlib4

[Moritz Doll]

I want to fix my earlier hacky solution of the instance priority in to_additive, but the file Algebra.Group.OrderSynonym fails with some very weird messages (see https://github.com/leanprover-community/mathlib4/actions/runs/3562129264/jobs/5983590994 ). I've checked what my code is doing and it sets the correct priority, so I suspect there is yet another bug in to_additive

[Moritz Doll]

oh and there seems to be bug in to_additive that primed names cause issues (@[to_additive OrderDual.SMul'] is not doing anything)

[Floris van Doorn]

mathlib4#765

[Floris van Doorn]

This is not a bug in to_additive, just a few errors with the usage of to_additive in relation to automatically generated instance names. I pushed a fix.

[Floris van Doorn]

I cannot reproduce your last bug. I think you were not seeing any output from @[to_additive? ...] since the declaration already exists. Note: after mathlib4#718 @[to_additive? ...] should always give some output.

[Moritz Doll]

thanks for looking into it - should be align the to_additive version as well?

[Moritz Doll]

as for the primed variables: I've printf debugged to_additive to see whether the instance priority was set correctly and for the primed variables there was no output and hovering over the name in to_additive also gave nothing

[Floris van Doorn]

Moritz Doll said:

thanks for looking into it - should be align the to_additive version as well?

I don't know. It's never done, but I expect we indeed do need that as well (which means we're probably missing hundreds of #align's)

[Jireh Loreaux]

I've been aligning all the additive versions. It's definitely necessary if the non-additive version needed aligning.

[Yakov Pechersky]

In what instances does one need to align the instance names? In general, most instances do not get referenced by name.

[Jireh Loreaux]

I align instances that are manually named as well as parent projections for classes which extend other classes as these are most likely to be referenced by name.