Definitions to support lake setup-file builds.

def Lake.buildImportsAndDeps (leanFile : Lake.FilePath) (imports : Array Lake.Module) : Lake.FetchM (Lake.BuildJob (Array Lake.FilePath))

Builds an Array of module imports for a Lean file. 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.