Documentation

Lake.Build.Module

Module Facet Builds #

Build function definitions for a module's builtin facets.

Compute library directories and build external library Jobs of the given packages.

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

    Build the dynlibs of the transitive imports that want precompilation and the dynlibs of their imports.

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

      Recursively parse the Lean files of a module and its imports building an Array product of its direct local imports.

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

        Recursively compute a module's transitive imports.

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

          Recursively compute a module's precompiled imports.

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

            Recursively build a module's dependencies, including:

            • Transitive local imports
            • Shared libraries (e.g., extern_lib targets or precompiled modules)
            • extraDepTargets of its library
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Recursively build a Lean module. Fetch its dependencies and then elaborate the Lean source file, producing all possible artifacts (i.e., .olean, ilean, and .c).

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

                The ModuleFacetConfig for the builtin oleanFacet.

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

                  The ModuleFacetConfig for the builtin ileanFacet.

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

                    The ModuleFacetConfig for the builtin cFacet.

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

                      Recursively build the module's object file from its C file produced by lean.

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

                        Recursively build the shared library of a module (e.g., for --load-dynlib).

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

                          A name-configuration map for the initial set of Lake module facets (e.g., lean.{imports, c, o, dynlib]).

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