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
  • 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 Dynlib)
                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

                    Other #

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

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

                    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.LeanLib.recBuildDefaultFacets (self : LeanLib) :
                        FetchM (Job Unit)

                        Build the default facets for the library.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        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
                            • One or more equations did not get rendered due to their size.
                            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