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

  • 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

Estimated changes

added def asDotGraph
added def graph
added def importGraphCLI
added def main