import graph

Stream: Is there code for X?

[Kenny Lau]

Is there a tool to see the actual import graph of mathlib? For example, given two files, I would like to see the (shortest) path of imports from A to B

[Kenny Lau]

this feels like a standard CS exercise

[Yaël Dillies]

Do you know the lake exe graph suite?

[Kenny Lau]

is there a list of lake modules? I can't find 'graph' in https://github.com/leanprover/lake

[Bryan Gin-ge Chen]

I think you get it with mathlib (?), but the repo is here https://github.com/leanprover-community/import-graph

[Kenny Lau]

is the graph for mathlib published anywhere?

[Bryan Gin-ge Chen]

We have this page, so the data must be somewhere: https://leanprover-community.github.io//mathlib4_docs/mathlib.html

Give me a sec.

[Bryan Gin-ge Chen]

This should contain the graph for the latest commit of master (in .dot format, I think): https://github.com/leanprover-community/mathlib4/actions/runs/16864223820/artifacts/3729548120

Looks like we're uploading these as artifacts for every build job. If you go to the workflow page (e.g. by clicking on the green checkmark next to a commit, finding one of the "continuous integration ..." jobs, clicking "Details", and then going to the Summary page), there should be an artifact at the bottom of the page named "import-graph". Note that these are only kept for 90 days.

[Kenny Lau]

that's a slightly non-trivial path

[Kenny Lau]

I think it would be more beginner friendly if this was available on the docs page somewhere

[Kenny Lau]

in html form

[Bryan Gin-ge Chen]

I agree. It probably would be a fun project!

[Kenny Lau]

what software can i use to visualise the dot graph?

[Yaël Dillies]

Here's one: https://dreampuf.github.io/GraphvizOnline/

[Kenny Lau]

i tried that, the graph is way too big for that

[Yaël Dillies]

What are the start and end points of your graph?

[Kenny Lau]

i guess if i have start and end points then it would be shorter

[Kenny Lau]

but i just downloaded the whole graph file above

[Yaël Dillies]

Try running lake exe graph --from A --to B

[Kenny Lau]

is there a way to find the generators for the common descendents of A and B?

[Kim Morrison]

Read the source code for import-graph. It has some basic graph manipulations already there, it should be straightforward to implement things like this yourself.

[Kim Morrison]

The existing functions there give you the import graph as something like a HashMap Name (HashSet Name), I forget exactly what. Then it's just map manipulations to do whatever graph query you want.