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]

                                Whether to the library's Lean code is platform-independent. Returns the library's platformIndependent configuration if non-none. Otherwise, falls back to the package's.

                                Equations
                                Instances For
                                  @[inline]

                                  The library's defaultFacets configuration.

                                  Equations
                                  Instances For
                                    @[inline]

                                    The library's nativeFacets configuration.

                                    Equations
                                    Instances For
                                      @[inline]

                                      The arguments to pass to lean --server when running the Lean language server. serverOptions is the the accumulation of:

                                      • the package's leanOptions
                                      • the package's moreServerOptions
                                      • the library's leanOptions
                                      • the library's moreServerOptions
                                      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 backend type for modules of this library. Prefer the library's backend configuration, then the package's, then the default (which is C for now).

                                          Equations
                                          Instances For
                                            @[inline]

                                            The arguments to pass to lean when compiling the library's Lean files. leanArgs is the accumulation of:

                                            • the package's leanOptions
                                            • the package's moreLeanArgs
                                            • the library's leanOptions
                                            • the library's moreLeanArgs
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            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