Applying stacks tags slows down mathlib

Stream: mathlib4

[Michael Rothgang]

Looking at FieldTheory/SeparablyGenerated.lean from #30998, one striking thing are some slow declarations towards the end. Using set_option profiler true, I get a quite surprising outcome: the bottleneck is applying the stacks attribute.

• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top yields "attribute application took 4.28s", with the only attribute being @[stacks 0H71]
• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fg (right afterwards) takes 850ms to apply @[stacks 030W "(2) ⇒ (1) finitely genenerated case"]

Any ideas why this is so slow? @Damiano Testa I believe you initially wrote this.

[Anne Baanen]

Maybe this is being measured weirdly due to async elaboration? @[stacks] modifies the docstring, so one possibility is it has to wait for the whole declaration to be elaborated before the docstring becomes available (not sure that this is indeed the case, but it seems possible).