refactor: include package in module info

fixes various issues with `lake print-paths` builds
2021-12-13 19:08:06 -05:00 · 2021-12-13 19:08:06 -05:00 · 8f4b203b2f
commit 8f4b203b2f
parent e054596cfa
4 changed files with 104 additions and 80 deletions
--- a/Lake/Build/Binary.lean
+++ b/Lake/Build/Binary.lean
@ -33,9 +33,8 @@ def Package.moduleOTarget (mod : Name) (self : Package) : FileTarget :=

 protected def Package.staticLibTarget (self : Package) : FileTarget :=
 Target.mk self.staticLibFile do
-    let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleTargetMap (← self.getModuleArray) $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let moduleTargetMap ← self.buildModuleMap $
+      recBuildModuleOleanAndCTargetWithLocalImports
    let oFileTargets := self.oFileTargetsOf moduleTargetMap
    staticLibTarget self.staticLibFile oFileTargets |>.materializeAsync

@ -59,9 +58,8 @@ def Package.linkTargetsOf

 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
  Target.mk self.sharedLibFile do
-    let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleTargetMap (← self.getModuleArray) $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let moduleTargetMap ← self.buildModuleMap $
+      recBuildModuleOleanAndCTargetWithLocalImports
    let linkTargets ← self.linkTargetsOf moduleTargetMap
    let target := leanSharedLibTarget self.sharedLibFile linkTargets self.moreLinkArgs
    target.materializeAsync
@ -74,7 +72,7 @@ def Package.buildSharedLib (self : Package) : BuildM FilePath :=
 protected def Package.binTarget (self : Package) : FileTarget :=
  Target.mk self.binFile do
    let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleTargetMap #[self.binRoot] $
+    let moduleTargetMap ← buildModuleMap #[⟨self, self.binRoot⟩] $
      recBuildModuleOleanAndCTargetWithLocalImports depTarget
    let pkgLinkTargets ← self.linkTargetsOf moduleTargetMap
    let linkTargets :=
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@ -140,6 +140,13 @@ protected def Package.moduleOleanTargetOnly (self : Package)

 -- # Recursive Building

+structure ModuleInfo where
+  pkg : Package
+  name : Name
+
+def ModuleInfo.srcFile (self : ModuleInfo) : FilePath :=
+  self.pkg.modToSrc self.name
+
 /-
 Produces a recursive module target builder that
 builds the target module after recursively building its local imports
@ -147,37 +154,35 @@ builds the target module after recursively building its local imports
 -/
 def recBuildModuleWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m]
-(build : Name → FilePath → String → List α → BuildM α)
-: RecBuild Name α m := fun mod recurse => do
+(build : Package → Name → FilePath → String → List α → BuildM α)
+: RecBuild ModuleInfo α m := fun info recurse => do
  have : MonadLift BuildM m := ⟨liftM⟩
  have : MonadFunctor BuildM m := ⟨fun f => monadMap (m := BuildM) f⟩
-  let pkg ← getPackage
-  let leanFile := pkg.modToSrc mod
-  let contents ← IO.FS.readFile leanFile
-  let (imports, _, _) ← Elab.parseImports contents leanFile.toString
+  let contents ← IO.FS.readFile info.srcFile
+  let (imports, _, _) ← Elab.parseImports contents info.srcFile.toString
  -- we construct the import targets even if a rebuild is not required
  -- because other build processes (ex. `.o`) rely on the map being complete
  let importTargets ← imports.filterMapM fun imp => OptionT.run do
    let mod := imp.module
    let pkg ← OptionT.mk <| getPackageForModule? mod
-    adaptPackage pkg <| recurse mod
-  build mod leanFile contents importTargets
+    adaptPackage pkg <| recurse ⟨pkg, mod⟩
+  adaptPackage info.pkg <| build info.pkg info.name info.srcFile contents importTargets

 def recBuildModuleOleanAndCTargetWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
