WorkspaceModel and shake

This file defines interactions between a WorkspaceModel and shake. The import hierarchy and workspace model data allows us to turn needs into imports and compare different imports with respect to minimality. Notably, it provides

• WorkspaceModel.toRawImports, which converts the indices in a Needs into Imports (without doing any reduction)
• DeclNeeds.toSimultaneousImportNeeds, which bakes the needs expressed in DeclNeeds into a single ImportNeeds
• ImportNeeds.providersByLib, which calculates (per library) which modules provide the given ImportNeeds

def ImportGraph.WorkspaceModel.toRawImports (w : WorkspaceModel) (n : Shake.Needs) (skipInit : Bool := true) : Array Lean.Import

Assuming that the indices in Needs correspond to module indices in the provided workspace model, record an Import for each set index in Needs in some order. This does not remove redundant imports. By default, this skips modules with prefix Init.

Equations

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

def ImportGraph.WorkspaceModel.implicitInitNeeds (w : WorkspaceModel) (base : Shake.Needs) : Shake.Needs

Every non-prelude file adds public import Init and public meta import Init to every file behind the scenes. This repesents (exactly) those two files. This should be added to any base : Needs which should represent what a typical file actually gets. Returns base unchanged if Init is not in the workspace model (this should be impossible).

Equations

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

def ImportGraph.Shake.ImportNeeds.ofExtraModUses (w : WorkspaceModel) (uses : List Lean.ExtraModUse) (init : ImportNeeds := ∅) : ImportNeeds

Convert extra mod uses into ImportNeeds.

Unfortunately, ExtraModUse has no notion of allowMeta, so we make the unimposing choice to set allowMeta := true. Note that a conservative choice would insist on non-meta, but extra mod uses are frequently from metaprograms which are already meta (and thus records a non-meta extra mod use) or from e.g. lemmas used in tactic proofs (which allow meta). So we accept unlikely possible breakage to avoid suggesting e.g. meta import Foo; import Foo or missing out on viable declaration locations in #find_home.

Equations

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

def ImportGraph.Shake.DeclNeeds.toSimultaneousImportNeeds (w : WorkspaceModel) (declNeeds : DeclNeeds) (declImportNeeds : ImportNeeds := ∅) : StanceM ImportNeeds

Collapse the ImportNeeds of all declarations in DeclNeeds. This is incorrect for splitting up declarations, but adequate for moving them to a single place.

Equations

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

def ImportGraph.Shake.ImportNeeds.providersByLib (w : WorkspaceModel) (needs : ImportNeeds) (league : Option ModuleBitset := none) : Std.HashMap LibIdx (Array ModIdx)

Computes a mapping LibIdx → Array ModIdx assigning to each library in the workspace model an array of modules which provide needs : ImportNeeds and are minimal. Namely, provider modules which are downstream of other provider modules (ignoring module system annotations) are knocked out.

It then ranks the "winning" modules first by import depth among imports from the same library (i.e. not counting imports of upstream libraries towards the depth), then by number of previous modules from the same library, then by absolute number of previous modules, then alphabetically.

league : ModuleBitset specifies the modules among which the competition is conducted. If none, this is all modules.

Equations

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