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

def Lake.OpaquePostUpdateHook (pkg : Lean.Name) : 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

@[implicit_reducible]

instance Lake.instInhabitedPackage : Inhabited Package

@[implicit_reducible]

instance Lake.Package.instHashable : Hashable Package

@[implicit_reducible]

instance Lake.Package.instBEq : BEq Package

@[inline]

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

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

@[implicit_reducible]

instance Lake.Package.instQueryJson : QueryJson Package

@[implicit_reducible]

instance Lake.Package.instQueryText : QueryText Package

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

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

@[inline]

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

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

@[reducible, inline]

abbrev Lake.PackageSet : Type

@[inline]

def Lake.PackageSet.empty : PackageSet

@[reducible, inline]

abbrev Lake.OrdPackageSet : Type

@[inline]

def Lake.OrdPackageSet.empty : OrdPackageSet

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

• fn : PostUpdateFn pkgName

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lake.instTypeNamePostUpdateHookDecl : TypeName PostUpdateHookDecl

@[inline]

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

Returns whether this package is root package of the workspace.

@[inline]

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

For internal use. Whether this package is Lean itself.

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

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

@[inline]

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

The package version.

@[inline]

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

The package's versionTags configuration.

@[inline]

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

The package's description configuration.

@[inline]

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

The package's keywords configuration.

@[inline]

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

The package's homepage configuration.

@[inline]

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

The package's reservoir configuration.

@[inline]

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

The package's license configuration.

@[inline]

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

The package's licenseFiles configuration.

@[inline]

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

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

@[inline]

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

The package's readmeFile configuration.

@[inline]

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

The package's dir joined with its relReadmeFile.

@[inline]

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

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

@[inline]

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

The full path to the package's Lake directory (i.e, dir joined with 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).

@[inline]

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

The package's dir joined with its relPkgsDir.

@[inline]

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

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

@[inline]

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

The package's dir joined with its buildDir configuration.

@[inline]

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

The package's testDriverArgs configuration.

@[inline]

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

The package's lintDriverArgs configuration.

@[inline]

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

The package's extraDepTargets configuration.

@[inline]

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

The package's platformIndependent configuration.

@[inline]

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

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

@[inline]

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

The package's releaseRepo/releaseRepo? configuration.

@[inline]

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

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

@[inline]

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

The package's lakeDir joined with its buildArchive.

@[inline]

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

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

@[inline]

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

The package's preferReleaseBuild configuration.

@[inline]

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

The package's precompileModules configuration.

@[inline]

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

The package's moreGlobalServerArgs configuration.

@[inline]

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

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

@[inline]

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

The package's buildType configuration.

@[inline]

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

The package's backend configuration.

@[inline]

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

The package's allowImportAll configuration.

@[inline]

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

The package's dynlibs configuration.

@[inline]

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

The package's plugins configuration.

@[inline]

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

The package's leanOptions configuration.

@[inline]

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

The package's moreLeanArgs configuration.

@[inline]

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

The package's weakLeanArgs configuration.

@[inline]

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

The package's moreLeancArgs configuration.

@[inline]

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

The package's weakLeancArgs configuration.

@[inline]

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

The package's moreLinkObjs configuration.

@[inline]

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

The package's moreLinkLibs configuration.

@[inline]

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

The package's moreLinkArgs configuration.

@[inline]

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

The package's weakLinkArgs configuration.

@[inline]

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

The package's dir joined with its srcDir configuration.

@[inline]

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

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

@[inline]

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

The package's buildDir joined with its leanLibDir configuration.

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

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

@[inline]

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

The package's buildDir joined with its binDir configuration.

@[inline]

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

The package's buildDir joined with its irDir configuration.

@[inline]

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

The package's libPrefixOnWindows configuration.

@[inline]

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

The package's enableArtifactCache? configuration.

@[inline]

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

The package's restoreAllArtifacts configuration.

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

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

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.

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

Whether the given module is considered local to the package.

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

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

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

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