tooling for checking imports in mathlib

Stream: general

[Kevin Buzzard]

A recent mathlib PR has the diff for Mathlib/RingTheory/PowerSeries/WellKnown.lean starting

- import Mathlib.RingTheory.PowerSeries.Basic
+ import Mathlib.RingTheory.PowerSeries.Inverse
import Mathlib.Data.Nat.Parity
+ import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Algebra.BigOperators.NatAntidiagonal

This file is imported by Bernoulli numbers, it's not a leaf file, so I feel obliged to check that this import change isn't disruptive in some way. But can I do this automatically? Is there some sort of program which can be run giving this change a score out of 10 for metrics which people who understand import trees care about? For example it could inform us that the longest pole just doubled.

[Kevin Buzzard]

imports.png

Here's another one on another PR. I really don't know how to judge these things.

[Sebastian Ullrich]

Metrics such as pole length could be added to the speedcenter, but need an explicit !bench to be reported before merging

[Patrick Massot]

A much more immediate information would be the number of dependencies of a given file before and after the change. The import graph stuff should be able to say that.

[Rémy Degenne]

@Moritz Firsching did some work investigating the number of new imports (by calling several times lake exe graph to some files with a build in between) for that PR: https://github.com/leanprover-community/mathlib4/pull/10635#issuecomment-2022734136
Perhaps that can be a starting point for a new tool?

[Peiran Wu]

Kevin Buzzard said:

imports.png

Here's another one on another PR. I really don't know how to judge these things.

This looks like my PR. I've just tried lake exe pole --to <Module> and it seems the longest pole wouldn't change. On the current master branch, Mathlib.Algebra.Module.Torsion has a pole length of 95 whereas the newly added Mathlib.Data.ZMod.Module has 76. The 4 removed imports were redundant before the change, but I haven't considered whether their removal affects the performance in any way.

[Damiano Testa]

I have been playing a bit with imports and have also found few tools to help with this. What do you think of adding this function?

import Lean.Elab.Command

open Lean in
elab "#imports " id:(ident)? : command => do
  let imps := (← getEnv).allImportedModuleNames.map (·.toString)
  let idStr := match id with
                | some id => id.getId.toString
                | none => ""
  let found := imps.filter (idStr.isPrefixOf)
  match found with
    | #[] => logWarningAt (id.getD default) m!"No file starting with '{idStr}' is imported"
    | #[f] => logInfoAt (id.getD default) m!"'{f}' is imported"
    | _ => logInfoAt (id.getD default) m!"Keep typing to refine\n{found}"

#imports -- everything up to `Lean.Elab.Command`

#imports Lean.Data.N
-- Keep typing to refine
-- [Lean.Data.Name, Lean.Data.NameMap, Lean.Data.NameTrie]

#imports Lean.Data.NameT
-- 'Lean.Data.NameTrie' is imported

#imports X
-- No file starting with 'X' is imported

[Kim Morrison]

Nice would be a tool that reports a list of the transitively imported files that are not actually used. This has the usual constants / syntax / tactics problems, of course.

Back in Lean 3 days we had this: the analogue of lake exe graph could highlight unused transitive imports (based only on observed constants).

[Kim Morrison]

Also nice would be if the "incremental" version of #min_imports could report on the impact (how many new files are transitively imported by the necessary import increase for this declaration?)

[Damiano Testa]

Kim, I think that what you want is likely close: #min_imports and especially the linter version seem very promising.

I am testing the minImports linter on all of Mathlib and I am getting very few errors on necessary imports. Currently, the only source of errors that I am not yet sure how to address are custom attributes, especially aesops rule_sets. Other than that, even "nameless instances" are yielding!

[Damiano Testa]

In fact, #min_imports in X can already report all the constants implied by X, whether they are syntax, tactic or Expr-generated.