Commit 2023-07-10 05:24 02ea90a0
View on Github →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