lakefile.toml

name = "importGraph"
description = "Tools to analyse and visualise the import structure of Lean packages and their files."
license = "Apache-2.0"
licenseFiles = ["LICENSE"]

defaultTargets = ["ImportGraph", "graph"]
testRunner = "ImportGraphTest"

[[require]]
name = "Cli"
scope = "leanprover"
rev = "main"

[[require]]
name = "batteries"
scope = "leanprover-community"
rev = "main"

[[lean_lib]]
name = "ImportGraph"

# `lake exe graph` constructs import graphs in `.dot` or graphical formats.
[[lean_exe]]
name = "graph"
root = "Main"
# Enables the use of the Lean interpreter by the executable (e.g., `runFrontend`)
# at the expense of increased binary size on Linux.
# Remove this line if you do not need such functionality.
supportInterpreter = true

[[lean_lib]]
name = "ImportGraphTest"