def Lake.osDescriptor : String

A string descriptor of the System.Platform OS (windows, macOS, or linux).

Equations

• Lake.osDescriptor = if System.Platform.isWindows = true then "windows" else if System.Platform.isOSX = true then "macOS" else "linux"

def Lake.archiveSuffix : String

A tar.gz file name suffix encoding the the current Platform. (i.e, osDescriptor joined with System.Platform.numBits).

Equations

• Lake.archiveSuffix = toString "" ++ toString Lake.osDescriptor ++ toString "-" ++ toString System.Platform.numBits ++ toString ".tar.gz"

def Lake.nameToArchive (name? : Option String) : String

If name?, {name}-{archiveSuffix}, otherwise just archiveSuffix.

Equations

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

def Lake.stringToLegalOrSimpleName (s : String) : Lake.Name

First tries to convert a string into a legal name. If that fails, defaults to making it a simple name (e.g., Lean.Name.mkSimple). Currently used for package and target names taken from the CLI.

Equations

• Lake.stringToLegalOrSimpleName s = if Lean.Name.isAnonymous (String.toName s) = true then Lean.Name.mkSimple s else String.toName s

Defaults

def Lake.defaultManifestFile : String

The default setting for a PackageConfig's manifestFile option.

Equations

• Lake.defaultManifestFile = "lake-manifest.json"

def Lake.defaultBuildDir : Lake.FilePath

The default setting for a PackageConfig's buildDir option.

Equations

• Lake.defaultBuildDir = { toString := "build" }

def Lake.defaultLeanLibDir : Lake.FilePath

The default setting for a PackageConfig's leanLibDir option.

Equations

• Lake.defaultLeanLibDir = { toString := "lib" }

def Lake.defaultNativeLibDir : Lake.FilePath

The default setting for a PackageConfig's nativeLibDir option.

Equations

• Lake.defaultNativeLibDir = { toString := "lib" }

def Lake.defaultBinDir : Lake.FilePath

The default setting for a PackageConfig's binDir option.

Equations

• Lake.defaultBinDir = { toString := "bin" }

def Lake.defaultIrDir : Lake.FilePath

The default setting for a PackageConfig's irDir option.

Equations

• Lake.defaultIrDir = { toString := "ir" }

PackageConfig

structure Lake.PackageConfigextends Lake.WorkspaceConfig , Lake.LeanConfig : Type

• packagesDir : Lake.FilePath
• buildType : Lake.BuildType
• moreLeanArgs : Array String
• weakLeanArgs : Array String
• moreLeancArgs : Array String
• weakLeancArgs : Array String
• moreLinkArgs : Array String
• weakLinkArgs : Array String
• name : Lake.Name

  The Name of the package.

• manifestFile : String

  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

  Additional arguments to pass to the Lean language server (i.e., lean --server) launched by lake server.

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

• buildArchive? : Option String

  The name of the build archive on GitHub. Defaults to none. The archive's full file name will be nameToArchive buildArchive?.

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

A Package's declarative configuration.

instance Lake.instInhabitedPackageConfig : Inhabited Lake.PackageConfig

Equations

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

Package

structure Lake.Package : Type

• dir : Lake.FilePath

  The path to the package's directory.

• config : Lake.PackageConfig

  The package's user-defined configuration.

• configEnv : Lean.Environment

  The elaboration environment of the package's configuration file.

• leanOpts : Lean.Options

  The Lean Options the package configuration was elaborated with.

• remoteUrl? : Option String

  The URL to this package's Git remote.

• gitTag? : Option String

  The Git tag of this package.

• opaqueDeps : Array Lake.OpaquePackage

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

• 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 s.config.name)

  External library targets for the package.

• opaqueTargetConfigs : Lake.DNameMap (Lake.OpaqueTargetConfig s.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).

A Lake package -- its location plus its configuration.

instance Lake.instNonemptyPackage : Nonempty Lake.Package

Equations

• Lake.instNonemptyPackage = Lake.instNonemptyPackage.proof_1

instance Lake.OpaquePackage.instCoePackageOpaquePackage : Coe Lake.Package Lake.OpaquePackage

Equations

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

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

Equations

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

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

Equations

• Lake.OpaquePackage.unsafeMk = unsafeCast

@[simp]

axiom Lake.OpaquePackage.get_mk : ∀ {x : Lake.Package}, Lake.OpaquePackage.get (Lake.OpaquePackage.mk x) = x

instance Lake.OpaquePackage.instCoeOpaquePackagePackage : Coe Lake.OpaquePackage Lake.Package

Equations

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

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

Equations

• Lake.OpaquePackage.unsafeGet = unsafeCast

@[implemented_by Lake.OpaquePackage.unsafeMk]

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

@[implemented_by Lake.OpaquePackage.unsafeGet]

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

instance Lake.instHashablePackage : Hashable Lake.Package

Equations

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

instance Lake.instBEqPackage : BEq Lake.Package

Equations

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

The package's name.

Equations

• Lake.Package.name self = self.config.name

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

