Linter for large files (by instruction)?

Stream: mathlib4

[Matthew Ballard]

Piggybacking on another thread. Given that we have massively shrunk the leading file by instruction size, it might make sense to cap the number of instructions a single file requires.

We don’t want to be in a situation where a single file dominates the build process like in the past.

[Kevin Buzzard]

Can we lint for that?

[Emilie (Shad Amethyst)]

I fear that things like adding new simp lemmas might cause other modules to trip the linter down the line, forcing refactors to be done in PRs that would otherwise only add new things

[Alex J. Best]

I don't know if this fits into the linter framework, but maybe max (num instructions for individual file) could be added as a metric to speedcenter, so it is easier to see if this changes

[Kim Morrison]

Alternatively, a bot posting on zulip periodically.

[Matthew Ballard]

Also, small changes that are +1T in instructions should be flagged.

[Yury G. Kudryashov]

In mathlib3 times, a PR causing a timeout and waiting for a fix of this timeout was not that uncommon.

[Matthew Ballard]

To illustrate how surprising it can be #9721 has this for its bench results.

[Yury G. Kudryashov]

Do we know which part of #9721 causes this?

[Matthew Ballard]

I think it’s the import. CoeFun searches get more expensive. It’s fixed in #8386 but I wouldn’t have caught it