import graph

Stream: mathlib4

[Yury G. Kudryashov]

Do we have something like leanproject import-graph for Lean 4?

[Yury G. Kudryashov]

Ping here. Can we ask lake/lean about all module goals and their dependencies?

[Scott Morrison]

This was discussed in the last porting meeting. Tentatively, I think the answer is "no we can't do that right now, but we'd like to be able to, and this seems like a good first project in learning how to work with lake". :-)

[Scott Morrison]

@Yury G. Kudryashov #5441 provides some basic functionality for inspecting the import graph. Currently it only provides the import graph of the current file, but with some frontend magic we could ask about not-yet-imported files, too.

This is not asking lake, and in particular is relying on having all the oleans in place.

[Scott Morrison]

And now #5513 provides most of the functionality of leanproject import-graph.

[Scott Morrison]

import_graph.jpg