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

    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

      The ModuleFacetConfig for the builtin importsFacet.

      Equations
      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

            The ModuleFacetConfig for the builtin transImportsFacet.

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

                Recursively compute a module's precompiled imports.

                Equations
                Instances For

                  The ModuleFacetConfig for the builtin precompileImportsFacet.

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

                      The ModuleFacetConfig for the builtin depsFacet.

                      Equations
                      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

                                            The ModuleFacetConfig for the builtin coFacet.

                                            Equations
                                            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).

                                                      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