-: RecBuild Name ActiveOleanAndCTarget m :=
-  recBuildModuleWithLocalImports fun mod leanFile contents importTargets => do
+: RecBuild ModuleInfo ActiveOleanAndCTarget m :=
+  recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
    let importTarget ← ActiveTarget.collectOpaqueList <| importTargets.map (·.oleanTarget)
    let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    (← getPackage).moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.run'
+    pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.run'

 def recBuildModuleOleanTargetWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
-: RecBuild Name ActiveFileTarget m :=
-  recBuildModuleWithLocalImports fun mod leanFile contents importTargets => do
+: RecBuild ModuleInfo ActiveFileTarget m :=
+  recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
    let importTarget ← ActiveTarget.collectOpaqueList importTargets
    let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    (← getPackage).moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.run
+    pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.run

 -- ## Definitions

@ -187,19 +192,36 @@ abbrev ModuleBuildM (α) :=
  EStateT (List Name) (NameMap α) BuildM

 abbrev RecModuleBuild (o) :=
-  RecBuild Name o (ModuleBuildM o)
+  RecBuild ModuleInfo o (ModuleBuildM o)

 abbrev RecModuleTargetBuild (i) :=
  RecModuleBuild (ActiveBuildTarget i)

 -- ## Builders

-def buildModule (mod : Name)
+/-- Build a single module using the recursive module build function `build`. -/
+def buildModule (mod : ModuleInfo)
 [Inhabited o] (build : RecModuleBuild o) : BuildM o := do
  failOnBuildCycle <| ← RBTopT.run' do
-    buildRBTop (cmp := Name.quickCmp) build id mod
+    buildRBTop (cmp := Name.quickCmp) build ModuleInfo.name mod

-def buildModules (mods : Array Name)
+/--
+Build each module using the recursive module function `build`,
+constructing an `Array`  of the results.
+-/
+def buildModuleArray (mods : Array ModuleInfo)
 [Inhabited o] (build : RecModuleBuild o) : BuildM (Array o) := do
  failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <|
-    buildRBTop (cmp := Name.quickCmp) build id
+    buildRBTop (cmp := Name.quickCmp) build ModuleInfo.name
+
+/--
+Build each module using the recursive module function `build`,
+constructing a module-target `NameMap`  of the results.
+-/
+def buildModuleMap [Inhabited o]
+(infos : Array ModuleInfo) (build : RecModuleBuild o)
+: BuildM (NameMap o) := do
+  let (x, objMap) ← RBTopT.run do
+    infos.forM fun info => discard <| buildRBTop build ModuleInfo.name info
+  failOnBuildCycle x
+  return objMap
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@ -34,42 +34,42 @@ def buildExtraDepsTarget : BuildM ActiveOpaqueTarget := do
  ActiveTarget.collectOpaqueArray <| ← do
    (← getWorkspace).packageArray.mapM (·.extraDepTarget.run)

-/--
-Build each module and using the given recursive module build function,
-constructing a module-target `NameMap`  of the results.
-/
-def buildModuleTargetMap [Inhabited i]
-(mods : Array Name) (build : RecModuleTargetBuild i)
-: BuildM (NameMap (ActiveBuildTarget i)) := do
-  let (x, targetMap) ← RBTopT.run do
-    mods.forM fun mod => discard <| buildRBTop build id mod
-  failOnBuildCycle x
-  return targetMap
-
-/--
-Build each module and using the given recursive module build function,
-constructing a single opaque target for the whole build.
-/
-def buildModulesTarget [Inhabited i] (mods : Array Name)
-(build : RecModuleTargetBuild i) : BuildM ActiveOpaqueTarget := do
-  failOnBuildCycle <| ← RBTopT.run' do
-    let targets ← mods.mapM fun mod =>
-      (·.withoutInfo) <$> buildRBTop build id mod
-    ActiveTarget.collectOpaqueArray targets
-
 -- # Build Package Modules

