max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lake: ensure valid use of (sync := true) (#8531)

Browse source 
This PR fixes some places in Lake where `(sync := true)` was incorrectly
used on code that could block, and more generally improves `(sync :;=
true)` usage.
This commit is contained in:
Mac Malone 2025-05-29 20:19:25 -04:00 • committed by GitHub
parent 77e16407e4
commit 3fdaf24b49
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/lake/Lake/Build/Common.lean
View file

@ -451,8 +451,8 @@ def buildSharedLib
(extraDepTrace : JobM _ := pure BuildTrace.nil)
(plugin := false) (linkDeps := Platform.isWindows)
: SpawnM (Job Dynlib) :=
(Job.collectArray linkObjs "linkObjs").bindM fun objs => do
(Job.collectArray linkLibs "linkLibs").mapM (sync := true) fun libs => do
(Job.collectArray linkObjs "linkObjs").bindM (sync := true) fun objs => do
(Job.collectArray linkLibs "linkLibs").mapM fun libs => do
addPureTrace traceArgs "traceArgs"
addPlatformTrace -- shared libraries are platform-dependent artifacts
addTrace (← extraDepTrace)
@ -472,8 +472,8 @@ def buildLeanSharedLib
(weakArgs traceArgs : Array String := #[]) (plugin := false)
(linkDeps := Platform.isWindows)
: SpawnM (Job Dynlib) :=
(Job.collectArray linkObjs "linkObjs").bindM fun objs => do
(Job.collectArray linkLibs "linkLibs").mapM (sync := true) fun libs => do
(Job.collectArray linkObjs "linkObjs").bindM (sync := true) fun objs => do
(Job.collectArray linkLibs "linkLibs").mapM fun libs => do
addLeanTrace
addPureTrace traceArgs "traceArgs"
addPlatformTrace -- shared libraries are platform-dependent artifacts
@ -494,8 +494,8 @@ def buildLeanExe
(linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
(weakArgs traceArgs : Array String := #[]) (sharedLean : Bool := false)
: SpawnM (Job FilePath) :=
(Job.collectArray linkObjs "linkObjs").bindM fun objs => do
(Job.collectArray linkLibs "linkLibs").mapM (sync := true) fun libs => do
(Job.collectArray linkObjs "linkObjs").bindM (sync := true) fun objs => do
(Job.collectArray linkLibs "linkLibs").mapM fun libs => do
addLeanTrace
addPureTrace traceArgs "traceArgs"
addPlatformTrace -- executables are platform-dependent artifacts

4
src/lake/Lake/Build/Imports.lean
View file

@ -36,9 +36,9 @@ def buildImportsAndDeps
let impLibsJob ← fetchImportLibs precompileImports
let dynlibsJob ← root.dynlibs.fetchIn root
let pluginsJob ← root.plugins.fetchIn root
modJob.bindM fun _ =>
modJob.bindM (sync := true) fun _ =>
impLibsJob.bindM (sync := true) fun impLibs =>
dynlibsJob.bindM (sync := true) fun dynlibs =>
pluginsJob.bindM (sync := true) fun plugins =>
externLibsJob.mapM (sync := true) fun externLibs => do
externLibsJob.mapM fun externLibs => do
computeModuleDeps impLibs externLibs dynlibs plugins

4
src/lake/Lake/Build/Module.lean
View file

@ -229,13 +229,13 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg "module dynlibs"
let pluginsJob ← mod.plugins.fetchIn mod.pkg "module plugins"
extraDepJob.bindM fun _ => do
extraDepJob.bindM (sync := true) fun _ => do
importJob.bindM (sync := true) fun _ => do
let depTrace ← takeTrace
impLibsJob.bindM (sync := true) fun impLibs => do
externLibsJob.bindM (sync := true) fun externLibs => do
dynlibsJob.bindM (sync := true) fun dynlibs => do
pluginsJob.mapM (sync := true) fun plugins => do
pluginsJob.mapM fun plugins => do
let libTrace ← takeTrace
setTraceCaption s!"{mod.name.toString}:deps"
let depTrace := depTrace.withCaption "deps"