structure Lake.BuildConfigextends Lake.LogConfig : Type

Configuration options for a Lake build.

• failLv : LogLevel
• outLv : LogLevel
• ansiMode : AnsiMode
• out : OutStream
• oldMode : Bool

  Whether to use modification times for trace checking.

• trustHash : Bool

  Whether to trust .hash files.

• noBuild : Bool

  Early exit if a target has to be rebuilt.

• failFast : Bool

  Stop scheduling new build jobs after the first required target failure.

• verbosity : Verbosity

  Verbosity level (-q, -v, or neither).

• showSuccess : Bool

  Whether to print a message when the build finishes successfully (if not quiet).

• outputsFile? : Option System.FilePath

  File to save tracked input-to-output mappings from the build of a package.

• outputsIdx : Nat

  When tracking input-to-output mappings, the workspace index of the tracked package.

• leanOptOverrides : Lean.NameMap Lean.LeanOptions

  Per-package Lean option overrides, applied to every module whose owning package's baseName appears as a key. When recFetchSetup builds module M, the LeanOptions associated with M.pkg.baseName (if any) are appended to M.leanOptions, overriding clashing entries.

  Used by lake lint to inject linter.extra/linter.all into every module of a target package (so transitively-imported first-party modules capture linter-tagged warnings), without touching dependencies.

• macosxDeploymentTarget? : Option String

  The miniumum OS version to target on MacOS.

  If a minimum is not set, linkers default the minimum to the host major version and will emit warnings if any lineed libraries (including system libraries) exceed the minium. Thus, the linker will complain when building on a system with an unset minimum and system libraries which require a higher minor version.

  ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
  

  To silence such warnings, Lake sets this far into the future by default (e.g., 99.0). However, that itself can be wrong if a consumer of Lean library uses the minimum OS version to determine compatibility (e.g., Python does this). The far-flung version would then imply zero compatibility.

  In such cases, the desired deployment target can be manually specified . Depending on the desired scope, it can be set per-target, for all targets within a buld (with this), or across all builds with the environment variable MACOSX_DEPLOYMENT_TARGET.

def Lake.BuildConfig.showProgress (cfg : BuildConfig) : Bool

Whether the build should show progress information.

Verbosity.quiet hides progress and, for a noBuild, Verbosity.verbose shows progress.

Equations

• cfg.showProgress = decide (cfg.noBuild = true ∧ (cfg.verbosity == Lake.Verbosity.verbose) = true ∨ (cfg.verbosity != Lake.Verbosity.quiet) = true)

def Lake.JobQueue : Type

Mutable reference of registered build jobs.

Equations

• Lake.JobQueue = IO.Ref (Array Lake.OpaqueJob)

@[inline]

def Lake.mkJobQueue : BaseIO JobQueue

Returns a new empty job queue.

Equations

• Lake.mkJobQueue = IO.mkRef #[]

structure Lake.BuildContextextends Lake.BuildConfig, Lake.Context : Type

A Lake context with a build configuration and additional build data.

• failLv : LogLevel
• outLv : LogLevel
• ansiMode : AnsiMode
• out : OutStream
• oldMode : Bool
• trustHash : Bool
• noBuild : Bool
• failFast : Bool
• verbosity : Verbosity
• showSuccess : Bool
• outputsFile? : Option System.FilePath
• outputsIdx : Nat
• leanOptOverrides : Lean.NameMap Lean.LeanOptions
• macosxDeploymentTarget? : Option String
• opaqueWs : OpaqueWorkspace
• leanTrace : BuildTrace
• leanIncludeDirs : Array (Option (System.FilePath × BuildTrace))
• registeredJobs : JobQueue
• outputsRef? : Option CacheRef

  Input-to-output(s) map for hashes of the tracked package's artifacts. If none, tracking outputs is disabled for this build.

• cancelTk? : Option IO.CancelToken

  Cancellation token for the build. Once the token is set, job continuations (e.g., Job.mapM / Job.bindM) error instead of scheduling new work; already-running tasks complete normally. If none, cancellation is disabled. Only the build monitor should set this token: reporting assumes that a counted failure exists when the token is set.

@[reducible, inline]

abbrev Lake.BuildT (m : Type → Type u_1) (α : Type) : Type u_1

A transformer to equip a monad with a BuildContext.

Equations

• Lake.BuildT = ReaderT Lake.BuildContext

@[reducible, inline]

abbrev Lake.MonadBuild (m : Type → Type u) : Type u

