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.

Equations
    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.sharedFacetConfig :
              LibraryFacetConfig sharedFacet

              The LibraryFacetConfig for the builtin sharedFacet.

              Equations
                Instances For

                  Other #

                  source
                  def Lake.LeanLib.extraDepFacetConfig :
                  LibraryFacetConfig extraDepFacet

                  The LibraryFacetConfig for the builtin extraDepFacet.

                  Equations
                    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
                            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