From b8e85f40cdfe923ac257e27ee789ceddf08754b0 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 1 Aug 2021 15:40:11 -0400 Subject: [PATCH] refactor: move `afterTarget*` into `ActiveBuildTarget` --- Lake/BuildBin.lean | 2 +- Lake/BuildTarget.lean | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) 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