@[inline]

def Lake.defaultBuildArchive (name : Lean.Name) : String

The default buildArchive configuration for a package with name.

Equations

• Lake.defaultBuildArchive name = toString "" ++ toString (name.toString false) ++ toString "-" ++ toString System.Platform.target ++ toString ".tar.gz"

PackageConfig

structure Lake.PackageConfig (name : Lean.Name) extends Lake.WorkspaceConfig, Lake.LeanConfig : Type

A Package's declarative configuration.

• packagesDir : System.FilePath
• buildType : BuildType
• leanOptions : Array LeanOption
• moreLeanArgs : Array String
• weakLeanArgs : Array String
• moreLeancArgs : Array String
• moreServerOptions : Array LeanOption
• weakLeancArgs : Array String
• moreLinkObjs : TargetArray System.FilePath
• moreLinkLibs : TargetArray Dynlib
• moreLinkArgs : Array String
• weakLinkArgs : Array String
• backend : Backend
• platformIndependent : Option Bool
• dynlibs : TargetArray Dynlib
• plugins : TargetArray Dynlib
• bootstrap : Bool

  For internal use. Whether this package is Lean itself.

• manifestFile : Option System.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 Lean.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.

• 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 : System.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 : System.FilePath

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

• leanLibDir : System.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 : System.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 : System.FilePath

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

• irDir : System.FilePath

  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

  A custom name for the build archive for the GitHub cloud release. If none (the default), Lake 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 : 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 : 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 System.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 : System.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).

• enableArtifactCache? : Option Bool

  Whether to enables Lake's local, offline artifact cache for the package.

  Artifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain. This can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.

  As a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.

  If none (the default), the cache will be disabled by default unless the LAKE_ARTIFACT_CACHE environment variable is set to true.

• libPrefixOnWindows : Bool

  Whether native libraries (of this package) should be prefixed with lib on Windows.

  Unlike Unix, Windows does not require native libraries to start with lib and, by convention, they usually do not. However, for consistent naming across all platforms, users may wish to enable this.

  Defaults to false.

instance Lake.PackageConfig.lintDriverArgs.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `lintDriverArgs (Array String)

Equations

• Lake.PackageConfig.lintDriverArgs.instConfigField = { toConfigProj := Lake.PackageConfig.lintDriverArgs._proj }

instance Lake.PackageConfig.lintDriver.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `lintDriver String

Equations

• Lake.PackageConfig.lintDriver.instConfigField = { toConfigProj := Lake.PackageConfig.lintDriver._proj }

instance Lake.PackageConfig.keywords.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `keywords (Array String)

Equations

• Lake.PackageConfig.keywords.instConfigField = { toConfigProj := Lake.PackageConfig.keywords._proj }

instance Lake.PackageConfig.buildDir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `buildDir System.FilePath

Equations

• Lake.PackageConfig.buildDir.instConfigField = { toConfigProj := Lake.PackageConfig.buildDir._proj }

instance Lake.PackageConfig.nativeLibDir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `nativeLibDir System.FilePath

Equations

• Lake.PackageConfig.nativeLibDir.instConfigField = { toConfigProj := Lake.PackageConfig.nativeLibDir._proj }

instance Lake.PackageConfig.version.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `version StdVer

Equations

• Lake.PackageConfig.version.instConfigField = { toConfigProj := Lake.PackageConfig.version._proj }

instance Lake.PackageConfig.extraDepTargets.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `extraDepTargets (Array Lean.Name)

Equations

• Lake.PackageConfig.extraDepTargets.instConfigField = { toConfigProj := Lake.PackageConfig.extraDepTargets._proj }

instance Lake.PackageConfig.enableArtifactCache?.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `enableArtifactCache? (Option Bool)

Equations

• Lake.PackageConfig.enableArtifactCache?.instConfigField = { toConfigProj := Lake.PackageConfig.enableArtifactCache?._proj }

instance Lake.PackageConfig.testDriverArgs.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `testDriverArgs (Array String)

Equations

• Lake.PackageConfig.testDriverArgs.instConfigField = { toConfigProj := Lake.PackageConfig.testDriverArgs._proj }

instance Lake.PackageConfig.srcDir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `srcDir System.FilePath

Equations

• Lake.PackageConfig.srcDir.instConfigField = { toConfigProj := Lake.PackageConfig.srcDir._proj }

