From 72487e5650eabe66ccae8dfbfe11521de5453f58 Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 18 Apr 2023 11:22:23 -0400 Subject: [PATCH] fix: remove olean/ilean duplication in module traces --- Lake/Build/Facets.lean | 10 +++++++++- Lake/Build/Info.lean | 1 + Lake/Build/Module.lean | 22 ++++++++++++++-------- 3 files changed, 24 insertions(+), 9 deletions(-) diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 40ef44a3cf..c46b94cee6 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -48,11 +48,19 @@ instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) := /-- The core compilation / elaboration of the Lean file via `lean`, which produce the Lean binaries of the module (i.e., `olean`, `ilean`, `c`). -It is thus the facet used by default for building imports of a module. +Its trace just includes its dependencies. -/ abbrev Module.leanBinFacet := `bin module_data bin : BuildJob Unit +/-- +The `leanBinFacet` combined with the module's trace +(i.e., the trace of its `olean` and `ilean`). +It is the facet used for building Lean imports of a module. +-/ +abbrev Module.importBinFacet := `importBin +module_data importBin : BuildJob Unit + /-- The `olean` file produced by `lean` -/ abbrev Module.oleanFacet := `olean module_data olean : BuildJob FilePath diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 3bd211be43..fd5c6787f0 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -193,6 +193,7 @@ abbrev imports := self.facet importsFacet abbrev transImports := self.facet transImportsFacet abbrev precompileImports := self.facet precompileImportsFacet abbrev leanBin := self.facet leanBinFacet +abbrev importBin := self.facet importBinFacet abbrev olean := self.facet oleanFacet abbrev ilean := self.facet ileanFacet abbrev c := self.facet cFacet diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 99bc1ddc7b..528a86db47 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -13,7 +13,7 @@ namespace Lake def Module.buildUnlessUpToDate (mod : Module) (dynlibPath : SearchPath) (dynlibs : Array FilePath) -(depTrace : BuildTrace) : BuildM BuildTrace := do +(depTrace : BuildTrace) : BuildM PUnit := do let isOldMode ← getIsOldMode let argTrace : BuildTrace := pureHash mod.leanArgs let srcTrace : BuildTrace ← computeTrace mod.leanFile @@ -29,7 +29,6 @@ def Module.buildUnlessUpToDate (mod : Module) (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) unless isOldMode do modTrace.writeToFile mod.traceFile - return mixTrace (← computeTrace mod) depTrace /-- Compute library directories and build external library Jobs of the given packages. -/ def recBuildExternDynlibs (pkgs : Array Package) @@ -85,7 +84,7 @@ def Module.importsFacetConfig : ModuleFacetConfig importsFacet := mkFacetConfig (·.recParseImports) /-- Recursively compute a module's transitive imports. -/ -partial def Module.recComputeTransImports (mod : Module) : IndexBuildM (Array Module) := do +def Module.recComputeTransImports (mod : Module) : IndexBuildM (Array Module) := do (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do return set.appendArray (← imp.transImports.fetch) |>.insert imp @@ -94,7 +93,7 @@ def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet := mkFacetConfig (·.recComputeTransImports) /-- Recursively compute a module's precompiled imports. -/ -partial def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Module) := do +def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Module) := do (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do if imp.shouldPrecompile then return set.appendArray (← imp.transImports.fetch) |>.insert imp @@ -117,7 +116,7 @@ private def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.insert mod.pkg |>.toArray let (externJobs, libDirs) ← recBuildExternDynlibs pkgs - let importJob ← BuildJob.mixArray <| ← imports.mapM (·.leanBin.fetch) + let importJob ← BuildJob.mixArray <| ← imports.mapM (·.importBin.fetch) let externDynlibsJob ← BuildJob.collectArray externJobs let modDynlibsJob ← BuildJob.collectArray modJobs @@ -136,13 +135,19 @@ private def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) -/ let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path) - let trace ← mod.buildUnlessUpToDate dynlibPath dynlibs depTrace - return ((), trace) + mod.buildUnlessUpToDate dynlibPath dynlibs depTrace + return ((), depTrace) /-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/ def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet := mkFacetJobConfig (·.recBuildLeanCore) +/-- The `ModuleFacetConfig` for the builtin `importBinFacet`. -/ +def Module.importBinFacetConfig : ModuleFacetConfig importBinFacet := + mkFacetJobConfigSmall fun mod => do + (← mod.leanBin.fetch).bindSync fun _ depTrace => + return ((), mixTrace (← computeTrace mod) depTrace) + /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/ def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet := mkFacetJobConfigSmall fun mod => do @@ -153,7 +158,7 @@ def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet := def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet := mkFacetJobConfigSmall fun mod => do (← mod.leanBin.fetch).bindSync fun _ depTrace => - return (mod.ileanFile, depTrace) + return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace) /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/ def Module.cFacetConfig : ModuleFacetConfig cFacet := @@ -216,6 +221,7 @@ def initModuleFacetConfigs : DNameMap ModuleFacetConfig := |>.insert transImportsFacet transImportsFacetConfig |>.insert precompileImportsFacet precompileImportsFacetConfig |>.insert leanBinFacet leanBinFacetConfig + |>.insert importBinFacet importBinFacetConfig |>.insert oleanFacet oleanFacetConfig |>.insert ileanFacet ileanFacetConfig |>.insert cFacet cFacetConfig