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
        • self.name = self.config.name
        Instances For
          @[inline]

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

          Equations
          • self.srcDir = self.pkg.srcDir / self.config.srcDir
          Instances For
            @[inline]

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

            Equations
            • self.rootDir = self.srcDir
            Instances For
              @[inline]

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

              Equations
              • self.roots = self.config.roots
              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
                      • self.staticLibFile = self.pkg.nativeLibDir / self.staticLibFileName
                      Instances For
                        @[inline]

                        The path to the static library (with exported symbols) in the package's libDir.

                        Equations
                        • self.staticExportLibFile = self.pkg.nativeLibDir / self.staticLibFileName.addExtension "export"
                        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
                            • self.sharedLibFile = self.pkg.nativeLibDir / self.sharedLibFileName
                            Instances For
                              @[inline]

                              The library's extraDepTargets configuration.

                              Equations
                              • self.extraDepTargets = self.config.extraDepTargets
                              Instances For
                                @[inline]

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

                                Equations
                                • self.precompileModules = (self.pkg.precompileModules || self.config.precompileModules)
                                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
                                  • self.platformIndependent = HOrElse.hOrElse self.config.platformIndependent fun (x : Unit) => self.pkg.platformIndependent
                                  Instances For
                                    @[inline]

                                    The library's defaultFacets configuration.

                                    Equations
                                    • self.defaultFacets = self.config.defaultFacets
                                    Instances For
                                      @[inline]

                                      The library's nativeFacets configuration.

                                      Equations
                                      • self.nativeFacets shouldExport = self.config.nativeFacets shouldExport
                                      Instances For
                                        @[inline]

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

                                        • the package's leanOptions
                                        • the package's moreServerOptions
                                        • the library's leanOptions
                                        • the library's moreServerOptions
                                        Equations
                                        • self.serverOptions = self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions
                                        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
                                          • self.buildType = min self.pkg.buildType self.config.buildType
                                          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
                                            • self.backend = self.config.backend.orPreferLeft self.pkg.backend
                                            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
                                              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
                                                • self.weakLeanArgs = self.pkg.weakLeanArgs ++ self.config.weakLeanArgs
                                                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
                                                  • self.leancArgs = self.buildType.leancArgs ++ self.pkg.moreLeancArgs ++ self.config.moreLeancArgs
                                                  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
                                                    • self.weakLeancArgs = self.pkg.weakLeancArgs ++ self.config.weakLeancArgs
                                                    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
                                                      • self.linkArgs = self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
                                                      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
                                                        • self.weakLinkArgs = self.pkg.weakLinkArgs ++ self.config.weakLinkArgs
                                                        Instances For