`#min_imports` #

This module provides #min_imports, which minimizes the imports according to which are actually used in the declarations and syntax of the current file. It respects module-system relevant dependencies.

Note: testing #min_imports should not use #guard_msgs, as #min_imports reports back from the end of the file. Instead, this file exposes logAllMinImports and resetMinImports for testing.

Future work #

Refactor into more generic API usable by other infrastructure (in progress)
Improve the ergonomics around waiting for a message (loading widget, yellow bar)
Split out into API
Turn into an optional (expensive) linter
Account for non-persistent uses like example, #check, #eval under an option
#min_imports so far

Old `#min_imports` infrastructure #

source

def ImportGraph.Shake.Lean.Environment.minimalRequiredModules (env : Lean.Environment) :

Array Lean.Name

Does not work within the module system. Get the names of all needed imports.

Equations

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

Instances For

Modern `#min_imports` #

source

def ImportGraph.Shake.minImportsStx :

Lean.ParserDescr

Minimize the imports of the entire current module in the module system.

This command may be written anywhere in the file, and will still take into account the whole file. As such, the command will remain silent until the file finishes elaborating.

Currently, it accounts for constants, syntax, shake records, and runtime IR (except for attributes like @[inline]), but not yet meta IR from new meta defs.

To eliminate redundancies among the current file's imports without taking into account whether they are actually used or not, see #norm_imports.

This command currently only suggests module-system import blocks. It may still help with modulizing non-module files if all necessary imports are already modules, or by indicating which necessary imports are non-modules.

Equations