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 : Lake.LeanLib) :
Lake.IndexBuildM (Array Lake.Module)

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    partial def Lake.LeanLib.recCollectLocalModules.go (self : Lake.LeanLib) (root : Lake.Module) (mods : Array Lake.Module) (modSet : Lake.ModuleSet) :
    Lake.IndexBuildM (Array Lake.Module × Lake.ModuleSet)
    source
    def Lake.LeanLib.modulesFacetConfig :
    Lake.LibraryFacetConfig Lake.LeanLib.modulesFacet

    The LibraryFacetConfig for the builtin modulesFacet.

    Equations
    Instances For
      source
      def Lake.LeanLib.recBuildLean (self : Lake.LeanLib) :
      Lake.IndexBuildM (Lake.BuildJob Unit)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lake.LeanLib.leanArtsFacetConfig :
        Lake.LibraryFacetConfig Lake.LeanLib.leanArtsFacet

        The LibraryFacetConfig for the builtin leanArtsFacet.

        Equations
        Instances For
          source
          def Lake.LeanLib.recBuildStatic (self : Lake.LeanLib) :
          Lake.IndexBuildM (Lake.BuildJob Lake.FilePath)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lake.LeanLib.staticFacetConfig :
            Lake.LibraryFacetConfig Lake.LeanLib.staticFacet

            The LibraryFacetConfig for the builtin staticFacet.

            Equations
            Instances For

              Build Shared Lib #

              source
              def Lake.LeanLib.recBuildShared (self : Lake.LeanLib) :
              Lake.IndexBuildM (Lake.BuildJob Lake.FilePath)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lake.LeanLib.sharedFacetConfig :
                Lake.LibraryFacetConfig Lake.LeanLib.sharedFacet

                The LibraryFacetConfig for the builtin sharedFacet.

                Equations
                Instances For

                  Build extraDepTargets #

                  source
                  def Lake.LeanLib.recBuildExtraDepTargets (self : Lake.LeanLib) :
                  Lake.IndexBuildM (Lake.BuildJob Unit)

                  Build the extraDepTargets for the library and its package.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lake.LeanLib.extraDepFacetConfig :
                    Lake.LibraryFacetConfig Lake.LeanLib.extraDepFacet

                    The LibraryFacetConfig for the builtin extraDepFacet.

                    Equations
                    Instances For
                      source
                      def Lake.initLibraryFacetConfigs :
                      Lake.DNameMap Lake.LibraryFacetConfig

                      A library facet name to build function map that contains builders for the initial set of Lake library facets (e.g., lean, static, and shared).

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