Definitions to support lake print-paths builds.

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

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.

    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.

      Instances For