diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index cdeccb93d3..d16faab4f2 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -39,19 +39,19 @@ instance : ComputeHash ModuleTargetInfo := ⟨ModuleArtifact.computeHash⟩ end ModuleArtifact -abbrev ModuleTarget := ActiveBuildTarget ModuleTargetInfo +abbrev ActiveModuleTarget := ActiveBuildTarget ModuleTargetInfo -namespace ModuleTarget +namespace ActiveModuleTarget -def oleanFile (self : ModuleTarget) := self.info.oleanFile -def oleanTarget (self : ModuleTarget) : ActiveFileTarget := +def oleanFile (self : ActiveModuleTarget) := self.info.oleanFile +def oleanTarget (self : ActiveModuleTarget) : ActiveFileTarget := self.withInfo self.oleanFile -def cFile (self : ModuleTarget) := self.info.cFile -def cTarget (self : ModuleTarget) : ActiveFileTarget := +def cFile (self : ActiveModuleTarget) := self.info.cFile +def cTarget (self : ActiveModuleTarget) : ActiveFileTarget := self.withInfo self.cFile -end ModuleTarget +end ActiveModuleTarget -- # Trace Checking @@ -87,7 +87,7 @@ def mkModuleTarget [GetMTime i] [ComputeHash i] (info : i) def fetchModuleTarget (pkg : Package) (moreOleanDirs : List FilePath) (mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget) -: BuildM ModuleTarget := do +: BuildM ActiveModuleTarget := do let cFile := pkg.modToC mod let oleanFile := pkg.modToOlean mod let info := ModuleTargetInfo.mk oleanFile cFile @@ -128,7 +128,7 @@ def recFetchModuleWithLocalImports (pkg : Package) def recFetchModuleTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] (pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) -: RecFetch Name ModuleTarget m := +: RecFetch Name ActiveModuleTarget m := recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do let allDepsTarget ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets fetchModuleTarget pkg moreOleanDirs mod leanFile contents allDepsTarget @@ -143,7 +143,7 @@ def recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] -- ## Definitions abbrev ModuleFetchM (α) := - -- equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget BuildM`. + -- equivalent to `RBTopT (cmp := Name.quickCmp) Name ActiveModuleTarget BuildM`. -- phrased this way to use `NameMap` EStateT (List Name) (NameMap α) BuildM @@ -151,7 +151,7 @@ abbrev ModuleFetch (α) := RecFetch Name α (ModuleFetchM α) abbrev OleanTargetFetch := ModuleFetch OleanTarget -abbrev ModuleTargetFetch := ModuleFetch ModuleTarget +abbrev ModuleTargetFetch := ModuleFetch ActiveModuleTarget abbrev OleanTargetMap := NameMap OleanTarget -abbrev ModuleTargetMap := NameMap ModuleTarget +abbrev ModuleTargetMap := NameMap ActiveModuleTarget diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index 91e797bd0d..e7b78eabb5 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -27,7 +27,7 @@ def package (self : ActivePackageTarget) := def moduleTargetMap (self : ActivePackageTarget) : ModuleTargetMap := self.info.2 -def moduleTargets (self : ActivePackageTarget) : Array (Name × ModuleTarget) := +def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveModuleTarget) := self.moduleTargetMap.fold (fun arr k v => arr.push (k, v)) #[] end ActivePackageTarget @@ -36,7 +36,7 @@ end ActivePackageTarget def Package.buildModuleTargetDAGFor (mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) -(self : Package) : BuildM (ModuleTarget × ModuleTargetMap) := do +(self : Package) : BuildM (ActiveModuleTarget × ModuleTargetMap) := do let fetch := recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget failOnImportCycle <| ← buildRBTop fetch mod |>.run {} @@ -57,7 +57,7 @@ def Package.buildOleanTargetDAG def Package.buildModuleTargets (mods : List Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) -: BuildM (List ModuleTarget) := do +: BuildM (List ActiveModuleTarget) := do let fetch : ModuleTargetFetch := recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}