Did linting in CI get slower?

Stream: mathlib4

[Michael Stoll]

Watching CI runs, I got the impression that the "lint mathlib" step got noticeably slower: until very recently (last week or so), it took a bit over 4 minutes, now it is a bit over 5 minutes. Is this just because Mathlib has been growing a lot, or are there deeper reasons?

[Michael Stoll]

It seems to approach 6 minutes by now...

[Michael Rothgang]

Wild guess: is #18033 related? (Pending fix in #19260.)

[Michael Rothgang]

Getting some data: the speed-center reports that the linting step did not get much slower in the past week.

[Michael Stoll]

It looks like there has been a slow but fairly steady increase (in wall clock time) since mid-October.

[Michael Rothgang]

Looking at all of November, #17904 seems to have increased linting instructions by ~4-5% (roughly corresponding to a 15s wall-time increase).

[Michael Rothgang]

(Wall-clock times are fairly noisy; instructions are more stable and seem well-correlated across that time interval.)

[Michael Stoll]

Sure, but wall-clock time is what you see on the CI run.

[Michael Rothgang]

Agreed. My point is: for pinpointing regressions, instructions can be more helpful.

[Michael Stoll]

(It is still much better than in the good old final days of mathlib3, when linting took almost an hour each time...)

[Damiano Testa]

The header linter silencing was definitely a performance fiasco, but I don't think that the linting step of CI was affected: the header linter runs during build, not in the later step, I think.

[Michael Rothgang]

(By the way, I don't mean to pick on your PR in particular. I also remember one PR of mine regressing things pretty badly - and getting fixes eventually.)