instance Lake.OpaquePostUpdateHook.instNonempty {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.

• wsIdx : Nat

  The index of the package in the workspace. Used to disambiguate packages with the same name.

• baseName : Lean.Name

  The assigned name of the package.

• keyName : Lean.Name

  The package identifier used in target keys and configuration types.

• origName : Lean.Name

  The name specified by 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.keyName self.origName

  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.keyName)

  Target configurations in the order declared by the package.

• targetDeclMap : DNameMap (NConfigDecl self.keyName)

  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.keyName)

  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.

• inputsRef? : Option CacheRef

  Input-to-output(s) map for hashes of package artifacts. If none, the artifact cache is disabled for the package.

• outputsRef? : Option CacheRef

  Input-to-output(s) map for hashes of package artifacts. If none, the artifact cache is disabled for the package.

def Lake.instInhabitedPackage.default : Package

Equations

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

instance Lake.instInhabitedPackage : Inhabited Package

Equations

• Lake.instInhabitedPackage = { default := Lake.instInhabitedPackage.default }

instance Lake.Package.instHashable : Hashable Package

Equations

• Lake.Package.instHashable = { hash := fun (pkg : Lake.Package) => hash pkg.keyName }

instance Lake.Package.instBEq : BEq Package

Equations

• Lake.Package.instBEq = { beq := fun (p1 p2 : Lake.Package) => p1.wsIdx == p2.wsIdx }

@[inline]

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

Pretty prints the package's name. Used when outputting package names.

Equations

• self.prettyName = self.baseName.toString false

instance Lake.Package.instQueryJson : QueryJson Package

Equations

• Lake.Package.instQueryJson = { queryJson := fun (x : Lake.Package) => Lean.toJson x.keyName }

instance Lake.Package.instQueryText : QueryText Package

Equations

• Lake.Package.instQueryText = { queryText := fun (x : Lake.Package) => x.prettyName }

@[reducible, inline, deprecated "Use `baseName`, `keyName`, or `prettyName` instead" (since := "2025-12-03")]

abbrev Lake.Package.name (self : Package) : Lean.Name

Equations

• Lake.Package.name = Lake.Package.baseName

@[inline]

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

The (unscoped) name of the package as it appears in Reservoir URLs (before URI-encoding).

Equations

• self.reservoirName = self.origName.toString false

@[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

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

A package with a name known at type-level.

• wsIdx : Nat
• baseName : Lean.Name
• keyName : Lean.Name
• origName : Lean.Name
• dir : System.FilePath
• relDir : System.FilePath
• config : PackageConfig self.keyName self.origName
• configFile : System.FilePath
• relConfigFile : System.FilePath
• relManifestFile : System.FilePath
• scope : String
• remoteUrl : String
• depConfigs : Array Dependency
• targetDecls : Array (PConfigDecl self.keyName)
• targetDeclMap : DNameMap (NConfigDecl self.keyName)
• defaultTargets : Array Lean.Name
• scripts : Lean.NameMap Script
• defaultScripts : Array Script
• postUpdateHooks : Array (OpaquePostUpdateHook self.keyName)
• buildArchive : String
• testDriver : String
• lintDriver : String
• inputsRef? : Option CacheRef
• outputsRef? : Option CacheRef
• keyName_eq : self.keyName = n

@[deprecated Lake.NPackage.keyName_eq (since := "2025-12-03")]

theorem Lake.NPackage.name_eq {n : Lean.Name} {self : NPackage n} : self.keyName = n

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

Equations

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

instance Lake.NPackage.instCoeDepPackageKeyName {pkg : Package} : CoeDep Package pkg (NPackage pkg.keyName)

Equations

• Lake.NPackage.instCoeDepPackageKeyName = { coe := { toPackage := pkg, keyName_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 := Lake.instInhabitedPostUpdateHook.default }

def Lake.instInhabitedPostUpdateHook.default {a✝ : Lean.Name} : PostUpdateHook a✝

Equations

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

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.instCoeGet {name : Lean.Name} : Coe (OpaquePostUpdateHook name) (PostUpdateHook name)

Equations

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

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

Equations

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

@[implemented_by _private.Lake.Config.Package.0.Lake.OpaquePostUpdateHook.unsafeMk]

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

@[implemented_by _private.Lake.Config.Package.0.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.isRoot (self : Package) : Bool

Returns whether this package is root package of the workspace.

Equations

• self.isRoot = (self.wsIdx == 0)

@[inline]

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

For internal use. Whether this package is Lean itself.

Equations

• self.bootstrap = self.config.bootstrap

def Lake.Package.id? (self : Package) : Option Lean.PkgId

The identifier passed to Lean to disambiguate the package's native symbols.

Equations

• self.id? = if self.bootstrap = true then none else some (self.origName.toString false)

@[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.isPlatformIndependent (self : Package) : Bool

Whether the package's has been configured with platformIndependent = true.

Equations

• self.isPlatformIndependent = (self.config.platformIndependent == some true)

@[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.allowImportAll (self : Package) : Bool

The package's allowImportAll configuration.

Equations

• self.allowImportAll = self.config.allowImportAll

@[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]

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?

@[inline]

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

The package's restoreAllArtifacts configuration.

Equations

• self.restoreAllArtifacts = self.config.restoreAllArtifacts

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

The directory within the Lake cache were package-scoped files are stored.

Equations

• self.cacheScope = self.baseName.toString false

def Lake.Package.findTargetDecl? (name : Lean.Name) (self : Package) : Option (NConfigDecl self.keyName 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