From 609ee229712aef1f3387b6262ca09fdc72a6936a Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 6 Aug 2021 01:05:19 -0400 Subject: [PATCH] refactor: LeanTrace/Target -> LakeTrace/Target --- Lake/Build.lean | 16 ++++++++-------- Lake/BuildTarget.lean | 26 +++++++++++++------------- Lake/BuildTrace.lean | 14 +++++++------- Lake/Package.lean | 4 ++-- examples/ffi/package.lean | 2 +- 5 files changed, 31 insertions(+), 31 deletions(-) diff --git a/Lake/Build.lean b/Lake/Build.lean index 7d39b0a0df..e8593f7479 100644 --- a/Lake/Build.lean +++ b/Lake/Build.lean @@ -28,7 +28,7 @@ protected def ModuleArtifact.getMTime (self : ModuleArtifact) : IO MTime := do instance : GetMTime ModuleArtifact := ⟨ModuleArtifact.getMTime⟩ -abbrev ModuleTarget := LeanTarget ModuleArtifact +abbrev ModuleTarget := LakeTarget ModuleArtifact namespace ModuleTarget @@ -48,7 +48,7 @@ def cTarget (self : ModuleTarget) : ActiveFileTarget := end ModuleTarget -abbrev PackageTarget := LeanTarget (Package × NameMap ModuleTarget) +abbrev PackageTarget := LakeTarget (Package × NameMap ModuleTarget) namespace PackageTarget @@ -96,7 +96,7 @@ def skipIfNewer [GetMTime a] a `LEAN_PATH` that includes `oleanDirs`. -/ def fetchAfterDirectLocalImports -(pkg : Package) (oleanDirs : List FilePath) (depsTarget : LeanTarget PUnit) +(pkg : Package) (oleanDirs : List FilePath) (depsTarget : LakeTarget 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 @@ -145,18 +145,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 : LeanTarget PUnit) +(mod : Name) (oleanDirs : List FilePath) (depsTarget : LakeTarget 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 : LeanTarget PUnit) (self : Package) := +(oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit) (self : Package) := self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depsTarget def Package.buildModuleTargets (mods : List Name) (oleanDirs : List FilePath) -(depsTarget : LeanTarget PUnit) (self : Package) +(depsTarget : LakeTarget PUnit) (self : Package) : IO (List ModuleTarget) := do let fetch : ModuleTargetFetch := fetchAfterDirectLocalImports self oleanDirs depsTarget @@ -167,7 +167,7 @@ def Package.buildModuleTargets def Package.buildTargetWithDepTargetsFor (mod : Name) (depTargets : List PackageTarget) (self : Package) : IO PackageTarget := do - let depsTarget ← LeanTarget.all <| + let depsTarget ← LakeTarget.all <| (← self.buildMoreDepsTarget).withArtifact arbitrary :: depTargets let oLeanDirs := depTargets.map (·.package.oleanDir) let (target, targetMap) ← self.buildModuleTargetDAGFor mod oLeanDirs depsTarget @@ -214,7 +214,7 @@ def Package.buildModuleTargetsWithDeps (deps : List Package) (mods : List Name) (self : Package) : IO (List ModuleTarget) := do let oleanDirs := deps.map (·.oleanDir) - let depsTarget ← LeanTarget.all <| + let depsTarget ← LakeTarget.all <| (← self.buildMoreDepsTarget).withArtifact arbitrary :: (← deps.mapM (·.buildTarget)) self.buildModuleTargets mods oleanDirs depsTarget diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index 8de2b4ecc6..3a566a378e 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -220,30 +220,30 @@ def mk (file : FilePath) (depMTime : MTime) (task : BuildTask) : ActiveFileTarge end ActiveFileTarget -------------------------------------------------------------------------------- --- # Lean Target +-- # Lake Target -------------------------------------------------------------------------------- -abbrev LeanTarget a := - ActiveBuildTarget LeanTrace a +abbrev LakeTarget a := + ActiveBuildTarget LakeTrace a -namespace LeanTarget +namespace LakeTarget -def nil : LeanTarget PUnit := +def nil : LakeTarget PUnit := ActiveTarget.pure () Inhabited.default -def hash (self : LeanTarget a) := self.trace.hash -def mtime (self : LeanTarget a) := self.trace.mtime +def hash (self : LakeTarget a) := self.trace.hash +def mtime (self : LakeTarget a) := self.trace.mtime -def all (targets : List (LeanTarget a)) : IO (LeanTarget PUnit) := do +def all (targets : List (LakeTarget a)) : IO (LakeTarget PUnit) := do let hash := Hash.foldList 0 <| targets.map (·.hash) let mtime := MTime.listMax <| targets.map (·.mtime) let task ← BuildTask.all <| targets.map (·.task) return ActiveTarget.mk () ⟨hash, mtime⟩ task -def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LeanTarget a := - {target with trace := LeanTrace.fromMTime target.trace} +def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LakeTarget a := + {target with trace := LakeTrace.fromMTime target.trace} -def buildOpaqueFromFileTarget (target : FileTarget) : IO (LeanTarget PUnit) := do - LeanTarget.fromMTimeTarget <| ← Target.runAsync target.withoutArtifact +def buildOpaqueFromFileTarget (target : FileTarget) : IO (LakeTarget PUnit) := do + LakeTarget.fromMTimeTarget <| ← Target.runAsync target.withoutArtifact -end LeanTarget +end LakeTarget diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean index 0b0d86b9ee..9aca4f6a06 100644 --- a/Lake/BuildTrace.lean +++ b/Lake/BuildTrace.lean @@ -49,17 +49,17 @@ def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do -- # Combined Trace -structure LeanTrace where +structure LakeTrace where hash : Hash mtime : MTime deriving Inhabited -namespace LeanTrace +namespace LakeTrace -def fromHash (hash : Hash) : LeanTrace := - LeanTrace.mk hash 0 +def fromHash (hash : Hash) : LakeTrace := + LakeTrace.mk hash 0 -def fromMTime (mtime : MTime) : LeanTrace := - LeanTrace.mk 0 mtime +def fromMTime (mtime : MTime) : LakeTrace := + LakeTrace.mk 0 mtime -end LeanTrace +end LakeTrace diff --git a/Lake/Package.lean b/Lake/Package.lean index 6238fefd3b..1652b8cbd4 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -51,7 +51,7 @@ structure PackageConfig where libName : String := moduleRoot.toString (escape := false) depsDir : FilePath := defaultDepsDir dependencies : List Dependency := [] - buildMoreDepsTarget : IO (LeanTarget PUnit) := LeanTarget.nil + buildMoreDepsTarget : IO (LakeTarget PUnit) := LakeTarget.nil scripts : HashMap String Script := HashMap.empty deriving Inhabited @@ -85,7 +85,7 @@ def moduleRootName (self : Package) : String := def dependencies (self : Package) : List Dependency := self.config.dependencies -def buildMoreDepsTarget (self : Package) : IO (ActiveBuildTarget LeanTrace PUnit) := +def buildMoreDepsTarget (self : Package) : IO (ActiveBuildTarget LakeTrace PUnit) := self.config.buildMoreDepsTarget def leanArgs (self : Package) : Array String := diff --git a/examples/ffi/package.lean b/examples/ffi/package.lean index df33816062..8c98700f12 100644 --- a/examples/ffi/package.lean +++ b/examples/ffi/package.lean @@ -27,5 +27,5 @@ def package : PackageConfig := { linkArgs := #[cLib.toString] -- specify the lib target as an additional dependency buildMoreDepsTarget := do - LeanTarget.buildOpaqueFromFileTarget <| ← computeCLibTarget + LakeTarget.buildOpaqueFromFileTarget <| ← computeCLibTarget }