diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean index 6ac551290b..255c31fe86 100644 --- a/Lake/BuildMonad.lean +++ b/Lake/BuildMonad.lean @@ -5,6 +5,7 @@ Authors: Mac Malone -/ import Lake.Task import Lake.Trace +import Lake.RealM import Lake.LogMonad import Lake.InstallPath @@ -21,7 +22,8 @@ structure BuildContext where lakeInstall : LakeInstall deriving Inhabited -abbrev BuildM := ReaderT BuildContext <| LogT <| IO +abbrev BuildCoreM := LogT <| EIO PUnit +abbrev BuildM := ReaderT BuildContext BuildCoreM -------------------------------------------------------------------------------- -- # Build Monad Utilities @@ -45,31 +47,80 @@ def getLeanc : BuildM FilePath := def getLakeInstall : BuildM LakeInstall := (·.lakeInstall) <$> read -namespace BuildM +namespace BuildCoreM -def convErrors (self : BuildM α) : BuildM α := do - try self catch e => - /- - Remark: Actual error should have already been logged earlier. - However, if the error was thrown by something that did not know it was - in `BuildM` (e.g., a general `Target`), it may have not been. +def run (logMethods : LogMethods (EIO PUnit)) (self : BuildCoreM α) : IO α := + ReaderT.run self logMethods |>.toIO fun _ => IO.userError "build failed" - TODO: Use an `OptionT` in `BuildM` to properly record build failures. - -/ - logError s!"build error: {toString e}" - throw <| IO.userError "build failed" +def runWith (logMethods : LogMethods (EIO PUnit)) (self : BuildCoreM α) : EIO PUnit α := + ReaderT.run self logMethods -def run (logMethods : LogMethods IO) (ctx : BuildContext) (self : BuildM α) : IO α := - (convErrors self) ctx logMethods +protected def failure : BuildCoreM α := + throw () -end BuildM +protected def orElse (self : BuildCoreM α) (f : Unit → BuildCoreM α) : BuildCoreM α := + tryCatch self f + +instance : Alternative BuildCoreM where + failure := BuildCoreM.failure + orElse := BuildCoreM.orElse + +def runIO (x : IO α) : BuildCoreM α := do + match (← RealM.runIO' x) with + | Except.ok a => pure a + | Except.error e => do + logError (toString e) + failure + +instance : MonadLift IO BuildCoreM := ⟨runIO⟩ + +end BuildCoreM + +def BuildM.run (logMethods : LogMethods (EIO PUnit)) (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!" {·}") - let msg := s!"build cycle detected:\n{"\n".intercalate cycle}" - logError msg - throw <| IO.userError msg + logError s!"build cycle detected:\n{"\n".intercalate cycle}" + failure +/-- TODO: Replace with an `EIOTask PUnit` once Lean supports such a thing. -/ abbrev BuildTask := IOTask + +namespace BuildTask + +def spawn (act : BuildCoreM α) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask α) := + fun meths => BuildCoreM.runWith meths do IO.asTask (act.run meths) prio + +instance : Async BuildCoreM BuildTask := ⟨spawn⟩ + +protected def await (self : BuildTask α) : BuildCoreM α := do + match (← IO.wait self) with + | Except.ok a => pure a + | Except.error e => logError (toString e); failure + +instance : Await BuildTask BuildCoreM := ⟨BuildTask.await⟩ + +protected def mapAsync (f : α → BuildCoreM β) (self : BuildTask α) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask β) := + fun meths => BuildCoreM.runWith meths do self.mapAsync (fun a => f a |>.run meths) prio + +instance : MapAsync BuildCoreM BuildTask := ⟨BuildTask.mapAsync⟩ + +protected def bindAsync (self : BuildTask α) (f : α → BuildCoreM (BuildTask β)) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask β) := + fun meths => BuildCoreM.runWith meths do self.bindAsync (fun a => f a |>.run meths) prio + +instance : BindAsync BuildCoreM BuildTask := ⟨BuildTask.bindAsync⟩ + +protected def seqLeftAsync (self : BuildTask α) (act : BuildCoreM β) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask α) := + fun meths => BuildCoreM.runWith meths do self.seqLeftAsync (act.run meths) prio + +instance : SeqLeftAsync BuildCoreM BuildTask := ⟨BuildTask.seqLeftAsync⟩ + +protected def seqRightAsync (self : BuildTask α) (act : BuildCoreM β) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask β) := + fun meths => BuildCoreM.runWith meths do self.seqRightAsync (act.run meths) prio + +instance : SeqRightAsync BuildCoreM BuildTask := ⟨BuildTask.seqRightAsync⟩ + +end BuildTask diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index a467d4cc0d..c99157282f 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -28,20 +28,6 @@ abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace /-- A `BuildTarget` that produces a file. -/ abbrev FileTarget := BuildTarget FilePath -namespace FileTarget - -variable [ComputeTrace FilePath m BuildTrace] [MonadLiftT m BuildM] - -def computeSync (path : FilePath) : FileTarget := - Target.mk path do pure <$> try computeTrace path catch e => - logError (toString e); throw e - -def computeAsync (path : FilePath) : FileTarget := - Target.mk path do async <| try computeTrace path catch e => - logError (toString e); throw e - -end FileTarget - -- ## Active /-- An `ActiveBuildTarget` that produces a file. -/ diff --git a/Lake/BuildTargets.lean b/Lake/BuildTargets.lean index f25040904a..ddf08b4262 100644 --- a/Lake/BuildTargets.lean +++ b/Lake/BuildTargets.lean @@ -11,7 +11,9 @@ namespace Lake -- # General Utilities -def inputFileTarget := FileTarget.computeAsync +def inputFileTarget (path : FilePath) : FileTarget := + Target.computeAsync path + instance : Coe FilePath FileTarget := ⟨inputFileTarget⟩ def buildFileUnlessUpToDate (file : FilePath) diff --git a/Lake/Compile.lean b/Lake/Compile.lean index 5346890bf5..9d3ae1b77e 100644 --- a/Lake/Compile.lean +++ b/Lake/Compile.lean @@ -9,8 +9,7 @@ namespace Lake open System def createParentDirs (path : FilePath) : BuildM PUnit := do - if let some dir := path.parent then - try IO.FS.createDirAll dir catch e => logError (toString e) + if let some dir := path.parent then IO.FS.createDirAll dir def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do let envStr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} " @@ -21,10 +20,9 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do | none => cmdStr let child ← IO.Process.spawn args let exitCode ← child.wait - if exitCode != 0 then - let msg := s!"external command {args.cmd} exited with status {exitCode}" - logError msg -- log errors early - throw <| IO.userError msg + if exitCode != 0 then -- log errors early + logError s!"external command {args.cmd} exited with status {exitCode}" + failure def compileOlean (leanFile oleanFile : FilePath) (oleanDirs : List FilePath := []) (rootDir : FilePath := ".") diff --git a/Lake/LogMonad.lean b/Lake/LogMonad.lean index 16941f5935..853ab04395 100644 --- a/Lake/LogMonad.lean +++ b/Lake/LogMonad.lean @@ -3,6 +3,8 @@ 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.RealM + namespace Lake -- # Typeclass @@ -33,15 +35,15 @@ def nop [Pure m] : LogMethods m := instance [Pure m] : Inhabited (LogMethods m) := ⟨LogMethods.nop⟩ -def io : LogMethods IO where - logInfo msg := IO.println msg - logWarning msg := IO.eprintln s!"warning: {msg}" - logError msg := IO.eprintln s!"error: {msg}" +def io [MonadLiftT RealM m] : LogMethods m where + logInfo msg := RealM.runIO_ <| IO.println msg + logWarning msg := RealM.runIO_ <| IO.eprintln s!"warning: {msg}" + logError msg := RealM.runIO_ <| IO.eprintln s!"error: {msg}" -def eio : LogMethods IO where - logInfo msg := IO.eprintln s!"info: {msg}" - logWarning msg := IO.eprintln s!"warning: {msg}" - logError msg := IO.eprintln s!"error: {msg}" +def eio [MonadLiftT RealM m] : LogMethods m where + logInfo msg := RealM.runIO_ <| IO.eprintln s!"info: {msg}" + logWarning msg := RealM.runIO_ <| IO.eprintln s!"warning: {msg}" + logError msg := RealM.runIO_ <| IO.eprintln s!"error: {msg}" end LogMethods @@ -58,5 +60,15 @@ instance [Monad m] : MonadLog (LogT m) where logWarning msg := do (← read).logWarning msg logError msg := do (← read).logError msg -def LogT.adaptMethods [Monad m] (f : LogMethods m → LogMethods m) (self : LogT m α) : LogT m α := +namespace LogT + +abbrev run (methods : LogMethods m) (self : LogT m α) : m α := + ReaderT.run self methods + +abbrev runWith (methods : LogMethods m) (self : LogT m α) : m α := + ReaderT.run self methods + +abbrev adaptMethods [Monad m] (f : LogMethods m → LogMethods m) (self : LogT m α) : LogT m α := ReaderT.adapt f self + +end LogT diff --git a/Lake/RealM.lean b/Lake/RealM.lean new file mode 100644 index 0000000000..384db53b87 --- /dev/null +++ b/Lake/RealM.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +namespace Lake + +/-- An `IO`/`EIO` monad that can't error. -/ +def RealM := EIO Empty + +instance : Monad RealM := inferInstanceAs (Monad (EIO Empty)) +instance [Inhabited α] : Inhabited (RealM α) := inferInstanceAs (Inhabited (EIO Empty α)) + +namespace RealM + +abbrev run (self : RealM α) : EIO Empty α := + self + +def toEIO (self : RealM α) : EIO ε α := + fun s => match self s with + | EStateM.Result.ok a s => EStateM.Result.ok a s + +instance : MonadLift RealM (EIO ε) := ⟨toEIO⟩ + +abbrev toIO (self : RealM α) : IO α := + self.toEIO + +def runEIO (f : ε → RealM α) (x : EIO ε α) : RealM α := + x.catchExceptions f + +abbrev runIO (f : IO.Error → RealM α) (x : IO α) : RealM α := + runEIO f x + +def runEIO' (x : EIO ε α) : RealM (Except ε α) := + fun s => match x s with + | EStateM.Result.ok a s => EStateM.Result.ok (Except.ok a) s + | EStateM.Result.error e s => EStateM.Result.ok (Except.error e) s + +abbrev runIO' (x : IO α) : RealM (Except IO.Error α) := + runEIO' x + +def runEIO_ (x : EIO ε α) : RealM PUnit := + fun s => match x s with + | EStateM.Result.ok a s => EStateM.Result.ok () s + | EStateM.Result.error e s => EStateM.Result.ok () s + +abbrev runIO_ (x : IO α) : RealM PUnit := + runEIO_ x