use llvm-objcopy

Author: Rob23oba

src/lake/Lake/Build/Module.lean

@@ -833,15 +833,24 @@ public def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
 Recursively build the module's object file from its C file produced by `lean`.
 This version does not export any Lean symbols.
 -/
-private def Module.recBuildLeanCToONoExport (self : Module) : FetchM (Job FilePath) := do
+private def Module.recBuildOExportToONoExport (self : Module) : FetchM (Job FilePath) := do
   let suffix := if (← getIsVerbose) then " (without exports)" else ""
   withRegisterJob s!"{self.name}:c.o{suffix}" <| withCurrPackage self.pkg do
-  -- TODO: add option to pass a target triplet for cross compilation
-  buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs self.leanIncludeDir?
+  try
+    (← self.coExport.fetch).mapM fun path => do
+      discard <| IO.Process.run {
+        cmd := "llvm-objcopy"
+        args := #["--remove-section", ".drectve", path.toString, self.coNoExportFile.toString]
+      }
+      return self.coNoExportFile
+  catch _ =>
+    -- fallback if we don't have llvm-objcopy
+    -- TODO: add option to pass a target triplet for cross compilation
+    buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs self.leanIncludeDir?
 
 /-- The `ModuleFacetConfig` for the builtin `coNoExportFacet`. -/
 public def Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet :=
-  mkFacetJobConfig recBuildLeanCToONoExport
+  mkFacetJobConfig recBuildOExportToONoExport
 
 /-- The `ModuleFacetConfig` for the builtin `coFacet`. -/
 public def Module.coFacetConfig : ModuleFacetConfig coFacet :=