structure Lake.BuildConfig : Type

• oldMode : Bool
• trustHash : Bool

Configuration options for a Lake build.

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

• oldMode : Bool
• trustHash : Bool
• opaqueWs : Lake.OpaqueWorkspace
• leanTrace : Lake.BuildTrace
• startedBuilds : IO.Ref Nat
• finishedBuilds : IO.Ref Nat

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

@[inline, reducible]

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

@[inline]

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

Equations

• Lake.getLeanTrace = (fun x => 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 => 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 => x.oldMode) <$> Lake.getBuildConfig

@[inline]

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

Equations

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

@[inline, reducible]

abbrev Lake.SchedulerM (α : Type) : Type

The monad for the Lake build manager.

Equations

• Lake.SchedulerM = Lake.BuildT (Lake.LogT BaseIO)

@[inline, reducible]

abbrev Lake.BuildM (α : Type) : Type

The core monad for Lake builds.

Equations

• Lake.BuildM = Lake.BuildT Lake.LogIO

@[inline, reducible]

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

A transformer to equip a monad with a Lake build store.

Equations

• Lake.BuildStoreT = StateT Lake.BuildStore

@[inline, reducible]

abbrev Lake.BuildCycle : Type

A Lake build cycle.

Equations

• Lake.BuildCycle = Lake.Cycle Lake.BuildKey

@[inline, reducible]

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

A transformer for monads that may encounter a build cycle.

Equations

• Lake.BuildCycleT = Lake.CycleT Lake.BuildKey

@[inline, reducible]

abbrev Lake.RecBuildM (α : Type) : Type

A recursive build of a Lake build store that may encounter a cycle.

Equations

• Lake.RecBuildM = Lake.BuildCycleT (Lake.BuildStoreT Lake.BuildM)

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

Equations

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

@[inline]

def Lake.BuildM.run {α : Type} (ctx : Lake.BuildContext) (self : Lake.BuildM α) : Lake.LogIO α

Equations

• Lake.BuildM.run ctx self = self ctx

def Lake.BuildM.catchFailure {α : Type} (f : Unit → BaseIO α) (self : Lake.BuildM α) : Lake.SchedulerM α

Equations

• Lake.BuildM.catchFailure f self ctx logMethods = Lake.OptionIO.catchFailure f (self ctx logMethods)

def Lake.logStep (message : String) : Lake.BuildM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.createParentDirs (path : Lake.FilePath) : IO Unit

Equations

• Lake.createParentDirs path = match System.FilePath.parent path with | some dir => IO.FS.createDirAll dir | x => pure PUnit.unit