From 88af2ca4b7ddfc9389b17641d1770187c0b89b74 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 9 Oct 2021 17:25:39 -0400 Subject: [PATCH] refactor: reorg build package code --- Lake/BuildBin.lean | 47 +++++---- Lake/BuildModule.lean | 41 ++++++-- Lake/BuildPackage.lean | 226 ++++++++++++++++++++++++----------------- 3 files changed, 187 insertions(+), 127 deletions(-) diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index 90f3a37681..8260896bdb 100644 --- a/Lake/BuildBin.lean +++ b/Lake/BuildBin.lean @@ -7,48 +7,53 @@ import Lake.BuildPackage import Lake.BuildTargets open System +open Lean (Name) + namespace Lake -- # Build Package .o Files def ActivePackageTarget.oFileTargets -(self : ActivePackageTarget) : Array FileTarget := +(self : ActivePackageTarget OleanAndC) : Array FileTarget := self.moduleTargets.map fun (mod, target) => let oFile := self.package.modToO mod - let cTarget := Target.active target.cTarget + let cTarget := Target.active <| ActiveOleanAndCTarget.cTarget target leanOFileTarget oFile cTarget self.package.moreLeancArgs +def Package.moduleOTarget (mod : Name) (self : Package) : FileTarget := + let oFile := self.modToO mod + let cTarget := self.moduleOleanAndCTarget mod |>.cTarget + leanOFileTarget oFile cTarget self.moreLeancArgs + -- # Build Package Lib -protected def ActivePackageTarget.staticLibTarget (self : ActivePackageTarget) : FileTarget := +protected def ActivePackageTarget.staticLibTarget (self : ActivePackageTarget OleanAndC) : FileTarget := staticLibTarget self.package.staticLibFile self.oFileTargets -def ActivePackageTarget.staticLibTargets (self : ActivePackageTarget) : Array FileTarget := +def ActivePackageTarget.staticLibTargets (self : ActivePackageTarget OleanAndC) : Array FileTarget := #[self.staticLibTarget] ++ self.package.moreLibTargets def Package.staticLibTarget (self : Package) : FileTarget := Target.mk self.staticLibFile do - (← self.buildTarget).staticLibTarget.materializeAsync + (← self.buildOleanAndCTarget).staticLibTarget.materializeAsync -def Package.buildLib (pkg : Package) : BuildM FilePath := - pkg.staticLibTarget.build +def Package.buildLib (self : Package) : BuildM FilePath := + self.staticLibTarget.build -- # Build Package Bin -def ActivePackageTarget.linkTargets -(depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : Array FileTarget := - self.oFileTargets ++ self.package.moreLibTargets ++ depTargets.concatMap (·.staticLibTargets) - -protected def ActivePackageTarget.binTarget -(depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : FileTarget := - let linkTargets := self.linkTargets depTargets - leanBinTarget self.package.binFile linkTargets self.package.moreLinkArgs - def Package.binTarget (self : Package) : FileTarget := Target.mk self.binFile do - let depTargets ← self.buildDepTargets - let pkgTarget ← self.buildModuleOleanAndCTargetsWithDepTargets #[self.binRoot] depTargets - pkgTarget.binTarget depTargets >>= (·.materializeAsync) + let depTargets ← self.buildDepTargets buildOleanAndCTargetWithDepTargets + let depTarget ← self.buildDepTargetWith depTargets + let moreOleanDirs := packageTargetsToOleanDirs depTargets + let build := self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget + let pkgTarget ← self.buildModuleDAGTarget self.binRoot build + let linkTargets := + pkgTarget.oFileTargets ++ self.moreLibTargets ++ + depTargets.concatMap (·.staticLibTargets) + let target := leanBinTarget self.binFile linkTargets self.moreLinkArgs + target.materializeAsync -def Package.buildBin (pkg : Package) : BuildM FilePath := - pkg.binTarget.build +def Package.buildBin (self : Package) : BuildM FilePath := + self.binTarget.build diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index 013d9060ac..62cc217e5a 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -42,6 +42,20 @@ instance : CheckExists OleanAndC := ⟨OleanAndC.checkExists⟩ end OleanAndC +abbrev OleanAndCTarget := BuildTarget OleanAndC + +namespace OleanAndCTarget + +def oleanFile (self : OleanAndCTarget) := self.info.oleanFile +def oleanTarget (self : OleanAndCTarget) : FileTarget := + self.withInfo self.oleanFile + +def cFile (self : OleanAndCTarget) := self.info.cFile +def cTarget (self : OleanAndCTarget) : FileTarget := + self.withInfo self.cFile + +end OleanAndCTarget + abbrev ActiveOleanAndCTarget := ActiveBuildTarget OleanAndC namespace ActiveOleanAndCTarget @@ -96,7 +110,7 @@ def moduleOleanTarget moduleTarget oleanFile leanFile hashFile contents depTarget do compileOlean leanFile oleanFile oleanDirs rootDir leanArgs (← getLean) -protected def Package.moduleOleanAndCTarget +protected def Package.moduleOleanAndCTargetOnly (self : Package) (moreOleanDirs : List FilePath) (mod : Name) (leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) := let cFile := self.modToC mod @@ -106,7 +120,7 @@ protected def Package.moduleOleanAndCTarget moduleOleanAndCTarget leanFile cFile oleanFile traceFile oleanDirs contents depTarget self.rootDir self.moreLeanArgs -protected def Package.moduleOleanTarget +protected def Package.moduleOleanTargetOnly (self : Package) (moreOleanDirs : List FilePath) (mod : Name) (leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) := let oleanFile := self.modToOlean mod @@ -142,15 +156,15 @@ def Package.recBuildModuleOleanAndCTargetWithLocalImports [Monad m] [MonadLiftT recBuildModuleWithLocalImports self fun mod leanFile contents importTargets => do let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets - self.moduleOleanAndCTarget moreOleanDirs mod leanFile contents allDepsTarget |>.run + self.moduleOleanAndCTargetOnly moreOleanDirs mod leanFile contents allDepsTarget |>.run -def Package.recBuildModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] +def Package.recBuildModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] (self : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) : RecBuild Name ActiveFileTarget m := recBuildModuleWithLocalImports self fun mod leanFile contents importTargets => do let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets - self.moduleOleanTarget moreOleanDirs mod leanFile contents allDepsTarget |>.run + self.moduleOleanTargetOnly moreOleanDirs mod leanFile contents allDepsTarget |>.run -- ## Definitions @@ -159,11 +173,16 @@ abbrev ModuleBuildM (α) := -- phrased this way to use `NameMap` EStateT (List Name) (NameMap α) BuildM -abbrev ModuleBuild (α) := - RecBuild Name α (ModuleBuildM α) +abbrev RecModuleBuild (i) := + RecBuild Name (ActiveBuildTarget i) (ModuleBuildM (ActiveBuildTarget i)) -abbrev OleanTargetBuild := ModuleBuild ActiveFileTarget -abbrev OleanAndCTargetBuild := ModuleBuild ActiveOleanAndCTarget +-- ## Builders -abbrev OleanTargetMap := NameMap ActiveFileTarget -abbrev OleanAndCTargetMap := NameMap ActiveOleanAndCTarget +def buildModuleTarget (mod : Name) [Inhabited i] +(build : RecModuleBuild i) : BuildM (ActiveBuildTarget i) := do + failOnBuildCycle <| ← RBTopT.run' <| buildRBTop (cmp := Name.quickCmp) build id mod + +def buildModuleTargets (mods : Array Name) [Inhabited i] +(build : RecModuleBuild i) : BuildM (Array (ActiveBuildTarget i)) := do + failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| + buildRBTop (cmp := Name.quickCmp) build id diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index fabeae5e9f..8aed0781a8 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -17,107 +17,50 @@ namespace Lake -- # Build Target -abbrev ActivePackageTarget := ActiveBuildTarget (Package × NameMap ActiveOleanAndCTarget) +abbrev PackageTarget := BuildTarget Package + +abbrev ActivePackageTarget i := ActiveBuildTarget (Package × NameMap (ActiveBuildTarget i)) namespace ActivePackageTarget -def package (self : ActivePackageTarget) := +def package (self : ActivePackageTarget i) := self.info.1 -def moduleTargetMap (self : ActivePackageTarget) : NameMap ActiveOleanAndCTarget := +def moduleTargetMap (self : ActivePackageTarget i) : NameMap (ActiveBuildTarget i) := self.info.2 -def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveOleanAndCTarget) := +def moduleTargets (self : ActivePackageTarget i) : Array (Name × ActiveBuildTarget i) := self.moduleTargetMap.fold (fun arr k v => arr.push (k, v)) #[] end ActivePackageTarget /-- Returns the `oleanDir`s of the given package targets in reverse order. -/ -def packageTargetsToOleanDirs (targets : Array ActivePackageTarget) : List FilePath := +def packageTargetsToOleanDirs (targets : Array (ActivePackageTarget i)) : List FilePath := targets.map (·.package.oleanDir) |>.foldl (flip List.cons) [] --- # Build Modules - -def Package.buildModuleOleanAndCTargetDAG -(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveOleanAndCTarget × OleanAndCTargetMap) := do - let buildMod : OleanAndCTargetBuild := - self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget - let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run - (← failOnBuildCycle resE, map) - -def Package.buildModuleOleanTargetDAG -(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveFileTarget × OleanTargetMap) := do - let buildMod : OleanTargetBuild := - self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget - let (resE, map) ← RBTopT.run <| mods.mapM (buildRBTop buildMod id) - (← failOnBuildCycle resE, map) - -def Package.buildOleanAndCTargetDAG -(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveOleanAndCTarget × OleanAndCTargetMap) := do - self.buildModuleOleanAndCTargetDAG (← self.getModuleArray) moreOleanDirs depTarget - -def Package.buildOleanTargetDAG -(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveFileTarget × OleanTargetMap) := do - self.buildModuleOleanTargetDAG (← self.getModuleArray) moreOleanDirs depTarget - -def Package.buildModuleOleanAndCTargets -(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveOleanAndCTarget) := do - let buildMod : OleanAndCTargetBuild := - self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget - failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| buildRBTop buildMod id - -def Package.buildModuleOleanTargets -(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveFileTarget) := do - let buildMod : OleanTargetBuild := - self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget - failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| buildRBTop buildMod id - -def Package.buildOleanAndCTargets -(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveOleanAndCTarget) := do - self.buildModuleOleanAndCTargets (← self.getModuleArray) moreOleanDirs depTarget - -def Package.buildOleanTargets -(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) -(self : Package) : BuildM (Array ActiveFileTarget) := do - self.buildModuleOleanTargets (← self.getModuleArray) moreOleanDirs depTarget - --- # Configure/Build Packages +-- # Build Packages +/-- + Builds the package's `extraDepTarget` and combines it with + the given package targets to create a single active opaque target. +-/ def Package.buildDepTargetWith -(depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do +(depTargets : Array (ActivePackageTarget i)) (self : Package) : BuildM ActiveOpaqueTarget := do let extraDepTarget ← self.extraDepTarget.run let depTarget ← ActiveTarget.collectOpaqueArray depTargets extraDepTarget.mixOpaqueAsync depTarget -def Package.buildModuleOleanAndCTargetsWithDepTargets -(mods : Array Name) (depTargets : Array ActivePackageTarget) (self : Package) -: BuildM ActivePackageTarget := do - let depTarget ← self.buildDepTargetWith depTargets - let moreOleanDirs := packageTargetsToOleanDirs depTargets - let (targets, targetMap) ← self.buildModuleOleanAndCTargetDAG mods moreOleanDirs depTarget - let target ← ActiveTarget.collectOpaqueArray targets - return target.withInfo ⟨self, targetMap⟩ - -def Package.buildOleanAndCTargetsWithDepTargets -(depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do - self.buildModuleOleanAndCTargetsWithDepTargets (← self.getModuleArray) depTargets - /-- - The main package build function. + Build an active package target after + resolving the package's dependencies and recursively building them. - It resolves the package's dependencies and recursively builds them. - For each package, it compiles its modules into `.olean` and `.c` files. + To build each package, run the given `build` function on it, + which takes the package and its building dependencies as arguments. -/ def recBuildPackageWithDeps -[Monad m] [MonadLiftT BuildM m] [MonadStore Name (Array ActivePackageTarget) m] -: RecBuild Package (Array ActivePackageTarget) m := fun pkg buildPkg => do +[Monad m] [MonadLiftT BuildM m] [MonadStore Name (Array (ActivePackageTarget i)) m] +[Inhabited i] (build : Array (ActivePackageTarget i) → Package → BuildM (ActivePackageTarget i)) +: RecBuild Package (Array (ActivePackageTarget i)) m := fun pkg buildPkg => do let mut depTargets := #[] for dep in pkg.dependencies do let targets? ← fetch? dep.name @@ -128,29 +71,121 @@ def recBuildPackageWithDeps let depPkg ← liftM (m := BuildM) <| resolveDep pkg dep buildPkg depPkg depTargets := depTargets ++ targets - let pkgTarget ← pkg.buildOleanAndCTargetsWithDepTargets depTargets + let pkgTarget ← build depTargets pkg depTargets.push pkgTarget -def buildPackageTargetsWithDeps (pkgs : Array Package) : BuildM (Array ActivePackageTarget) := do +/-- + Build the package along with its dependencies + by using the given `build` function recursively. +-/ +def Package.buildRec (self : Package) [Inhabited i] +(build : Array (ActivePackageTarget i) → Package → BuildM (ActivePackageTarget i)) +: BuildM (ActivePackageTarget i) := do + let recBuild := recBuildPackageWithDeps build + let targets ← failOnBuildCycle <| ← RBTopT.run' <| + buildRBTop (cmp := Name.quickCmp) recBuild Package.name self + targets.back + +/-- + Build an `Array` of `Package`s along with their dependencies + by using the given `build` function recursively. +-/ +def buildPackageArrayWithDeps (pkgs : Array Package) [Inhabited i] +(build : Array (ActivePackageTarget i) → Package → BuildM (ActivePackageTarget i)) +: BuildM (Array (ActivePackageTarget i)) := do failOnBuildCycle <| ← RBTopT.run' <| pkgs.concatMapM fun pkg => - buildRBTop (cmp := Name.quickCmp) recBuildPackageWithDeps Package.name pkg + buildRBTop (cmp := Name.quickCmp) (recBuildPackageWithDeps build) Package.name pkg -def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do - (← buildPackageTargetsWithDeps #[self]).back +/-- Build the dependencies of a package (as targets) using the given `build` function. -/ +def Package.buildDepTargets [Inhabited i] +(build : Array (ActivePackageTarget i) → Package → BuildM (ActivePackageTarget i)) (self : Package) +: BuildM (Array (ActivePackageTarget i)) := do + buildPackageArrayWithDeps (← self.resolveDirectDeps) build -def Package.buildDepTargets (self : Package) : BuildM (Array ActivePackageTarget) := do - buildPackageTargetsWithDeps (← self.resolveDirectDeps) -def Package.buildDeps (self : Package) : BuildM (Array Package) := do - let targets ← self.buildDepTargets - targets.mapM fun target => Functor.mapConst target.info.1 target.materialize +/-- + Build an active target for the package by + running the given `RecModuleBuild` on the given root module. +-/ +def Package.buildModuleDAGTarget [Inhabited i] (mod : Name) +(buildMod : RecModuleBuild i) (self : Package) : BuildM (ActivePackageTarget i) := do + let (targetE, targetMap) ← RBTopT.run do + buildRBTop buildMod id mod + let target ← failOnBuildCycle targetE + return target.withInfo ⟨self, targetMap⟩ -def Package.build (self : Package) : BuildM PUnit := do - let depTargets ← self.buildDepTargets +/-- + Build an active target for the package by + running the given `RecModuleBuild` on the given root modules. +-/ +def Package.buildModulesDAGTarget [Inhabited i] (mods : Array Name) +(buildMod : RecModuleBuild i) (self : Package) : BuildM (ActivePackageTarget i) := do + let (targetsE, targetMap) ← RBTopT.run do + mods.mapM fun mod => buildRBTop buildMod id mod + let targets ← failOnBuildCycle targetsE + let target ← ActiveTarget.collectOpaqueArray targets + return target.withInfo ⟨self, targetMap⟩ + +/-- + Build an active target for the package by + running the given `RecModuleBuild` on each of its top-level modules + (i.e., those specified in its `libGlobs` configuration). +-/ +def Package.buildTarget [Inhabited i] +(buildMod : RecModuleBuild i) (self : Package) : BuildM (ActivePackageTarget i) := do + self.buildModulesDAGTarget (← self.getModuleArray) buildMod + +-- # Build Package Modules + +def Package.buildOleanTargetWithDepTargets +(depTargets : Array (ActivePackageTarget FilePath)) (self : Package) +: BuildM (ActivePackageTarget FilePath) := do let depTarget ← self.buildDepTargetWith depTargets let moreOleanDirs := packageTargetsToOleanDirs depTargets - let targets ← self.buildOleanTargets moreOleanDirs depTarget - discard <| ActiveTarget.materializeArray targets + self.buildTarget <| self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget + +/-- Build the `.olean` and files of package and its dependencies' modules. -/ +def Package.buildOleanTarget (self : Package) : BuildM (ActivePackageTarget FilePath) := do + self.buildRec buildOleanTargetWithDepTargets + +def Package.buildOleanAndCTargetWithDepTargets +(depTargets : Array (ActivePackageTarget OleanAndC)) (self : Package) +: BuildM (ActivePackageTarget OleanAndC) := do + let depTarget ← self.buildDepTargetWith depTargets + let moreOleanDirs := packageTargetsToOleanDirs depTargets + self.buildTarget <| self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget + +/-- Build the `.olean` and `.c` files of package and its dependencies' modules. -/ +def Package.buildOleanAndCTarget (self : Package) : BuildM (ActivePackageTarget OleanAndC) := do + self.buildRec buildOleanAndCTargetWithDepTargets + +def Package.buildDepOleans (self : Package) : BuildM PUnit := do + let targets ← self.buildDepTargets buildOleanTargetWithDepTargets + targets.forM fun target => discard <| target.materialize + +def Package.oleanTarget (self : Package) : PackageTarget := + Target.mk self do pure (← self.buildOleanTarget).task + +def Package.build (self : Package) : BuildM PUnit := do + discard (← self.buildOleanTarget).materialize + +-- # Build Specific Modules of the Package + +def Package.moduleOleanTarget (mod : Name) (self : Package) : FileTarget := + Target.mk (self.modToOlean mod) do + let depTargets ← self.buildDepTargets buildOleanTargetWithDepTargets + let depTarget ← self.buildDepTargetWith depTargets + let moreOleanDirs := packageTargetsToOleanDirs depTargets + let build := self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget + pure (← buildModuleTarget mod build).task + +def Package.moduleOleanAndCTarget (mod : Name) (self : Package) : OleanAndCTarget := + Target.mk ⟨self.modToOlean mod, self.modToC mod⟩ do + let depTargets ← self.buildDepTargets buildOleanAndCTargetWithDepTargets + let depTarget ← self.buildDepTargetWith depTargets + let moreOleanDirs := packageTargetsToOleanDirs depTargets + let build := self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget + pure (← buildModuleTarget mod build).task -- # Build Imports @@ -168,16 +203,17 @@ def Package.filterLocalImports def Package.buildImportsAndDeps (imports : List String := []) (self : Package) : BuildM (List Package) := do -- resolve and build deps - let depTargets ← self.buildDepTargets + let depTargets ← self.buildDepTargets buildOleanTargetWithDepTargets let depTarget ← self.buildDepTargetWith depTargets let depPkgs := depTargets.map (·.package) |>.foldl (flip List.cons) [] if imports.isEmpty then -- wait for deps to finish building discard depTarget.materialize else - -- build additional imports + -- build local imports from list let moreOleanDirs := depPkgs.map (·.oleanDir) let localImports := self.filterLocalImports imports - let oleanTargets ← self.buildModuleOleanTargets localImports moreOleanDirs depTarget - oleanTargets.forM (discard ·.materialize) + let build := self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget + let targets ← buildModuleTargets localImports build + targets.forM (discard ·.materialize) return self :: depPkgs