-/-- Build the `.olean` and files of package and its dependencies' modules. -/
-def Package.buildOleanTarget (self : Package) : BuildM ActiveOpaqueTarget := do
+/--
+Build the `extraDepTarget` of a package and its (transitive) dependencies
+and then build their modules recursively using the given `build` function,
+constructing a `NameMap` of the results.
+-/
+protected def Package.buildModuleMap [Inhabited o]
+(build : ActiveOpaqueTarget → RecModuleBuild o) (self : Package)
+: BuildM (NameMap o) := do
  let depTarget ← self.buildExtraDepsTarget
-  buildModulesTarget (← self.getModuleArray) <|
-    recBuildModuleOleanTargetWithLocalImports depTarget
+  let infos := (← self.getModuleArray).map fun mod => ModuleInfo.mk self mod
+  buildModuleMap infos (build depTarget)
+
+/--
+Build the `extraDepTarget` of a package and its (transitive) dependencies
+and then build their modules recursively using the given `build` function,
+constructing a single opaque target for the whole build.
+-/
+def Package.buildTarget [Inhabited i]
+(build : ActiveOpaqueTarget → RecModuleTargetBuild i) (self : Package)
+: BuildM ActiveOpaqueTarget := do
+  let depTarget ← self.buildExtraDepsTarget
+  let mods ← self.getModuleArray
+  failOnBuildCycle <| ← RBTopT.run' do
+    let targets ← mods.mapM fun mod => (·.withoutInfo) <$>
+      buildRBTop (build depTarget) ModuleInfo.name (ModuleInfo.mk self mod)
+    ActiveTarget.collectOpaqueArray targets
+
+/-- Build the `.olean` files of package and its dependencies' modules. -/
+def Package.buildOleanTarget (self : Package) : BuildM ActiveOpaqueTarget := do
+  self.buildTarget <| recBuildModuleOleanTargetWithLocalImports

 /-- Build the `.olean` and `.c` files of package and its dependencies' modules. -/
 def Package.buildOleanAndCTarget (self : Package) : BuildM ActiveOpaqueTarget := do
-  let depTarget ← self.buildExtraDepsTarget
-  buildModulesTarget (← self.getModuleArray) <|
-    recBuildModuleOleanAndCTargetWithLocalImports depTarget
+  self.buildTarget <| recBuildModuleOleanAndCTargetWithLocalImports

 def Package.buildDepOleans (self : Package) : BuildM PUnit := do
  let targets ← self.dependencies.mapM fun dep => do
@ -88,24 +88,27 @@ def Package.moduleOleanTarget (mod : Name) (self : Package) : FileTarget :=
  Target.mk (self.modToOlean mod) do
    let depTarget ← self.buildExtraDepsTarget
    let build := recBuildModuleOleanTargetWithLocalImports depTarget
-    return (← buildModule mod build).task
+    return (← buildModule ⟨self, mod⟩ build).task

 def Package.moduleOleanAndCTarget (mod : Name) (self : Package) : OleanAndCTarget :=
  Target.mk ⟨self.modToOlean mod, self.modToC mod⟩ do
    let depTarget ← self.buildExtraDepsTarget
    let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
-    return (← buildModule mod build).task
+    return (← buildModule ⟨self, mod⟩ build).task

 -- # Build Imports

-/-- Pick the local imports of the workspace from a list of import strings. -/
-def Workspace.filterLocalImports
-(imports : List String) (self : Workspace) : Array Name := Id.run <| do
+/--
+Construct an `Array` of `ModuleInfo`s for the workspace-local modules of
+a `List` of import strings.
+-/
+def Workspace.processImportList
+(imports : List String) (self : Workspace) : Array ModuleInfo := Id.run do
  let mut localImports := #[]
  for imp in imports do
-    let impName := imp.toName
-    if self.isLocalModule impName then
-      localImports := localImports.push impName
+    let mod := imp.toName
+    if let some pkg := self.packageForModule? mod then
+      localImports := localImports.push ⟨pkg, mod⟩
  return localImports

 /--
