Definitions to support lake print-paths builds.

def Lake.Workspace.processImportList (imports : List String) (self : Lake.Workspace) : Array Lake.Module

Construct an Array of Modules for the workspace-local modules of a List of import strings.

Equations

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

def Lake.recBuildImports (imports : Array Lake.Module) : Lake.IndexBuildM (Array (Lake.BuildJob Unit) × Array (Lake.BuildJob Lake.Dynlib) × Array (Lake.BuildJob Lake.Dynlib))

Recursively build a set of imported modules and return their build jobs, the build jobs of their precompiled modules and the build jobs of said modules' external libraries.

Equations

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

def Lake.buildImportsAndDeps (imports : List String) : Lake.BuildM (Array Lake.FilePath)

Builds the workspace-local modules of list of imports. Used by lake print-paths to build modules for the Lean server. Returns the set of module dynlibs built (so they can be loaded by the server).

Builds only module .olean and .ilean files if the package is configured as "Lean-only". Otherwise, also builds .c files.

Equations

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