From e8a2786d6d4defa29f8991eb03e1dd975311e5ae Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 26 Mar 2024 09:00:25 +0000 Subject: [PATCH] fix: actually catch the error code from MoveFileEx (#3753) A user on Zulip [reported seeing an error code of "no error"](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60lake.20update.60.20broken.20on.20Windows.20.28.3F.29/near/429134334) here. --- src/runtime/io.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 25d2ef9026..2b3fb8e7cf 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -788,17 +788,21 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean // so we have to call the underlying windows API directly to get behavior consistent // with the unix-like OSs bool ok = MoveFileEx(string_cstr(from), string_cstr(to), MOVEFILE_REPLACE_EXISTING) != 0; + if (!ok) { + // TODO: actually produce the right type of IO error + return io_result_mk_error((sstream() + << "failed to rename '" << string_cstr(from) << "' to '" << string_cstr(to) << "': " << GetLastError()).str()); + } #else bool ok = std::rename(string_cstr(from), string_cstr(to)) == 0; -#endif - if (ok) { - return io_result_mk_ok(box(0)); - } else { + if (!ok) { std::ostringstream s; s << string_cstr(from) << " and/or " << string_cstr(to); object_ref out{mk_string(s.str())}; return io_result_mk_error(decode_io_error(errno, out.raw())); } +#endif + return io_result_mk_ok(box(0)); } extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) {