Empty lines linter

Stream: ecosystem infrastructure

[Ruben Van de Velde]

Do we want to enable the empty line linter from #25945 in downstream projects? cc @Damiano Testa

[Damiano Testa]

The question is "Is it a good idea that the linter is now active on downstream projects", right?

[Damiano Testa]

I agree that this is a purely stylistic choice. Right now, the linter is activated as a "standard mathlib set" linter. I view this set of linters as those linters that enforce all mathlib convention's, including the style ones, to maintain code uniformity.

[Damiano Testa]

I am now wondering whether maybe there should be two "standard" linter sets:

• the linters that are "universally" a good idea to have on,
• the linters that are active on mathlib and enforce some more project-dependent convention.

[Damiano Testa]

I consider the empty lines linter a linter of the second kind.