From 9c87db2d775be89171ae5da1fec7870490822dee Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 2 Apr 2025 17:16:41 +0200
Subject: [PATCH] fix: filter empty arguments from FFI flags (#7793)

This PR prevents compilation issues on some local dev configurations
---
 src/Lean/Compiler/FFI.lean | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/FFI.lean b/src/Lean/Compiler/FFI.lean
index 85e95a3730..2aa167af43 100644
--- a/src/Lean/Compiler/FFI.lean
+++ b/src/Lean/Compiler/FFI.lean
@@ -14,29 +14,32 @@ namespace Lean.Compiler.FFI
 @[extern "lean_get_leanc_extra_flags"]
 private opaque getLeancExtraFlags : Unit → String
 
+private def flagsStringToArray (s : String) : Array String :=
+  s.splitOn.toArray |>.filter (· ≠ "")
+
 /-- Return C compiler flags for including Lean's headers. -/
 def getCFlags (leanSysroot : FilePath) : Array String :=
-  #["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn
+  #["-I", (leanSysroot / "include").toString] ++ flagsStringToArray (getLeancExtraFlags ())
 
 @[extern "lean_get_leanc_internal_flags"]
 private opaque getLeancInternalFlags : Unit → String
 
 /-- Return C compiler flags needed to use the C compiler bundled with the Lean toolchain. -/
 def getInternalCFlags (leanSysroot : FilePath) : Array String :=
-  (getLeancInternalFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
+  flagsStringToArray (getLeancInternalFlags ()) |>.map (·.replace "ROOT" leanSysroot.toString)
 
 @[extern "lean_get_linker_flags"]
 private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 
 /-- Return linker flags for linking against Lean's libraries. -/
 def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
-  #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn
+  #["-L", (leanSysroot / "lib" / "lean").toString] ++ flagsStringToArray (getBuiltinLinkerFlags linkStatic)
 
 @[extern "lean_get_internal_linker_flags"]
 private opaque getBuiltinInternalLinkerFlags : Unit → String
 
 /-- Return linker flags needed to use the linker bundled with the Lean toolchain. -/
 def getInternalLinkerFlags (leanSysroot : FilePath) : Array String :=
-  (getBuiltinInternalLinkerFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
+  flagsStringToArray (getBuiltinInternalLinkerFlags ()) |>.map (·.replace "ROOT" leanSysroot.toString)
 
 end Lean.Compiler.FFI