Zulip Chat Archive

Stream: new members

Topic: Mathlib modules in topological sort

Giovanni Mascellani (May 02 2023 at 21:06):

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 (May 02 2023 at 21:18):

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 (May 04 2023 at 20:06):

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 (May 04 2023 at 20:16):

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

Giovanni Mascellani (May 04 2023 at 20:18):

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 (May 04 2023 at 20:20):

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 (May 04 2023 at 20:20):

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

Giovanni Mascellani (May 04 2023 at 20:24):

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 (May 04 2023 at 20:28):

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

Last updated: Dec 20 2023 at 11:08 UTC