From 7ee2f76f0fec554b8fa22a6c2723e329332eaddd Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 4 Aug 2022 18:58:17 -0400
Subject: [PATCH] refactor: move fetching releases to extraDep build

---
 Lake/Build/Module.lean  | 15 ++++-----------
 Lake/Build/Package.lean | 12 +++++++++++-
 2 files changed, 15 insertions(+), 12 deletions(-)

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`. -/