def Lake.noBuildCode : Lake.ExitCode

Exit code to return if --no-build is set and a build is required.

Equations

• Lake.noBuildCode = 3

structure Lake.BuildConfig : Type

Configuration options for a Lake build.

• oldMode : Bool
• trustHash : Bool
• noBuild : Bool

  Early exit if a target has to be rebuilt.

• verbosity : Lake.Verbosity
• failIfWarnings : Bool

  Fail the top-level build if warnings have been logged. Unlike some build systems, this does NOT convert warnings to errors, and it does not abort jobs when warnings are logged (i.e., dependent jobs will still continue unimpeded).

• useStdout : Bool

  Report build output on stdout. Otherwise, Lake uses stderr.

@[reducible, inline]

abbrev Lake.JobResult (α : Type u_1) : Type u_1

Equations

• Lake.JobResult α = Lake.EResult Nat Lake.Log α

@[reducible, inline]

abbrev Lake.JobTask (α : Type u_1) : Type u_1

Equations

• Lake.JobTask α = Lake.BaseIOTask (Lake.JobResult α)

structure Lake.Job (α : Type u) : Type u

A Lake job.

• task : Lake.JobTask α

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 : Lake.Verbosity
• failIfWarnings : Bool
• useStdout : Bool
• opaqueWs : Lake.OpaqueWorkspace
• leanTrace : Lake.BuildTrace
• registeredJobs : IO.Ref (Array (String × Lake.Job Unit))

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

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

Equations

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

@[inline]

def Lake.getLeanTrace {m : Type → Type u_1} [Monad m] : Lake.BuildT m Lake.BuildTrace

Equations

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

@[inline]

def Lake.getBuildConfig {m : Type → Type u_1} [Monad m] : Lake.BuildT m Lake.BuildConfig

Equations

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

@[inline]

def Lake.getIsOldMode {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

Equations

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

@[inline]

def Lake.getTrustHash {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

Equations

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

@[inline]

def Lake.getNoBuild {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

Equations

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

@[inline]

def Lake.getVerbosity {m : Type → Type u_1} [Monad m] : Lake.BuildT m Lake.Verbosity

Equations

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

@[inline]

def Lake.getIsVerbose {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

Equations

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

@[inline]

def Lake.getIsQuiet {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

Equations

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

@[reducible, inline]

abbrev Lake.CoreBuildM (α : Type) : Type

The internal core monad of Lake builds. Not intended for user use.

Equations

• Lake.CoreBuildM = Lake.BuildT Lake.LogIO

@[reducible, inline]

abbrev Lake.JobM (α : Type) : Type

The monad of asynchronous Lake jobs.

Equations

• Lake.JobM = Lake.CoreBuildM

@[reducible, inline]

abbrev Lake.SpawnM (α : Type) : Type

The monad used to spawn asynchronous Lake build jobs. Lifts into FetchM.

Equations

• Lake.SpawnM = Lake.BuildT BaseIO

@[reducible, inline, deprecated Lake.SpawnM]

abbrev Lake.SchedulerM (α : Type) : Type

The monad used to spawn asynchronous Lake build jobs. Replaced by SpawnM.

Equations

• Lake.SchedulerM = Lake.SpawnM