linting time

Stream: general

[Bryan Gin-ge Chen]

The time it takes to lint mathlib has been creeping upwards again lately. It now takes almost 90 minutes, whereas it was closer to 65 minutes at the beginning of December and 48 minutes near the end of September. See the CI times for master, which are mostly spent linting, due to cached oleans.

Is this scaling as expected?

[Gabriel Ebner]

Linting spends most of time in the simp lemmas. I would expect the simp linters to have quadratic runtime. (Every simp lemma is linted using the simplifier, whose slowness is presumably linear in the number of simp lemmas.)

[Bryan Gin-ge Chen]

Thanks to #6293 by Gabriel, the linting time is back down to 45 minutes!

[Kevin Buzzard]

See you again in July!

[Scott Morrison]

If only number of cores available also grew quadratically. :-)

[Eric Wieser]

We could presumably go further and lint declarations with even- and odd- length names in separate jobs