Documentation

Lake.Build.Module

Module Facet Builds #

Build function definitions for a module's builtin facets.

source
def Lake.recBuildExternDynlibs (pkgs : Array Lake.Package) :
Lake.IndexBuildM (Array (Lake.BuildJob Lake.Dynlib) × Array Lake.FilePath)

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

Instances For
    source
    def Lake.recBuildPrecompileDynlibs (imports : Array Lake.Module) :
    Lake.IndexBuildM (Array (Lake.BuildJob Lake.Dynlib) × Array (Lake.BuildJob Lake.Dynlib) × Array Lake.FilePath)

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

    Instances For
      source
      partial def Lake.recBuildPrecompileDynlibs.go (imports : Array Lake.Module) (pkgs : Lake.OrdPackageSet) (modSet : Lake.ModuleSet) (jobs : Array (Lake.BuildJob Lake.Dynlib)) (shouldPrecompile : Bool) :
      Lake.IndexBuildM (Lake.OrdPackageSet × Lean.HashSet Lake.Module × Array (Lake.BuildJob Lake.Dynlib))
      source
      def Lake.Module.recParseImports (mod : Lake.Module) :
      Lake.IndexBuildM (Array Lake.Module)

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

      Instances For
        source
        def Lake.Module.importsFacetConfig :
        Lake.ModuleFacetConfig Lake.Module.importsFacet

        The ModuleFacetConfig for the builtin importsFacet.

        Instances For
          source
          def Lake.Module.recComputeTransImports (mod : Lake.Module) :
          Lake.IndexBuildM (Array Lake.Module)

          Recursively compute a module's transitive imports.

          Instances For
            source
            def Lake.Module.transImportsFacetConfig :
            Lake.ModuleFacetConfig Lake.Module.transImportsFacet

            The ModuleFacetConfig for the builtin transImportsFacet.

            Instances For
              source
              def Lake.Module.recComputePrecompileImports (mod : Lake.Module) :
              Lake.IndexBuildM (Array Lake.Module)

              Recursively compute a module's precompiled imports.

              Instances For
                source
                def Lake.Module.precompileImportsFacetConfig :
                Lake.ModuleFacetConfig Lake.Module.precompileImportsFacet

                The ModuleFacetConfig for the builtin precompileImportsFacet.

                Instances For
                  source
                  def Lake.Module.recBuildDeps (mod : Lake.Module) :
                  Lake.IndexBuildM (Lake.BuildJob (Lake.SearchPath × Array Lake.FilePath))

                  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
                    source
                    def Lake.Module.depsFacetConfig :
                    Lake.ModuleFacetConfig Lake.Module.depsFacet

                    The ModuleFacetConfig for the builtin depsFacet.

                    Instances For
                      source
                      def Lake.Module.recBuildLean (mod : Lake.Module) :
                      Lake.IndexBuildM (Lake.BuildJob Unit)

                      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
                        source
                        def Lake.Module.leanArtsFacetConfig :
                        Lake.ModuleFacetConfig Lake.Module.leanArtsFacet

                        The ModuleFacetConfig for the builtin leanArtsFacet.

                        Instances For
                          source
                          def Lake.Module.oleanFacetConfig :
                          Lake.ModuleFacetConfig Lake.Module.oleanFacet

                          The ModuleFacetConfig for the builtin oleanFacet.

                          Instances For
                            source
                            def Lake.Module.ileanFacetConfig :
                            Lake.ModuleFacetConfig Lake.Module.ileanFacet

                            The ModuleFacetConfig for the builtin ileanFacet.

                            Instances For
                              source
                              def Lake.Module.cFacetConfig :
                              Lake.ModuleFacetConfig Lake.Module.cFacet

                              The ModuleFacetConfig for the builtin cFacet.

                              Instances For
                                source
                                def Lake.Module.recBuildLeanO (self : Lake.Module) :
                                Lake.IndexBuildM (Lake.BuildJob Lake.FilePath)

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

                                Instances For
                                  source
                                  def Lake.Module.oFacetConfig :
                                  Lake.ModuleFacetConfig Lake.Module.oFacet

                                  The ModuleFacetConfig for the builtin oFacet.

                                  Instances For
                                    source
                                    def Lake.Module.recBuildDynlib (mod : Lake.Module) :
                                    Lake.IndexBuildM (Lake.BuildJob Lake.Dynlib)

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

                                    Instances For
                                      source
                                      def Lake.Module.dynlibFacetConfig :
                                      Lake.ModuleFacetConfig Lake.Module.dynlibFacet

                                      The ModuleFacetConfig for the builtin dynlibFacet.

                                      Instances For
                                        source
                                        def Lake.initModuleFacetConfigs :
                                        Lake.DNameMap Lake.ModuleFacetConfig

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

                                        Instances For