instance Lake.PackageConfig.buildArchive.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `buildArchive (Option String)

Equations

• Lake.PackageConfig.buildArchive.instConfigField = { toConfigProj := Lake.PackageConfig.buildArchive._proj }

instance Lake.PackageConfig.toLeanConfig.instConfigParent {name : Lean.Name} : ConfigParent (PackageConfig name) LeanConfig

Equations

• Lake.PackageConfig.toLeanConfig.instConfigParent = { toConfigProj := Lake.PackageConfig.toLeanConfig._proj }

instance Lake.PackageConfig.preferReleaseBuild.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `preferReleaseBuild Bool

Equations

• Lake.PackageConfig.preferReleaseBuild.instConfigField = { toConfigProj := Lake.PackageConfig.preferReleaseBuild._proj }

instance Lake.PackageConfig.versionTags.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `versionTags StrPat

Equations

• Lake.PackageConfig.versionTags.instConfigField = { toConfigProj := Lake.PackageConfig.versionTags._proj }

instance Lake.PackageConfig.license.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `license String

Equations

• Lake.PackageConfig.license.instConfigField = { toConfigProj := Lake.PackageConfig.license._proj }

instance Lake.PackageConfig.releaseRepo?.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `releaseRepo? (Option String)

Equations

• Lake.PackageConfig.releaseRepo?.instConfigField = { toConfigProj := Lake.PackageConfig.releaseRepo._proj }

instance Lake.PackageConfig.releaseRepo.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `releaseRepo (Option String)

Equations

• Lake.PackageConfig.releaseRepo.instConfigField = { toConfigProj := Lake.PackageConfig.releaseRepo._proj }

instance Lake.PackageConfig.irDir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `irDir System.FilePath

Equations

• Lake.PackageConfig.irDir.instConfigField = { toConfigProj := Lake.PackageConfig.irDir._proj }

instance Lake.PackageConfig.readmeFile.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `readmeFile System.FilePath

Equations

• Lake.PackageConfig.readmeFile.instConfigField = { toConfigProj := Lake.PackageConfig.readmeFile._proj }

instance Lake.PackageConfig.homepage.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `homepage String

Equations

• Lake.PackageConfig.homepage.instConfigField = { toConfigProj := Lake.PackageConfig.homepage._proj }

instance Lake.PackageConfig.licenseFiles.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `licenseFiles (Array System.FilePath)

Equations

• Lake.PackageConfig.licenseFiles.instConfigField = { toConfigProj := Lake.PackageConfig.licenseFiles._proj }

instance Lake.PackageConfig.enableArtifactCache.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `enableArtifactCache (Option Bool)

Equations

• Lake.PackageConfig.enableArtifactCache.instConfigField = { toConfigProj := Lake.PackageConfig.enableArtifactCache?._proj }

instance Lake.PackageConfig.description.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `description String

Equations

• Lake.PackageConfig.description.instConfigField = { toConfigProj := Lake.PackageConfig.description._proj }

instance Lake.PackageConfig.binDir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `binDir System.FilePath

Equations

• Lake.PackageConfig.binDir.instConfigField = { toConfigProj := Lake.PackageConfig.binDir._proj }

instance Lake.PackageConfig.buildArchive?.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `buildArchive? (Option String)

Equations

• Lake.PackageConfig.buildArchive?.instConfigField = { toConfigProj := Lake.PackageConfig.buildArchive._proj }

instance Lake.PackageConfig.reservoir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `reservoir Bool

Equations

• Lake.PackageConfig.reservoir.instConfigField = { toConfigProj := Lake.PackageConfig.reservoir._proj }

instance Lake.PackageConfig.manifestFile.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `manifestFile (Option System.FilePath)

Equations

• Lake.PackageConfig.manifestFile.instConfigField = { toConfigProj := Lake.PackageConfig.manifestFile._proj }

instance Lake.PackageConfig.instConfigMeta : ConfigInfo `Lake.PackageConfig

Equations

• Lake.PackageConfig.instConfigMeta = { fields := Lake.PackageConfig._fields }

instance Lake.PackageConfig.bootstrap.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `bootstrap Bool

Equations

• Lake.PackageConfig.bootstrap.instConfigField = { toConfigProj := Lake.PackageConfig.bootstrap._proj }

instance Lake.PackageConfig.precompileModules.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `precompileModules Bool

Equations

• Lake.PackageConfig.precompileModules.instConfigField = { toConfigProj := Lake.PackageConfig.precompileModules._proj }

instance Lake.PackageConfig.testDriver.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `testDriver String

