List of Mathlib files ranked by number of dependents?

Stream: mathlib4

[Louis Cabarion]

As I understand it, lake build Mathlib/A/B.lean builds that file plus everything that (directly or indirectly) imports it. Is that correct?

If that is the case, then rebuild time depends on both the file’s contents and the number of its dependents. For heavily used files, the dependent rebuild cost should dominate. In particular, I’d expect Mathlib/Init.lean to be the worst case, since nearly everything depends on it. Is that right?

Is there an easy way to get a list of Mathlib files ordered by "number of dependents" (as a rough proxy for rebuild time)? Doesn’t need to be exact: just approximate ordering would help.

[Kim Morrison]

Have a look at the import-graph library (this is already required into Mathlib; it provides the lake exe graph command line tool). It has functions that give you the transitive dependencies, and it should be possible to cook up what you want fairly easily from that.

[Michael Rothgang]

There's also a script (in #24065) to list files in topological order.

[Damiano Testa]

There is also #general > Sort lines by import order of files @ 💬, with a Lean implementation of the sort order.