A monad equipped with a Lake build context.

Equations

• Lake.MonadBuild m = MonadReaderOf Lake.BuildContext m

@[instance_reducible]

instance Lake.instMonadLiftLakeMBuildTOfPure {m : Type → Type u_1} [Pure m] : MonadLift LakeM (BuildT m)

Equations

• Lake.instMonadLiftLakeMBuildTOfPure = { monadLift := fun {α : Type} (x : Lake.LakeM α) (ctx : Lake.BuildContext) => pure (Lake.LakeM.run ctx.toContext x) }

@[inline]

def Lake.getBuildContext {m : Type → Type u_1} [MonadBuild m] : m BuildContext

Equations

• Lake.getBuildContext = readThe Lake.BuildContext

@[inline]

def Lake.getLeanTrace {m : Type → Type u_1} [Functor m] [MonadBuild m] : m BuildTrace

Equations

• Lake.getLeanTrace = (fun (x : Lake.BuildContext) => x.leanTrace) <$> Lake.getBuildContext

@[inline]

def Lake.getBuildConfig {m : Type → Type u_1} [Functor m] [MonadBuild m] : m BuildConfig

Equations

• Lake.getBuildConfig = (fun (x : Lake.BuildContext) => x.toBuildConfig) <$> Lake.getBuildContext

@[inline]

def Lake.getIsOldMode {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

Whether to use modification times for trace checking.

Equations

• Lake.getIsOldMode = (fun (x : Lake.BuildConfig) => x.oldMode) <$> Lake.getBuildConfig

@[inline]

def Lake.getTrustHash {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

Whether to trust .hash files.

Equations

• Lake.getTrustHash = (fun (x : Lake.BuildConfig) => x.trustHash) <$> Lake.getBuildConfig

@[inline]

def Lake.getNoBuild {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

Early exit if a target has to be rebuilt.

Equations

• Lake.getNoBuild = (fun (x : Lake.BuildConfig) => x.noBuild) <$> Lake.getBuildConfig

@[inline]

def Lake.getVerbosity {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Verbosity

Verbosity level (-q, -v, or neither).

Equations

• Lake.getVerbosity = (fun (x : Lake.BuildConfig) => x.verbosity) <$> Lake.getBuildConfig

@[inline]

def Lake.getIsVerbose {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

Equations

• Lake.getIsVerbose = (fun (x : Lake.Verbosity) => x == Lake.Verbosity.verbose) <$> Lake.getVerbosity

@[inline]

def Lake.getIsQuiet {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

Equations

• Lake.getIsQuiet = (fun (x : Lake.Verbosity) => x == Lake.Verbosity.quiet) <$> Lake.getVerbosity

@[inline]

def Lake.getLeanOptOverrides {m : Type → Type u_1} [Functor m] [MonadBuild m] : m (Lean.NameMap Lean.LeanOptions)

Per-package Lean option overrides, applied to every module whose owning package's baseName appears as a key. When recFetchSetup builds module M, the LeanOptions associated with M.pkg.baseName (if any) are appended to M.leanOptions, overriding clashing entries.

Used by lake lint to inject linter.extra/linter.all into every module of a target package (so transitively-imported first-party modules capture linter-tagged warnings), without touching dependencies.

Equations

• Lake.getLeanOptOverrides = (fun (x : Lake.BuildConfig) => x.leanOptOverrides) <$> Lake.getBuildConfig

@[inline]

def Lake.getMacOSXDeploymentTarget? {m : Type → Type u_1} [Functor m] [MonadBuild m] : m (Option String)

The miniumum OS version to target on MacOS.

If a minimum is not set, linkers default the minimum to the host major version and will emit warnings if any lineed libraries (including system libraries) exceed the minium. Thus, the linker will complain when building on a system with an unset minimum and system libraries which require a higher minor version.

ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0

To silence such warnings, Lake sets this far into the future by default (e.g., 99.0). However, that itself can be wrong if a consumer of Lean library uses the minimum OS version to determine compatibility (e.g., Python does this). The far-flung version would then imply zero compatibility.

In such cases, the desired deployment target can be manually specified . Depending on the desired scope, it can be set per-target, for all targets within a buld (with this), or across all builds with the environment variable MACOSX_DEPLOYMENT_TARGET.

Equations

• Lake.getMacOSXDeploymentTarget? = (fun (x : Lake.BuildConfig) => x.macosxDeploymentTarget?) <$> Lake.getBuildConfig