# 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.

Find the imports of a given module.

## Equations

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

## Instances For

Construct the import graph of the current file.

## Equations

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

## Instances For

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.

## Instances For

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

## Instances For

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.

## Instances For

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.

## Instances For

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.

## Instances For

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`

.

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.

## Instances For

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)

## Instances For

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")

## Instances For

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.

## Instances For

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")

## Instances For

## Equations

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

## Instances For

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

## Instances For

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.

## Instances For

## Equations

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

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.

## Instances For

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.