HepLean 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.FetchM (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.FetchM (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.FetchM (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
          @[specialize #[]]
          def Lake.LeanLib.recBuildStatic (self : Lake.LeanLib) (shouldExport : Bool) :
          Lake.FetchM (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
              source
              def Lake.LeanLib.staticExportFacetConfig :
              Lake.LibraryFacetConfig Lake.LeanLib.staticExportFacet

              The LibraryFacetConfig for the builtin staticExportFacet.

              Equations
              Instances For

                Build Shared Lib #

                source
                def Lake.LeanLib.recBuildShared (self : Lake.LeanLib) :
                Lake.FetchM (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.FetchM (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