Documentation

Lake.Config.LeanLib

structure Lake.LeanLib :

A Lean library -- its package plus its configuration.

Instances For
    @[inline]

    The Lean libraries of the package (as an Array).

    Equations
    Instances For
      @[inline]

      Try to find a Lean library in the package with the given name.

      Equations
      Instances For
        @[inline]

        The library's well-formed name.

        Equations
        Instances For
          @[inline]

          The package's srcDir joined with the library's srcDir.

          Equations
          Instances For
            @[inline]

            The library's root directory for lean (i.e., srcDir).

            Equations
            Instances For
              @[inline]

              The names of the library's root modules (i.e., the library's roots configuration).

              Equations
              Instances For
                @[inline]

                Whether the given module is considered local to the library.

                Equations
                Instances For
                  @[inline]

                  Whether the given module is a buildable part of the library.

                  Equations
                  Instances For
                    @[inline]

                    The file name of the library's static binary (i.e., its .a)

                    Equations
                    Instances For
                      @[inline]

                      The path to the static library in the package's libDir.

                      Equations
                      Instances For
                        @[inline]

                        The file name of the library's shared binary (i.e., its dll, dylib, or so) .

                        Equations
                        Instances For
                          @[inline]

                          The path to the shared library in the package's libDir.

                          Equations
                          Instances For
                            @[inline]

                            The library's extraDepTargets configuration.

                            Equations
                            Instances For
                              @[inline]

                              Whether to precompile the library's modules. Is true if either the package or the library have precompileModules set.

                              Equations
                              Instances For
                                @[inline]

                                The library's defaultFacets configuration.

                                Equations
                                Instances For
                                  @[inline]

                                  The library's nativeFacets configuration.

                                  Equations
                                  Instances For
                                    @[inline]

                                    The build type for modules of this library. That is, the minimum of package's buildType and the library's buildType.

                                    Equations
                                    Instances For
                                      @[inline]

                                      The arguments to pass to lean when compiling the library's Lean files. That is, the package's moreLeanArgs plus the library's moreLeanArgs.

                                      Equations
                                      Instances For
                                        @[inline]

                                        The arguments to weakly pass to lean when compiling the library's Lean files. That is, the package's weakLeanArgs plus the library's weakLeanArgs.

                                        Equations
                                        Instances For
                                          @[inline]

                                          The arguments to pass to leanc when compiling the library's Lean-produced C files. That is, the build type's leancArgs, the package's moreLeancArgs, and then the library's moreLeancArgs.

                                          Equations
                                          Instances For
                                            @[inline]

                                            The arguments to weakly pass to leanc when compiling the library's Lean-produced C files. That is, the package's weakLeancArgs plus the library's weakLeancArgs.

                                            Equations
                                            Instances For
                                              @[inline]

                                              The arguments to pass to leanc when linking the shared library. That is, the package's moreLinkArgs plus the library's moreLinkArgs.

                                              Equations
                                              Instances For
                                                @[inline]

                                                The arguments to weakly pass to leanc when linking the shared library. That is, the package's weakLinkArgs plus the library's weakLinkArgs.

                                                Equations
                                                Instances For