@ -115,18 +118,19 @@ Builds only module `.olean` files if the default package facet is
 just `oleans`. Otherwise, builds both `.olean` and `.c` files.
 -/
 def buildImportsAndDeps (imports : List String := []) : BuildM PUnit := do
-  let depTarget ← buildExtraDepsTarget
+  let pkg ← getPackage
+  let depTarget ← pkg.buildExtraDepsTarget
  if imports.isEmpty then
    -- wait for deps to finish building
    depTarget.build
  else
    -- build local imports from list
-    let localImports := (← getWorkspace).filterLocalImports imports
-    if (← getPackage).defaultFacet == PackageFacet.oleans then
+    let infos := (← getWorkspace).processImportList imports
+    if pkg.defaultFacet == PackageFacet.oleans then
      let build := recBuildModuleOleanTargetWithLocalImports depTarget
-      let targets ← buildModules localImports build
+      let targets ← buildModuleArray infos build
      targets.forM (·.build)
    else
      let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
-      let targets ← buildModules localImports build
+      let targets ← buildModuleArray infos build
      targets.forM (·.build)
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@ -34,34 +34,34 @@ def parseTargetBaseSpec (ws : Workspace) (rootPkg : Package) (spec : String) : I
  | _ =>
    error s!"invalid target spec '{spec}' (too many '/')"

-def parseTargetSpec (ws : Workspace) (rootPkg : Package) (spec : String) : IO (Package × OpaqueTarget) := do
+def parseTargetSpec (ws : Workspace) (rootPkg : Package) (spec : String) : IO (BuildTarget Package) := do
  match spec.splitOn ":" with
  | [rootSpec] =>
    let (pkg, mod?) ← parseTargetBaseSpec ws rootPkg rootSpec
    if let some mod := mod? then
-      return (pkg, pkg.moduleOleanTarget mod |>.withoutInfo)
+      return pkg.moduleOleanTarget mod |>.withInfo pkg
    else
-      return (pkg, pkg.defaultTarget)
+      return pkg.defaultTarget |>.withInfo pkg
  | [rootSpec, facet] =>
    let (pkg, mod?) ← parseTargetBaseSpec ws rootPkg rootSpec
    if let some mod := mod? then
      if facet == "olean" then
-        return (pkg, pkg.moduleOleanTarget mod |>.withoutInfo)
+        return pkg.moduleOleanTarget mod |>.withInfo pkg
      else if facet == "c" then
-        return (pkg, pkg.moduleOleanAndCTarget mod |>.withoutInfo)
+        return pkg.moduleOleanAndCTarget mod |>.withInfo pkg
      else if facet == "o" then
-        return (pkg, pkg.moduleOTarget mod |>.withoutInfo)
+        return pkg.moduleOTarget mod |>.withInfo pkg
      else
        error s!"unknown module facet '{facet}'"
    else
      if facet == "bin" then
-        return (pkg, pkg.binTarget.withoutInfo)
+        return pkg.binTarget.withInfo pkg
      else if facet == "staticLib" then
-        return (pkg, pkg.staticLibTarget.withoutInfo)
+        return pkg.staticLibTarget.withInfo pkg
      else if facet == "sharedLib" then
-        return (pkg, pkg.sharedLibTarget.withoutInfo)
+        return pkg.sharedLibTarget.withInfo pkg
      else if facet == "oleans" then
-        return (pkg, pkg.oleanTarget.withoutInfo)
+        return pkg.oleanTarget.withInfo pkg
      else
        error s!"unknown package facet '{facet}'"
  | _ =>
@ -73,4 +73,4 @@ def build (targetSpecs : List String) : BuildM PUnit := do
  if targets.isEmpty then
    pkg.defaultTarget.build
  else
-    targets.forM fun (pkg, t) => adaptPackage pkg <| t.build
+    targets.forM fun t => adaptPackage t.info <| discard <| t.build