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
  • 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
      Instances For
        @[inline]
        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
            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

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

                Equations
                Instances For
                  @[inline]

                  Fetch the dynlibs of a list of imports. For internal use.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Lake.computeModuleDeps (impLibs externLibs dynlibs plugins : Array Dynlib) :
                    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

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

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

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

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

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

                              The ModuleFacetConfig for the builtin leanArtsFacet.

                              Equations
                              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

                                      The ModuleFacetConfig for the builtin bcFacet.

                                      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 with -DLEAN_EXPORTING set, which exports Lean symbols defined within the C files.

                                        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. This version does not export any Lean symbols.

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

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

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

                                              The ModuleFacetConfig for the builtin oExportFacet.

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

                                                The ModuleFacetConfig for the builtin oNoExportFacet.

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

                                                  The ModuleFacetConfig for the builtin oFacet.

                                                  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 or --plugin).

                                                    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., imports, c, o, dynlib).

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      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