#norm_imports for interactive normalization of import blocks

This file provides #norm_imports, which, when run in some file, suggests normalizing that file's imports by

1. removing redundant imports that are implied by other imports
2. sorting and grouping the imports in a standard order

#norm_imports currently only works in the module system. This restriction may be removed in the future.

Note that this does not take into account dependencies from the current file, which should be handled by #min_imports.

Future work

• Make this work outside of the module system.
• Allow configuration of the formatting behavior in accordance with Import.pretty's options.
• Allow sorting by "height" of the source library in the package dependency graph, e.g. Lean modules coming first/last, etc.

def ImportGraph.NormImports.«command#norm_imports» : Lean.ParserDescr

Normalizes the imports of the current file. This removes rendundant imports and formats the resulting import block in a standard fashion, ensuring that the same modules are available at the same visibilities and phases. It does not take into account the declarations or usages of those modules in the current file.

#norm_imports will keep any direct imports of ImportGraph.Tools.NormImports, ImportGraph.Tools, or ImportGraph in place, while ignoring them for the calculation of the redundant imports.

Equations

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