Documentation

Lake.Config.Package

@[inline]

The default buildArchive configuration for a package with name.

Equations
Instances For
    inductive Lake.StrPat :

    A String pattern. Matches some subset of strings.

    Instances For

      Matches nothing.

      Equations
      Instances For

        Whether a string is "version-like". That is, a v followed by a digit.

        Equations
        Instances For

          Matches a "version-like" string: a v followed by a digit.

          Equations
          Instances For

            Default string pattern for a Package's versionTags.

            Equations
            Instances For

              Builtin StrPat presets available to TOML for versionTags.

              Equations
              Instances For

                Returns whether the string s matches the pattern.

                Equations
                Instances For

                  PackageConfig #

                  A Package's declarative configuration.

                  • packagesDir : Lake.FilePath
                  • buildType : Lake.BuildType
                  • leanOptions : Array Lake.LeanOption
                  • moreLeanArgs : Array String
                  • weakLeanArgs : Array String
                  • moreLeancArgs : Array String
                  • moreServerOptions : Array Lake.LeanOption
                  • weakLeancArgs : Array String
                  • moreLinkArgs : Array String
                  • weakLinkArgs : Array String
                  • backend : Lake.Backend
                  • platformIndependent : Option Bool
                  • name : Lake.Name

                    The Name of the package.

                  • manifestFile : Option Lake.FilePath

                    This field is deprecated.

                    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

                    Deprecated in favor of moreGlobalServerArgs. Additional arguments to pass to the Lean language server (i.e., lean --server) launched by lake serve, both for this package and also for any packages browsed from this one in the same session.

                  • moreGlobalServerArgs : Array String

                    Additional arguments to pass to the Lean language server (i.e., lean --server) launched by lake serve, both for this package and also for any packages browsed from this one in the same session.

                  • 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., .lake/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.

                  • 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

                    A custom name for the build archive for the GitHub cloud release. If none (the default), Lake uses buildArchive, which defaults to {(pkg-)name}-{System.Platform.target}.tar.gz.

                  • buildArchive : String

                    A custom name for the build archive for the GitHub cloud release. Defaults to {(pkg-)name}-{System.Platform.target}.tar.gz.

                  • 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.

                  • testDriver : String

                    The name of the script, executable, or library by lake test when this package is the workspace root. To point to a definition in another package, use the syntax <pkg>/<def>.

                    A script driver will be run by lake test with the arguments configured in testDriverArgs followed by any specified on the CLI (e.g., via lake lint -- <args>...). An executable driver will be built and then run like a script. A library will just be built.

                  • testDriverArgs : Array String

                    Arguments to pass to the package's test driver. These arguments will come before those passed on the command line via lake test -- <args>....

                  • lintDriver : String

                    The name of the script or executable used by lake lint when this package is the workspace root. To point to a definition in another package, use the syntax <pkg>/<def>.

                    A script driver will be run by lake lint with the arguments configured in lintDriverArgs followed by any specified on the CLI (e.g., via lake lint -- <args>...). An executable driver will be built and then run like a script.

                  • lintDriverArgs : Array String

                    Arguments to pass to the package's linter. These arguments will come before those passed on the command line via lake lint -- <args>....

                  • version : Lake.StdVer

                    The package version. Versions have the form:

                    v!"<major>.<minor>.<patch>[-<specialDescr>]"
                    

                    A version with a - suffix is considered a "prerelease".

                    Lake suggest the following guidelines for incrementing versions:

                    • Major version increment (e.g., v1.3.0 → v2.0.0) Indicates significant breaking changes in the package. Package users are not expected to update to the new version without manual intervention.

                    • Minor version increment (e.g., v1.3.0 → v1.4.0) Denotes notable changes that are expected to be generally backwards compatible. Package users are expected to update to this version automatically and should be able to fix any breakages and/or warnings easily.

                    • Patch version increment (e.g., v1.3.0 → v1.3.1) Reserved for bug fixes and small touchups. Package users are expected to update automatically and should not expect significant breakage, except in the edge case of users relying on the behavior of patched bugs.

                    Note that backwards-incompatible changes may occur at any version increment. The is because the current nature of Lean (e.g., transitive imports, rich metaprogramming, reducibility in proofs), makes it infeasible to define a completely stable interface for a package. Instead, the different version levels indicate a change's intended significance and how difficult migration is expected to be.

                    Versions of form the 0.x.x are considered development versions prior to first official release. Like prerelease, they are not expected to closely follow the above guidelines.

                    Packages without a defined version default to 0.0.0.

                  • versionTags : Lake.StrPat

                    Git tags of this package's repository that should be treated as versions. Package indices (e.g., Reservoir) can make use of this information to determine the Git revisions corresponding to released versions.

                    Defaults to tags that are "version-like". That is, start with a v followed by a digit.

                  • description : String

                    A short description for the package (e.g., for Reservoir).

                  • keywords : Array String

                    Custom keywords associated with the package. Reservoir can make use of a package's keywords to group related packages together and make it easier for users to discover them.

                    Good keywords include the domain (e.g., math, software-verification, devtool), specific subtopics (e.g., topology, cryptology), and significant implementation details (e.g., dsl, ffi, cli). For instance, Lake's keywords could be devtool, cli, dsl, package-manager, and build-system.

                  • homepage : String

                    A URL to information about the package.

                    Reservoir will already include a link to the package's GitHub repository (if the package is sourced from there). Thus, users are advised to specify something else for this (if anything).

                  • license : String

                    The package's license (if one). Should be a valid SPDX License Expression.

                    Reservoir requires that packages uses an OSI-approved license to be included in its index, and currently only supports single identifier SPDX expressions. For, a list of OSI-approved SPDX license identifiers, see the SPDX LIcense List.

                  • licenseFiles : Array Lake.FilePath

                    Files containing licensing information for the package.

                    These should be the license files that users are expected to include when distributing package sources, which may be more then one file for some licenses. For example, the Apache 2.0 license requires the reproduction of a NOTICE file along with the license (if such a file exists).

                    Defaults to #["LICENSE"].

                  • readmeFile : Lake.FilePath

                    The path to the package's README.

                    A README should be a Markdown file containing an overview of the package. Reservoir displays the rendered HTML of this file on a package's page. A nonstandard location can be used to provide a different README for Reservoir and GitHub.

                    Defaults to README.md.

                  • reservoir : Bool

                    Whether Reservoir should include the package in its index. When set to false, Reservoir will not add the package to its index and will remove it if it was already there (when Reservoir is next updated).

                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.

                    Package #

                    structure Lake.Package :

                    A Lake package -- its location plus its configuration.

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

                              The package's name.

                              Equations
                              • self.name = self.config.name
                              Instances For
                                structure Lake.NPackage (name : Lake.Name) extends Lake.Package :

                                A package with a name known at type-level.

                                Instances For
                                  @[simp]
                                  theorem Lake.NPackage.name_eq {name : Lake.Name} (self : Lake.NPackage name) :
                                  self.name = name
                                  Equations
                                  • Lake.instCoeOutNPackagePackage = { coe := Lake.NPackage.toPackage }
                                  Equations
                                  • Lake.instCoeDepPackageNPackageName = { coe := { toPackage := pkg, name_eq := } }
                                  @[reducible, inline]

                                  The package's name.

                                  Equations
                                  • x.name = n
                                  Instances For
                                    @[reducible, inline]
                                    abbrev Lake.PostUpdateFn (pkgName : Lake.Name) :

                                    The type of a post-update hooks monad. IO equipped with logging ability and information about the Lake configuration.

                                    Equations
                                    Instances For
                                      structure Lake.PostUpdateHook (pkgName : Lake.Name) :
                                      Instances For
                                        Equations
                                        • Lake.instInhabitedPostUpdateHook = { default := { fn := default } }
                                        Equations
                                        Equations
                                        • Lake.OpaquePostUpdateHook.instCoePostUpdateHook_1 = { coe := Lake.OpaquePostUpdateHook.get }
                                        Equations
                                        • Lake.OpaquePostUpdateHook.instCoePostUpdateHook = { coe := Lake.OpaquePostUpdateHook.mk }
                                        @[implemented_by Lake.OpaquePostUpdateHook.unsafeGet]
                                        @[implemented_by Lake.OpaquePostUpdateHook.unsafeMk]
                                        Instances For
                                          @[inline]

                                          The package version.

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

                                            The package's versionTags configuration.

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

                                              The package's description configuration.

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

                                                The package's keywords configuration.

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

                                                  The package's homepage configuration.

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

                                                    The package's reservoir configuration.

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

                                                      The package's license configuration.

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

                                                        The package's licenseFiles configuration.

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

                                                          The package's dir joined with each of its relLicenseFiles.

                                                          Equations
                                                          Instances For
                                                            @[inline]

                                                            The package's readmeFile configuration.

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

                                                              The package's dir joined with its relReadmeFile.

                                                              Equations
                                                              • self.readmeFile = self.dir / self.config.readmeFile
                                                              Instances For
                                                                @[inline]

                                                                The package's direct dependencies.

                                                                Equations
                                                                Instances For
                                                                  @[inline]

                                                                  The path to the package's Lake directory relative to dir (e.g., .lake).

                                                                  Equations
                                                                  Instances For
                                                                    @[inline]

                                                                    The full path to the package's Lake directory (i.e, dir joined with relLakeDir).

                                                                    Equations
                                                                    • self.lakeDir = self.dir / self.relLakeDir
                                                                    Instances For
                                                                      @[inline]

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

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

                                                                        The package's dir joined with its relPkgsDir.

                                                                        Equations
                                                                        • self.pkgsDir = self.dir / self.relPkgsDir
                                                                        Instances For
                                                                          @[inline]

                                                                          The full path to the package's configuration file.

                                                                          Equations
                                                                          • self.configFile = self.dir / self.relConfigFile
                                                                          Instances For
                                                                            @[inline]

                                                                            The path to the package's JSON manifest of remote dependencies.

                                                                            Equations
                                                                            • self.manifestFile = self.dir / self.relManifestFile
                                                                            Instances For
                                                                              @[inline]

                                                                              The package's dir joined with its buildDir configuration.

                                                                              Equations
                                                                              • self.buildDir = self.dir / self.config.buildDir
                                                                              Instances For
                                                                                @[inline]

                                                                                The package's testDriverArgs configuration.

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

                                                                                  The package's lintDriverArgs configuration.

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

                                                                                    The package's extraDepTargets configuration.

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

                                                                                      The package's platformIndependent configuration.

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

                                                                                        The package's releaseRepo/releaseRepo? configuration.

                                                                                        Equations
                                                                                        • self.releaseRepo? = HOrElse.hOrElse self.config.releaseRepo fun (x : Unit) => self.config.releaseRepo?
                                                                                        Instances For
                                                                                          @[inline]

                                                                                          The packages remoteUrl as an Option (none if empty).

                                                                                          Equations
                                                                                          • self.remoteUrl? = if self.remoteUrl.isEmpty = true then some self.remoteUrl else none
                                                                                          Instances For
                                                                                            @[inline]

                                                                                            The package's buildArchive/buildArchive? configuration.

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

                                                                                              The package's lakeDir joined with its buildArchive.

                                                                                              Equations
                                                                                              • self.buildArchiveFile = self.lakeDir / { toString := self.buildArchive }
                                                                                              Instances For
                                                                                                @[inline]

                                                                                                The path where Lake stores the package's barrel (downloaded from Reservoir).

                                                                                                Equations
                                                                                                • self.barrelFile = self.lakeDir / { toString := "build.barrel" }
                                                                                                Instances For
                                                                                                  @[inline]

                                                                                                  The package's preferReleaseBuild configuration.

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

                                                                                                    The package's precompileModules configuration.

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

                                                                                                      The package's moreGlobalServerArgs configuration.

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

                                                                                                        The package's moreServerOptions configuration appended to its leanOptions configuration.

                                                                                                        Equations
                                                                                                        • self.moreServerOptions = self.config.leanOptions ++ self.config.moreServerOptions
                                                                                                        Instances For
                                                                                                          @[inline]

                                                                                                          The package's buildType configuration.

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

                                                                                                            The package's backend configuration.

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

                                                                                                              The package's leanOptions configuration.

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

                                                                                                                The package's moreLeanArgs configuration appended to its leanOptions configuration.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline]

                                                                                                                  The package's weakLeanArgs configuration.

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

                                                                                                                    The package's moreLeancArgs configuration.

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

                                                                                                                      The package's weakLeancArgs configuration.

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

                                                                                                                        The package's moreLinkArgs configuration.

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

                                                                                                                          The package's weakLinkArgs configuration.

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

                                                                                                                            The package's dir joined with its srcDir configuration.

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

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

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

                                                                                                                                The package's buildDir joined with its leanLibDir configuration.

                                                                                                                                Equations
                                                                                                                                • self.leanLibDir = self.buildDir / self.config.leanLibDir
                                                                                                                                Instances For
                                                                                                                                  @[inline]

                                                                                                                                  The package's buildDir joined with its nativeLibDir configuration.

                                                                                                                                  Equations
                                                                                                                                  • self.nativeLibDir = self.buildDir / self.config.nativeLibDir
                                                                                                                                  Instances For
                                                                                                                                    @[inline]

                                                                                                                                    The package's buildDir joined with its binDir configuration.

                                                                                                                                    Equations
                                                                                                                                    • self.binDir = self.buildDir / self.config.binDir
                                                                                                                                    Instances For
                                                                                                                                      @[inline]

                                                                                                                                      The package's buildDir joined with its irDir configuration.

                                                                                                                                      Equations
                                                                                                                                      • self.irDir = self.buildDir / self.config.irDir
                                                                                                                                      Instances For

                                                                                                                                        Whether the given module is considered local to the package.

                                                                                                                                        Equations
                                                                                                                                        Instances For

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

                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For

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

                                                                                                                                            Equations
                                                                                                                                            Instances For