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.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.