Definitions to support lake setup-file builds.

def Lake.recBuildImports (imports : Array Lake.Module) : Lake.FetchM (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 : Array Lake.Module) : Lake.FetchM (Lake.BuildJob (Array Lake.FilePath))

Builds an Array of module imports. Used by lake setup-file to build modules for the Lean server and by lake lean to build the imports of a file. Returns the set of module dynlibs built (so they can be loaded by Lean).

Equations

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