diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index 78aa195be3..47809013e0 100644 --- a/Lake/BuildBin.lean +++ b/Lake/BuildBin.lean @@ -12,7 +12,7 @@ namespace Lake def buildLeanO (oFile : FilePath) (cTarget : ActiveBuildTarget t FilePath) (leancArgs : Array String := #[]) : IO BuildTask := - afterTarget cTarget <| compileLeanO oFile cTarget.artifact leancArgs + cTarget >> compileLeanO oFile cTarget.artifact leancArgs def fetchLeanOFileTarget (oFile : FilePath) (cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO ActiveFileTarget := diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index 82d213995d..2e0913d3df 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -88,21 +88,21 @@ def nil [Inhabited t] : ActiveBuildTarget t PUnit := def materialize (self : ActiveBuildTarget t α) : IO PUnit := self.task.await -end ActiveBuildTarget +-- ### Combinators --- ## Combinators - -def afterTarget (target : ActiveBuildTarget t a) (act : IO PUnit) : IO BuildTask := +def after (target : ActiveBuildTarget t a) (act : IO PUnit) : IO BuildTask := afterTask target.task act -def afterTargetList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO BuildTask := +def afterList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO BuildTask := afterTaskList (targets.map (·.task)) act instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO BuildTask) := - ⟨afterTarget⟩ + ⟨ActiveBuildTarget.after⟩ instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO BuildTask) := - ⟨afterTargetList⟩ + ⟨ActiveBuildTarget.afterList⟩ + +end ActiveBuildTarget -------------------------------------------------------------------------------- -- # File Targets