@[inline]

def Lake.defaultBuildArchive (name : Lake.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.PackageConfigextends Lake.WorkspaceConfig , Lake.LeanConfig : Type

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

• irDir : Lake.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.

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

instance Lake.instInhabitedPackageConfig : Inhabited Lake.PackageConfig

Equations

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

Package

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

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

Equations

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

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

Equations

• ⋯ = ⋯

structure Lake.Package : Type

A Lake package -- its location plus its configuration.

• dir : Lake.FilePath

  The path to the package's directory.

• relDir : Lake.FilePath

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

• config : Lake.PackageConfig

  The package's user-defined configuration.

• relConfigFile : Lake.FilePath

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

• relManifestFile : Lake.FilePath

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

• remoteUrl? : Option String

  The URL to this package's Git remote.

• opaqueDeps : Array Lake.OpaquePackage

  (Opaque references to) the package's direct dependencies.

• depConfigs : Array Lake.Dependency

  Dependency configurations for the package.

• leanLibConfigs : Lake.OrdNameMap Lake.LeanLibConfig

  Lean library configurations for the package.

• leanExeConfigs : Lake.OrdNameMap Lake.LeanExeConfig

  Lean binary executable configurations for the package.

• externLibConfigs : Lake.DNameMap (Lake.ExternLibConfig self.config.name)

  External library targets for the package.

• opaqueTargetConfigs : Lake.DNameMap (Lake.OpaqueTargetConfig self.config.name)

  (Opaque references to) targets defined in the package.

• defaultTargets : Array Lake.Name

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

• scripts : Lake.NameMap Lake.Script

  Scripts for the package.

• defaultScripts : Array Lake.Script

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

• postUpdateHooks : Array (Lake.OpaquePostUpdateHook self.config.name)

  Post-lake update hooks for the package.

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

instance Lake.instNonemptyPackage : Nonempty Lake.Package

Equations

• Lake.instNonemptyPackage = ⋯

instance Lake.OpaquePackage.instCoePackage_1 : Coe Lake.OpaquePackage Lake.Package

Equations

• Lake.OpaquePackage.instCoePackage_1 = { coe := Lake.OpaquePackage.get }

@[implemented_by Lake.OpaquePackage.unsafeMk]

opaque Lake.OpaquePackage.mk : Lake.Package → Lake.OpaquePackage

unsafe def Lake.OpaquePackage.unsafeGet : Lake.OpaquePackage → Lake.Package

Equations

• Lake.OpaquePackage.unsafeGet = unsafeCast

instance Lake.OpaquePackage.instInhabitedOfPackage [Inhabited Lake.Package] : Inhabited Lake.OpaquePackage

Equations

• Lake.OpaquePackage.instInhabitedOfPackage = { default := Lake.OpaquePackage.mk default }

unsafe def Lake.OpaquePackage.unsafeMk : Lake.Package → Lake.OpaquePackage

Equations

• Lake.OpaquePackage.unsafeMk = unsafeCast

@[implemented_by Lake.OpaquePackage.unsafeGet]

opaque Lake.OpaquePackage.get : Lake.OpaquePackage → Lake.Package

instance Lake.OpaquePackage.instCoePackage : Coe Lake.Package Lake.OpaquePackage

Equations

• Lake.OpaquePackage.instCoePackage = { coe := Lake.OpaquePackage.mk }

instance Lake.instHashablePackage : Hashable Lake.Package

Equations

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

instance Lake.instBEqPackage : BEq Lake.Package

Equations

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

@[reducible, inline]

abbrev Lake.PackageSet : Type

Equations

• Lake.PackageSet = Lean.HashSet Lake.Package

@[inline]

def Lake.PackageSet.empty : Lake.PackageSet

Equations

• Lake.PackageSet.empty = Lean.HashSet.empty

@[reducible, inline]

abbrev Lake.OrdPackageSet : Type

Equations

• Lake.OrdPackageSet = Lake.OrdHashSet Lake.Package

@[inline]

def Lake.OrdPackageSet.empty : Lake.OrdPackageSet

Equations

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

@[reducible, inline]

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

The package's name.

Equations

• self.name = self.config.name

structure Lake.NPackage (name : Lake.Name) extends Lake.Package : Type

A package with a name known at type-level.

• dir : Lake.FilePath
• relDir : Lake.FilePath
• config : Lake.PackageConfig
• relConfigFile : Lake.FilePath
• relManifestFile : Lake.FilePath
• remoteUrl? : Option String
• opaqueDeps : Array Lake.OpaquePackage
• depConfigs : Array Lake.Dependency
• leanLibConfigs : Lake.OrdNameMap Lake.LeanLibConfig
• leanExeConfigs : Lake.OrdNameMap Lake.LeanExeConfig
• externLibConfigs : Lake.DNameMap (Lake.ExternLibConfig self.config.name)
• opaqueTargetConfigs : Lake.DNameMap (Lake.OpaqueTargetConfig self.config.name)
• defaultTargets : Array Lake.Name
• scripts : Lake.NameMap Lake.Script
• defaultScripts : Array Lake.Script
• postUpdateHooks : Array (Lake.OpaquePostUpdateHook self.config.name)
• testDriver : String
• lintDriver : String
• name_eq : self.name = name

@[simp]

theorem Lake.NPackage.name_eq {name : Lake.Name} (self : Lake.NPackage name) : self.name = name

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lake.NPackage.name {n : Lake.Name} : Lake.NPackage n → Lake.Name

The package's name.

Equations

• x.name = n

@[reducible, inline]

abbrev Lake.PostUpdateFn (pkgName : Lake.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 : Lake.Name) : Type

• fn : Lake.PostUpdateFn pkgName

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

Equations

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

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

Equations

• Lake.OpaquePostUpdateHook.unsafeMk = unsafeCast

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

Equations

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

@[implemented_by Lake.OpaquePostUpdateHook.unsafeGet]

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

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

Equations

• Lake.OpaquePostUpdateHook.unsafeGet = unsafeCast

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

Equations

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

@[implemented_by Lake.OpaquePostUpdateHook.unsafeMk]

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

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

Equations

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

structure Lake.PostUpdateHookDecl : Type

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

@[inline]

def Lake.Package.deps (self : Lake.Package) : Array Lake.Package

The package's direct dependencies.

Equations

• self.deps = Array.map (fun (x : Lake.OpaquePackage) => x.get) self.opaqueDeps

@[inline]

def Lake.Package.relLakeDir : Lake.Package → Lake.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 : Lake.Package) : Lake.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 : Lake.Package) : Lake.FilePath

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

