to_additive perf

Stream: general

[Reid Barton]

Is to_additive super slow? I'm building mathlib locally and whenever it seems "stuck" for a second or two it's on a lemma with to_additive whose proof often looks otherwise totally trivial

[Reid Barton]

It could just be a matter of which files it's on currently I suppose

[Reid Barton]

right now the slow things it's working on are category theory files that have multiple tidy invocations per lemma, and s l o w l y crunching through group_theory.subgroup.basic

[Floris van Doorn]

Uh oh... The changes I made to to_additive (a couple of months ago) could definitely have some performance issues.

[Reid Barton]

e.g. it just spent several seconds "parsing" at
https://github.com/leanprover-community/mathlib/blob/c7441af1c38511c70c05fb82029af4e1cb3d6275/src/deprecated/subgroup.lean#L187

[Floris van Doorn]

I'll take a look

[Floris van Doorn]

I cannot reproduce:

subgroup.lean:188:6
parsing took 0.329ms
subgroup.lean:188:6
type checking of mem_norm_comm_iff took 0.0853ms
subgroup.lean:188:6
decl post-processing of mem_norm_comm_iff took 13.2ms
subgroup.lean:188:6
elaboration of mem_norm_comm_iff took 1.78ms

[Floris van Doorn]

vandoorn@pc93-178:~/projects/mathlib((HEAD detached at origin/master))$ time lean --make src/deprecated/subgroup.lean

real    0m1.488s
user    0m1.342s
sys 0m0.148s

[Floris van Doorn]

Does the file (or individual declarations) compile more quickly if you remove to_additive?

[Reid Barton]

Hmm

[Reid Barton]

I don't really want to do experiments like that at the moment, but I can try later