Equations
Instances For
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.
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.
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. Input-to-content map for hashes of package artifacts. If
none
, the artifact cache is disabled for the package.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- Lake.instHashablePackage = { hash := fun (pkg : Lake.Package) => hash pkg.name }
Equations
- Lake.instBEqPackage = { beq := fun (p1 p2 : Lake.Package) => p1.name == p2.name }
Equations
Instances For
Equations
Instances For
Equations
Instances For
Instances For
Equations
- Lake.instToJsonPackage = { toJson := fun (x : Lake.Package) => Lean.toJson x.name }
Equations
- Lake.instToStringPackage = { toString := fun (x : Lake.Package) => x.name.toString }
A package with a name known at type-level.
- config : PackageConfig self.name
- targetDecls : Array (PConfigDecl self.name)
- targetDeclMap : DNameMap (NConfigDecl self.name)
- postUpdateHooks : Array (OpaquePostUpdateHook self.name)
Instances For
Equations
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)
Instances For
- fn : PostUpdateFn pkgName
Instances For
Equations
Instances For
Equations
Equations
Equations
Equations
The package's versionTags
configuration.
Equations
- self.versionTags = self.config.versionTags
Instances For
The package's description
configuration.
Equations
- self.description = self.config.description
Instances For
The package's licenseFiles
configuration.
Equations
- self.relLicenseFiles = Array.map (fun (x : System.FilePath) => x.normalize) self.config.licenseFiles
Instances For
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
Instances For
The package's readmeFile
configuration.
Equations
- self.relReadmeFile = self.config.readmeFile.normalize
Instances For
The package's dir
joined with its relReadmeFile
.
Equations
- self.readmeFile = self.dir / self.relReadmeFile
Instances For
The path to the package's Lake directory relative to dir
(e.g., .lake
).
Equations
Instances For
The full path to the package's Lake directory (i.e, dir
joined with relLakeDir
).
Equations
- self.lakeDir = self.dir / self.relLakeDir
Instances For
The path for storing the package's remote dependencies relative to dir
(i.e., packagesDir
).
Equations
- self.relPkgsDir = self.config.packagesDir.normalize
Instances For
The package's dir
joined with its relPkgsDir
.
Equations
- self.pkgsDir = self.dir / self.relPkgsDir
Instances For
The path to the package's JSON manifest of remote dependencies.
Equations
- self.manifestFile = self.dir / self.relManifestFile
Instances For
The package's testDriverArgs
configuration.
Equations
- self.testDriverArgs = self.config.testDriverArgs
Instances For
The package's lintDriverArgs
configuration.
Equations
- self.lintDriverArgs = self.config.lintDriverArgs
Instances For
The package's extraDepTargets
configuration.
Equations
- self.extraDepTargets = self.config.extraDepTargets
Instances For
The package's platformIndependent
configuration.
Equations
- self.platformIndependent = self.config.platformIndependent
Instances For
The package's releaseRepo
/releaseRepo?
configuration.
Equations
- self.releaseRepo? = self.config.releaseRepo
Instances For
The package's lakeDir
joined with its buildArchive
.
Equations
- self.buildArchiveFile = self.lakeDir / { toString := self.buildArchive }
Instances For
The path where Lake stores the package's barrel (downloaded from Reservoir).
Instances For
The package's preferReleaseBuild
configuration.
Equations
- self.preferReleaseBuild = self.config.preferReleaseBuild
Instances For
The package's precompileModules
configuration.
Equations
- self.precompileModules = self.config.precompileModules
Instances For
The package's moreGlobalServerArgs
configuration.
Equations
- self.moreGlobalServerArgs = self.config.moreGlobalServerArgs
Instances For
The package's moreServerOptions
configuration appended to its leanOptions
configuration.
Equations
- self.moreServerOptions = Lean.LeanOptions.ofArray self.config.leanOptions ++ self.config.moreServerOptions
Instances For
The package's leanOptions
configuration.
Equations
- self.leanOptions = Lean.LeanOptions.ofArray self.config.leanOptions
Instances For
The package's moreLeanArgs
configuration.
Equations
- self.moreLeanArgs = self.config.moreLeanArgs
Instances For
The package's weakLeanArgs
configuration.
Equations
- self.weakLeanArgs = self.config.weakLeanArgs
Instances For
The package's moreLeancArgs
configuration.
Equations
- self.moreLeancArgs = self.config.moreLeancArgs
Instances For
The package's weakLeancArgs
configuration.
Equations
- self.weakLeancArgs = self.config.weakLeancArgs
Instances For
The package's moreLinkObjs
configuration.
Equations
- self.moreLinkObjs = self.config.moreLinkObjs
Instances For
The package's moreLinkLibs
configuration.
Equations
- self.moreLinkLibs = self.config.moreLinkLibs
Instances For
The package's moreLinkArgs
configuration.
Equations
- self.moreLinkArgs = self.config.moreLinkArgs
Instances For
The package's weakLinkArgs
configuration.
Equations
- self.weakLinkArgs = self.config.weakLinkArgs
Instances For
The package's buildDir
joined with its leanLibDir
configuration.
Equations
- self.leanLibDir = self.buildDir / self.config.leanLibDir.normalize
Instances For
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
Instances For
The package's buildDir
joined with its nativeLibDir
configuration.
Equations
- self.nativeLibDir = self.buildDir / self.config.nativeLibDir.normalize
Instances For
The package's libPrefixOnWindows
configuration.
Equations
- self.libPrefixOnWindows = self.config.libPrefixOnWindows
Instances For
The package's enableArtifactCache?
configuration.
Equations
- self.enableArtifactCache? = self.config.enableArtifactCache?
Instances For
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
Instances For
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
Instances For
Whether the given module is considered local to the package.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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