From 3fdaf24b49ccc1392c53afe50480a211a285e31f Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 29 May 2025 20:19:25 -0400
Subject: [PATCH] fix: lake: ensure valid use of `(sync := true)` (#8531)

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.
---
 src/lake/Lake/Build/Common.lean  | 12 ++++++------
 src/lake/Lake/Build/Imports.lean |  4 ++--
 src/lake/Lake/Build/Module.lean  |  4 ++--
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 5ce4276ed5..50fb09dc5a 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -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
diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean
index e21b258d49..77dfcb3f20 100644
--- a/src/lake/Lake/Build/Imports.lean
+++ b/src/lake/Lake/Build/Imports.lean
@@ -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
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 31d68d8ddf..c49fc5ce7f 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -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"