Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

Commit

Permalink
refactor: move fetching releases to extraDep build
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed Aug 4, 2022
1 parent 884e166 commit 7ee2f76
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 12 deletions.
15 changes: 4 additions & 11 deletions Lake/Build/Module.lean
Original file line number Diff line number Diff line change
Expand Up @@ -88,35 +88,28 @@ 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
let modDynlibsJob ← BuildJob.collectArray modJobs

-- 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
Expand Down
12 changes: 11 additions & 1 deletion Lake/Build/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`. -/
Expand Down

0 comments on commit 7ee2f76

Please sign in to comment.