Documentation

Lake.Config.Package

A string descriptor of the System.Platform OS (windows, macOS, or linux).

Instances For

    A tar.gz file name suffix encoding the the current Platform. (i.e, osDescriptor joined with System.Platform.numBits).

    Instances For

      If name?, {name}-{archiveSuffix}, otherwise just archiveSuffix.

      Instances For

        First tries to convert a string into a legal name. If that fails, defaults to making it a simple name (e.g., Lean.Name.mkSimple). Currently used for package and target names taken from the CLI.

        Instances For

          Defaults #

          The default setting for a PackageConfig's manifestFile option.

          Instances For

            The default setting for a PackageConfig's buildDir option.

            Instances For

              The default setting for a PackageConfig's leanLibDir option.

              Instances For

                The default setting for a PackageConfig's nativeLibDir option.

                Instances For

                  The default setting for a PackageConfig's binDir option.

                  Instances For

                    The default setting for a PackageConfig's irDir option.

                    Instances For

                      PackageConfig #

                      • packagesDir : Lake.FilePath
                      • buildType : Lake.BuildType
                      • moreLeanArgs : Array String
                      • weakLeanArgs : Array String
                      • moreLeancArgs : Array String
                      • weakLeancArgs : Array String
                      • moreLinkArgs : Array String
                      • weakLinkArgs : Array String
                      • name : Lake.Name

                        The Name of the package.

                      • manifestFile : String

                        The path of a package's manifest file, which stores the exact versions of its resolved dependencies.

                        Defaults to defaultManifestFile (i.e., lake-manifest.json).

                      • extraDepTargets : Array Lake.Name

                        An Array of target names to build whenever the package is used.

                      • precompileModules : Bool

                        Whether to compile each of the package's module into a native shared library that is loaded whenever the module is imported. This speeds up evaluation of metaprograms and enables the interpreter to run functions marked @[extern].

                        Defaults to false.

                      • moreServerArgs : Array String

                        Additional arguments to pass to the Lean language server (i.e., lean --server) launched by lake server.

                      • srcDir : Lake.FilePath

                        The directory containing the package's Lean source files. Defaults to the package's directory.

                        (This will be passed to lean as the -R option.)

                      • buildDir : Lake.FilePath

                        The directory to which Lake should output the package's build results. Defaults to defaultBuildDir (i.e., build).

                      • leanLibDir : Lake.FilePath

                        The build subdirectory to which Lake should output the package's binary Lean libraries (e.g., .olean, .ilean files). Defaults to defaultLeanLibDir (i.e., lib).

                      • nativeLibDir : Lake.FilePath

                        The build subdirectory to which Lake should output the package's native libraries (e.g., .a, .so, .dll files). Defaults to defaultNativeLibDir (i.e., lib).

                      • binDir : Lake.FilePath

                        The build subdirectory to which Lake should output the package's binary executable. Defaults to defaultBinDir (i.e., bin).

                      • The build subdirectory to which Lake should output the package's intermediary results (e.g., .c and .o files). Defaults to defaultIrDir (i.e., ir).

                      • releaseRepo? : Option String

                        The URL of the GitHub repository to upload and download releases of this package. If none (the default), for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses gh's default.

                      • buildArchive? : Option String

                        The name of the build archive on GitHub. Defaults to none. The archive's full file name will be nameToArchive buildArchive?.

                      • preferReleaseBuild : Bool

                        Whether to prefer downloading a prebuilt release (from GitHub) rather than building this package from the source when this package is used as a dependency.

                      A Package's declarative configuration.

                      Instances For

                        Package #

                        structure Lake.Package :

                        A Lake package -- its location plus its configuration.

                        Instances For
                          @[implemented_by Lake.OpaquePackage.unsafeMk]
                          @[implemented_by Lake.OpaquePackage.unsafeGet]
                          @[inline, reducible]
                          Instances For
                            @[inline]
                            Instances For
                              @[inline, reducible]
                              Instances For
                                @[inline, reducible]

                                The package's name.

                                Instances For
                                  structure Lake.NPackage (name : Lake.Name) extends Lake.Package :

                                  A package with a name known at type-level.

                                  Instances For
                                    @[inline, reducible]

                                    The package's name.

                                    Instances For
                                      @[inline]

                                      The package's direct dependencies.

                                      Instances For
                                        @[inline]

                                        The path for storing the package's remote dependencies relative to dir (i.e., packagesDir).

                                        Instances For
                                          @[inline]

                                          The package's dir joined with its relPkgsDir

                                          Instances For
                                            @[inline]

                                            The package's JSON manifest of remote dependencies.

                                            Instances For
                                              @[inline]

                                              The package's dir joined with its buildDir configuration.

                                              Instances For
                                                @[inline]

                                                The package's extraDepTargets configuration.

                                                Instances For
                                                  @[inline]

                                                  The package's releaseRepo? configuration.

                                                  Instances For

                                                    The package's URL × tag release. Tries releaseRepo? first and then falls back to remoteUrl?.

                                                    Instances For
                                                      @[inline]

                                                      The package's buildArchive? configuration.

                                                      Instances For
                                                        @[inline]

                                                        The file name of the package's build archive derived from buildArchive?.

                                                        Instances For
                                                          @[inline]

                                                          The package's buildDir joined with its buildArchive configuration.

                                                          Instances For
                                                            @[inline]

                                                            The package's preferReleaseBuild configuration.

                                                            Instances For
                                                              @[inline]

                                                              The package's precompileModules configuration.

                                                              Instances For
                                                                @[inline]

                                                                The package's moreServerArgs configuration.

                                                                Instances For
                                                                  @[inline]

                                                                  The package's buildType configuration.

                                                                  Instances For
                                                                    @[inline]

                                                                    The package's moreLeanArgs configuration.

                                                                    Instances For
                                                                      @[inline]

                                                                      The package's weakLeanArgs configuration.

                                                                      Instances For
                                                                        @[inline]

                                                                        The package's moreLeancArgs configuration.

                                                                        Instances For
                                                                          @[inline]

                                                                          The package's weakLeancArgs configuration.

                                                                          Instances For
                                                                            @[inline]

                                                                            The package's moreLinkArgs configuration.

                                                                            Instances For
                                                                              @[inline]

                                                                              The package's weakLinkArgs configuration.

                                                                              Instances For
                                                                                @[inline]

                                                                                The package's dir joined with its srcDir configuration.

                                                                                Instances For
                                                                                  @[inline]

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

                                                                                  Instances For
                                                                                    @[inline]

                                                                                    The package's buildDir joined with its leanLibDir configuration.

                                                                                    Instances For
                                                                                      @[inline]

                                                                                      The package's buildDir joined with its nativeLibDir configuration.

                                                                                      Instances For
                                                                                        @[inline]

                                                                                        The package's buildDir joined with its binDir configuration.

                                                                                        Instances For
                                                                                          @[inline]

                                                                                          The package's buildDir joined with its irDir configuration.

                                                                                          Instances For

                                                                                            Whether the given module is considered local to the package.

                                                                                            Instances For

                                                                                              Whether the given module is in the package (i.e., can build it).

                                                                                              Instances For

                                                                                                Remove the package's build outputs (i.e., delete its build directory).

                                                                                                Instances For