Mathlib linters in downstream projects

Stream: general

[Damiano Testa]

Mathlib defines several linters and tries to be mindful of which ones are on both in mathlib and downstream, and which ones are on in mathlib and off downstream.

[Damiano Testa]

However, some projects may want to align with mathlib's choices by default, without having to track closely changes to mathlib and updating their lakefiles continuously.

[Damiano Testa]

Should there be an option like Mathlib.linter.all which, when true, means that all the linters that are on in mathlib are automatically on downstream? This would mean adding a single (weak) option to the lakefile of downstream projects and then all the mathlib linters are active.

[Kevin Buzzard]

That would suit me fine! I find myself adding mathlib linters bit by bit. Presumably I'd be able to do "all mathlib linters apart from these two"?

[Damiano Testa]

I would have to think about how overriding works, but of course it is something desirable.

[Damiano Testa]

(And it is your FLT stream where this has come up most recently!)

[Damiano Testa]

So, basically there should be mechanism that allows to say "all linters except...". Right now you can only do "no linters, except...".

[Damiano Testa]

Having such a mechanism would be useful for all repositories that are developing material with the idea of upstreaming to mathlib.

[Anne Baanen]

Damiano Testa said:

Should there be an option like Mathlib.linter.all which, when true, means that all the linters that are on in mathlib are automatically on downstream? This would mean adding a single (weak) option to the lakefile of downstream projects and then all the mathlib linters are active.

Good news! lean4#8106 is intended to make exactly this possible!

[Anne Baanen]

The way linters are checked currently, explicitly set individual linter options have highest priority, then linter.all, then the option default value. So you can enable or disable all linters at once using set_option linter.all false, then dis/enable specific ones with set_option linter.myFavouriteLinter true.

[Michael Rothgang]

This is great; the code looks basically good to me. (See github for my detailed comments.)