Equations

• Lake.PackageConfig.testDriver.instConfigField = { toConfigProj := Lake.PackageConfig.testDriver._proj }

instance Lake.PackageConfig.moreGlobalServerArgs.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `moreGlobalServerArgs (Array String)

Equations

• Lake.PackageConfig.moreGlobalServerArgs.instConfigField = { toConfigProj := Lake.PackageConfig.moreGlobalServerArgs._proj }

instance Lake.PackageConfig.toWorkspaceConfig.instConfigParent {name : Lean.Name} : ConfigParent (PackageConfig name) WorkspaceConfig

Equations

• Lake.PackageConfig.toWorkspaceConfig.instConfigParent = { toConfigProj := Lake.PackageConfig.toWorkspaceConfig._proj }

instance Lake.PackageConfig.libPrefixOnWindows.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `libPrefixOnWindows Bool

Equations

• Lake.PackageConfig.libPrefixOnWindows.instConfigField = { toConfigProj := Lake.PackageConfig.libPrefixOnWindows._proj }

instance Lake.PackageConfig.moreServerArgs.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `moreServerArgs (Array String)

Equations

• Lake.PackageConfig.moreServerArgs.instConfigField = { toConfigProj := Lake.PackageConfig.moreGlobalServerArgs._proj }

instance Lake.PackageConfig.leanLibDir.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `leanLibDir System.FilePath

Equations

• Lake.PackageConfig.leanLibDir.instConfigField = { toConfigProj := Lake.PackageConfig.leanLibDir._proj }

