Documentation

Lake.Build.Module

Module Facet Builds #

Build function definitions for a module's builtin facets.

@[deprecated "Deprecated without replacement" (since := "2025-03-28")]

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

Equations
    Instances For

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

      Equations
        Instances For

          The ModuleFacetConfig for the builtin importsFacet.

          Equations
            Instances For
              Instances For
                @[inline]
                Equations
                  Instances For

                    Recursively compute a module's transitive imports.

                    Equations
                      Instances For

                        The ModuleFacetConfig for the builtin transImportsFacet.

                        Equations
                          Instances For
                            Equations
                              Instances For

                                Recursively compute a module's precompiled imports.

                                Equations
                                  Instances For

                                    The ModuleFacetConfig for the builtin precompileImportsFacet.

                                    Equations
                                      Instances For

                                        Fetch dynlibs of the packages' external libraries. For internal use.

                                        Equations
                                          Instances For

                                            For internal use.

                                            Fetches the library dynlibs of a list of non-local imports. Modules are loaded as part of their whole library.

                                            Equations
                                              Instances For
                                                def Lake.computeModuleDeps (impLibs externLibs dynlibs plugins : Array Dynlib) :
                                                Equations
                                                  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
                                                      Instances For

                                                        The ModuleFacetConfig for the builtin depsFacet.

                                                        Equations
                                                          Instances For

                                                            Remove cached file hashes of the module build outputs (in .hash files).

                                                            Equations
                                                              Instances For

                                                                Cache the file hashes of the module build outputs in .hash files.

                                                                Equations
                                                                  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, .c, and .bc).

                                                                    Equations
                                                                      Instances For

                                                                        The ModuleFacetConfig for the builtin leanArtsFacet.

                                                                        Equations
                                                                          Instances For

                                                                            The ModuleFacetConfig for the builtin oleanFacet.

                                                                            Equations
                                                                              Instances For

                                                                                The ModuleFacetConfig for the builtin ileanFacet.

                                                                                Equations
                                                                                  Instances For

                                                                                    The ModuleFacetConfig for the builtin cFacet.

                                                                                    Equations
                                                                                      Instances For

                                                                                        The ModuleFacetConfig for the builtin bcFacet.

                                                                                        Equations
                                                                                          Instances For

                                                                                            Recursively build the module's object file from its C file produced by lean with -DLEAN_EXPORTING set, which exports Lean symbols defined within the C files.

                                                                                            Equations
                                                                                              Instances For

                                                                                                The ModuleFacetConfig for the builtin coExportFacet.

                                                                                                Equations
                                                                                                  Instances For

                                                                                                    Recursively build the module's object file from its C file produced by lean. This version does not export any Lean symbols.

                                                                                                    Equations
                                                                                                      Instances For

                                                                                                        The ModuleFacetConfig for the builtin coNoExportFacet.

                                                                                                        Equations
                                                                                                          Instances For

                                                                                                            The ModuleFacetConfig for the builtin coFacet.

                                                                                                            Equations
                                                                                                              Instances For

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

                                                                                                                Equations
                                                                                                                  Instances For

                                                                                                                    The ModuleFacetConfig for the builtin bcoFacet.

                                                                                                                    Equations
                                                                                                                      Instances For

                                                                                                                        The ModuleFacetConfig for the builtin oExportFacet.

                                                                                                                        Equations
                                                                                                                          Instances For

                                                                                                                            The ModuleFacetConfig for the builtin oNoExportFacet.

                                                                                                                            Equations
                                                                                                                              Instances For

                                                                                                                                The ModuleFacetConfig for the builtin oFacet.

                                                                                                                                Equations
                                                                                                                                  Instances For

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

                                                                                                                                    Equations
                                                                                                                                      Instances For

                                                                                                                                        The ModuleFacetConfig for the builtin dynlibFacet.

                                                                                                                                        Equations
                                                                                                                                          Instances For

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

                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                @[reducible, inline]

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

                                                                                                                                                Equations
                                                                                                                                                  Instances For