Commit 2023-07-10 05:24 02ea90a0

feat: lake exe graph, as replacement for leanproject import-graph (#5513) Example usage:

lake exe graph --from Mathlib.Topology.Constructions --to Mathlib/Topology/Homotopy/Contractible.lean --reduce import_graph.pdf

producing

• import_graph.pdf Current features:

• supports --to and --from to select a slice of the full import graph
• accepts either module names or file names
• supports --reduce to perform transitive reduction
• output to .dot files, or if you have graphviz installed output to any supported format (e.g. .pdf as above). Still missing:
• --show-unused (although all the machinery is now in place to do this)
• --exclude-tactics