Tools for analyzing imports.

Provides the commands

• #redundant_imports which lists any transitively redundant imports in the current module.
• #min_imports which 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.

def Lean.Environment.importsOf (env : Lean.Environment) (n : Lean.Name) : Array Lean.Name

Find the imports of a given module.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Environment.importGraph (env : Lean.Environment) : Lean.NameMap (Array Lean.Name)

Construct the import graph of the current file.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Environment.importGraph.process (env : Lean.Environment) (i : Lean.Name) (m : Lean.NameMap (Array Lean.Name)) : Lean.NameMap (Array Lean.Name)

def Lean.Environment.findRedundantImports (env : Lean.Environment) (imports : Array Lean.Name) : Lean.NameSet

Return the redundant imports (i.e. those transitively implied by another import) amongst a candidate list of imports.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Environment.findRedundantImports.visit (Γ : Lean.NameMap (Array Lean.Name)) (targets : Array Lean.Name) (visited : Lean.NameSet) (seen : Lean.NameSet) (n : Lean.Name) : Lean.NameSet × Lean.NameSet

def Lean.NameMap.transitiveClosure (m : Lean.NameMap (Array Lean.Name)) : Lean.NameMap Lean.NameSet

Compute the transitive closure of an import graph.

Equations

• m.transitiveClosure = Lean.RBMap.fold (fun (r : Lean.NameMap Lean.NameSet) (n : Lean.Name) (i : Array Lean.Name) => Lean.NameMap.transitiveClosure.process m r n i) ∅ m

partial def Lean.NameMap.transitiveClosure.process (m : Lean.NameMap (Array Lean.Name)) (r : Lean.NameMap Lean.NameSet) (n : Lean.Name) (i : Array Lean.Name) : Lean.NameMap Lean.NameSet

def Lean.NameMap.transitiveReduction (m : Lean.NameMap (Array Lean.Name)) : Lean.NameMap (Array Lean.Name)

Compute the transitive reduction of an import graph.

Typical usage is transitiveReduction (← importGraph).

Equations

• One or more equations did not get rendered due to their size.

def Lean.NameMap.downstreamOf (m : Lean.NameMap (Array Lean.Name)) (targets : Lean.NameSet) : Lean.NameMap (Array Lean.Name)

Restrict an import graph to only the downstream dependencies of some set of modules.

Equations

• One or more equations did not get rendered due to their size.

def Lean.NameMap.upstreamOf (m : Lean.NameMap (Array Lean.Name)) (targets : Lean.NameSet) : Lean.NameMap (Array Lean.Name)

Restrict an import graph to only the transitive imports of some set of modules.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.NameMap.transitiveFilteredUpstream (node : Lean.Name) (graph : Lean.NameMap (Array Lean.Name)) (filter : Lean.Name → Bool) (replacement : optParam (Option Lean.Name) none) : List Lean.Name

Filter the list of edges … → node inside graph by the function filter.

Any such upstream node source where filter source returns true will be replaced by all its upstream nodes. This results in a list of all unfiltered nodes in the graph that either had an edge to node or had an indirect edge to node going through filtered nodes.

Will panic if the node is not in the graph.

def Lean.NameMap.filterGraph (graph : Lean.NameMap (Array Lean.Name)) (filter : Lean.Name → Bool) (replacement : optParam (Option Lean.Name) none) : Lean.NameMap (Array Lean.Name)

Filters the graph removing all nodes where filter n returns false. Additionally, replace edges from removed nodes by all the transitive edges.

This means there is a path between two nodes in the filtered graph iff there exists such a path in the original graph.

If the optional (replacement : Name) is provided, a corresponding node will be added together with edges to all nodes which had an incoming edge from any filtered node.

Equations

• One or more equations did not get rendered due to their size.

def unusedTransitiveImports (amongst : List Lean.Name) : Lean.CoreM (List (Lean.Name × List Lean.Name))

Returns a List (Name × List Name) with a key for each module n in amongst, whose corresponding value is the list of modules m in amongst which are transitively imported by n, but no declaration in n makes use of a declaration in m.

The current implementation is too slow to run on the entirety of Mathlib, although it should be fine for any sequential chain of imports in Mathlib.

Equations

• One or more equations did not get rendered due to their size.

def redundantImports (n? : optParam (Option Lean.Name) none) : Lean.CoreM Lean.NameSet

Return the redundant imports (i.e. those transitively implied by another import) of a specified module (or the current module if none is specified).

Equations

• redundantImports n? = do let env ← Lean.getEnv let imports : Array Lean.Name := env.importsOf (n?.getD env.header.mainModule) pure (env.findRedundantImports imports)

def «command#redundant_imports» : Lean.ParserDescr

List the imports in this file which can be removed because they are transitively implied by another import.

Equations

• «command#redundant_imports» = Lean.ParserDescr.node `command#redundant_imports 1024 (Lean.ParserDescr.symbol "#redundant_imports")

def Lean.Environment.minimalRequiredModules (env : Lean.Environment) : Array Lean.Name

Return the names of the modules in which constants used in the current file were defined, with modules already transitively imported removed.

Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.

Equations

• One or more equations did not get rendered due to their size.

def «command#min_imports» : Lean.ParserDescr

Try to compute a minimal set of imports for this file, by analyzing the declarations.

This must be run at the end of the file, and is not aware of syntax and tactics, so the results will likely need to be adjusted by hand.

Equations

• «command#min_imports» = Lean.ParserDescr.node `command#min_imports 1024 (Lean.ParserDescr.symbol "#min_imports")

def «command#minimize_imports» : Lean.ParserDescr

Equations

• «command#minimize_imports» = Lean.ParserDescr.node `command#minimize_imports 1024 (Lean.ParserDescr.symbol "#minimize_imports")

def Lean.Name.findHome (n : Lean.Name) (env : Option Lean.Environment) : Lean.CoreM Lean.NameSet

Find locations as high as possible in the import hierarchy where the named declaration could live.

def getModuleUri (modName : Lean.Name) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.DocumentUri)

Tries to resolve the module modName to a source file URI. This has to be done in the Lean server since the Environment does not keep track of source URIs.

Equations

• One or more equations did not get rendered due to their size.

structure GoToModuleLinkProps : Type

• modName : Lean.Name

instance instRpcEncodableGoToModuleLinkProps : Lean.Server.RpcEncodable GoToModuleLinkProps

Equations

• instRpcEncodableGoToModuleLinkProps = { rpcEncode := instRpcEncodableGoToModuleLinkProps.enc✝, rpcDecode := instRpcEncodableGoToModuleLinkProps.dec✝ }

def GoToModuleLink : Lean.Widget.Module

When clicked, this widget component jumps to the source of the module modName, assuming a source URI can be found for the module.

Equations

• One or more equations did not get rendered due to their size.

def «command#find_home!_» : Lean.ParserDescr

Find locations as high as possible in the import hierarchy where the named declaration could live. Using #find_home! will forcefully remove the current file. Note that this works best if used in a file with import Mathlib.

The current file could still be the only suggestion, even using #find_home! lemma. The reason is that #find_home! scans the import graph below the current file, selects all the files containing declarations appearing in lemma, excluding the current file itself and looks for all least upper bounds of such files.

For a simple example, if lemma is in a file importing only A.lean and B.lean and uses one lemma from each, then #find_home! lemma returns the current file.

Equations

• One or more equations did not get rendered due to their size.