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 «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 : Environment) : Array 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 : Name) (env : Option Environment) : CoreM 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.

def «command#import_diff_» : Lean.ParserDescr

#import_diff foo bar ... computes the new transitive imports that are added to a given file when modules foo, bar, ... are added to the set of imports of the file. More precisely, it computes the import diff between when foo, bar, ... are added to the imports and when foo, bar, ... are removed from the imports.

Note: the command also works when some of the modules passed as arguments are already present in the file's imports.

Equations

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