instance Lake.PackageConfig.testRunner.instConfigField {name : Lean.Name} : ConfigField (PackageConfig name) `testRunner String

Equations

• Lake.PackageConfig.testRunner.instConfigField = { toConfigProj := Lake.PackageConfig.testDriver._proj }

instance Lake.PackageConfig.instConfigFields {name : Lean.Name} : ConfigFields (PackageConfig name)

Equations

• Lake.PackageConfig.instConfigFields = { fields := Lake.PackageConfig._fields }

instance Lake.instInhabitedPackageConfig {a✝ : Lean.Name} : Inhabited (PackageConfig a✝)

Equations

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

instance Lake.instEmptyCollectionPackageConfig {n : Lean.Name} : EmptyCollection (PackageConfig n)

Equations

• Lake.instEmptyCollectionPackageConfig = { emptyCollection := { } }

@[reducible, inline]

abbrev Lake.PackageConfig.name {n : Lean.Name} : PackageConfig n → Lean.Name

The package's name.

Equations

• x✝.name = n

structure Lake.PackageDecl : Type

A package declaration from a configuration written in Lean.

• name : Lean.Name
• config : PackageConfig self.name

instance Lake.instTypeNamePackageDecl : TypeName PackageDecl

Equations

• Lake.instTypeNamePackageDecl = Lake.inst✝

Package

opaque Lake.OpaquePostUpdateHook.nonemptyType (pkg : Lean.Name) : NonemptyType

instance Lake.instNonemptyOpaquePostUpdateHook {pkg : Lean.Name} : Nonempty (OpaquePostUpdateHook pkg)

def Lake.OpaquePostUpdateHook (pkg : Lean.Name) : Type

Equations

• Lake.OpaquePostUpdateHook pkg = (Lake.OpaquePostUpdateHook.nonemptyType pkg).type

structure Lake.Package : Type

A Lake package -- its location plus its configuration.

• name : Lean.Name

  The name of the package.

• dir : System.FilePath

  The absolute path to the package's directory.

• relDir : System.FilePath

  The path to the package's directory relative to the workspace.

• config : PackageConfig self.name

  The package's user-defined configuration.

• configFile : System.FilePath

  The absolute path to the package's configuration file.

• relConfigFile : System.FilePath

  The path to the package's configuration file (relative to dir).

• relManifestFile : System.FilePath

  The path to the package's JSON manifest of remote dependencies (relative to dir).

• scope : String

  The package's scope (e.g., in Reservoir).

• remoteUrl : String

  The URL to this package's Git remote.

• depConfigs : Array Dependency

  Dependency configurations for the package.

• targetDecls : Array (PConfigDecl self.name)

  Target configurations in the order declared by the package.

• targetDeclMap : DNameMap (NConfigDecl self.name)

  Name-declaration map of target configurations in the package.

• defaultTargets : Array Lean.Name

  The names of the package's targets to build by default (i.e., on a bare lake build of the package).

• scripts : Lean.NameMap Script

  Scripts for the package.

• defaultScripts : Array Script

  The names of the package's scripts run by default (i.e., on a bare lake run of the package).

• postUpdateHooks : Array (OpaquePostUpdateHook self.name)

  Post-lake update hooks for the package.

• buildArchive : String

  The package's buildArchive/buildArchive? configuration.

• testDriver : String

  The driver used for lake test when this package is the workspace root.

• lintDriver : String

  The driver used for lake lint when this package is the workspace root.

• cacheRef? : Option CacheRef

  Input-to-content map for hashes of package artifacts. If none, the artifact cache is disabled for the package.

instance Lake.instInhabitedPackage : Inhabited Package

Equations

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

instance Lake.instHashablePackage : Hashable Package

Equations

• Lake.instHashablePackage = { hash := fun (pkg : Lake.Package) => hash pkg.name }

instance Lake.instBEqPackage : BEq Package

Equations

• Lake.instBEqPackage = { beq := fun (p1 p2 : Lake.Package) => p1.name == p2.name }

@[reducible, inline]

abbrev Lake.PackageSet : Type

Equations

• Lake.PackageSet = Std.HashSet Lake.Package

@[inline]

def Lake.PackageSet.empty : PackageSet

Equations

• Lake.PackageSet.empty = ∅

@[reducible, inline]

abbrev Lake.OrdPackageSet : Type

Equations

• Lake.OrdPackageSet = Lake.OrdHashSet Lake.Package

@[inline]

def Lake.OrdPackageSet.empty : OrdPackageSet

Equations

• Lake.OrdPackageSet.empty = Lake.OrdHashSet.empty

instance Lake.instToJsonPackage : Lean.ToJson Package

Equations

• Lake.instToJsonPackage = { toJson := fun (x : Lake.Package) => Lean.toJson x.name }

instance Lake.instToStringPackage : ToString Package

Equations

• Lake.instToStringPackage = { toString := fun (x : Lake.Package) => x.name.toString }

structure Lake.NPackage (n : Lean.Name) extends Lake.Package : Type

A package with a name known at type-level.

• name : Lean.Name
• dir : System.FilePath
• relDir : System.FilePath
• config : PackageConfig self.name
• configFile : System.FilePath
• relConfigFile : System.FilePath
• relManifestFile : System.FilePath
• scope : String
• remoteUrl : String
• depConfigs : Array Dependency
• targetDecls : Array (PConfigDecl self.name)
• targetDeclMap : DNameMap (NConfigDecl self.name)
• defaultTargets : Array Lean.Name
• scripts : Lean.NameMap Script
• defaultScripts : Array Script
• postUpdateHooks : Array (OpaquePostUpdateHook self.name)
• buildArchive : String
• testDriver : String
• lintDriver : String
• cacheRef? : Option CacheRef
• name_eq : self.name = n

instance Lake.instCoeOutNPackagePackage {n : Lean.Name} : CoeOut (NPackage n) Package

Equations

• Lake.instCoeOutNPackagePackage = { coe := Lake.NPackage.toPackage }

instance Lake.instCoeDepPackageNPackageName {pkg : Package} : CoeDep Package pkg (NPackage pkg.name)

Equations

• Lake.instCoeDepPackageNPackageName = { coe := { toPackage := pkg, name_eq := ⋯ } }

@[reducible, inline]

abbrev Lake.PostUpdateFn (pkgName : Lean.Name) : Type

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

Equations

• Lake.PostUpdateFn pkgName = (Lake.NPackage pkgName → Lake.LakeT Lake.LogIO PUnit)

structure Lake.PostUpdateHook (pkgName : Lean.Name) : Type

• fn : PostUpdateFn pkgName

instance Lake.instInhabitedPostUpdateHook {a✝ : Lean.Name} : Inhabited (PostUpdateHook a✝)

Equations

• Lake.instInhabitedPostUpdateHook = { default := { fn := default } }

@[implemented_by Lake.OpaquePostUpdateHook.unsafeMk]

opaque Lake.OpaquePostUpdateHook.mk {name : Lean.Name} : PostUpdateHook name → OpaquePostUpdateHook name

instance Lake.OpaquePostUpdateHook.instInhabitedOfPostUpdateHook {name : Lean.Name} [Inhabited (PostUpdateHook name)] : Inhabited (OpaquePostUpdateHook name)

Equations

• Lake.OpaquePostUpdateHook.instInhabitedOfPostUpdateHook = { default := Lake.OpaquePostUpdateHook.mk default }

instance Lake.OpaquePostUpdateHook.instCoePostUpdateHook {name : Lean.Name} : Coe (PostUpdateHook name) (OpaquePostUpdateHook name)

Equations

• Lake.OpaquePostUpdateHook.instCoePostUpdateHook = { coe := Lake.OpaquePostUpdateHook.mk }

instance Lake.OpaquePostUpdateHook.instCoePostUpdateHook_1 {name : Lean.Name} : Coe (OpaquePostUpdateHook name) (PostUpdateHook name)

Equations

• Lake.OpaquePostUpdateHook.instCoePostUpdateHook_1 = { coe := Lake.OpaquePostUpdateHook.get }

unsafe def Lake.OpaquePostUpdateHook.unsafeGet {name : Lean.Name} : OpaquePostUpdateHook name → PostUpdateHook name

Equations

• Lake.OpaquePostUpdateHook.unsafeGet = unsafeCast

unsafe def Lake.OpaquePostUpdateHook.unsafeMk {name : Lean.Name} : PostUpdateHook name → OpaquePostUpdateHook name

Equations

• Lake.OpaquePostUpdateHook.unsafeMk = unsafeCast

@[implemented_by Lake.OpaquePostUpdateHook.unsafeGet]

opaque Lake.OpaquePostUpdateHook.get {name : Lean.Name} : OpaquePostUpdateHook name → PostUpdateHook name

structure Lake.PostUpdateHookDecl : Type

• pkg : Lean.Name
• fn : PostUpdateFn self.pkg

instance Lake.instTypeNamePostUpdateHookDecl : TypeName PostUpdateHookDecl

Equations

• Lake.instTypeNamePostUpdateHookDecl = Lake.inst✝

@[inline]

def Lake.Package.bootstrap (self : Package) : Bool

For internal use. Whether this package is Lean itself.

Equations

• self.bootstrap = self.config.bootstrap

@[inline]

def Lake.Package.version (self : Package) : LeanVer

The package version.

Equations

• self.version = self.config.version

@[inline]

def Lake.Package.versionTags (self : Package) : StrPat

The package's versionTags configuration.

Equations

• self.versionTags = self.config.versionTags

@[inline]

def Lake.Package.description (self : Package) : String

The package's description configuration.

Equations

• self.description = self.config.description

@[inline]

def Lake.Package.keywords (self : Package) : Array String

The package's keywords configuration.

Equations

• self.keywords = self.config.keywords

@[inline]

def Lake.Package.homepage (self : Package) : String

The package's homepage configuration.

Equations

• self.homepage = self.config.homepage

@[inline]

def Lake.Package.reservoir (self : Package) : Bool

The package's reservoir configuration.

Equations

• self.reservoir = self.config.reservoir

@[inline]

def Lake.Package.license (self : Package) : String

The package's license configuration.

Equations

• self.license = self.config.license

@[inline]

def Lake.Package.relLicenseFiles (self : Package) : Array System.FilePath

The package's licenseFiles configuration.

Equations

• self.relLicenseFiles = Array.map (fun (x : System.FilePath) => x.normalize) self.config.licenseFiles

@[inline]

def Lake.Package.licenseFiles (self : Package) : Array System.FilePath

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

Equations

• self.licenseFiles = Array.map (fun (x : System.FilePath) => self.dir / x.normalize) self.relLicenseFiles

@[inline]

def Lake.Package.relReadmeFile (self : Package) : System.FilePath

The package's readmeFile configuration.

Equations

• self.relReadmeFile = self.config.readmeFile.normalize

@[inline]

def Lake.Package.readmeFile (self : Package) : System.FilePath

The package's dir joined with its relReadmeFile.

Equations

• self.readmeFile = self.dir / self.relReadmeFile

@[inline]

def Lake.Package.relLakeDir : Package → System.FilePath

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

Equations

• x✝.relLakeDir = Lake.defaultLakeDir

@[inline]

def Lake.Package.lakeDir (self : Package) : System.FilePath

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

Equations

• self.lakeDir = self.dir / self.relLakeDir

@[inline]

def Lake.Package.relPkgsDir (self : Package) : System.FilePath

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

Equations

• self.relPkgsDir = self.config.packagesDir.normalize

@[inline]

def Lake.Package.pkgsDir (self : Package) : System.FilePath

The package's dir joined with its relPkgsDir.

Equations

• self.pkgsDir = self.dir / self.relPkgsDir

@[inline]

def Lake.Package.manifestFile (self : Package) : System.FilePath

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

Equations

• self.manifestFile = self.dir / self.relManifestFile

@[inline]

def Lake.Package.buildDir (self : Package) : System.FilePath

The package's dir joined with its buildDir configuration.

Equations

• self.buildDir = self.dir / self.config.buildDir.normalize

@[inline]

def Lake.Package.testDriverArgs (self : Package) : Array String

The package's testDriverArgs configuration.

Equations

• self.testDriverArgs = self.config.testDriverArgs

@[inline]

def Lake.Package.lintDriverArgs (self : Package) : Array String

The package's lintDriverArgs configuration.

Equations

• self.lintDriverArgs = self.config.lintDriverArgs

@[inline]

def Lake.Package.extraDepTargets (self : Package) : Array Lean.Name

The package's extraDepTargets configuration.

Equations

• self.extraDepTargets = self.config.extraDepTargets

@[inline]

def Lake.Package.platformIndependent (self : Package) : Option Bool

The package's platformIndependent configuration.

Equations

• self.platformIndependent = self.config.platformIndependent

@[inline]

def Lake.Package.releaseRepo? (self : Package) : Option String

The package's releaseRepo/releaseRepo? configuration.

Equations

• self.releaseRepo? = self.config.releaseRepo

@[inline]

def Lake.Package.remoteUrl? (self : Package) : Option String

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

Equations

• self.remoteUrl? = if self.remoteUrl.isEmpty = true then some self.remoteUrl else none

@[inline]

def Lake.Package.buildArchiveFile (self : Package) : System.FilePath

The package's lakeDir joined with its buildArchive.

Equations

• self.buildArchiveFile = self.lakeDir / { toString := self.buildArchive }

@[inline]

def Lake.Package.barrelFile (self : Package) : System.FilePath

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

Equations

• self.barrelFile = self.lakeDir / { toString := "build.barrel" }

@[inline]

def Lake.Package.preferReleaseBuild (self : Package) : Bool

The package's preferReleaseBuild configuration.

Equations

• self.preferReleaseBuild = self.config.preferReleaseBuild

@[inline]

def Lake.Package.precompileModules (self : Package) : Bool

The package's precompileModules configuration.

Equations

• self.precompileModules = self.config.precompileModules

@[inline]

def Lake.Package.moreGlobalServerArgs (self : Package) : Array String

The package's moreGlobalServerArgs configuration.

Equations

• self.moreGlobalServerArgs = self.config.moreGlobalServerArgs

@[inline]

def Lake.Package.moreServerOptions (self : Package) : Lean.LeanOptions

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

Equations

• self.moreServerOptions = Lean.LeanOptions.ofArray self.config.leanOptions ++ self.config.moreServerOptions

@[inline]

def Lake.Package.buildType (self : Package) : BuildType

The package's buildType configuration.

Equations

• self.buildType = self.config.buildType

@[inline]

def Lake.Package.backend (self : Package) : Backend

The package's backend configuration.

Equations

• self.backend = self.config.backend

@[inline]

def Lake.Package.dynlibs (self : Package) : TargetArray Dynlib

The package's dynlibs configuration.

Equations

• self.dynlibs = self.config.dynlibs

@[inline]

def Lake.Package.plugins (self : Package) : TargetArray Dynlib

The package's plugins configuration.

Equations

• self.plugins = self.config.plugins

@[inline]

def Lake.Package.leanOptions (self : Package) : Lean.LeanOptions

The package's leanOptions configuration.

Equations

• self.leanOptions = Lean.LeanOptions.ofArray self.config.leanOptions

@[inline]

def Lake.Package.moreLeanArgs (self : Package) : Array String

The package's moreLeanArgs configuration.

Equations

• self.moreLeanArgs = self.config.moreLeanArgs

@[inline]

def Lake.Package.weakLeanArgs (self : Package) : Array String

The package's weakLeanArgs configuration.

Equations

• self.weakLeanArgs = self.config.weakLeanArgs

@[inline]

def Lake.Package.moreLeancArgs (self : Package) : Array String

The package's moreLeancArgs configuration.

Equations

• self.moreLeancArgs = self.config.moreLeancArgs

@[inline]

def Lake.Package.weakLeancArgs (self : Package) : Array String

The package's weakLeancArgs configuration.

Equations

• self.weakLeancArgs = self.config.weakLeancArgs

@[inline]

def Lake.Package.moreLinkObjs (self : Package) : TargetArray System.FilePath

The package's moreLinkObjs configuration.

Equations

• self.moreLinkObjs = self.config.moreLinkObjs

@[inline]

def Lake.Package.moreLinkLibs (self : Package) : TargetArray Dynlib

The package's moreLinkLibs configuration.

Equations

• self.moreLinkLibs = self.config.moreLinkLibs

@[inline]

def Lake.Package.moreLinkArgs (self : Package) : Array String

The package's moreLinkArgs configuration.

Equations

• self.moreLinkArgs = self.config.moreLinkArgs

@[inline]

def Lake.Package.weakLinkArgs (self : Package) : Array String

The package's weakLinkArgs configuration.

Equations

• self.weakLinkArgs = self.config.weakLinkArgs

@[inline]

def Lake.Package.srcDir (self : Package) : System.FilePath

The package's dir joined with its srcDir configuration.

Equations

• self.srcDir = self.dir / self.config.srcDir.normalize

@[inline]

def Lake.Package.rootDir (self : Package) : System.FilePath

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

Equations

• self.rootDir = self.srcDir

@[inline]

def Lake.Package.leanLibDir (self : Package) : System.FilePath

The package's buildDir joined with its leanLibDir configuration.

Equations

• self.leanLibDir = self.buildDir / self.config.leanLibDir.normalize

@[inline]

def Lake.Package.staticLibDir (self : Package) : System.FilePath

Where static libraries for the package are located. The package's buildDir joined with its nativeLibDir configuration.

Equations

• self.staticLibDir = self.buildDir / self.config.nativeLibDir.normalize

@[inline]

def Lake.Package.sharedLibDir (self : Package) : System.FilePath

Where shared libraries for the package are located. The package's buildDir joined with its nativeLibDir configuration.

Equations

• self.sharedLibDir = self.buildDir / self.config.nativeLibDir.normalize

@[inline, deprecated "Use staticLibDir or sharedLibDir instead." (since := "2025-03-29")]

def Lake.Package.nativeLibDir (self : Package) : System.FilePath

The package's buildDir joined with its nativeLibDir configuration.

Equations

• self.nativeLibDir = self.buildDir / self.config.nativeLibDir.normalize

@[inline]

def Lake.Package.binDir (self : Package) : System.FilePath

The package's buildDir joined with its binDir configuration.

Equations

• self.binDir = self.buildDir / self.config.binDir.normalize

@[inline]

def Lake.Package.irDir (self : Package) : System.FilePath

The package's buildDir joined with its irDir configuration.

Equations

• self.irDir = self.buildDir / self.config.irDir.normalize

@[inline]

def Lake.Package.libPrefixOnWindows (self : Package) : Bool

The package's libPrefixOnWindows configuration.

Equations

• self.libPrefixOnWindows = self.config.libPrefixOnWindows

@[inline]

def Lake.Package.enableArtifactCache? (self : Package) : Option Bool

The package's enableArtifactCache? configuration.

Equations

• self.enableArtifactCache? = self.config.enableArtifactCache?

def Lake.Package.inputsFileIn (cache : Cache) (self : Package) : System.FilePath

The file where the package's input-to-content mapping is stored in the Lake cache.

Equations

• Lake.Package.inputsFileIn cache self = Lake.Cache.inputsFile (self.name.toString false) cache

def Lake.Package.findTargetDecl? (name : Lean.Name) (self : Package) : Option (NConfigDecl self.name name)

Try to find a target configuration in the package with the given name.

Equations

• Lake.Package.findTargetDecl? name self = Std.DTreeMap.get? self.targetDeclMap name

def Lake.Package.isLocalModule (mod : Lean.Name) (self : Package) : Bool

Whether the given module is considered local to the package.

Equations

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

def Lake.Package.isBuildableModule (mod : Lean.Name) (self : Package) : Bool

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.

def Lake.Package.clean (self : Package) : IO PUnit

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

Equations

• self.clean = do let __do_lift ← liftM self.buildDir.pathExists if __do_lift = true then IO.FS.removeDirAll self.buildDir else pure PUnit.unit