#min_imports in a command to find minimal imports

#min_imports in stx scans the syntax stx to find a collection of minimal imports that should be sufficient for stx to make sense. If stx is a command, then it also elaborates stx and, in case it is a declaration, then it also finds the imports implied by the declaration.

Unlike the related #find_home, this command takes into account notation and tactic information.

Limitations

Parsing of attributes is hard and the command makes minimal effort to support them. Here is an example where the command fails to notice a dependency:

import Mathlib.Data.Sym.Sym2.Init -- the actual minimal import
import Aesop.Frontend.Attribute   -- the import that `#min_imports in` suggests

import Mathlib.Tactic.MinImports

-- import Aesop.Frontend.Attribute
#min_imports in
@[aesop (rule_sets := [Sym2]) [safe [constructors, cases], norm]]
inductive Rel (α : Type) : α × α → α × α → Prop
  | refl (x y : α) : Rel _ (x, y) (x, y)
  | swap (x y : α) : Rel _ (x, y) (y, x)

-- `import Mathlib.Data.Sym.Sym2.Init` is not detected by `#min_imports in`.

Todo

Examples When parsing an example, #min_imports in retrieves all the information that it can from the Syntax of the example, but, since the example is not added to the environment, it fails to retrieve any Expr information about the proof term. It would be desirable to make #min_imports in example ... inspect the resulting proof and report imports, but this feature is missing for the moment.

Using InfoTrees It may be more efficient (not necessarily in terms of speed, but of simplicity of code), to inspect the InfoTrees for each command and retrieve information from there. I have not looked into this yet.

partial def Mathlib.Command.MinImports.getSyntaxNodeKinds : Lean.Syntax → Lean.NameSet

getSyntaxNodeKinds stx takes a Syntax input stx and returns the NameSet of all the SyntaxNodeKinds and all the identifiers contained in stx.

def Mathlib.Command.MinImports.getVisited (env : Lean.Environment) (decl : Lean.Name) : Lean.NameSet

extracts the names of the declarations in env on which decl depends.

Equations

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

def Mathlib.Command.MinImports.getId (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.Syntax

getId stx takes as input a Syntax stx. If stx contains a declId, then it returns the ident-syntax for the declId. If stx is a nameless instance, then it also tries to fetch the ident for the instance. Otherwise it returns .missing.

Equations

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

partial def Mathlib.Command.MinImports.getIds : Lean.Syntax → Lean.NameSet

getIds stx extracts all identifiers, collecting them in a NameSet.

def Mathlib.Command.MinImports.getAttrNames (stx : Lean.Syntax) : Lean.NameSet

getAttrNames stx extracts attributes from stx. It does not collect simp, ext, to_additive. It should collect almost all other attributes, e.g., fun_prop.

Equations

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

def Mathlib.Command.MinImports.getAttrs (env : Lean.Environment) (stx : Lean.Syntax) : Lean.NameSet

getAttrs env stx returns all attribute declaration names contained in stx and registered in the Environment env`.

Equations

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

def Mathlib.Command.MinImports.previousInstName : Lean.Name → Lean.Name

previousInstName nm takes as input a name nm, assuming that it is the name of an auto-generated "nameless" instance. If nm ends in ..._n, where n is a number, it returns the same name, but with _n replaced by _(n-1), unless n ≤ 1, in which case it simply removes the _n suffix.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Command.MinImports.previousInstName x✝ = x✝

def Mathlib.Command.MinImports.getAllDependencies (cmd id : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.NameSet

getAllDependencies cmd id takes a Syntax input cmd and returns the NameSet of all the declaration names that are implied by

• the SyntaxNodeKinds,
• the attributes of cmd (if there are any),
• the identifiers contained in cmd,
• if cmd adds a declaration d to the environment, then also all the module names implied by d. The argument id is expected to be an identifier. It is used either for the internally generated name of a "nameless" instance or when parsing an identifier representing the name of a declaration.

Note that the return value does not contain dependencies of the dependencies; you can use Lean.NameSet.transitivelyUsedConstants to get those.

Equations

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

def Mathlib.Command.MinImports.getAllImports (cmd id : Lean.Syntax) (dbg? : Bool := false) : Lean.Elab.Command.CommandElabM Lean.NameSet

getAllImports cmd id takes a Syntax input cmd and returns the NameSet of all the module names that are implied by

• the SyntaxNodeKinds,
• the attributes of cmd (if there are any),
• the identifiers contained in cmd,
• if cmd adds a declaration d to the environment, then also all the module names implied by d. The argument id is expected to be an identifier. It is used either for the internally generated name of a "nameless" instance or when parsing an identifier representing the name of a declaration.

Equations

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

def Mathlib.Command.MinImports.getIrredundantImports (env : Lean.Environment) (importNames : Lean.NameSet) : Lean.NameSet

getIrredundantImports env importNames takes an Environment and a NameSet as inputs. Assuming that importNames are module names, it returns the NameSet consisting of a minimal collection of module names whose transitive closure is enough to parse (and elaborate) cmd.

Equations

• Mathlib.Command.MinImports.getIrredundantImports env importNames = Lean.RBTree.diff importNames (env.findRedundantImports (Lean.RBTree.toArray importNames))

def Mathlib.Command.MinImports.minImpsCore (stx id : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

minImpsCore stx id is the internal function to elaborate the #min_imports in command. It collects the irredundant imports to parse and elaborate stx and logs

import A
import B
...
import Z

The id input is expected to be the name of the declaration that is currently processed. It is used to provide the internally generated name for "nameless" instances.

Equations

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

def Mathlib.Command.MinImports.minImpsStx : Lean.ParserDescr

#min_imports in cmd scans the syntax cmd and the declaration obtained by elaborating cmd to find a collection of minimal imports that should be sufficient for cmd to work.

Equations

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

def Mathlib.Command.MinImports.«command#min_importsIn_» : Lean.ParserDescr

#min_imports in cmd scans the syntax cmd and the declaration obtained by elaborating cmd to find a collection of minimal imports that should be sufficient for cmd to work.

Equations

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