Definitions to support lake setup-file
builds.
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.
Instances For
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.