ec8b351445
* add `def OptionIO := EIO PUnit` * add `OptionIOTask` for `OptionIO` * rename `BuildCoreM` -> `BuildIO` * rename `Util.LogT` -> `Util.Log` * generalize `error` to `MonadError` * generalize` Cli.build`
35 lines
913 B
Text
35 lines
913 B
Text
/-
|
||
Copyright (c) 2021 Mac Malone. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Mac Malone
|
||
-/
|
||
import Lake.Util.Task
|
||
import Lake.Config.InstallPath
|
||
import Lake.Config.OpaquePackage
|
||
import Lake.Build.Trace
|
||
import Lake.Build.IO
|
||
|
||
open System
|
||
namespace Lake
|
||
|
||
structure BuildContext where
|
||
package : OpaquePackage
|
||
leanInstall : LeanInstall
|
||
lakeInstall : LakeInstall
|
||
leanTrace : BuildTrace
|
||
|
||
abbrev BuildM :=
|
||
ReaderT BuildContext BuildIO
|
||
|
||
/-- `Task` type for `BuildM`/`BuildIO`. -/
|
||
abbrev BuildTask :=
|
||
OptionIOTask
|
||
|
||
def BuildM.run (logMethods : LogMethods BaseIO) (ctx : BuildContext) (self : BuildM α) : IO α :=
|
||
self ctx |>.run logMethods
|
||
|
||
def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
|
||
| Except.ok a => a
|
||
| Except.error cycle => do
|
||
let cycle := cycle.map (s!" {·}")
|
||
error s!"build cycle detected:\n{"\n".intercalate cycle}"
|