A string descriptor of the System.Platform
OS (windows
, macOS
, or linux
).
Instances For
A tar.gz
file name suffix encoding the the current Platform.
(i.e, osDescriptor
joined with System.Platform.numBits
).
Instances For
If name?
, {name}-{archiveSuffix}
, otherwise just archiveSuffix
.
Instances For
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.
Instances For
Defaults #
The default setting for a PackageConfig
's manifestFile
option.
Instances For
The default setting for a PackageConfig
's buildDir
option.
Instances For
The default setting for a PackageConfig
's leanLibDir
option.
Instances For
The default setting for a PackageConfig
's nativeLibDir
option.
Instances For
The default setting for a PackageConfig
's binDir
option.
Instances For
The default setting for a PackageConfig
's irDir
option.
Instances For
PackageConfig #
- packagesDir : Lake.FilePath
- buildType : Lake.BuildType
- 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
). 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
. Additional arguments to pass to the Lean language server (i.e.,
lean --server
) launched bylake 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 todefaultLeanLibDir
(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 todefaultNativeLibDir
(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 todefaultIrDir
(i.e.,ir
). 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, usesgh
's default.The name of the build archive on GitHub. Defaults to
none
. The archive's full file name will benameToArchive 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.
Instances For
Package #
- 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. The URL to this package's Git remote.
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.
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.
Instances For
The package's name.
Instances For
- dir : Lake.FilePath
- config : Lake.PackageConfig
- configEnv : Lean.Environment
- leanOpts : Lean.Options
- 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)
- 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.
Instances For
The package's name.
Instances For
The package's direct dependencies.
Instances For
The path for storing the package's remote dependencies relative to dir
(i.e., packagesDir
).
Instances For
The package's JSON manifest of remote dependencies.
Instances For
The package's URL × tag release.
Tries releaseRepo?
first and then falls back to remoteUrl?
.
Instances For
Whether the given module is considered local to the package.
Instances For
Whether the given module is in the package (i.e., can build it).
Instances For
Remove the package's build outputs (i.e., delete its build directory).