Documentation

Lake.Build.Imports

Definitions to support lake print-paths builds.

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

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