group_theory/subgroup is slow

Stream: general

[Mario Carneiro]

Does anyone else observe group_theory/subgroup.lean compiling extremely slowly? Opening it in the editor it seems like it takes 1-3 seconds per command, including one line trivial rfl proofs. I haven't timed it but it looks like the whole file (which is 2200 lines) takes about 10-15 minutes

[Mario Carneiro]

The obvious culprit would be the @[to_additive] attribute and/or running user attributes in general

[Gabriel Ebner]

Takes about 15 seconds here on mathlib master (both in the editor as well as on the command line).

[Gabriel Ebner]

One notable performance issue of to_additive is that it disables async elaboration of proofs (it waits for the proof on the main thread).