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