From 43d1dfe72c089bf28fbd977a01a23a58baa4bf3d Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 21 Aug 2021 23:52:34 -0400 Subject: [PATCH] refactor: cleanup opaque target interfaces --- Lake/Async.lean | 3 ++ Lake/BuildModule.lean | 12 +++---- Lake/BuildPackage.lean | 28 ++++++++------- Lake/BuildTarget.lean | 79 +++++++++++++++++++++++++++++++++--------- Lake/Package.lean | 6 ++-- Lake/Target.lean | 66 ++++++++++++++++++++++++++--------- 6 files changed, 139 insertions(+), 55 deletions(-) diff --git a/Lake/Async.lean b/Lake/Async.lean index 0ad823408e..836f3d5e80 100644 --- a/Lake/Async.lean +++ b/Lake/Async.lean @@ -74,6 +74,9 @@ instance [SeqRightAsync m n] : SeqRightAsync (ReaderT ρ m) n where -- # List/Array Utilities -------------------------------------------------------------------------------- +def andThenAsync [Pure m] [BindAsync m n] (ta : n α) (tb : n β) : m (n β) := + bindAsync ta fun _ => pure tb + -- ## Sequencing Lists/Arrays of Asynchronous Tasks section diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index d2c4704b81..0df6c5e7bb 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -62,14 +62,14 @@ def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) : /- Produces a recursive module target fetcher that - builds the target module after waiting for `depsTarget` to materialize + builds the target module after waiting for `depTargets` to materialize and recursively fetching its local imports (relative to `pkg`). The module is built with the configuration from `pkg` and a `LEAN_PATH` that includes `oleanDirs`. -/ def fetchModuleWithLocalImports -(pkg : Package) (oleanDirs : List FilePath) (depsTarget : ActiveBuildTarget PUnit) +(pkg : Package) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) {m} [Monad m] [MonadLiftT BuildM m] [MonadExceptOf IO.Error m] : RecFetch Name ModuleTarget m := have : MonadLift BuildM m := ⟨liftM⟩ let leanPath := SearchPath.toString <| pkg.oleanDir :: oleanDirs @@ -85,8 +85,8 @@ def fetchModuleWithLocalImports -- calculate trace let leanMTime ← getMTime leanFile let leanHash := Hash.compute contents - let depTrace := depsTarget.trace.mix <| - mixTraceList <| importTargets.map (·.trace) + let depTrace := mixTrace depTarget.trace + (mixTraceList <| importTargets.map (·.trace)) let maxMTime := max leanMTime depTrace.mtime let fullHash := Hash.mix leanHash depTrace.hash let hashFile := pkg.modToHashFile mod @@ -95,9 +95,9 @@ def fetchModuleWithLocalImports -- construct target let cFile := pkg.modToC mod let oleanFile := pkg.modToOlean mod - let importTasks := importTargets.map (·.task) + let depTasks := depTarget.task :: importTargets.map (·.task) ActiveTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ← - skipIf sameHash <| afterTaskList (m := BuildM) (depsTarget.task :: importTasks) do + skipIf sameHash <| afterTaskList (m := BuildM) depTasks do compileOleanAndC leanFile oleanFile cFile leanPath pkg.rootDir pkg.leanArgs IO.FS.writeFile hashFile fullHash.toString diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index 01f20ab14b..fed4bdae93 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -35,20 +35,20 @@ end PackageTarget -- # Build Modules def Package.buildModuleTargetDAGFor -(mod : Name) (oleanDirs : List FilePath) (depsTarget : ActiveBuildTarget PUnit) +(mod : Name) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) : BuildM (ModuleTarget × NameMap ModuleTarget) := do - let fetch := fetchModuleWithLocalImports self oleanDirs depsTarget + let fetch := fetchModuleWithLocalImports self oleanDirs depTarget failOnCycle <| ← buildRBTop fetch mod |>.run {} def Package.buildModuleTargetDAG -(oleanDirs : List FilePath) (depsTarget : ActiveBuildTarget PUnit) (self : Package) := - self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depsTarget +(oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) := + self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depTarget def Package.buildModuleTargets (mods : List Name) (oleanDirs : List FilePath) -(depsTarget : ActiveBuildTarget PUnit) (self : Package) +(depTarget : ActiveOpaqueTarget) (self : Package) : BuildM (List ModuleTarget) := do - let fetch : ModuleTargetFetch := fetchModuleWithLocalImports self oleanDirs depsTarget + let fetch : ModuleTargetFetch := fetchModuleWithLocalImports self oleanDirs depTarget failOnCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {} -- # Configure/Build Packages @@ -56,10 +56,11 @@ def Package.buildModuleTargets def Package.buildTargetWithDepTargetsFor (mod : Name) (depTargets : List PackageTarget) (self : Package) : BuildM PackageTarget := do - let depsTarget ← ActiveTarget.all <| - (← self.buildMoreDepsTarget).withArtifact arbitrary :: depTargets - let oLeanDirs := depTargets.map (·.package.oleanDir) - let (target, targetMap) ← self.buildModuleTargetDAGFor mod oLeanDirs depsTarget + let extraDepTarget ← self.buildExtraDepTarget + let depTarget ← ActiveOpaqueTarget.collectList depTargets + let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget + let oleanDirs := depTargets.map (·.package.oleanDir) + let (target, targetMap) ← self.buildModuleTargetDAGFor mod oleanDirs allDepsTarget return {target with artifact := ⟨self, targetMap⟩} def Package.buildTargetWithDepTargets @@ -103,9 +104,10 @@ def Package.buildModuleTargetsWithDeps (deps : List Package) (mods : List Name) (self : Package) : BuildM (List ModuleTarget) := do let oleanDirs := deps.map (·.oleanDir) - let depsTarget ← ActiveTarget.all <| - (← self.buildMoreDepsTarget).withArtifact arbitrary :: (← deps.mapM (·.buildTarget)) - self.buildModuleTargets mods oleanDirs depsTarget + let extraDepTarget ← self.buildExtraDepTarget + let depTarget ← ActiveOpaqueTarget.collectList <| ← deps.mapM (·.buildTarget) + let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget + self.buildModuleTargets mods oleanDirs allDepsTarget def Package.buildModulesWithDeps (deps : List Package) (mods : List Name) (self : Package) diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index ad191f64a3..5d03eb5a87 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -13,33 +13,27 @@ namespace Lake -- # Build Targets -------------------------------------------------------------------------------- --- ## Inactive Target - +/-- A Lake build target. -/ abbrev BuildTarget a := Target LakeTrace BuildM BuildTask a namespace BuildTarget -def nil : BuildTarget PUnit := - Target.pure () LakeTrace.nil - -def hash (self : BuildTarget a) := self.trace.hash -def mtime (self : BuildTarget a) := self.trace.mtime +abbrev hash (self : BuildTarget a) := self.trace.hash +abbrev mtime (self : BuildTarget a) := self.trace.mtime end BuildTarget --- ## Active Target +-- ## Active +/-- An active Lake build target. -/ abbrev ActiveBuildTarget a := ActiveTarget LakeTrace BuildTask a namespace ActiveBuildTarget -def nil : ActiveBuildTarget PUnit := - ActiveTarget.pure () LakeTrace.nil - -def hash (self : ActiveBuildTarget a) := self.trace.hash -def mtime (self : ActiveBuildTarget a) := self.trace.mtime +abbrev hash (self : ActiveBuildTarget a) := self.trace.hash +abbrev mtime (self : ActiveBuildTarget a) := self.trace.mtime end ActiveBuildTarget @@ -47,19 +41,70 @@ end ActiveBuildTarget -- # File Targets -------------------------------------------------------------------------------- --- ## File Target - +/-- A `BuildTarget` that produces a file. -/ abbrev FileTarget := BuildTarget FilePath namespace FileTarget -def compute (file : FilePath) : IO FileTarget := +abbrev compute (file : FilePath) : IO FileTarget := Target.compute file end FileTarget --- ## Active File Target +-- ## Active +/-- An `ActiveBuildTarget` that produces a file. -/ abbrev ActiveFileTarget := ActiveBuildTarget FilePath + +-------------------------------------------------------------------------------- +-- # Opaque Targets +-------------------------------------------------------------------------------- + +/-- A `BuildTarget` with no artifact information. -/ +abbrev OpaqueTarget := + BuildTarget PUnit + +namespace OpaqueTarget + +abbrev nil : OpaqueTarget := + Target.pure () LakeTrace.nil + +abbrev collectList (targets : List (BuildTarget a)) : OpaqueTarget := + Target.collectOpaqueList targets + +abbrev collectArray (targets : Array (BuildTarget a)) : OpaqueTarget := + Target.collectOpaqueArray targets + +def andThenTargetAsync (t1 t2 : OpaqueTarget) : OpaqueTarget := + let trace := mixTrace t1.trace t2.trace + Target.opaque trace do + let tk1 ← t1.materializeAsync + let tk2 ← t2.materializeAsync + andThenAsync tk1 tk2 + +end OpaqueTarget + +-- ## Active + +/-- An `ActiveBuildTarget` with no artifact information. -/ +abbrev ActiveOpaqueTarget := + ActiveBuildTarget PUnit + +namespace ActiveOpaqueTarget + +abbrev nil : ActiveOpaqueTarget := + ActiveTarget.pure () LakeTrace.nil + +abbrev collectList (targets : List (ActiveBuildTarget a)) : BuildM ActiveOpaqueTarget := + ActiveTarget.collectOpaqueList targets + +abbrev collectArray (targets : Array (ActiveBuildTarget a)) : BuildM ActiveOpaqueTarget := + ActiveTarget.collectOpaqueArray targets + +def andThenTargetAsync (t1 t2 : ActiveOpaqueTarget) : BuildM ActiveOpaqueTarget := do + let trace := mixTrace t1.trace t2.trace + ActiveTarget.opaque trace <| ← andThenAsync t1.task t2.task + +end ActiveOpaqueTarget diff --git a/Lake/Package.lean b/Lake/Package.lean index 707c340604..b023a8c89a 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -52,7 +52,7 @@ structure PackageConfig where buildMoreLibTargets : BuildM (Array ActiveFileTarget) := #[] depsDir : FilePath := defaultDepsDir dependencies : List Dependency := [] - buildMoreDepsTarget : BuildM (ActiveBuildTarget PUnit) := ActiveBuildTarget.nil + buildExtraDepTarget : BuildM ActiveOpaqueTarget := ActiveOpaqueTarget.nil scripts : HashMap String Script := HashMap.empty deriving Inhabited @@ -86,8 +86,8 @@ def moduleRootName (self : Package) : String := def dependencies (self : Package) : List Dependency := self.config.dependencies -def buildMoreDepsTarget (self : Package) : BuildM (ActiveBuildTarget PUnit) := - self.config.buildMoreDepsTarget +def buildExtraDepTarget (self : Package) : BuildM ActiveOpaqueTarget := + self.config.buildExtraDepTarget def leanArgs (self : Package) : Array String := self.config.leanArgs diff --git a/Lake/Target.lean b/Lake/Target.lean index 5219e76e82..bd74a8262b 100644 --- a/Lake/Target.lean +++ b/Lake/Target.lean @@ -64,29 +64,42 @@ namespace ActiveTarget def mk (artifact : a) (trace : t) (task : m PUnit) : ActiveTarget t m a := ⟨artifact, trace, task⟩ -def opaque (trace : t) (task : m PUnit) : ActiveTarget t m PUnit := - ⟨(), trace, task⟩ - protected def pure [Pure m] (artifact : a) (trace : t) : ActiveTarget t m a := ⟨artifact, trace, pure ()⟩ -def nil [Pure m] [Inhabited t] : ActiveTarget t m PUnit := - ActiveTarget.pure () Inhabited.default - def materialize [Await n m] (self : ActiveTarget t n α) : m PUnit := await self.task -def andThen [SeqRightAsync m n] (target : ActiveTarget t n a) (act : m PUnit) : m (n PUnit) := - seqRightAsync target.task act +-- ## Opaque Active Targets -instance [SeqRightAsync m n] : HAndThen (ActiveTarget t n a) (m PUnit) (m (n PUnit)) := - ⟨andThen⟩ +def opaque (trace : t) (task : m PUnit) : ActiveTarget t m PUnit := + ⟨(), trace, task⟩ -def all [Monad m] [Pure n] [BindAsync m n] [Async m n] [NilTrace t] [MixTrace t] - (targets : List (ActiveTarget t n a)) : m (ActiveTarget t n PUnit) := do +section +variable [NilTrace t] [MixTrace t] [Monad m] [Pure n] [BindAsync m n] [Async m n] + +def collectOpaqueList (targets : List (ActiveTarget t n a)) : m (ActiveTarget t n PUnit) := do let task ← joinTaskList <| targets.map (·.task) let trace := mixTraceList <| targets.map (·.trace) - return ActiveTarget.mk () trace task + ActiveTarget.opaque trace task + +def collectOpaqueArray (targets : Array (ActiveTarget t n a)) : m (ActiveTarget t n PUnit) := do + let task ← joinTaskArray <| targets.map (·.task) + let trace := mixTraceArray <| targets.map (·.trace) + ActiveTarget.opaque trace task + +end + +-- ## Sequencing + +section +variable [SeqRightAsync m n] + +def andThen (target : ActiveTarget t n a) (act : m PUnit) : m (n PUnit) := + seqRightAsync target.task act + +instance : HAndThen (ActiveTarget t n a) (m PUnit) (m (n PUnit)) := ⟨andThen⟩ +end end ActiveTarget @@ -124,15 +137,14 @@ namespace Target def mk (artifact : a) (trace : t) (task : m (n PUnit)) : Target t m n a := ⟨artifact, trace, task⟩ -def opaque (trace : t) (task : m (n PUnit)) : Target t m n PUnit := - ⟨(), trace, task⟩ - protected def pure [Pure m] [Pure n] (artifact : a) (trace : t) : Target t m n a := ⟨artifact, trace, pure (pure ())⟩ def compute [ComputeTrace a m' t] [Monad m'] [Pure m] [Pure n] (artifact : a) : m' (Target t m n a) := do Target.pure artifact <| ← computeTrace artifact +-- ## Materializing + def run [Monad m] (self : Target t m n a) : m (ActiveTarget t n a) := do self.withTask <| ← self.task @@ -159,6 +171,26 @@ def materializeArray [Await n m] (targets : Array (Target t m n a)) : m PUnit : end +-- ## Opaque Targets + +def opaque (trace : t) (task : m (n PUnit)) : Target t m n PUnit := + ⟨(), trace, task⟩ + +section +variable [NilTrace t] [MixTrace t] [Monad m] [Pure n] [BindAsync m n] [Async m n] + +def collectOpaqueList (targets : List (Target t m n a)) : Target t m n PUnit := + let trace := mixTraceList <| targets.map (·.trace) + Target.opaque trace do Target.materializeListAsync targets + +def collectOpaqueArray (targets : Array (Target t m n a)) : Target t m n PUnit := + let trace := mixTraceArray <| targets.map (·.trace) + Target.opaque trace do Target.materializeArrayAsync targets + +end + +-- ## Sequencing + section variable [SeqRightAsync m n] [Bind m] @@ -170,6 +202,8 @@ end end Target +-- ## Combinators + section variable [Monad m] [BindAsync m n] [Async m n]