diff --git a/src/Leanc.lean b/src/Leanc.lean index 111eef50ac..da517a3bf8 100644 --- a/src/Leanc.lean +++ b/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 diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean index d5bba969d9..0f3c2ab84c 100644 --- a/src/lake/Lake/Config/LeanExe.lean +++ b/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. diff --git a/tests/compiler/utf8Path.lean b/tests/compiler/utf8Path.lean new file mode 100644 index 0000000000..2a35d4fdd6 --- /dev/null +++ b/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") diff --git a/tests/compiler/utf8Path.lean.expected.out b/tests/compiler/utf8Path.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2