diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 00278f5..a21176a 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -88,16 +88,9 @@ def Module.recBuildLean (mod : Module) (art : LeanArtifact) : IndexBuildM (BuildJob (if art = .leanBin then Unit else FilePath)) := do let leanOnly := mod.isLeanOnly ∧ art ≠ .c - -- Fetch prebuilt module if desired - let isDepPkgModule := mod.pkg.name ≠ (← getWorkspace).root.name - let releaseJob ← do - if isDepPkgModule ∧ mod.pkg.preferReleaseBuild then - mod.pkg.release.fetch - else - pure .nil - -- Compute and build dependencies let (imports, _) ← mod.imports.fetch + let extraDepJob ← mod.pkg.extraDep.fetch let (modJobs, externJobs, libDirs) ← recBuildPrecompileDynlibs mod.pkg imports let importJob ← BuildJob.mixArray <| ← imports.mapM (·.leanBin.fetch) let externDynlibsJob ← BuildJob.collectArray externJobs @@ -105,18 +98,18 @@ def Module.recBuildLean (mod : Module) (art : LeanArtifact) -- Build Module let modJob : BuildJob Unit ← show SchedulerM _ from do - releaseJob.bindAsync fun _ _ => do + extraDepJob.bindAsync fun _ _ => do importJob.bindAsync fun _ importTrace => do modDynlibsJob.bindAsync fun modDynlibs modTrace => do externDynlibsJob.bindSync fun externDynlibs externTrace => do let depTrace := importTrace.mix <| modTrace.mix externTrace - let dynlibPath := libDirs ++ externDynlibs.filterMap ( ·.1) + let dynlibPath := libDirs ++ externDynlibs.filterMap ( ·.1) |>.toList -- NOTE: Lean wants the external library symbols before module symbols -- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care) let dynlibs := externDynlibs.map (.mk <| nameToSharedLib ·.2) ++ modDynlibs.map (.mk <| nameToSharedLib ·) - let trace ← mod.buildUnlessUpToDate dynlibPath.toList dynlibs depTrace leanOnly + let trace ← mod.buildUnlessUpToDate dynlibPath dynlibs depTrace leanOnly return ((), trace) -- Save All Resulting Jobs & Return Requested One diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index fa5d5d6..3f49655 100644 --- a/Lake/Build/Package.lean +++ b/Lake/Build/Package.lean @@ -27,9 +27,19 @@ def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do def Package.depsFacetConfig : PackageFacetConfig depsFacet := mkFacetConfig Package.recComputeDeps -/-- Build the `extraDepTarget` for the package and its transitive dependencies. -/ +/-- +Build the `extraDepTarget` for the package and its transitive dependencies. +Also fetch pre-built releases for the package's' dependencies. +-/ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do let job ← self.deps.foldlM (do ·.mix <| ← ·.extraDep.fetch) BuildJob.nil + -- Fetch dependency's pre-built release if desired + let isDepPkg := self.name ≠ (← getWorkspace).root.name + let job ← do + if isDepPkg ∧ self.preferReleaseBuild then + job.mix <| ← self.release.fetch + else + return job job.mix <| ← self.extraDepTarget /-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/