minImports linter request

Stream: mathlib4

[Kim Morrison]

@Damiano Testa, how hard would it be to have the minImports warning include the change in total transitive imports, e.g.

Imports increased by 37 to
[Aesop.Frontend.Attribute, Aesop.Frontend.Tactic, Mathlib.Combinatorics.Quiver.Basic]

[Kim Morrison]

This would be really helpful for identifying bigger jumps, without requiring intimate knowledge of the library (and remembering/checking what the previous warning said).

[Damiano Testa]

All the information is there, since the imports that the linter suggests are a subset of the available ones. I guess the only function that is missing is one that computes the number of transitive imports with input an array of imports.

[Damiano Testa]

For that, Johan wrote a python script that the PR summary uses, but I imagine that it would not be hard to update that to a Lean version.

[Damiano Testa]

As a side comment, if you are using the minImports linter, maybe I can also import it somewhere in the mathlib hierarchy, say in Tactic.Common? I see that it is already imported in Tactic.Common!

[Damiano Testa]

I'll take a look at what is in ImportGraph to see whether transitive import counts are "close".

[Damiano Testa]

The linter currently stores the "surface" imports, that is what you obtain from all imports so far by removing the redundant ones.

[Damiano Testa]

I get easily confused by this, but "transitive imports" means "number of edges in the transitive closure", right?

[Kim Morrison]

Sure. How many more files are in the environment as a result of the change in imports.

[Kim Morrison]

There's a function Lean.NameMap.transitiveClosure provided in import-graph. Applying that to Lean.Environment.importGraph should give you what you want.

[Kim Morrison]

So I think one that just takes the union of the values of that map, over the imports that minImports prints in the warning, and compute the difference in the size of that union, before and after.

[Damiano Testa]

Ok, yes that is simpler than figuring out numbers of edges and, as you say, it uses functions that already exist. I'll try to get it done today!

[Damiano Testa]

#18303

[Damiano Testa]

I find the ImportGraph API a little confusing: the new reports are probably slower than they could be and I can see that what I am doing is likely repeating quite a few computations, but I am not really sure how to streamline it.

[Kim Morrison]

@Damiano Testa, why not stash env.importGraph, as well as the transitive closure of that, in an IO.Ref too? These data do not change throughout the file, and so need not be recomputed.

[Damiano Testa]

Ok, I'll try that.

[Damiano Testa]

I added the import graph to the IO.Ref and it does appear snappier. I did not time it, but the difference is noticeable.

[Kim Morrison]

Thanks! I left some more comments.

[Damiano Testa]

Comments accepted, except for one that I do not know how to implement. :smile:

[Kim Morrison]

I've clarified!