fix: Unicode path support for Lean Windows executables (#10133)

This PR fixes compatibility of Lean-generated executables with Unicode
file system paths on Windows

Fixes #2554

src/Leanc.lean

@@ -40,7 +40,9 @@ Interesting options:
   let cflags := getCFlags root
   let mut cflagsInternal := getInternalCFlags root
   let mut ldflagsInternal := getInternalLinkerFlags root
-  let ldflags := getLinkerFlags root linkStatic
+  let mut ldflags := getLinkerFlags root linkStatic
+  if System.Platform.isWindows && !args.contains "-shared" then
+    ldflags := ldflags ++ #["-Wl,--whole-archive", "-lleanmanifest", "-Wl,--no-whole-archive"]
 
   for arg in args do
     match arg with

src/lake/Lake/Config/LeanExe.lean

@@ -82,13 +82,15 @@ The arguments to pass to `leanc` when linking the binary executable.
 
 By default, the package's plus the executable's `moreLinkArgs`.
 If `supportInterpreter := true`, Lake prepends `-rdynamic` on non-Windows
-systems.
+systems. On Windows, it links in a manifest for Unicode path support.
 -/
-public def linkArgs (self : LeanExe) : Array String :=
+public def linkArgs (self : LeanExe) : Array String := Id.run do
+  let mut linkArgs := self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
   if self.config.supportInterpreter && !Platform.isWindows then
-    #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
-  else
-    self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+    linkArgs := #["-rdynamic"] ++ linkArgs
+  else if System.Platform.isWindows then
+    linkArgs := linkArgs ++ #["-Wl,--whole-archive", "-lleanmanifest", "-Wl,--no-whole-archive"]
+  return linkArgs
 
 /--
 Whether the Lean shared library should be dynamically linked to the executable.

tests/compiler/utf8Path.lean

@@ -0,0 +1,4 @@
+/-! Lean executables should be able to handle UTF 8 paths. -/
+
+def main : IO Unit := do
+  assert! (← System.FilePath.pathExists "../lean/run/utf8英語.lean")