Documentation

Lake.Build.Library

Library Facet Builds #

Build function definitions for a library's builtin facets.

Build Lean & Static Lib #

source
def Lake.LeanLib.recCollectLocalModules (self : LeanLib) :
FetchM (Job (Array Module))

Collect the local modules of a library. That is, the modules from getModuleArray plus their local transitive imports.

Equations
    Instances For
      source
      partial def Lake.LeanLib.recCollectLocalModules.go (self : LeanLib) (root : Module) (mods : Array Module) (modSet : ModuleSet) :
      FetchM (Array Module × ModuleSet)
      source
      def Lake.LeanLib.modulesFacetConfig :
      LibraryFacetConfig modulesFacet

      The LibraryFacetConfig for the builtin modulesFacet.

      Equations
        Instances For
          source
          def Lake.LeanLib.recBuildLean (self : LeanLib) :
          FetchM (Job Unit)
          Equations
            Instances For
              source
              def Lake.LeanLib.leanArtsFacetConfig :
              LibraryFacetConfig leanArtsFacet

              The LibraryFacetConfig for the builtin leanArtsFacet.

              Equations
                Instances For
                  source
                  @[specialize #[]]
                  def Lake.LeanLib.recBuildStatic (self : LeanLib) (shouldExport : Bool) :
                  FetchM (Job System.FilePath)
                  Equations
                    Instances For
                      source
                      def Lake.LeanLib.staticFacetConfig :
                      LibraryFacetConfig staticFacet

                      The LibraryFacetConfig for the builtin staticFacet.

                      Equations
                        Instances For
                          source
                          def Lake.LeanLib.staticExportFacetConfig :
                          LibraryFacetConfig staticExportFacet

                          The LibraryFacetConfig for the builtin staticExportFacet.

                          Equations
                            Instances For

                              Build Shared Lib #

                              source
                              def Lake.LeanLib.recBuildShared (self : LeanLib) :
                              FetchM (Job Dynlib)
                              Equations
                                Instances For
                                  source
                                  def Lake.LeanLib.sharedFacetConfig :
                                  LibraryFacetConfig sharedFacet

                                  The LibraryFacetConfig for the builtin sharedFacet.

                                  Equations
                                    Instances For

                                      Other #

                                      source
                                      def Lake.LeanLib.recBuildExtraDepTargets (self : LeanLib) :
                                      FetchM (Job Unit)

                                      Build extra target dependencies of the library (e.g., extraDepTargets, needs).

                                      Equations
                                        Instances For
                                          source
                                          def Lake.LeanLib.extraDepFacetConfig :
                                          LibraryFacetConfig extraDepFacet

                                          The LibraryFacetConfig for the builtin extraDepFacet.

                                          Equations
                                            Instances For
                                              source
                                              def Lake.LeanLib.recBuildDefaultFacets (self : LeanLib) :
                                              FetchM (Job Unit)

                                              Build the default facets for the library.

                                              Equations
                                                Instances For
                                                  source
                                                  def Lake.LeanLib.defaultFacetConfig :
                                                  LibraryFacetConfig defaultFacet

                                                  The LibraryFacetConfig for the builtin defaultFacet.

                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lake.LeanLib.initFacetConfigs :
                                                      DNameMap LeanLibFacetConfig

                                                      A name-configuration map for the initial set of Lean library facets (e.g., lean, static, shared).

                                                      Equations
                                                        Instances For
                                                          source
                                                          @[reducible, inline]
                                                          abbrev Lake.initLibraryFacetConfigs :
                                                          DNameMap LibraryFacetConfig

                                                          A name-configuration map for the initial set of Lean library facets (e.g., lean, static, shared).

                                                          Equations
                                                            Instances For