speeding up linting

Stream: mathlib4

[Jeremy Tan]

I have a related question. How can we speed up linting? I think much of the linting we do is unnecessary, and I've observed that now times for linting are routinely in the 15-min range rather than ~10 min

[Jeremy Tan]

For simple PRs like a plain mathlib port, right now linting takes up a majority of the time needed

[Jeremy Tan]

Would it be possible to cache linting results like we already do for the build?

[Scott Morrison]

Caching linting is quite hard. The most time consuming part is the simp normal form linter, which really is a global test of the simp-set. There's nothing really to cache.

[Notification Bot]

4 messages were moved here from #mathlib4 > mathlib4 speedcenter by Sebastian Ullrich.

[Yaël Dillies]

In mathlib3, for comparison, building takes ~6h and linting 40min.

[Sebastian Ullrich]

I moved this conversation as it's not about how to measure performance, but do we want to track the global linter in the speedcenter as well? The benchmarking machine is roughly twice as fast as the CI runner, so it would add some 5 minutes to each run.

[Eric Wieser]

Yaël Dillies said:

In mathlib3, for comparison, building takes ~6h and linting 40min.

I'm pretty sure linting is more like 1hr now

[Yaël Dillies]

Good old times...

[Gabriel Ebner]

@Sebastian Ullrich that would be great.