Documentation

Lake.Build.Module

Module Facet Builds #

Build function definitions for a module's builtin facets.

source
def Lake.Module.buildUnlessUpToDate (mod : Lake.Module) (dynlibPath : Lake.SearchPath) (dynlibs : Array Lake.FilePath) (depTrace : Lake.BuildTrace) :
Lake.BuildM PUnit
Instances For
    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 transitive local imports and shared library dependencies.

                    Instances For
                      source
                      def Lake.Module.depsFacetConfig :
                      Lake.ModuleFacetConfig Lake.Module.depsFacet

                      The ModuleFacetConfig for the builtin depsFacet.

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

                        Recursively build a module and its dependencies.

                        Instances For
                          source
                          def Lake.Module.leanBinFacetConfig :
                          Lake.ModuleFacetConfig Lake.Module.leanBinFacet

                          The ModuleFacetConfig for the builtin leanBinFacet.

                          Instances For
                            source
                            def Lake.Module.importBinFacetConfig :
                            Lake.ModuleFacetConfig Lake.Module.importBinFacet

                            The ModuleFacetConfig for the builtin importBinFacet.

                            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