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 (Array 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 : 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
      • One or more equations did not get rendered due to their size.
      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
          • One or more equations did not get rendered due to their size.
          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 System.FilePath)
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lake.LeanLib.sharedFacetConfig :
                  LibraryFacetConfig sharedFacet

                  The LibraryFacetConfig for the builtin sharedFacet.

                  Equations
                  Instances For

                    Build extraDepTargets #

                    source
                    def Lake.LeanLib.recBuildExtraDepTargets (self : LeanLib) :
                    FetchM (Job 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 :
                      LibraryFacetConfig extraDepFacet

                      The LibraryFacetConfig for the builtin extraDepFacet.

                      Equations
                      Instances For
                        source
                        def Lake.initLibraryFacetConfigs :
                        DNameMap 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