structure Lake.BuildConfig : Type

Configuration options for a Lake build.

• oldMode : Bool

  Use modification times for trace checking.

• trustHash : Bool

  Whether to trust .hash files.

• noBuild : Bool

  Early exit if a target has to be rebuilt.

• verbosity : Verbosity

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

• failLv : LogLevel

  Fail the top-level build if entries of at least this level have been logged.

  Unlike some build systems, this does NOT convert such log entries to errors, and it does not abort jobs when warnings are logged (i.e., dependent jobs will still continue unimpeded).

• outLv : LogLevel

  The minimum log level for an log entry to be reported.

• out : OutStream

  The stream to which Lake reports build progress. By default, Lake uses stderr.

• ansiMode : AnsiMode

  Whether to use ANSI escape codes in build output.

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)

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

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

• oldMode : Bool
• trustHash : Bool
• noBuild : Bool
• verbosity : Verbosity
• failLv : LogLevel
• outLv : LogLevel
• out : OutStream
• ansiMode : AnsiMode
• opaqueWs : OpaqueWorkspace
• leanTrace : BuildTrace
• registeredJobs : IO.Ref (Array OpaqueJob)

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

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

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

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

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