• dir : Lake.FilePath
• config : Lake.PackageConfig
• configEnv : Lean.Environment
• leanOpts : Lean.Options
• remoteUrl? : Option String
• gitTag? : Option String
• opaqueDeps : Array Lake.OpaquePackage
• leanLibConfigs : Lake.OrdNameMap Lake.LeanLibConfig
• leanExeConfigs : Lake.OrdNameMap Lake.LeanExeConfig
• externLibConfigs : Lake.DNameMap (Lake.ExternLibConfig s.toPackage.config.name)
• opaqueTargetConfigs : Lake.DNameMap (Lake.OpaqueTargetConfig s.toPackage.config.name)
• defaultTargets : Array Lake.Name
• scripts : Lake.NameMap Lake.Script
• defaultScripts : Array Lake.Script
• name_eq : Lake.Package.name s.toPackage = name

A package with a name known at type-level.

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 (Lake.Package.name pkg))

Equations

• Lake.instCoeDepPackageNPackageName = { coe := { toPackage := pkg, name_eq := (_ : Lake.Package.name pkg = Lake.Package.name pkg) } }

@[inline, reducible]

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

The package's name.

Equations

• Lake.NPackage.name x = n

@[inline]

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

The package's direct dependencies.

Equations

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

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

• Lake.Package.relPkgsDir self = self.config.toWorkspaceConfig.packagesDir

@[inline]

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

The package's dir joined with its relPkgsDir

Equations

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

@[inline]

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

The package's JSON manifest of remote dependencies.

Equations

• Lake.Package.manifestFile self = self.dir / { toString := self.config.manifestFile }

@[inline]

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

The package's dir joined with its buildDir configuration.

Equations

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

@[inline]

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

The package's extraDepTargets configuration.

Equations

• Lake.Package.extraDepTargets self = self.config.extraDepTargets

@[inline]

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

The package's releaseRepo? configuration.

Equations

• Lake.Package.releaseRepo? self = self.config.releaseRepo?

def Lake.Package.release? (self : Lake.Package) : Option (String × String)

The package's URL × tag release. Tries releaseRepo? first and then falls back to remoteUrl?.

Equations

• Lake.Package.release? self = do let url ← HOrElse.hOrElse (Lake.Package.releaseRepo? self) fun x => self.remoteUrl? let tag ← self.gitTag? pure (url, tag)

@[inline]

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

The package's buildArchive? configuration.

Equations

• Lake.Package.buildArchive? self = self.config.buildArchive?

@[inline]

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

The file name of the package's build archive derived from buildArchive?.

Equations

• Lake.Package.buildArchive self = Lake.nameToArchive (Lake.Package.buildArchive? self)

@[inline]

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

The package's buildDir joined with its buildArchive configuration.

Equations

• Lake.Package.buildArchiveFile self = Lake.Package.buildDir self / { toString := Lake.Package.buildArchive self }

@[inline]

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

The package's preferReleaseBuild configuration.

Equations

• Lake.Package.preferReleaseBuild self = self.config.preferReleaseBuild

@[inline]

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

The package's precompileModules configuration.

Equations

• Lake.Package.precompileModules self = self.config.precompileModules

@[inline]

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

The package's moreServerArgs configuration.

Equations

• Lake.Package.moreServerArgs self = self.config.moreServerArgs

@[inline]

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

The package's buildType configuration.

Equations

• Lake.Package.buildType self = self.config.toLeanConfig.buildType

@[inline]

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

The package's moreLeanArgs configuration.

Equations

• Lake.Package.moreLeanArgs self = self.config.toLeanConfig.moreLeanArgs

@[inline]

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

The package's weakLeanArgs configuration.

Equations

• Lake.Package.weakLeanArgs self = self.config.toLeanConfig.weakLeanArgs

@[inline]

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

The package's moreLeancArgs configuration.

Equations

• Lake.Package.moreLeancArgs self = self.config.toLeanConfig.moreLeancArgs

@[inline]

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

The package's weakLeancArgs configuration.

Equations

• Lake.Package.weakLeancArgs self = self.config.toLeanConfig.weakLeancArgs

@[inline]

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

The package's moreLinkArgs configuration.

Equations

• Lake.Package.moreLinkArgs self = self.config.toLeanConfig.moreLinkArgs

@[inline]

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

The package's weakLinkArgs configuration.

Equations

• Lake.Package.weakLinkArgs self = self.config.toLeanConfig.weakLinkArgs

@[inline]

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

The package's dir joined with its srcDir configuration.

Equations

• Lake.Package.srcDir self = 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

• Lake.Package.rootDir self = Lake.Package.srcDir self

@[inline]

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

The package's buildDir joined with its leanLibDir configuration.

Equations

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

@[inline]

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

The package's buildDir joined with its nativeLibDir configuration.

Equations

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

@[inline]

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

The package's buildDir joined with its binDir configuration.

Equations

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

@[inline]

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

The package's buildDir joined with its irDir configuration.

Equations

• Lake.Package.irDir self = Lake.Package.buildDir self / 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.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

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