long file linter

Stream: mathlib4

[Sébastien Gouëzel]

The long file linter is active by default on downstream projects, if I understand correctly. Is that by design? (It's typically the kind of linter that I understand for mathlib, but not for other projects which should be more free on this kind of business). I know it can be deactivated if needed, but my question is if it should belong to the default linters there.

[Damiano Testa]

I agree with your assessment: the linter should be on by default on mathlib and off by default on downstream projects.

[Damiano Testa]

I think that I wrote the linter before this was possible and simply forgot to set this up correctly once it became available.

[Damiano Testa]

#16481 (assuming I got the syntax right!)