Equations

• self.relPkgsDir = self.config.packagesDir

@[inline]

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

The package's dir joined with its relPkgsDir.

Equations

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

@[inline]

def Lake.Package.configFile (self : Lake.Package) : Lake.FilePath

The full path to the package's configuration file.

Equations

• self.configFile = self.dir / self.relConfigFile

@[inline]

def Lake.Package.manifestFile (self : Lake.Package) : Lake.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 : Lake.Package) : Lake.FilePath

The package's dir joined with its buildDir configuration.

Equations

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

@[inline]

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

The package's testDriverArgs configuration.

Equations

• self.testDriverArgs = self.config.testDriverArgs

@[inline]

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

The package's lintDriverArgs configuration.

Equations

• self.lintDriverArgs = self.config.lintDriverArgs

@[inline]

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

The package's extraDepTargets configuration.

Equations

• self.extraDepTargets = self.config.extraDepTargets

@[inline]

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

The package's platformIndependent configuration.

Equations

• self.platformIndependent = self.config.platformIndependent

@[inline]

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

The package's releaseRepo/releaseRepo? configuration.

Equations

• self.releaseRepo? = HOrElse.hOrElse self.config.releaseRepo fun (x : Unit) => self.config.releaseRepo?

@[inline]

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

The package's buildArchive/buildArchive? configuration.

Equations

• self.buildArchive = self.config.buildArchive

@[inline]

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

The package's lakeDir joined with its buildArchive.

Equations

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

@[inline]

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

The package's preferReleaseBuild configuration.

Equations

• self.preferReleaseBuild = self.config.preferReleaseBuild

@[inline]

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

The package's precompileModules configuration.

Equations

• self.precompileModules = self.config.precompileModules

@[inline]

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

The package's moreGlobalServerArgs configuration.

Equations

• self.moreGlobalServerArgs = self.config.moreGlobalServerArgs

@[inline]

def Lake.Package.moreServerOptions (self : Lake.Package) : Array Lake.LeanOption

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

Equations

• self.moreServerOptions = self.config.leanOptions ++ self.config.moreServerOptions

@[inline]

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

The package's buildType configuration.

Equations

• self.buildType = self.config.buildType

@[inline]

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

The package's backend configuration.

Equations

• self.backend = self.config.backend

@[inline]

def Lake.Package.leanOptions (self : Lake.Package) : Array Lake.LeanOption

The package's leanOptions configuration.

Equations

• self.leanOptions = self.config.leanOptions

@[inline]

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

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

Equations

• self.moreLeanArgs = Array.map (fun (x : Lake.LeanOption) => x.asCliArg) self.config.leanOptions ++ self.config.moreLeanArgs

@[inline]

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

The package's weakLeanArgs configuration.

Equations

• self.weakLeanArgs = self.config.weakLeanArgs

@[inline]

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

The package's moreLeancArgs configuration.

Equations

• self.moreLeancArgs = self.config.moreLeancArgs

@[inline]

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

The package's weakLeancArgs configuration.

Equations

• self.weakLeancArgs = self.config.weakLeancArgs

@[inline]

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

The package's moreLinkArgs configuration.

Equations

• self.moreLinkArgs = self.config.moreLinkArgs

@[inline]

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

The package's weakLinkArgs configuration.

Equations

• self.weakLinkArgs = self.config.weakLinkArgs

@[inline]

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

The package's dir joined with its srcDir configuration.

Equations

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

@[inline]

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

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

Equations

• self.rootDir = self.srcDir

@[inline]

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

The package's buildDir joined with its leanLibDir configuration.

Equations

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

@[inline]

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

The package's buildDir joined with its nativeLibDir configuration.

Equations

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

@[inline]

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

The package's buildDir joined with its binDir configuration.

Equations

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

@[inline]

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

The package's buildDir joined with its irDir configuration.

Equations

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

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

Whether the given module is considered local to the package.

Equations

• Lake.Package.isLocalModule mod self = Lake.RBArray.any (fun (lib : Lake.LeanLibConfig) => Lake.LeanLibConfig.isLocalModule mod lib) self.leanLibConfigs

def Lake.Package.isBuildableModule (mod : Lake.Name) (self : Lake.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 : Lake.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