From 7199eea687b70b0c8adde4a6acae59f4124b6152 Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 14 Dec 2021 14:12:43 -0500 Subject: [PATCH] refactor: cleanup/improve Target utils --- Lake/Build/Module.lean | 8 +++---- Lake/Build/Package.lean | 10 ++++----- Lake/Build/Target.lean | 43 +++++++++++++++++++++++++------------ Lake/Build/TargetTypes.lean | 6 ++++++ 4 files changed, 44 insertions(+), 23 deletions(-) diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 99c21a1845..b5c54866da 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -82,8 +82,8 @@ abbrev cTarget (self : ActiveOleanAndCTarget) := self.info.cTarget end ActiveOleanAndCTarget -def OleanAndCTarget.run' (self : OleanAndCTarget) : BuildM ActiveOleanAndCTarget := do - let t ← self.run +def OleanAndCTarget.activate (self : OleanAndCTarget) : BuildM ActiveOleanAndCTarget := do + let t ← Target.activate self let oleanTask ← t.mapAsync fun info depTrace => do return mixTrace (← computeTrace info.oleanFile) depTrace let cTask ← t.mapAsync fun info _ => do @@ -174,7 +174,7 @@ def recBuildModuleOleanAndCTargetWithLocalImports recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do let importTarget ← ActiveTarget.collectOpaqueList <| importTargets.map (·.oleanTarget) let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget - pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.run' + pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.activate def recBuildModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x) @@ -182,7 +182,7 @@ def recBuildModuleOleanTargetWithLocalImports recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do let importTarget ← ActiveTarget.collectOpaqueList importTargets let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget - pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.run + pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.activate -- ## Definitions diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index 55affae456..50d5873dcb 100644 --- a/Lake/Build/Package.lean +++ b/Lake/Build/Package.lean @@ -18,7 +18,7 @@ namespace Lake /-- Build the `extraDepTarget` of all dependent packages into a single target. -/ protected def Package.buildExtraDepsTarget (self : Package) : BuildM ActiveOpaqueTarget := do let collect pkg depTargets := do - let extraDepTarget ← self.extraDepTarget.run + let extraDepTarget ← self.extraDepTarget.activate let depTarget ← ActiveTarget.collectOpaqueArray depTargets extraDepTarget.mixOpaqueAsync depTarget let build dep recurse := do @@ -32,7 +32,7 @@ protected def Package.buildExtraDepsTarget (self : Package) : BuildM ActiveOpaqu /-- Build the `extraDepTarget` of all workspace packages into a single target. -/ def buildExtraDepsTarget : BuildM ActiveOpaqueTarget := do ActiveTarget.collectOpaqueArray <| ← do - (← getWorkspace).packageArray.mapM (·.extraDepTarget.run) + (← getWorkspace).packageArray.mapM (·.extraDepTarget.activate) -- # Build Package Modules @@ -121,15 +121,15 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build let depTarget ← self.buildExtraDepsTarget if imports.isEmpty then -- wait for deps to finish building - depTarget.build + depTarget.buildOpaque else -- build local imports from list let infos := (← getWorkspace).processImportList imports if self.defaultFacet == PackageFacet.oleans then let build := recBuildModuleOleanTargetWithLocalImports depTarget let targets ← buildModuleArray infos build - targets.forM (·.build) + targets.forM (·.buildOpaque) else let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget let targets ← buildModuleArray infos build - targets.forM (·.build) + targets.forM (·.buildOpaque) diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean index 1f141f84f9..b4e1f76ee1 100644 --- a/Lake/Build/Target.lean +++ b/Lake/Build/Target.lean @@ -52,13 +52,13 @@ protected def bindAsync [BindAsync n k] [MonadLiftT n m] (self : ActiveTarget i protected def bindOpaqueAsync [BindAsync n k] [MonadLiftT n m] (self : ActiveTarget i k α) (f : α → n (k β)) : m (k β) := liftM <| bindAsync self.task f -def materializeAsync [Pure m] (self : ActiveTarget i k t) : m (k t) := - pure self.task - def materialize [Await k m'] [MonadLiftT m' m] (self : ActiveTarget i k t) : m t := liftM <| await self.task -def build [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m PUnit := +def build [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m i := + Functor.mapConst self.info self.materialize + +def buildOpaque [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m PUnit := discard <| self.materialize def mixOpaqueAsync @@ -117,6 +117,12 @@ def withTask (task : m' (k' t')) (self : Target i m k t) : Target i m' k' t' := def opaque (task : m (k t)) : Target PUnit m k t := mk () task +def opaqueAsync [Async m n k] [MonadLiftT n n'] (act : m t) : Target PUnit n' k t := + mk () (liftM <| async act) + +protected def async [Async m n k] [MonadLiftT n n'] (info : i) (act : m t) : Target i n' k t := + mk info (liftM <| async act) + def active [Pure m] (target : ActiveTarget i k t) : Target i m k t := mk target.info <| pure target.task @@ -132,9 +138,27 @@ def computeSync [ComputeTrace i m' t] [MonadLiftT m' m] [Functor m] [Pure k] (in def computeAsync [ComputeTrace i m' t] [MonadLiftT m' m] [Async m n k] [MonadLiftT n m] (info : i) : Target i m k t := mk info <| liftM <| async <| liftM (n := m) <| ComputeTrace.computeTrace info -def run [Monad m] (self : Target i m k t) : m (ActiveTarget i k t) := +def activate [Functor m] (self : Target i m k t) : m (ActiveTarget i k t) := Functor.map (fun t => ActiveTarget.mk self.info t) self.task +def materializeAsync (self : Target i m k t) : m (k t) := + self.task + +def materialize [Await k n] [MonadLiftT n m] [Bind m] (self : Target i m k t) : m t := do + self.task >>= (liftM ∘ await) + +def build [Await k n] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i m k t) : m i := do + Functor.mapConst self.info self.materialize + +def buildOpaque [Await k n] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i m k t) : m PUnit := do + discard self.materialize + +def buildAsync [Functor m] [Functor k] (self : Target i m k t) : m (k i) := + Functor.mapConst self.info <$> self.task + +def buildOpaqueAsync [Functor m] [Functor k] (self : Target i m k t) : m (k PUnit) := + discard <$> self.task + protected def mapAsync [BindAsync' m n k] [MonadLiftT n m] [Bind m] (self : Target i m k α) (f : i → α → m β) : m (k β) := self.task >>= fun tk => liftM <| bindAsync' tk (f self.info) @@ -147,15 +171,6 @@ protected def bindAsync [BindAsync n k] [MonadLiftT n m] [Bind m] (self : Target protected def bindOpaqueAsync [BindAsync n k] [MonadLiftT n m] [Bind m] (self : Target i m k α) (f : α → n (k β)) : m (k β) := self.task >>= fun tk => liftM <| bindAsync tk f -def materializeAsync (self : Target i m k t) : m (k t) := - self.task - -def materialize [Await k n] [MonadLiftT n m] [Bind m] (self : Target i m k t) : m t := do - self.task >>= (liftM ∘ await) - -def build [Await k n] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i m k t) : m i := do - Functor.mapConst self.info self.materialize - def mixOpaqueAsync [MixTrace t] [SeqMapAsync n k] [MonadLiftT n m] [Monad m] (t1 : Target α m k t) (t2 : Target β m k t) : Target PUnit m k t := diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean index 07e1e30026..a6a5b6b479 100644 --- a/Lake/Build/TargetTypes.lean +++ b/Lake/Build/TargetTypes.lean @@ -40,6 +40,12 @@ abbrev ActiveFileTarget := ActiveBuildTarget FilePath /-- A `BuildTarget` with no artifact information. -/ abbrev OpaqueTarget := BuildTarget PUnit +@[inline] def OpaqueTarget.mk (act : BuildM (BuildTask BuildTrace)) : OpaqueTarget := + Target.opaque act + +@[inline] def OpaqueTarget.async (act : BuildM BuildTrace) : OpaqueTarget := + Target.opaqueAsync act + -- ## Active /-- An `ActiveBuildTarget` with no artifact information. -/