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.

Instances For

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

    Instances For

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

      Instances For

        The ModuleFacetConfig for the builtin importsFacet.

        Instances For

          Recursively compute a module's transitive imports.

          Instances For

            The ModuleFacetConfig for the builtin transImportsFacet.

            Instances For

              Recursively compute a module's precompiled imports.

              Instances For

                The ModuleFacetConfig for the builtin precompileImportsFacet.

                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
                  Instances For

                    The ModuleFacetConfig for the builtin depsFacet.

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

                      Instances For

                        The ModuleFacetConfig for the builtin leanArtsFacet.

                        Instances For

                          The ModuleFacetConfig for the builtin oleanFacet.

                          Instances For

                            The ModuleFacetConfig for the builtin ileanFacet.

                            Instances For

                              The ModuleFacetConfig for the builtin cFacet.

                              Instances For

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

                                Instances For

                                  The ModuleFacetConfig for the builtin oFacet.

                                  Instances For

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

                                    Instances For

                                      The ModuleFacetConfig for the builtin dynlibFacet.

                                      Instances For

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

                                        Instances For