From 672814dd06b7bf8840ed0439fbe9b62e05937884 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 17 Jun 2024 11:42:59 -0400
Subject: [PATCH] feat: expose flags for the bundled C compiler

---
 src/Lean/Compiler/FFI.lean | 14 ++++++++++++++
 src/Leanc.lean             | 30 ++++++++++++++----------------
 src/util/ffi.cpp           |  8 ++++++++
 3 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Compiler/FFI.lean b/src/Lean/Compiler/FFI.lean
index 4c63777cecd2..85e95a373086 100644
--- a/src/Lean/Compiler/FFI.lean
+++ b/src/Lean/Compiler/FFI.lean
@@ -18,6 +18,13 @@ private opaque getLeancExtraFlags : Unit → String
 def getCFlags (leanSysroot : FilePath) : Array String :=
   #["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn
 
+@[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)
+
 @[extern "lean_get_linker_flags"]
 private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 
@@ -25,4 +32,11 @@ private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
   #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn
 
+@[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)
+
 end Lean.Compiler.FFI
diff --git a/src/Leanc.lean b/src/Leanc.lean
index 1e397e7ecd75..111eef50ac43 100644
--- a/src/Leanc.lean
+++ b/src/Leanc.lean
@@ -8,10 +8,15 @@ import Lean.Compiler.FFI
 open Lean.Compiler.FFI
 
 def main (args : List String) : IO UInt32 := do
+  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
+    | some root => pure <| System.FilePath.mk root
+    | none      => pure <| (← IO.appDir).parent.get!
+  let mut cc := "@LEANC_CC@".replace "ROOT" root.toString
+
   if args.isEmpty then
-    IO.println "Lean C compiler
+    IO.println s!"Lean C compiler
 
-A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`,
+A simple wrapper around a C compiler. Defaults to `{cc}`,
 which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
 as-is to the wrapped compiler.
 
@@ -20,11 +25,6 @@ Interesting options:
 * `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit"
     return 1
 
-  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
-    | some root => pure <| System.FilePath.mk root
-    | none      => pure <| (← IO.appDir).parent.get!
-  let rootify s := s.replace "ROOT" root.toString
-
   -- It is difficult to identify the correct minor version here, leading to linking warnings like:
   -- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
   -- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
@@ -38,29 +38,27 @@ Interesting options:
 
   -- We assume that the CMake variables do not contain escaped spaces
   let cflags := getCFlags root
-  let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
-  let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
+  let mut cflagsInternal := getInternalCFlags root
+  let mut ldflagsInternal := getInternalLinkerFlags root
   let ldflags := getLinkerFlags root linkStatic
 
   for arg in args do
     match arg with
     | "--print-cflags" =>
-      IO.println <| " ".intercalate (cflags.map rootify |>.toList)
+      IO.println <| " ".intercalate cflags.toList
       return 0
     | "--print-ldflags" =>
-      IO.println <| " ".intercalate ((cflags ++ ldflags).map rootify |>.toList)
+      IO.println <| " ".intercalate (cflags ++ ldflags).toList
       return 0
     | _ => pure ()
 
-  let mut cc := "@LEANC_CC@"
   if let some cc' ← IO.getEnv "LEAN_CC" then
     cc := cc'
     -- these are intended for the bundled compiler only
-    cflagsInternal := []
-    ldflagsInternal := []
-  cc := rootify cc
+    cflagsInternal := #[]
+    ldflagsInternal := #[]
   let args := cflags ++ cflagsInternal ++ args ++ ldflagsInternal ++ ldflags ++ ["-Wno-unused-command-line-argument"]
-  let args := args.filter (!·.isEmpty) |>.map rootify
+  let args := args.filter (!·.isEmpty)
   if args.contains "-v" then
     IO.eprintln s!"{cc} {" ".intercalate args.toList}"
   let child ← IO.Process.spawn { cmd := cc, args, env }
diff --git a/src/util/ffi.cpp b/src/util/ffi.cpp
index 923fe818c30e..6e53d7cca5e3 100644
--- a/src/util/ffi.cpp
+++ b/src/util/ffi.cpp
@@ -13,7 +13,15 @@ extern "C" object * lean_get_leanc_extra_flags(object *) {
     return lean_mk_string("@LEANC_EXTRA_FLAGS@");
 }
 
+extern "C" object * lean_get_leanc_internal_flags(object *) {
+    return lean_mk_string("@LEANC_INTERNAL_FLAGS@");
+}
+
 extern "C" object * lean_get_linker_flags(uint8 link_static) {
     return lean_mk_string(link_static ? "@LEANC_STATIC_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@" : "@LEANC_SHARED_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@");
 }
+
+extern "C" object * lean_get_internal_linker_flags(object *) {
+    return lean_mk_string("@LEANC_INTERNAL_LINKER_FLAGS@");
+}
 }