From ddf02cb339b5b327918fd0c8c943c66cdadc5fe5 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 15 Aug 2021 19:04:28 -0400 Subject: [PATCH] refactor: merge build target into lake target --- Lake/Build.lean | 38 ++++------- Lake/BuildBin.lean | 18 +++-- Lake/BuildTarget.lean | 146 ++++++++++++++++++++--------------------- Lake/BuildTargets.lean | 4 +- Lake/BuildTrace.lean | 43 ++++++++++-- Lake/Package.lean | 4 +- 6 files changed, 143 insertions(+), 110 deletions(-) diff --git a/Lake/Build.lean b/Lake/Build.lean index 7d0bd6e1e5..bf1e9d86ff 100644 --- a/Lake/Build.lean +++ b/Lake/Build.lean @@ -28,21 +28,21 @@ protected def ModuleArtifact.getMTime (self : ModuleArtifact) : IO MTime := do instance : GetMTime ModuleArtifact := ⟨ModuleArtifact.getMTime⟩ -abbrev ModuleTarget := LakeTarget ModuleArtifact +abbrev ModuleTarget := ActiveLakeTarget ModuleArtifact namespace ModuleTarget def oleanFile (self : ModuleTarget) := self.artifact.oleanFile def oleanTarget (self : ModuleTarget) : ActiveFileTarget := - {self with artifact := self.oleanFile, trace := self.mtime} + {self with artifact := self.oleanFile} def cFile (self : ModuleTarget) := self.artifact.cFile def cTarget (self : ModuleTarget) : ActiveFileTarget := - {self with artifact := self.cFile, trace := self.mtime} + {self with artifact := self.cFile} end ModuleTarget -abbrev PackageTarget := LakeTarget (Package × NameMap ModuleTarget) +abbrev PackageTarget := ActiveLakeTarget (Package × NameMap ModuleTarget) namespace PackageTarget @@ -73,16 +73,6 @@ def checkIfSameHash (hash : Hash) (file : FilePath) : IO Bool := def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) := do if cond then pure (pure ()) else build -/-- - Construct a no-op target if the given artifact is up-to-date. - Otherwise, construct a target with the given build task. --/ -def skipIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) -[Pure n] [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m] (build : m (n PUnit)) -: m (ActiveTarget MTime n a) := do - ActiveTarget.mk artifact depMTime <| ← - skipIf (← checkIfNewer artifact depMTime) build - -- # Build Modules /- @@ -94,7 +84,7 @@ def skipIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) a `LEAN_PATH` that includes `oleanDirs`. -/ def fetchAfterDirectLocalImports -(pkg : Package) (oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit) +(pkg : Package) (oleanDirs : List FilePath) (depsTarget : ActiveLakeTarget PUnit) {m} [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m] : RecFetch Name ModuleTarget m := let leanPath := SearchPath.toString <| pkg.oleanDir :: oleanDirs fun mod fetch => do @@ -109,10 +99,10 @@ def fetchAfterDirectLocalImports -- calculate trace let leanMTime ← getMTime leanFile let leanHash := Hash.compute contents - let importHashes ← importTargets.map (·.hash) - let importMTimes ← importTargets.map (·.mtime) - let fullHash := Hash.mixList (leanHash :: depsTarget.hash :: importHashes) - let maxMTime := MTime.listMax (leanMTime :: depsTarget.mtime :: importMTimes) + let depTrace := depsTarget.trace.mix <| + LakeTrace.mixList <| importTargets.map (·.trace) + let maxMTime := max leanMTime depTrace.mtime + let fullHash := Hash.mix leanHash depTrace.hash let hashFile := pkg.modToHashFile mod let sameHash ← checkIfSameHash fullHash hashFile let mtime := ite sameHash 0 maxMTime @@ -143,18 +133,18 @@ def throwOnCycle (mx : IO (Except (List Name) α)) : IO α := throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}" def Package.buildModuleTargetDAGFor -(mod : Name) (oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit) +(mod : Name) (oleanDirs : List FilePath) (depsTarget : ActiveLakeTarget PUnit) (self : Package) : IO (ModuleTarget × NameMap ModuleTarget) := do let fetch := fetchAfterDirectLocalImports self oleanDirs depsTarget throwOnCycle <| buildRBTop fetch mod |>.run {} def Package.buildModuleTargetDAG -(oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit) (self : Package) := +(oleanDirs : List FilePath) (depsTarget : ActiveLakeTarget PUnit) (self : Package) := self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depsTarget def Package.buildModuleTargets (mods : List Name) (oleanDirs : List FilePath) -(depsTarget : LakeTarget PUnit) (self : Package) +(depsTarget : ActiveLakeTarget PUnit) (self : Package) : IO (List ModuleTarget) := do let fetch : ModuleTargetFetch := fetchAfterDirectLocalImports self oleanDirs depsTarget @@ -165,7 +155,7 @@ def Package.buildModuleTargets def Package.buildTargetWithDepTargetsFor (mod : Name) (depTargets : List PackageTarget) (self : Package) : IO PackageTarget := do - let depsTarget ← LakeTarget.all <| + let depsTarget ← ActiveLakeTarget.all <| (← self.buildMoreDepsTarget).withArtifact arbitrary :: depTargets let oLeanDirs := depTargets.map (·.package.oleanDir) let (target, targetMap) ← self.buildModuleTargetDAGFor mod oLeanDirs depsTarget @@ -212,7 +202,7 @@ def Package.buildModuleTargetsWithDeps (deps : List Package) (mods : List Name) (self : Package) : IO (List ModuleTarget) := do let oleanDirs := deps.map (·.oleanDir) - let depsTarget ← LakeTarget.all <| + let depsTarget ← ActiveLakeTarget.all <| (← self.buildMoreDepsTarget).withArtifact arbitrary :: (← deps.mapM (·.buildTarget)) self.buildModuleTargets mods oleanDirs depsTarget diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index 279f08e949..277ccb8a48 100644 --- a/Lake/BuildBin.lean +++ b/Lake/BuildBin.lean @@ -8,15 +8,25 @@ import Lake.Build open System namespace Lake +/-- + Construct a no-op target if the given artifact is up-to-date. + Otherwise, construct a target with the given build task. +-/ +def skipIfNewer +[GetMTime a] (artifact : a) (trace : LakeTrace) +(build : IO (IOTask PUnit)) : IO (ActiveLakeTarget a) := do + ActiveTarget.mk artifact trace <| ← + skipIf (← checkIfNewer artifact trace.mtime) build + -- # Build `.o` Files def buildLeanO (oFile : FilePath) -(cTarget : ActiveBuildTarget t FilePath) (leancArgs : Array String := #[]) : IO (IOTask PUnit) := +(cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO (IOTask PUnit) := cTarget >> compileLeanO oFile cTarget.artifact leancArgs def fetchLeanOFileTarget (oFile : FilePath) (cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO ActiveFileTarget := - skipIfNewer oFile cTarget.mtime <| buildLeanO oFile cTarget leancArgs + skipIfNewer oFile cTarget.trace <| buildLeanO oFile cTarget leancArgs -- # Build Package Lib @@ -33,7 +43,7 @@ def PackageTarget.buildStaticLib oFileTargets >> compileStaticLib self.package.staticLibFile oFiles def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO ActiveFileTarget := do - skipIfNewer self.package.staticLibFile self.mtime self.buildStaticLib + skipIfNewer self.package.staticLibFile self.trace self.buildStaticLib def Package.fetchStaticLibTarget (self : Package) : IO ActiveFileTarget := do (← self.buildTarget).fetchStaticLibTarget @@ -62,7 +72,7 @@ def PackageTarget.buildBin def PackageTarget.fetchBinTarget (depTargets : List PackageTarget) (self : PackageTarget) : IO ActiveFileTarget := - skipIfNewer self.package.binFile self.mtime <| self.buildBin depTargets + skipIfNewer self.package.binFile self.trace <| self.buildBin depTargets def Package.fetchBinTarget (self : Package) : IO ActiveFileTarget := do let depTargets ← self.buildDepTargets diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index a33d1db5f4..b98f36df60 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -79,36 +79,32 @@ def nil [Pure m] [Inhabited t] : ActiveTarget t m PUnit := def materialize [Await m n] (self : ActiveTarget t n α) : m PUnit := await self.task +def andThen [Monad m] [MonadAsync m n] (target : ActiveTarget t n a) (act : m PUnit) : m (n PUnit) := + mapAsync (fun _ => act) target.task + +instance [Monad m] [MonadAsync m n] : HAndThen (ActiveTarget t n a) (m PUnit) (m (n PUnit)) := + ⟨andThen⟩ + end ActiveTarget --- ## Active Build Target +-- ## Combinators -abbrev ActiveBuildTarget t a := - ActiveTarget t IOTask a +section +variable [Monad m] [MonadAsync m n] -namespace ActiveBuildTarget - --- ### Combinators - -def after (target : ActiveBuildTarget t a) (act : IO PUnit) : IO (IOTask PUnit) := - target.task.andThen act - -def afterList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO (IOTask PUnit) := +def afterActiveList (targets : List (ActiveTarget t n a)) (act : m PUnit) : m (n PUnit) := afterTaskList (targets.map (·.task)) act -def afterArray (targets : Array (ActiveBuildTarget t a)) (act : IO PUnit) : IO (IOTask PUnit) := +def afterActiveArray (targets : Array (ActiveTarget t n a)) (act : m PUnit) : m (n PUnit) := afterTaskArray (targets.map (·.task)) act -instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO (IOTask PUnit)) := - ⟨ActiveBuildTarget.after⟩ +instance : HAndThen (List (ActiveTarget t n a)) (m PUnit) (m (n PUnit)) := + ⟨afterActiveList⟩ -instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO (IOTask PUnit)) := - ⟨ActiveBuildTarget.afterList⟩ +instance : HAndThen (Array (ActiveTarget t n a)) (m PUnit) (m (n PUnit)) := + ⟨afterActiveArray⟩ - instance : HAndThen (Array (ActiveBuildTarget t a)) (IO PUnit) (IO (IOTask PUnit)) := - ⟨ActiveBuildTarget.afterArray⟩ - -end ActiveBuildTarget +end -------------------------------------------------------------------------------- -- # Inactive Target @@ -152,36 +148,76 @@ def materializeArrayAsync [Monad m] [Pure n] [MonadAsync m n] (targets : Array ( def materializeArray [Monad m] [Pure n] [MonadAsync m n] (targets : Array (Target t m a)) : m PUnit := do await <| ← materializeArrayAsync targets +def andThen [SeqRight m] (target : Target t m a) (act : m β) : m β := + target.task *> act + +instance [SeqRight m] : HAndThen (Target t m a) (m β) (m β) := ⟨andThen⟩ + end Target --- ## BuildTarget +-------------------------------------------------------------------------------- +-- # Build Targets +-------------------------------------------------------------------------------- -abbrev BuildTarget t a := - Target t IO a +-- ## Inactive Target + +abbrev LakeTarget a := + Target LakeTrace IO a + +namespace LakeTarget + +def nil : LakeTarget PUnit := + Target.pure () LakeTrace.nil + +def pure (artifact : a) (hash : Hash) (mtime : MTime) : LakeTarget a := + Target.pure artifact ⟨hash, mtime⟩ + +def hash (self : LakeTarget a) := self.trace.hash +def mtime (self : LakeTarget a) := self.trace.mtime + +end LakeTarget + +-- ## Active Target + +abbrev ActiveLakeTarget a := + ActiveTarget LakeTrace IOTask a + +namespace ActiveLakeTarget + +def nil : ActiveLakeTarget PUnit := + ActiveTarget.pure () LakeTrace.nil + +def hash (self : ActiveLakeTarget a) := self.trace.hash +def mtime (self : ActiveLakeTarget a) := self.trace.mtime + +def all (targets : List (ActiveLakeTarget a)) : IO (ActiveLakeTarget PUnit) := do + let hash := Hash.mixList <| targets.map (·.hash) + let mtime := MTime.listMax <| targets.map (·.mtime) + let task ← seqListAsync <| targets.map (·.task) + return ActiveTarget.mk () ⟨hash, mtime⟩ task + +end ActiveLakeTarget -------------------------------------------------------------------------------- -- # File Targets -------------------------------------------------------------------------------- --- ## File BaseTarget +-- ## File Target abbrev FileTarget := - BuildTarget MTime FilePath + LakeTarget FilePath namespace FileTarget -def mk (file : FilePath) (depMTime : MTime) (task : IO PUnit) : FileTarget := - ⟨file, depMTime, task⟩ - def compute (file : FilePath) : IO FileTarget := do - Target.pure file (← getMTime file) + Target.pure file <| ← LakeTrace.compute file end FileTarget --- ## Files BaseTarget +-- ## Files Target abbrev FilesTarget := - BuildTarget MTime (Array FilePath) + LakeTarget (Array FilePath) namespace FilesTarget @@ -195,20 +231,20 @@ def filesAsArray (self : FilesTarget) : Array FilePath := self.artifact def compute (files : Array FilePath) : IO FilesTarget := do - Target.pure files (MTime.arrayMax <| ← files.mapM getMTime) + Target.pure files <| LakeTrace.mixArray <| ← files.mapM LakeTrace.compute def singleton (target : FileTarget) : FilesTarget := target.withArtifact #[target.file] def collectList (targets : List FileTarget) : FilesTarget := let files := Array.mk <| targets.map (·.file) - let mtime := MTime.listMax <| targets.map (·.mtime) - Target.mk files mtime do Target.materializeList targets + let trace := LakeTrace.mixList <| targets.map (·.trace) + Target.mk files trace do Target.materializeList targets def collectArray (targets : Array FileTarget) : FilesTarget := let files := targets.map (·.file) - let mtime := MTime.arrayMax <| targets.map (·.mtime) - Target.mk files mtime do Target.materializeArray targets + let trace := LakeTrace.mixArray <| targets.map (·.trace) + Target.mk files trace do Target.materializeArray targets def collect (targets : Array FileTarget) : FilesTarget := collectArray targets @@ -222,40 +258,4 @@ instance : Coe (Array FileTarget) FilesTarget := ⟨FilesTarget.collectArray⟩ -- ## Active File Target abbrev ActiveFileTarget := - ActiveBuildTarget MTime FilePath - -namespace ActiveFileTarget - -def mk (file : FilePath) (depMTime : MTime) (task : IOTask PUnit) : ActiveFileTarget := - ActiveTarget.mk file depMTime task - -end ActiveFileTarget - --------------------------------------------------------------------------------- --- # Lake Target --------------------------------------------------------------------------------- - -abbrev LakeTarget a := - ActiveBuildTarget LakeTrace a - -namespace LakeTarget - -def nil : LakeTarget PUnit := - ActiveTarget.pure () Inhabited.default - -def hash (self : LakeTarget a) := self.trace.hash -def mtime (self : LakeTarget a) := self.trace.mtime - -def all (targets : List (LakeTarget a)) : IO (LakeTarget PUnit) := do - let hash := Hash.mixList <| targets.map (·.hash) - let mtime := MTime.listMax <| targets.map (·.mtime) - let task ← seqListAsync <| targets.map (·.task) - return ActiveTarget.mk () ⟨hash, mtime⟩ task - -def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LakeTarget a := - {target with trace := LakeTrace.fromMTime target.trace} - -def buildOpaqueFromFileTarget (target : FileTarget) : IO (LakeTarget PUnit) := do - LakeTarget.fromMTimeTarget <| ← Target.runAsync target.withoutArtifact - -end LakeTarget + ActiveLakeTarget FilePath diff --git a/Lake/BuildTargets.lean b/Lake/BuildTargets.lean index 7d44791505..c9c134142e 100644 --- a/Lake/BuildTargets.lean +++ b/Lake/BuildTargets.lean @@ -12,14 +12,14 @@ namespace Lake def oFileTarget (oFile : FilePath) (srcTarget : FileTarget) (args : Array String := #[]) (cmd := "c++") : FileTarget := - FileTarget.mk oFile srcTarget.trace <| + Target.mk oFile srcTarget.trace <| unless (← checkIfNewer oFile srcTarget.mtime) do srcTarget.materialize compileO oFile srcTarget.file args (cmd := "c++") def staticLibTarget (libFile : FilePath) (oFilesTarget : FilesTarget) : FileTarget := - FileTarget.mk libFile oFilesTarget.trace do + Target.mk libFile oFilesTarget.trace do unless (← checkIfNewer libFile oFilesTarget.mtime) do oFilesTarget.materialize compileStaticLib libFile oFilesTarget.filesAsArray diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean index 79ae01bfac..6ed4cc8826 100644 --- a/Lake/BuildTrace.lean +++ b/Lake/BuildTrace.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +open System namespace Lake -- # Hash Traces @@ -28,6 +29,9 @@ def mix (h1 h2 : Hash) : Hash := def mixList (hashes : List Hash) : Hash := hashes.foldl mix nil +def mixArray (hashes : Array Hash) : Hash := + hashes.foldl mix nil + protected def toString (self : Hash) : String := toString self.val @@ -35,6 +39,17 @@ instance : ToString Hash := ⟨Hash.toString⟩ end Hash +class ComputeHash (α) where + computeHash : α → IO Hash + +export ComputeHash (computeHash) + +def getFileHash (file : FilePath) : IO Hash := + Hash.compute <$> IO.FS.readFile file + +instance : ComputeHash FilePath := ⟨getFileHash⟩ +instance : ComputeHash String := ⟨pure ∘ Hash.compute⟩ + -- # Modification Time Traces open IO.FS (SystemTime) @@ -61,8 +76,10 @@ class GetMTime (α) where export GetMTime (getMTime) -instance : GetMTime System.FilePath where - getMTime file := do (← file.metadata).modified +def getFileMTime (file : FilePath) : IO MTime := do + (← file.metadata).modified + +instance : GetMTime FilePath := ⟨getFileMTime⟩ /-- Check if the artifact's `MTIme` is at least `depMTime`. -/ def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do @@ -73,14 +90,30 @@ def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do structure LakeTrace where hash : Hash mtime : MTime - deriving Inhabited namespace LakeTrace +def nil : LakeTrace := + mk Hash.nil 0 + +instance : Inhabited LakeTrace := ⟨nil⟩ + +def compute [ComputeHash a] [GetMTime a] (artifact : a) : IO LakeTrace := do + mk (← computeHash artifact) (← getMTime artifact) + def fromHash (hash : Hash) : LakeTrace := - LakeTrace.mk hash 0 + mk hash 0 def fromMTime (mtime : MTime) : LakeTrace := - LakeTrace.mk Hash.nil mtime + mk Hash.nil mtime + +def mix (t1 t2 : LakeTrace) : LakeTrace := + mk (Hash.mix t1.hash t2.hash) (max t1.mtime t2.mtime) + +def mixList (traces : List LakeTrace) : LakeTrace := + traces.foldl mix nil + +def mixArray (traces : Array LakeTrace) : LakeTrace := + traces.foldl mix nil end LakeTrace diff --git a/Lake/Package.lean b/Lake/Package.lean index 3aff1d67cf..5e3f26d21b 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -52,7 +52,7 @@ structure PackageConfig where buildMoreLibTargets : IO (Array ActiveFileTarget) := #[] depsDir : FilePath := defaultDepsDir dependencies : List Dependency := [] - buildMoreDepsTarget : IO (LakeTarget PUnit) := LakeTarget.nil + buildMoreDepsTarget : IO (ActiveLakeTarget PUnit) := ActiveLakeTarget.nil scripts : HashMap String Script := HashMap.empty deriving Inhabited @@ -86,7 +86,7 @@ def moduleRootName (self : Package) : String := def dependencies (self : Package) : List Dependency := self.config.dependencies -def buildMoreDepsTarget (self : Package) : IO (LakeTarget PUnit) := +def buildMoreDepsTarget (self : Package) : IO (ActiveLakeTarget PUnit) := self.config.buildMoreDepsTarget def leanArgs (self : Package) : Array String :=