diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean index 35fa4bf09a64..0e14e4e93572 100644 --- a/src/lake/Lake/Build/Executable.lean +++ b/src/lake/Lake/Build/Executable.lean @@ -23,11 +23,11 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) := let mut linkJobs := #[] for facet in self.root.nativeFacets self.supportInterpreter do linkJobs := linkJobs.push <| ← fetch <| self.root.facet facet.name - let imports ← self.root.transImports.fetch + let imports ← (← self.root.transImports.fetch).await for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name - let deps := (← fetch <| self.pkg.facet `deps).push self.pkg + let deps := (← (← fetch <| self.pkg.facet `deps).await).push self.pkg for dep in deps do for lib in dep.externLibs do linkJobs := linkJobs.push <| ← lib.static.fetch buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean index dd9e9c0d4bfc..df243cf6726a 100644 --- a/src/lake/Lake/Build/Imports.lean +++ b/src/lake/Lake/Build/Imports.lean @@ -27,7 +27,7 @@ def buildImportsAndDeps (leanFile : FilePath) (imports : Array Module) : FetchM else -- build local imports from list let modJob := Job.mixArray <| ← imports.mapM (·.olean.fetch) - let precompileImports ← computePrecompileImportsAux leanFile imports + let precompileImports ← (← computePrecompileImportsAux leanFile imports).await let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray let externLibJob := Job.collectArray <| ← pkgs.flatMapM (·.externLibs.mapM (·.dynlib.fetch)) diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean index c87e29ab6b43..31777c0f9649 100644 --- a/src/lake/Lake/Build/Info.lean +++ b/src/lake/Lake/Build/Info.lean @@ -125,15 +125,15 @@ definitions. /-- The direct local imports of the Lean module. -/ abbrev Module.importsFacet := `lean.imports -module_data lean.imports : Array Module +module_data lean.imports : Job (Array Module) /-- The transitive local imports of the Lean module. -/ abbrev Module.transImportsFacet := `lean.transImports -module_data lean.transImports : Array Module +module_data lean.transImports : Job (Array Module) /-- The transitive local imports of the Lean module. -/ abbrev Module.precompileImportsFacet := `lean.precompileImports -module_data lean.precompileImports : Array Module +module_data lean.precompileImports : Job (Array Module) /-- Shared library for `--load-dynlib`. -/ abbrev Module.dynlibFacet := `dynlib @@ -141,11 +141,11 @@ module_data dynlib : Job Dynlib /-- A Lean library's Lean modules. -/ abbrev LeanLib.modulesFacet := `modules -library_data modules : Array Module +library_data modules : Job (Array Module) /-- The package's complete array of transitive dependencies. -/ abbrev Package.depsFacet := `deps -package_data deps : Array Package +package_data deps : Job (Array Package) /-! diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 6090f0eae9a4..b72a7314180a 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/src/lake/Lake/Build/Job.lean @@ -32,6 +32,9 @@ def JobState.merge (a b : JobState) : JobState where @[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) := {s with log := f s.log} +@[inline] def JobState.logEntry (e : LogEntry) (s : JobState) := + s.modifyLog (·.push e) + /-- Add log entries to the beginning of the job's log. -/ def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α := match self with diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean index 426661e16689..4635000e7213 100644 --- a/src/lake/Lake/Build/Library.lean +++ b/src/lake/Lake/Build/Library.lean @@ -20,19 +20,19 @@ open System (FilePath) Collect the local modules of a library. That is, the modules from `getModuleArray` plus their local transitive imports. -/ -partial def LeanLib.recCollectLocalModules (self : LeanLib) : FetchM (Array Module) := do +partial def LeanLib.recCollectLocalModules (self : LeanLib) : FetchM (Job (Array Module)) := ensureJob do let mut mods := #[] let mut modSet := ModuleSet.empty for mod in (← self.getModuleArray) do (mods, modSet) ← go mod mods modSet - return mods + return Job.pure mods where go root mods modSet := do let mut mods := mods let mut modSet := modSet unless modSet.contains root do modSet := modSet.insert root - let imps ← root.imports.fetch + let imps ← (← root.imports.fetch).await for mod in imps do if self.isLocalModule mod.name then (mods, modSet) ← go mod mods modSet @@ -41,11 +41,11 @@ where /-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/ def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet := - mkFacetConfig LeanLib.recCollectLocalModules + mkFacetJobConfig LeanLib.recCollectLocalModules protected def LeanLib.recBuildLean (self : LeanLib) : FetchM (Job Unit) := do - let mods ← self.modules.fetch + let mods ← (← self.modules.fetch).await mods.foldlM (init := Job.nil) fun job mod => do return job.mix <| ← mod.leanArts.fetch @@ -61,7 +61,7 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet := else "" withRegisterJob s!"{self.name}:static{suffix}" do - let mods ← self.modules.fetch + let mods ← (← self.modules.fetch).await let oJobs ← mods.flatMapM fun mod => mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile @@ -81,7 +81,7 @@ def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFacet := protected def LeanLib.recBuildShared (self : LeanLib) : FetchM (Job FilePath) := do withRegisterJob s!"{self.name}:shared" do - let mods ← self.modules.fetch + let mods ← (← self.modules.fetch).await let oJobs ← mods.flatMapM fun mod => mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 6479d2d92381..f4bc6153d4bf 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -31,7 +31,8 @@ def recBuildExternDynlibs (pkgs : Array Package) Recursively parse the Lean files of a module and its imports building an `Array` product of its direct local imports. -/ -def Module.recParseImports (mod : Module) : FetchM (Array Module) := do +def Module.recParseImports (mod : Module) : FetchM (Job (Array Module)) := + withRegisterJob s!"{mod.name}:imports" <| Job.async do let contents ← IO.FS.readFile mod.leanFile let imports ← Lean.parseImports' contents mod.leanFile.toString let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp => @@ -40,41 +41,52 @@ def Module.recParseImports (mod : Module) : FetchM (Array Module) := do /-- The `ModuleFacetConfig` for the builtin `importsFacet`. -/ def Module.importsFacetConfig : ModuleFacetConfig importsFacet := - mkFacetConfig (·.recParseImports) + mkFacetJobConfig recParseImports + +structure ModuleImportData where + module : Module + transImports : Job (Array Module) + includeSelf : Bool @[inline] def collectImportsAux (leanFile : FilePath) (imports : Array Module) - (f : Module → FetchM (Bool × Array Module)) -: FetchM (Array Module) := do - withLogErrorPos do - let mut didError := false - let mut importSet := OrdModuleSet.empty - for imp in imports do - try - let (includeSelf, transImps) ← f imp - importSet := importSet.appendArray transImps - if includeSelf then importSet := importSet.insert imp - catch errPos => - dropLogFrom errPos - logError s!"{leanFile}: bad import '{imp.name}'" - didError := true - if didError then - failure - else - return importSet.toArray + (f : Module → FetchM (Bool × Job (Array Module))) +: FetchM (Job (Array Module)) := do + let imps ← imports.mapM fun imp => do + let (includeSelf, transImports) ← f imp + return {module := imp, transImports, includeSelf : ModuleImportData} + let task : JobTask OrdModuleSet := imps.foldl (init := .pure (.ok .empty {})) fun r imp => + r.bind (sync := true) fun r => + imp.transImports.task.map (sync := true) fun + | .ok transImps _ => + match r with + | .ok impSet s => + let impSet := impSet.appendArray transImps + let impSet := if imp.includeSelf then impSet.insert imp.module else impSet + .ok impSet s + | .error e s => .error e s + | .error _ _ => + let entry := LogEntry.error s!"{leanFile}: bad import '{imp.module.name}'" + match r with + | .ok _ s => .error 0 (s.logEntry entry) + | .error e s => .error e (s.logEntry entry) + return Job.ofTask <| task.map (sync := true) fun + | .ok impSet s => .ok impSet.toArray s + | .error e s => .error e s /-- Recursively compute a module's transitive imports. -/ -def Module.recComputeTransImports (mod : Module) : FetchM (Array Module) := do - collectImportsAux mod.leanFile (← mod.imports.fetch) fun imp => +def Module.recComputeTransImports (mod : Module) : FetchM (Job (Array Module)) := + withRegisterJob s!"{mod.name}:transImports" do + collectImportsAux mod.leanFile (← (← mod.imports.fetch).await) fun imp => (true, ·) <$> imp.transImports.fetch /-- The `ModuleFacetConfig` for the builtin `transImportsFacet`. -/ def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet := - mkFacetConfig (·.recComputeTransImports) + mkFacetJobConfig recComputeTransImports -@[inline] def computePrecompileImportsAux +def computePrecompileImportsAux (leanFile : FilePath) (imports : Array Module) -: FetchM (Array Module) := do +: FetchM (Job (Array Module)) := do collectImportsAux leanFile imports fun imp => if imp.shouldPrecompile then (true, ·) <$> imp.transImports.fetch @@ -82,12 +94,13 @@ def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet := (false, ·) <$> imp.precompileImports.fetch /-- Recursively compute a module's precompiled imports. -/ -def Module.recComputePrecompileImports (mod : Module) : FetchM (Array Module) := do - computePrecompileImportsAux mod.leanFile (← mod.imports.fetch) +def Module.recComputePrecompileImports (mod : Module) : FetchM (Job (Array Module)) := + withRegisterJob s!"{mod.name}:precompileImports" do + inline <| computePrecompileImportsAux mod.leanFile (← (← mod.imports.fetch).await) /-- The `ModuleFacetConfig` for the builtin `precompileImportsFacet`. -/ def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet := - mkFacetConfig (·.recComputePrecompileImports) + mkFacetJobConfig recComputePrecompileImports /-- Recursively build a module's dependencies, including: @@ -103,13 +116,14 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job (SearchPath × Array FilePa precompiled imports so that errors in the import block of transitive imports will not kill this job before the direct imports are built. -/ - let directImports ← mod.imports.fetch + let directImports ← (← mod.imports.fetch).await let importJob := Job.mixArray <| ← directImports.mapM fun imp => do if imp.name = mod.name then logError s!"{mod.leanFile}: module imports itself" imp.olean.fetch let precompileImports ← if mod.shouldPrecompile then mod.transImports.fetch else mod.precompileImports.fetch + let precompileImports ← precompileImports.await let modLibJobs ← precompileImports.mapM (·.dynlib.fetch) let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty let pkgs := if mod.shouldPrecompile then pkgs.insert mod.pkg else pkgs @@ -140,7 +154,7 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job (SearchPath × Array FilePa /-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/ def Module.depsFacetConfig : ModuleFacetConfig depsFacet := - mkFacetJobConfig (·.recBuildDeps) + mkFacetJobConfig recBuildDeps /-- Remove cached file hashes of the module build outputs (in `.hash` files). -/ def Module.clearOutputHashes (mod : Module) : IO PUnit := do @@ -292,7 +306,7 @@ def Module.recBuildDynlib (mod : Module) : FetchM (Job Dynlib) := withRegisterJob s!"{mod.name}:dynlib" do -- Compute dependencies - let transImports ← mod.transImports.fetch + let transImports ← (← mod.transImports.fetch).await let modJobs ← transImports.mapM (·.dynlib.fetch) let pkgs := transImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.insert mod.pkg |>.toArray diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 6c7bd2b2e6d3..48a4e9a12d22 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -8,6 +8,7 @@ import Lake.Util.Git import Lake.Util.Sugar import Lake.Build.Common import Lake.Build.Targets +import Lake.Build.Topological import Lake.Reservoir /-! # Package Facet Builds @@ -19,16 +20,17 @@ namespace Lake open Lean (Name) /-- Compute a topological ordering of the package's transitive dependencies. -/ -def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do - (·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do +def Package.recComputeDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do + (pure ·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do let some dep ← findPackage? cfg.name | error s!"{self.name}: package not found for dependency '{cfg.name}' \ (this is likely a bug in Lake)" - return (← fetch <| dep.facet `deps).foldl (·.insert ·) deps |>.insert dep + let depDeps ← (← fetch <| dep.facet `deps).await + return depDeps.foldl (·.insert ·) deps |>.insert dep /-- The `PackageFacetConfig` for the builtin `depsFacet`. -/ def Package.depsFacetConfig : PackageFacetConfig depsFacet := - mkFacetConfig Package.recComputeDeps + mkFacetJobConfig recComputeDeps /-- Tries to download and unpack the package's cached build archive diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index d349df91d7ff..3e11a65e76fb 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -137,22 +137,34 @@ protected def LogEntry.toString (self : LogEntry) (useAnsi := false) : String := instance : ToString LogEntry := ⟨LogEntry.toString⟩ +@[inline] def LogEntry.trace (message : String) : LogEntry := + {level := .trace, message} + +@[inline] def LogEntry.info (message : String) : LogEntry := + {level := .info, message} + +@[inline] def LogEntry.warning (message : String) : LogEntry := + {level := .warning, message} + +@[inline] def LogEntry.error (message : String) : LogEntry := + {level := .error, message} + class MonadLog (m : Type u → Type v) where logEntry (e : LogEntry) : m PUnit export MonadLog (logEntry) @[inline] def logVerbose [Monad m] [MonadLog m] (message : String) : m PUnit := do - logEntry {level := .trace, message} + logEntry (.trace message) @[inline] def logInfo [Monad m] [MonadLog m] (message : String) : m PUnit := do - logEntry {level := .info, message} + logEntry (.info message) @[inline] def logWarning [MonadLog m] (message : String) : m PUnit := - logEntry {level := .warning, message} + logEntry (.warning message) -@[inline] def logError [MonadLog m] (message : String) : m PUnit := - logEntry {level := .error, message} +@[inline] def logError [MonadLog m] (message : String) : m PUnit := + logEntry (.error message) @[specialize] def logSerialMessage (msg : SerialMessage) [MonadLog m] : m PUnit := let str := if msg.caption.trim.isEmpty then