diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean index febcd65b52..c6e6e424d0 100644 --- a/Lake/Build/Context.lean +++ b/Lake/Build/Context.lean @@ -19,7 +19,7 @@ namespace Lake abbrev BuildTask := OptionIOTask /-- A Lake build job. -/ -abbrev Job := BuildTask BuildTrace +abbrev Job := BuildTask Unit /-- A Lake context with some additional caching for builds. -/ structure BuildContext extends Context where diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean index fcbeabf572..c8676a8c8b 100644 --- a/Lake/Build/Imports.lean +++ b/Lake/Build/Imports.lean @@ -42,12 +42,12 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build let mods := (← getWorkspace).processImportList imports let (importTargets, bStore) ← RecBuildM.runIn {} <| mods.mapM fun mod => if mod.shouldPrecompile then - buildIndexTop mod.dynlib <&> (·.withoutInfo) + (discard ·.task) <$> buildIndexTop mod.dynlib else - buildIndexTop mod.leanBin + (discard ·.task) <$> buildIndexTop mod.leanBin let dynlibTargets := bStore.collectModuleFacetArray Module.dynlibFacet let externLibTargets := bStore.collectSharedExternLibs - importTargets.forM (·.buildOpaque) + importTargets.forM (liftM <| await ·) -- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care) let dynlibs ← dynlibTargets.mapM fun dynlib => do return FilePath.mk <| nameToSharedLib (← dynlib.build).toString diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 4058b80022..975219e990 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -102,7 +102,7 @@ export BuildInfo (build) @[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (ActiveBuildTarget α)) [h : FamilyDef Fam facet (ActiveBuildTarget α)] : FacetConfig Fam ι facet where build := cast (by rw [← h.family_key_eq_type]) build - getJob? := some (fun data => let_fun target := ofFamily data; (·.2) <$> target.task) + getJob? := some fun data => discard <| ofFamily data /-! ### Lean Executable Builds -/ diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean index 485db2c2ec..5fb0c26b34 100644 --- a/Lake/Build/Target.lean +++ b/Lake/Build/Target.lean @@ -13,81 +13,72 @@ namespace Lake /-! # Active Targets -/ -------------------------------------------------------------------------------- -structure ActiveTarget.{u,v} (ι : Type u) (k : Type u → Type v) (τ : Type u) where - task : k (ι × τ) - -instance [Inhabited ι] [Inhabited τ] [Pure k] : Inhabited (ActiveTarget ι k τ) := - ⟨⟨pure default⟩⟩ +def ActiveTarget.{u,v} (ι : Type u) (k : Type u → Type v) (τ : Type u) := + k (ι × τ) namespace ActiveTarget -def withoutInfo [Functor k] (target : ActiveTarget ι k t) : ActiveTarget PUnit k t := - mk <| (fun (_,t) => ((),t)) <$> target.task +@[inline] def mk (task : k (ι × τ)) : ActiveTarget ι k τ := + task -def «opaque» [Functor k] (task : k t) : ActiveTarget PUnit k t := +@[inline] def task (target : ActiveTarget ι k τ) : k (ι × τ) := + target + +instance [Inhabited ι] [Inhabited τ] [Pure k] : Inhabited (ActiveTarget ι k τ) := + ⟨mk <| pure default⟩ + +@[inline] def «opaque» [Functor k] (task : k t) : ActiveTarget PUnit k t := mk <| ((), ·) <$> task -protected def pure [Pure k] (info : ι) (trace : τ) : ActiveTarget ι k τ := - mk <| pure (info, trace) - -def nil [NilTrace τ] [Pure k] : ActiveTarget PUnit k τ := +@[inline] def nil [NilTrace τ] [Pure k] : ActiveTarget PUnit k τ := mk <| pure ((), nilTrace) -protected def bindSync [BindSync m n k] (self : ActiveTarget ι k α) (f : ι → α → m β) : n (k β) := - bindSync self.task fun (i, a) => f i a +@[inline] protected def bindSync [BindSync m n k] +(self : ActiveTarget ι k α) (f : ι → α → m β) : n (k β) := + bindSync self fun (i, a) => f i a -protected def bindOpaqueSync [BindSync m n k] (self : ActiveTarget ι k α) (f : α → m β) : n (k β) := - bindSync self.task fun (_, a) => f a +@[inline] protected def bindOpaqueSync [BindSync m n k] +(self : ActiveTarget ι k α) (f : α → m β) : n (k β) := + bindSync self fun (_, a) => f a -protected def bindAsync [BindAsync n k] (self : ActiveTarget ι k α) (f : ι → α → n (k β)) : n (k β) := - bindAsync self.task fun (i, a) => f i a +@[inline] protected def bindAsync [BindAsync n k] +(self : ActiveTarget ι k α) (f : ι → α → n (k β)) : n (k β) := + bindAsync self fun (i, a) => f i a -protected def bindOpaqueAsync [BindAsync n k] (self : ActiveTarget ι k α) (f : α → n (k β)) : n (k β) := - bindAsync self.task fun (_, a) => f a +@[inline] protected def bindOpaqueAsync [BindAsync n k] +(self : ActiveTarget ι k α) (f : α → n (k β)) : n (k β) := + bindAsync self fun (_, a) => f a -def materialize [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m τ := - (·.2) <$> liftM (await self.task) - -def materializeAsync [Functor k] (self : ActiveTarget ι k τ) : k τ := - (·.2) <$> self.task - -def build [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m ι := +@[inline] def build +[Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m ι := (·.1) <$> liftM (await self.task) -def buildOpaque [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m PUnit := - discard <| self.materialize +@[inline] def buildOpaque +[Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m PUnit := + discard <| liftM (await self.task) + +variable [MixTrace τ] [SeqWithAsync n k] [MonadLiftT n m] [Monad m] def mixOpaqueAsync -[MixTrace τ] [SeqWithAsync n k] [MonadLiftT n m] [Monad m] -(t1 : ActiveTarget α k τ) (t2 : ActiveTarget β k τ) : m (ActiveTarget PUnit k τ) := do - pure <| mk <| ← liftM <| seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.task t2.task +(t1 : ActiveTarget α k τ) (t2 : ActiveTarget β k τ) : m (ActiveTarget PUnit k τ) := + mk <$> liftM (seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1 t2) -section -variable [NilTrace τ] [MixTrace τ] - -def materializeList [Await k n] [MonadLiftT n m] [Monad m] (targets : List (ActiveTarget ι k τ)) : m τ := do - targets.foldlM (fun tr t => return mixTrace tr <| ← t.materialize) nilTrace - -def materializeArray [Await k n] [MonadLiftT n m] [Monad m] (targets : Array (ActiveTarget ι k τ)) : m τ := do - targets.foldlM (fun tr t => return mixTrace tr <| ← t.materialize) nilTrace - -variable [SeqWithAsync n k] [Monad n] [MonadLiftT n m] [Monad m] [Pure k] +variable [NilTrace τ] [Monad n] [Pure k] def collectList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget (List ι) k τ) := mk <$> do - liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) <| targets.map (·.task) + liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) targets def collectArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget (Array ι) k τ) := mk <$> do - liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) <| targets.map (·.task) + liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) targets variable [Functor k] def collectOpaqueList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do - liftM <| foldLeftListAsync (fun (_,t') t => mixTrace t t') nilTrace <| targets.map (·.task) + liftM <| foldLeftListAsync (fun (_,t') t => mixTrace t t') nilTrace targets def collectOpaqueArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do - liftM <| foldRightArrayAsync (fun t (_,t') => mixTrace t t') nilTrace <| targets.map (·.task) + liftM <| foldRightArrayAsync (fun t (_,t') => mixTrace t t') nilTrace targets -end end ActiveTarget -------------------------------------------------------------------------------- @@ -102,88 +93,46 @@ instance [Inhabited ι] [Inhabited τ] [Pure n] [Pure k] : Inhabited (Target ι namespace Target -def «opaque» [Functor n] [Functor k] (task : n (k τ)) : Target PUnit n k τ := - mk <| ((fun t => ((), t)) <$> ·) <$> task +@[inline] def active [Pure n] (target : ActiveTarget ι k τ) : Target ι n k τ := + mk <| pure target -def opaqueSync [Sync m n k] [Functor m] (act : m τ) : Target PUnit n k τ := - mk <| sync <| ((), ·) <$> act - -def opaqueAsync [Async m n k] [Functor m] (act : m τ) : Target PUnit n k τ := - mk <| async <| ((), ·) <$> act - -protected def sync [Sync m n k] [Functor m] (info : ι) (act : m τ) : Target ι n k τ := - mk <| sync <| (info, ·) <$> act - -protected def async [Async m n k] [Functor m] (info : ι) (act : m τ) : Target ι n k τ := - mk <| async <| (info, ·) <$> act - -def active [Pure n] (target : ActiveTarget ι k τ) : Target ι n k τ := - mk <| pure target.task - -protected def pure [Pure n] [Pure k] (info : ι) (trace : τ) : Target ι n k τ := - mk <| pure <| pure (info, trace) - -def nil [NilTrace τ] [Pure n] [Pure k] : Target PUnit n k τ := +@[inline] def nil [NilTrace τ] [Pure n] [Pure k] : Target PUnit n k τ := mk <| pure <| pure <| ((), nilTrace) -def computeSync [Functor m] [ComputeTrace ι m τ] [Sync m n k] (info : ι) : Target ι n k τ := - mk <| sync <| (info, ·) <$> ComputeTrace.computeTrace info - -def computeAsync [Functor m] [ComputeTrace ι m τ] [Async m n k] (info : ι) : Target ι n k τ := - mk <| async <| (info, ·) <$> ComputeTrace.computeTrace info - -def activate [Functor n] (self : Target ι n k τ) : n (ActiveTarget ι k τ) := +@[inline] def activate [Functor n] (self : Target ι n k τ) : n (ActiveTarget ι k τ) := (.mk ·) <$> self.task -def materializeAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k τ) := +@[inline] def materializeAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k τ) := ((·.2) <$> ·) <$> self.task def materialize [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m τ := liftM self.task >>= fun t => (·.2) <$> liftM (await t) -def build [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m ι := - liftM self.task >>= fun t => (·.1) <$> liftM (await t) - -def buildOpaque [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m PUnit := - discard self.materialize - -def buildAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k ι) := - ((·.1) <$> ·) <$> self.task - -def buildOpaqueAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k PUnit) := - discard <$> self.task - -protected def bindSync [BindSync m n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → m β) : n (k β) := +@[inline] protected def bindSync [BindSync m n k] [Bind n] +(self : Target ι n k τ) (f : ι → τ → m β) : n (k β) := self.task >>= fun tk => bindSync tk fun (i,t) => f i t -protected def bindOpaqueSync [BindSync m n k] [Bind n] (self : Target ι n k τ) (f : τ → m β) : n (k β) := +@[inline] protected def bindOpaqueSync +[BindSync m n k] [Bind n] (self : Target ι n k τ) (f : τ → m β) : n (k β) := self.task >>= fun tk => bindSync tk fun (_,t) => f t -protected def bindAsync [BindAsync n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → n (k β)) : n (k β) := +@[inline] protected def bindAsync +[BindAsync n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → n (k β)) : n (k β) := self.task >>= fun tk => bindAsync tk fun (i,t) => f i t -protected def bindOpaqueAsync [BindAsync n k] [Bind n] (self : Target ι n k τ) (f : τ → n (k β)) : n (k β) := +@[inline] protected def bindOpaqueAsync +[BindAsync n k] [Bind n] (self : Target ι n k τ) (f : τ → n (k β)) : n (k β) := self.task >>= fun tk => bindAsync tk fun (_,t) => f t def mixOpaqueAsync [MixTrace τ] [SeqWithAsync n k] [Functor k] [Monad n] -(t1 : Target α n k τ) (t2 : Target β n k τ) : Target PUnit n k τ := - mk do - let tk1 ← t1.materializeAsync - let tk2 ← t2.materializeAsync - ((fun t => ((),t)) <$> ·) <$> seqWithAsync mixTrace tk1 tk2 +(t1 : Target α n k τ) (t2 : Target β n k τ) : Target PUnit n k τ := mk do + let tk1 ← t1.materializeAsync + let tk2 ← t2.materializeAsync + ((fun t => ((),t)) <$> ·) <$> seqWithAsync mixTrace tk1 tk2 section variable [NilTrace τ] [MixTrace τ] - -def materializeList [Await k m] [MonadLiftT n m] [Monad m] (targets : List (Target ι n k τ)) : m τ := do - let tasks ← targets.mapM (·.task) - tasks.foldlM (fun tr τ => return mixTrace tr (← liftM <| await τ).2) nilTrace - -def materializeArray [Await k m] [MonadLiftT n m] [Monad m] (targets : Array (Target ι n k τ)) : m τ := do - let tasks ← targets.mapM (·.task) - tasks.foldlM (fun tr τ => return mixTrace tr (← liftM <| await τ).2) nilTrace - variable [SeqWithAsync n' k] [Monad n'] [MonadLiftT n' n] [Monad n] [Pure k] [Functor k] def materializeListAsync (targets : List (Target ι n k τ)) : n (k τ) := do @@ -192,15 +141,15 @@ def materializeListAsync (targets : List (Target ι n k τ)) : n (k τ) := do def materializeArrayAsync (targets : Array (Target ι n k τ)) : n (k τ) := do liftM <| foldRightArrayAsync mixTrace nilTrace (← targets.mapM (·.materializeAsync)) -def collectList (targets : List (Target ι n k τ)) : Target (List ι) n k τ := - mk do - let tasks ← targets.mapM (·.task) - liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) tasks +def collectList (targets : List (Target ι n k τ)) : Target (List ι) n k τ := mk do + let tasks ← targets.mapM (·.task) + let f := fun (i,t') (a,t) => (i :: a, mixTrace t t') + liftM <| foldLeftListAsync f ([], nilTrace) tasks -def collectArray (targets : Array (Target ι n k τ)) : Target (Array ι) n k τ := - mk do - let tasks ← targets.mapM (·.task) - liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) tasks +def collectArray (targets : Array (Target ι n k τ)) : Target (Array ι) n k τ := mk do + let tasks ← targets.mapM (·.task) + let f := fun (a,t) (i,t') => (a.push i, mixTrace t t') + liftM <| foldRightArrayAsync f (#[], nilTrace) tasks def collectOpaqueList (targets : List (Target ι n k τ)) : Target PUnit n k τ := mk <| ((fun t => ((), t)) <$> ·) <$> materializeListAsync targets diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean index a802a0fd29..1731e1a275 100644 --- a/Lake/Build/TargetTypes.lean +++ b/Lake/Build/TargetTypes.lean @@ -73,16 +73,3 @@ abbrev OpaqueTarget := BuildTarget Unit /-- An `ActiveBuildTarget` with no artifact information. -/ abbrev ActiveOpaqueTarget := ActiveBuildTarget Unit - -namespace OpaqueTarget - -abbrev mk (task : SchedulerM Job) : OpaqueTarget := - Target.opaque task - -abbrev mk' (task : BuildM Job) : OpaqueTarget := - Target.opaque <| task.catchFailure fun _ => pure failure - -abbrev async (act : BuildM BuildTrace) : OpaqueTarget := - Target.opaqueAsync act - -end OpaqueTarget diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 89350a35a3..31ecf74c33 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -17,7 +17,7 @@ structure BuildSpec where /-- Get the `Job` associated with some `ActiveBuildTarget` `BuildData`. -/ @[inline] def BuildData.toJob [FamilyDef BuildData k (ActiveBuildTarget α)] (data : BuildData k) : Job := - ofFamily data |>.materializeAsync + discard <| ofFamily data @[inline] def mkBuildSpec (info : BuildInfo) [FamilyDef BuildData info.key (ActiveBuildTarget α)] : BuildSpec :=