A simple tool to create import graphs of lake packages.


For creating different output formats than .dot (for example to create a .pdf file), you should have graphviz installed.


You can import this in any lean projects by the following line to your lakefile.lean:

require importGraph from git "" @ "main"

After running lake update -R importGraph in your project, you can create import graphs with

lake exe graph

A typical command is lake exe graph --reduce --to MyModule my_graph.pdf where MyModule follows the same module naming you would use to import it in lean. See lake exe graph --help for more options.


There are a few commands implemented, which help you analysing the imports of a file. These are accessible by adding import ImportGraph.Imports to your lean file.

  • #redundant_imports: lists any transitively redundant imports in the current module.
  • #minimize_imports: attempts to construct a minimal set of imports for the declarations in the current file. (Must be run at the end of the file. Tactics and macros may result in incorrect output.)
  • #find_home decl: suggests files higher up the import hierarchy to which decl could be moved.


This code has been extracted from mathlib and has mainly been written by Kim Morrison and a few other mathlib contributors.


For issues, questions, or feature requests, please reach out to Jon Eugster.