diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 506432b08e..c87a6f4119 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -1122,6 +1122,8 @@ structure Metadata where Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file. -/ type : FileType + /-- The number of hard links to the file. -/ + numLinks : UInt64 deriving Repr end FS diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index c6d9796ddf..7f1e96f870 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -1094,28 +1094,20 @@ structure Metadata where constant metadata : @& FilePath → IO IO.FS.Metadata */ -static obj_res timespec_to_obj(timespec const & ts) { +static obj_res timespec_to_obj(uv_timespec_t const & ts) { object * o = alloc_cnstr(0, 1, sizeof(uint32)); cnstr_set(o, 0, lean_int64_to_int(ts.tv_sec)); cnstr_set_uint32(o, sizeof(object *), ts.tv_nsec); return o; } -static obj_res metadata_core(struct stat const & st) { - object * mdata = alloc_cnstr(0, 2, sizeof(uint64) + sizeof(uint8)); -#ifdef __APPLE__ - cnstr_set(mdata, 0, timespec_to_obj(st.st_atimespec)); - cnstr_set(mdata, 1, timespec_to_obj(st.st_mtimespec)); -#elif defined(LEAN_WINDOWS) - // TODO: sub-second precision on Windows - cnstr_set(mdata, 0, timespec_to_obj(timespec { st.st_atime, 0 })); - cnstr_set(mdata, 1, timespec_to_obj(timespec { st.st_mtime, 0 })); -#else +static obj_res metadata_core(uv_stat_t const & st) { + object * mdata = alloc_cnstr(0, 2, 2 * sizeof(uint64) + sizeof(uint8)); cnstr_set(mdata, 0, timespec_to_obj(st.st_atim)); cnstr_set(mdata, 1, timespec_to_obj(st.st_mtim)); -#endif cnstr_set_uint64(mdata, 2 * sizeof(object *), st.st_size); - cnstr_set_uint8(mdata, 2 * sizeof(object *) + sizeof(uint64), + cnstr_set_uint64(mdata, 2 * sizeof(object *) + sizeof(uint64), st.st_nlink); + cnstr_set_uint8(mdata, 2 * sizeof(object *) + 2 * sizeof(uint64), S_ISDIR(st.st_mode) ? 0 : S_ISREG(st.st_mode) ? 1 : #ifndef LEAN_WINDOWS @@ -1130,11 +1122,16 @@ extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename) { if (strlen(fname) != lean_string_size(filename) - 1) { return mk_embedded_nul_error(filename); } - struct stat st; - if (stat(fname, &st) != 0) { - return io_result_mk_error(decode_io_error(errno, filename)); + uv_fs_t req; + int ret = uv_fs_stat(NULL, &req, fname, NULL); + if (ret < 0) { + uv_fs_req_cleanup(&req); + return io_result_mk_error(decode_uv_error(ret, filename)); + } else { + object* mdata = metadata_core(req.statbuf); + uv_fs_req_cleanup(&req); + return mdata; } - return metadata_core(st); } extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename) { @@ -1145,11 +1142,16 @@ extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename) { if (strlen(fname) != lean_string_size(filename) - 1) { return mk_embedded_nul_error(filename); } - struct stat st; - if (lstat(string_cstr(filename), &st) != 0) { - return io_result_mk_error(decode_io_error(errno, filename)); + uv_fs_t req; + int ret = uv_fs_lstat(NULL, &req, fname, NULL); + if (ret < 0) { + uv_fs_req_cleanup(&req); + return io_result_mk_error(decode_uv_error(ret, filename)); + } else { + object* mdata = metadata_core(req.statbuf); + uv_fs_req_cleanup(&req); + return mdata; } - return metadata_core(st); #endif } diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean index b4b0912b3f..4275c33c09 100644 --- a/tests/lean/run/IO_test.lean +++ b/tests/lean/run/IO_test.lean @@ -162,18 +162,21 @@ def testRemoveDirAll : IO Unit := do #eval testRemoveDirAll def testHardLink : IO Unit := do - let fn := "io_test/hardLinkTarget.txt" + let fn : System.FilePath := "io_test/hardLinkTarget.txt" let contents := "foo" writeFile fn contents - let linkFn := "io_test/hardLink.txt" + let linkFn : System.FilePath := "io_test/hardLink.txt" if (← System.FilePath.pathExists linkFn) then removeFile linkFn + check_eq "1" 1 (← fn.metadata).numLinks hardLink fn linkFn + check_eq "2" 2 (← fn.metadata).numLinks + check_eq "3" 2 (← linkFn.metadata).numLinks removeFile fn assert! !(← System.FilePath.pathExists fn) assert! (← System.FilePath.pathExists linkFn) let linkContents ← readFile linkFn - check_eq "1" contents linkContents + check_eq "4" contents linkContents #guard_msgs in #eval testHardLink