to_additive and instances

Stream: mathlib4

[Moritz Doll]

I've had linter errors for the to_additive and instance combination and tracked it down to this todo in to_additive: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ToAdditive.lean#L359
is there any news on that (this comment is 6 months old) and is it now possible to implement the instance attribute in to_additive?

[Riccardo Brasca]

Ah, if to_additive doesn't work on instances this at least explain some errors I've got!

[Moritz Doll]

if the linter complains that your def should be a lemma even though it is an instance, then yes

[Moritz Doll]

(this is what happened to me)

[Moritz Doll]

and of course it only complains at the additive versions

[Riccardo Brasca]

Yes, this is exactly what happened.

[Moritz Doll]

the easy way out is to do the instances by hand, but this is obviously stupid

[Riccardo Brasca]

As a workaround you can add it by hand, with a porting note. But I agree it's annoying, if we start doing this a lot we will surely forget to use to_additive later.

[Riccardo Brasca]

Ahah, I see we agree :D

[Moritz Doll]

Ok, so I've looked a bit more into this and the underlying issue seems to be that the part in to_additive that does the copying of attributes is in a CoreM monad, whereas adding instances is in MetaM. I did not find anything in the history in Lean 4 that suggests that there were any changes to how instances are added.
I don't really see why we cannot just bump the monad, the instance attribute obviously runs in the MetaM monad.

[Moritz Doll]

It doesn't look too bad actually: mathlib4#678 but I have to go to sleep now..
Is the defLemma linter included in #lint? I had it now that #lint did not complain, but CI did.