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