max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: use MoveFileEx for rename on win

Browse source
This commit is contained in:
Mario Carneiro 2023-09-15 02:06:11 -04:00 • committed by Sebastian Ullrich
parent 6bd0a615f1
commit f0af71a57b
2 changed files with 20 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/runtime/io.cpp
View file

@ -660,7 +660,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
}
extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean_object * /* w */) {
if (std::rename(string_cstr(from), string_cstr(to)) == 0) {
#ifdef LEAN_WINDOWS
// Note: On windows, std::rename gives an error if the `to` file already exists,
// 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;
#else
bool ok = std::rename(string_cstr(from), string_cstr(to)) == 0;
#endif
if (ok) {
return io_result_mk_ok(box(0));
} else {
std::ostringstream s;

20
tests/lean/run/IO_test.lean
View file

@ -35,6 +35,7 @@ pure ()
#eval test
def test2 : IO Unit := do
let fn1 := "bar2.txt";
let fn2 := "foo2.txt";
let xs₀ : String := "⟨[₂,α]⟩";
let xs₁ := "⟨[6,8,@]⟩";
@ -43,14 +44,15 @@ let xs₂ := "/* Handle.getLine : Handle → IO Unit */" ++
"/* is truncated at the first \'\\0\' character and the */" ++
"/* rest of the line is discarded. */";
-- multi-buffer line
withFile fn2 Mode.write $ fun h => pure ();
withFile fn1 Mode.write $ fun _h => pure ();
withFile fn2 Mode.write $ fun h => do
{ h.putStr xs₀;
h.putStrLn xs₀;
h.putStrLn xs₂;
h.putStrLn xs₁;
pure () };
withFile fn1 Mode.write $ fun h => do
h.putStr xs₀
h.putStrLn xs₀
h.putStrLn xs₂
h.putStrLn xs₁
withFile fn2 Mode.write $ fun h => h.putStr "overwritten"
rename fn1 fn2
let ys ← withFile fn2 Mode.read $ fun h => h.getLine;
IO.println ys;
check_eq "1" (xs₀ ++ xs₀ ++ "\n") ys;
@ -80,7 +82,7 @@ let xs₀ := "abc"
let xs₁ := ""
let xs₂ := "hello"
let xs₃ := "world"
withFile fn3 Mode.write $ fun h => do {
withFile fn3 Mode.write $ fun _h => do {
pure ()
}
let ys ← lines fn3
@ -100,7 +102,7 @@ pure ()
def test4 : IO Unit := do
let fn4 := "foo4.txt"
withFile fn4 Mode.write fun h => do pure ();
withFile fn4 Mode.write fun _h => do pure ();
let ys ← withFile fn4 Mode.read $ fun h => h.read 1;
check_eq "1" [] ys.toList
let ys ← withFile fn4 Mode.read $ fun h => h.read 1;