Unifying linters

Stream: mathlib4

[Damiano Testa]

Several times it has been reported that linters have a non-negligible effect on the build times for mathlib. For instance, #mathlib4 > `Mathlib.Init` is too slow is one example.

[Damiano Testa]

Since I have been developing quite a few of them, I feel responsible for trying to solve this issue.

[Damiano Testa]

Most of the linters scan the syntax looking for forbidden nodes and report. Others do something similar scanning the infotrees, instead of the syntax.

[Damiano Testa]

Right now, every new linter, performs the scan independently of all the others.

[Damiano Testa]

With a little re-organization, it would be possible to have a "master" linter that performs the scan of the syntax once and each "current" linter simply plucks information out of that scan to do the reporting.

[Damiano Testa]

From my perspective, there are two main advantages:

1. performance improvement;
2. all linters that get combined in the "master" one can be silenced with a single set_option for the "master" (although each would also retain its individual option, so that they can be silenced granularly as well).

[Damiano Testa]

The main disadvantage that I see with this is that new linters would have to fit into this machinery. If they do something that the machine does not currently contemplate, they would have to either be integrated (harder to code), or would again be independent (decreasing performance).

[Damiano Testa]

In conclusion, does trying to unify all/most linters look like a good idea?

[Sebastian Ullrich]

On master I see build linting 247.738s and build task-clock 27.332Ks, so we're talking about <1% build time, which would be reduced by an unclear percentage? I'm not sure that's non-negligible compared to other optimizations we could work on and are working on

[Damiano Testa]

I always have a hard time understanding those numbers: build linting is about 4 minutes, building all of mathlib takes about 50 minutes in CI. Why is that not closer to 10%?

[Thomas Murrills]

(Note: a while ago I experimented with something like this in #mathlib4>linting_rules (and foo_rules) for syntax node linters specifically. While I think it would be nice to make declaring linters easy and consistent, I can’t speak to whether it would actually give us a worthwhile performance benefit.)

[Damiano Testa]

Thomas, I had forgotten about your experiment: thank you for reminding me of it!

[Kim Morrison]

Damiano Testa said:

I always have a hard time understanding those numbers: build linting is about 4 minutes, building all of mathlib takes about 50 minutes in CI. Why is that not closer to 10%?

Parallelism.

[Damiano Testa]

Ah, so merging the linters could make the performance worse! I was definitely not expecting that!

[Kim Morrison]

Oh, I doubt that's an issue. It is the build that is benefitting from parallelism. Sebastian was talking about task-clock above (27Ks), while you were talking about wall-clock (50 minutes).

[Damiano Testa]

I kind of feel like everyone is tellking 2 + 2 and I am failing to understand that they mean 4.

[Damiano Testa]

Is the conclusion that at the moment unifying linters would be a negligible gain in performance and that it makes sense to think about other tools?