Why is CI lint so slow?

Stream: mathlib4

[Geoffrey Irving]

For https://github.com/leanprover-community/mathlib4/pull/7677#issuecomment-1763178710, my last commit took <8m to build, and >19m to lint. Is lint not well parallelized or cached?

[Jireh Loreaux]

The build is incremental, so it didn't have to build all of mathlib, but linting basically takes the same amount of time for every run. That's because much of the linting is a global check.

[Jireh Loreaux]

So, correct, it's not cached.

[Scott Morrison]

In particular, linting is checking a global property of the simp set (that the LHS doesn't already simplify via other simp lemmas), and there doesn't appear to be any useful way to cache information for this check.

[Geoffrey Irving]

^ Though that operation is certainly parallelizable. Is it run in parallel currently?

[Alex J. Best]

lintCore does use Tasks, https://github.com/leanprover/std4/blob/2b8aaf35445a336eafb3d73631df184e7c7b7691/Std/Tactic/Lint/Frontend.lean#L101, so I think the answer should be yes

[Scott Morrison]

Yes: make lint in Mathlib should max out your CPU!