lint test optimization

Stream: maths

[Arthur Paulino]

Do you guys think it's worth it to try to optimize lint tests by using the result of the previous test and a git diff to see what has changed since then? They're taking ~28 minutes per commit and tend to get larger and larger as mathlib grows and more and more frequent as more people join us

[Floris van Doorn]

The simplifier linters (like simp_nf) take almost all of the time, and they are "global" linters. That means that a change to declaration A can cause the linter to fail for declaration B

[Yakov Pechersky]

Are you asking for this for faster turn around time to confirm the validity of a commit? Some linters are file-local, thru are solely syntactic. Those are the ones that run first. The linters you're asking about are global linters, like checking if some simp lemma is stated in a form that another upstream simp lemma would simp away.

[Yakov Pechersky]

From your diff, you'd have to reconstruct the whole available environment of declarations.

[Arthur Paulino]

Are you asking for this for faster turn around time to confirm the validity of a commit?

Not exactly... I'm just wondering if we could lower the computational cost of the process