Speeding up lint

Stream: general

[Patrick Stevens]

Here's an idea to shoot down: could the PR-check linting step be run only over git diff --name-only HEAD $(git merge-base HEAD $basebranch) (where the $basebranch is usually going to be master)? If not, could we split up the lints into two chunks, one which is safe to run on that diff and one which is not? Linting has so far taken 17mins and counting on https://github.com/leanprover-community/mathlib/runs/3915905265, and I assume that's normal.

[Bryan Gin-ge Chen]

Linting usually takes about 35 minutes (though it looks like the linting run you linked finished in about 23 minutes; I guess Rob's office computer is faster than the machines most of our runners are on..). I don't think we could split linting up as you describe because some of the linters (especially the simp lemma linter) are explicitly meant to check interactions between all parts of the library at once.

[Alex J. Best]

I've also wondered about this, I think it should definitely be possible to have an attribute needs_context for linters that we can manually set to specify those that can be run independently of the enviroment (and hence declarations can't break if only later imports change for instance). However I think first we should check which linters are really the ones using time and why, maybe there are more low hanging fruit there, or maybe the simp linter is the slowst for example. With CI times increasing all the time it seems any more refined checks we can do will make everyones workflow easier.

[Johan Commelin]

The linting time is completely dominated by the simp linter.

[Patrick Stevens]

I guess if it's just one really slow linter, and lean4 has very different performance properties to lean3, and the port is happening Soon (TM), then it's probably better to wait until after the port before optimising things like this?

[Eric Wieser]

On a tangentially related note, it would be cool to have a github bot that prints all of the changed declarations in a PR, even if that information doesn't help the linter much

[Eric Wieser]

Especially for file-move PRs

[Alex J. Best]

This would be really great, also for metaprogramming changes, where it's hard to know if you inadvertently changed the meaning of something. Even just a diff of the doc-gen before and after would be pretty revealing

[Yaël Dillies]

Note that file moves are rather fine. Only imports can go wrong. What's more problematic is file splits.

[Yaël Dillies]

And yes I'm absolutely for this. I'd really suggested it somewhere.