Documentation

Lake.Build.Library

Library Facet Builds #

Build function definitions for a library's builtin facets.

Build Lean & Static Lib #

source
def Lake.LeanLib.leanArtsFacetConfig :
LibraryFacetConfig leanArtsFacet

The LibraryFacetConfig for the builtin leanArtsFacet.

Instances For
    source
    def Lake.LeanLib.staticFacetConfig :
    LibraryFacetConfig staticFacet

    The LibraryFacetConfig for the builtin staticFacet.

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

      The LibraryFacetConfig for the builtin staticExportFacet.

      Instances For

        Build Shared Lib #

        source
        def Lake.LeanLib.sharedFacetConfig :
        LibraryFacetConfig sharedFacet

        The LibraryFacetConfig for the builtin sharedFacet.

        Instances For

          Other #

          source
          def Lake.LeanLib.extraDepFacetConfig :
          LibraryFacetConfig extraDepFacet

          The LibraryFacetConfig for the builtin extraDepFacet.

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

            The LibraryFacetConfig for the builtin defaultFacet.

            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).

              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).

                Instances For