From 43d4c8fe9f5f4bc14f93fd744d6a04b4cb64014b Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 6 Oct 2025 14:22:07 -0400
Subject: [PATCH] feat: `IO.FS.hardLink` (#10676)

This PR adds the `IO.FS.hardLink` function, which can be used to create
hard links.

This is implemented via libuv's `uv_fs_link` function.

Lake hopes to make use of this function to decrease the storage cost of
restoring artifacts.

This PR also fixes some C implementation issues found in nearby similar
functions.
---
 src/Init/System/IO.lean     | 12 ++++++++++++
 src/runtime/io.cpp          | 23 ++++++++++++++++++++++-
 tests/lean/run/IO_test.lean | 17 +++++++++++++++++
 3 files changed, 51 insertions(+), 1 deletion(-)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 87aad13c2a..291d36f6b5 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -858,6 +858,18 @@ function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html
 -/
 @[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit
 
+/--
+Creates a new hard link.
+
+The `link` path will be a link pointing to the `orig` path.
+Note that systems often require these two paths to both be located on the same filesystem.
+If `orig` names a symbolic link, it is platform-specific whether the symbolic link is followed.
+
+This function coincides with the [POSIX `link`
+function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/link.html).
+-/
+@[extern "lean_io_hard_link"] opaque hardLink (orig link : @& FilePath) : IO Unit
+
 /--
 Creates a temporary file in the most secure manner possible, returning both a `Handle` to the
 already-opened file and its path.
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index fb7f525499..01c7f05b0d 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -1172,7 +1172,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean
     }
     const char* to_str = string_cstr(to);
     if (strlen(to_str) != lean_string_size(to) - 1) {
-        inc(to);
         return mk_embedded_nul_error(to);
     }
 #ifdef LEAN_WINDOWS
@@ -1197,6 +1196,26 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean
     return io_result_mk_ok(box(0));
 }
 
+/* hardLink (orig link : @& FilePath) : IO Unit */
+extern "C" LEAN_EXPORT obj_res lean_io_hard_link(b_obj_arg orig, b_obj_arg link, lean_object * /* w */) {
+    const char* orig_str = string_cstr(orig);
+    if (strlen(orig_str) != lean_string_size(orig) - 1) {
+        return mk_embedded_nul_error(orig);
+    }
+    const char* link_str = string_cstr(link);
+    if (strlen(link_str) != lean_string_size(link) - 1) {
+        return mk_embedded_nul_error(link);
+    }
+    uv_fs_t req;
+    int ret = uv_fs_link(NULL, &req, orig_str, link_str, NULL);
+    uv_fs_req_cleanup(&req);
+    if (ret < 0) {
+        return io_result_mk_error(decode_uv_error(ret, orig));
+    } else {
+        return io_result_mk_ok(box(0));
+    }
+}
+
 /* createTempFile : IO (Handle × FilePath) */
 extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) {
     char path[PATH_MAX];
@@ -1232,6 +1251,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) {
     // Differences from lean_io_create_tempdir start here
     ret = uv_fs_mkstemp(NULL, &req, path, NULL);
     if (ret < 0) {
+        uv_fs_req_cleanup(&req);
         // If mkstemp throws an error we cannot rely on path to contain a proper file name.
         return io_result_mk_error(decode_uv_error(ret, nullptr));
     } else {
@@ -1277,6 +1297,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempdir(lean_object * /* w */) {
     // Differences from lean_io_create_tempfile start here
     ret = uv_fs_mkdtemp(NULL, &req, path, NULL);
     if (ret < 0) {
+        uv_fs_req_cleanup(&req);
         // If mkdtemp throws an error we cannot rely on path to contain a proper file name.
         return io_result_mk_error(decode_uv_error(ret, nullptr));
     } else {
diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean
index 5e626891d4..3927589060 100644
--- a/tests/lean/run/IO_test.lean
+++ b/tests/lean/run/IO_test.lean
@@ -154,3 +154,20 @@ def testRemoveDirAll : IO Unit := do
     assert! (← System.FilePath.pathExists "io_test/symlink_target")
 
 #eval testRemoveDirAll
+
+def testHardLink : IO Unit := do
+  let fn := "io_test/hardLinkTarget.txt"
+  let contents := "foo"
+  writeFile fn contents
+  let linkFn := "io_test/hardLink.txt"
+  if (← System.FilePath.pathExists linkFn) then
+    removeFile linkFn
+  hardLink fn linkFn
+  removeFile fn
+  assert! !(← System.FilePath.pathExists fn)
+  assert! (← System.FilePath.pathExists linkFn)
+  let linkContents ← readFile linkFn
+  check_eq "1" contents linkContents
+
+#guard_msgs in
+#eval testHardLink