Mathlib modules in topological sort

Stream: new members

[Giovanni Mascellani]

Is there a (reasonably easy) way to list the mathlib modules listed in the left column of https://leanprover-community.github.io/mathlib_docs/ is some kind of topological sort?

[Eric Wieser]

The graph data is available at https://leanprover-community.github.io/mathlib_docs/import.gexf, which I think is a semi-standard format

[Giovanni Mascellani]

Thanks. For the benefit of posterity, this hacky oneliner produces a topological sort:

cat import.gexf | grep '<edge ' | sed -e 's| *<edge source="\(.*\)" target="\(.*\)" id=".*" />.*|\1 \2|' | tsort

[Eric Wieser]

To be clear, did you want _any_ topological sort, or the one that the files are actually imported in?

[Giovanni Mascellani]

Any topological sort is fine for me. My problem is that I'm starting getting a knowledge of mathlib, and it's a bit daunting at first. A topological sort helps me understanding what I should have a look first to build a mind map of the part of the library I'd like to investigate.

[Eric Wieser]

In case you hadn't noticed already, the right sidebar of #docs lets you jump to dependents and dependencies, which is a way to interactively walk through the dependency graph

[Eric Wieser]

Topological sorts don't sound that useful, because similar files can be arbitrarily far apart

[Giovanni Mascellani]

Thanks for the hint, though, together with some grepping, I find that the topological sort is better for having a bird's view, even if with the problem you mention.

[Eric Wieser]

https://eric-wieser.github.io/mathlib-import-graph/ is another option