From a67de7ebda6046f618454cb073f60a904db7e021 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Wed, 19 Mar 2025 22:58:10 -0400
Subject: [PATCH] fix: lake: use response files on Windows to avoid CLI length
 limits (#7576)

This PR changes Lake to produce and use response files on Windows when
building executables and libraries (static and shared). This is done to
avoid potentially exceeding Windows command line length limits.

Closes #4159.
---
 src/CMakeLists.txt               |  1 +
 src/lake/Lake/Build/Actions.lean | 29 ++++++++++++++++++++++-------
 src/lake/Lake/Build/Common.lean  |  4 ++--
 3 files changed, 25 insertions(+), 9 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 56a8384320..98b8c47a0c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -761,6 +761,7 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
   PATTERN "*.export"
   PATTERN "*.hash"
   PATTERN "*.trace"
+  PATTERN "*.rsp"
   EXCLUDE)
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index c8159f8570..470f266e68 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -80,6 +80,23 @@ def compileO
     args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
   }
 
+def mkArgs (basePath : FilePath) (args : Array String) : LogIO (Array String) := do
+  if Platform.isWindows then
+    -- Use response file to avoid potentially exceeding CLI length limits.
+    let rspFile := basePath.addExtension "rsp"
+    let h ← IO.FS.Handle.mk rspFile .write
+    args.forM fun arg =>
+      -- Escape special characters
+      let arg := arg.foldl (init := "") fun s c =>
+        if c == '\\' || c == '"' then
+          s.push '\\' |>.push c
+        else
+          s.push c
+      h.putStr s!"\"{arg}\"\n"
+    return #[s!"@{rspFile}"]
+  else
+    return args
+
 def compileStaticLib
   (libFile : FilePath) (oFiles : Array FilePath)
   (ar : FilePath := "ar")
@@ -87,7 +104,7 @@ def compileStaticLib
   createParentDirs libFile
   proc {
     cmd := ar.toString
-    args := #["rcs", libFile.toString] ++ oFiles.map toString
+    args := #["rcs", libFile.toString] ++ (← mkArgs libFile <| oFiles.map toString)
   }
 
 private def getMacOSXDeploymentEnv : BaseIO (Array (String × Option String)) := do
@@ -102,24 +119,22 @@ private def getMacOSXDeploymentEnv : BaseIO (Array (String × Option String)) :=
     return #[]
 
 def compileSharedLib
-  (libFile : FilePath) (linkArgs : Array String)
-  (linker : FilePath := "cc")
+  (libFile : FilePath) (linkArgs : Array String) (linker : FilePath := "cc")
 : LogIO Unit := do
   createParentDirs libFile
   proc {
     cmd := linker.toString
-    args := #["-shared", "-o", libFile.toString] ++ linkArgs
+    args := #["-shared", "-o", libFile.toString] ++ (← mkArgs libFile linkArgs)
     env := ← getMacOSXDeploymentEnv
   }
 
 def compileExe
-  (binFile : FilePath) (linkFiles : Array FilePath)
-  (linkArgs : Array String := #[]) (linker : FilePath := "cc")
+  (binFile : FilePath) (linkArgs : Array String) (linker : FilePath := "cc")
 : LogIO Unit := do
   createParentDirs binFile
   proc {
     cmd := linker.toString
-    args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
+    args := #["-o", binFile.toString] ++ (← mkArgs binFile linkArgs)
     env := ← getMacOSXDeploymentEnv
   }
 
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 36c8de46f1..59116f37ac 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -392,8 +392,8 @@ def buildLeanExe
     addPlatformTrace -- executables are platform-dependent artifacts
     buildFileUnlessUpToDate' exeFile do
       let lean ← getLeanInstall
-      let args := weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
-      compileExe exeFile links args lean.cc
+      let args := links.map toString ++ weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
+      compileExe exeFile args lean.cc
     return exeFile
 
 /--