fix: use MoveFileEx for rename on win

[digama0]

As discovered on Zulip, the C++ standard std::rename function does not overwrite the target on windows, unlike on linux and macos. https://doc.rust-lang.org/std/fs/fn.rename.html mentions that it uses MoveFileExW(from, to, MOVEFILE_REPLACE_EXISTING) on windows to address this issue, so we implement the same fix here.

[leanprover-community-mathlib4-bot]

• ❌ Mathlib branch lean-pr-testing-2546 built against this PR, but testing failed. (2023-09-15 12:58:32) View Log
• ✅ Mathlib branch lean-pr-testing-2546 has successfully built against this PR. (2023-09-18 02:24:13) View Log

[eyelash]

Does this work correctly for paths that contain (non-ASCII) Unicode characters?

[semorrison]

Could we add a test for the basic functionality? Might as well answer @eyelash's question at the same time.

Probably we should also copy the "platform specific behaviour" section from https://doc.rust-lang.org/std/fs/fn.rename.html, and/or include that link.

[digama0]

It is supposed to support non-ASCII, I don't see why it wouldn't, but it needs testing on a windows machine and I don't have one.

[eyelash]

It is supposed to support non-ASCII, I don't see why it wouldn't

The reason I was asking was because of these lines:

std::wstring wfrom(string_cstr(from), string_cstr(from) + string_size(from));
std::wstring wto(string_cstr(to), string_cstr(to) + string_size(to));

I'm assuming that string_cstr returns a UTF-8 string and MoveFileExW takes a UTF-16 string and I don't see any conversion from UTF-8 to UTF-16 here.

By the way just calling the standard library with UTF-8 strings on Windows often does not work for non-ASCII strings so there might be more problems in this file related to Unicode on Windows. The following page provides some more information: https://learn.microsoft.com/en-us/windows/apps/design/globalizing/use-utf8-code-page

[digama0]

I'm assuming that string_cstr returns a UTF-8 string and MoveFileExW takes a UTF-16 string and I don't see any conversion from UTF-8 to UTF-16 here.

The conversion is the wstring constructor, or at least it's supposed to... Like I said I have no ability to test this so someone else will have to tell me if it works.

[semorrison]

A test file would run on Windows during CI! :-)

[digama0]

I'm not sure I want to add tests which actually hit the filesystem...

[Kha]

Please use the MoveFileEx base function like we do everywhere else. We do use the UTF-8 codepage... sometimes #2554.

I'm not sure I want to add tests which actually hit the filesystem...

We already have IO_test.lean

[digama0]

Please use the MoveFileEx base function like we do everywhere else. We do use the UTF-8 codepage... sometimes #2554.

I'd be happy to use what is used elsewhere, I'm 100% cargo culting this code and don't do windows programming normally. But a grep for MoveFileEx comes up empty, do you have other examples?

[Kha]

Bad wording, I just meant that we never use the *W variants and instead trust in the codepage

[Kha]

Thanks!