← All repos

import-graph

Tool to analyse the import structure of lean projects.

GitHubreservoir.lean-lang.org/@leanprover-community/import-graph
lean4
Browse cluster: Lean4 Formal Verification & Cryptography →
361commits
22contributors
2languages

Tech stack & purpose

import-graph is a tool for analyzing the import structure of Lean 4 projects. It generates visual representations of module dependencies in multiple formats including PDF, HTML, JSON, and DOT, with the HTML output providing an interactive visualization. The tool is built in Lean and uses Lake as its build system, optionally leveraging Graphviz for format conversion. It was originally extracted from the Mathlib project by Kim Morrison and other contributors, with the HTML visualization adapted from Eric Wieser's earlier Lean 3 version, and is currently maintained by Jon Eugster and the broader Lean community.

Community & reference links

Languages

Lean
78.1%
HTML
21.9%

Contributors