to_additive, simps

Stream: mathlib4

[Yury G. Kudryashov]

Is it hard to write a linter (or modify simps) so that @[to_additive, simps] generates a warning/error?

[Yury G. Kudryashov]

As far as I understand, @[to_additive, simps] doesn't work as it is used to work in mathlib3, and we should use to_additive (attr := simps) instead.

[Mario Carneiro]

I thought that it already linted on this?

[Mario Carneiro]

@Floris van Doorn

[Yury G. Kudryashov]

I fix many of these in !4#2073 but I'm not sure that I didn't miss some.

[Yury G. Kudryashov]

@[simp, to_additive] generates a warning, @[to_additive, simps] doesn't.

[Floris van Doorn]

We indeed don't generate a linter warning for @[to_additive, simps] (yet?), since the warnings are implemented as part of to_additive.
I fix many of these occurrences in !4#1819 and !4#1885 (though I didn't go systematically though all occurrences of @[to_additive, simps] yet). Those PRs are awaiting review for 1-2 weeks.

[Floris van Doorn]

Note that !4#1819 turns the messages into actual linter errors, so you won't miss any of the ones that we are testing for. I'm also happy to modify simps so that it generates a linter error for @[to_additive, simps] (after some of my current refactors of the two attributes have been merged).

[Yury G. Kudryashov]

I'm sorry for duplicating effort. I should've searched github before starting my PR.

[Yury G. Kudryashov]

Which one do you prefer to merge first?

[Yury G. Kudryashov]

If we merge mine first, then I'm ready to merge new master into your branches.

[Yury G. Kudryashov]

About your PRs, I can't review meta code...

[Floris van Doorn]

I think it's fine to merge them in any order. The merge conflicts shouldn't be hard (especially since you didn't fix the warnings in Mathlib/Algebra/Group/OrderSynonym.lean and Mathlib/Data/Pi/Algebra.lean, which required the new features of !4#1819

[Floris van Doorn]

I merged yours