From 17795b02eebb6e1f83ce25fb71c53acf401708d8 Mon Sep 17 00:00:00 2001
From: Sofia Rodrigues <sofia@algebraic.dev>
Date: Tue, 31 Mar 2026 12:10:23 -0300
Subject: [PATCH] fix: missing borrow annotations in `Std.Internal.UV.System`
 (#13172)

This PR adds borrow annotations in `Std.Internal.UV.System`.
---
 src/Std/Internal/UV/System.lean |  6 +++---
 src/runtime/uv/system.cpp       | 16 ++++++++--------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Std/Internal/UV/System.lean b/src/Std/Internal/UV/System.lean
index 8f54870d58..ca2f4e8ecb 100644
--- a/src/Std/Internal/UV/System.lean
+++ b/src/Std/Internal/UV/System.lean
@@ -174,19 +174,19 @@ opaque osEnviron : IO (Array (String × String))
 Gets the value of an environment variable.
 -/
 @[extern "lean_uv_os_getenv"]
-opaque osGetenv : String → IO (Option String)
+opaque osGetenv : @& String → IO (Option String)
 
 /--
 Sets the value of an environment variable.
 -/
 @[extern "lean_uv_os_setenv"]
-opaque osSetenv : String → String → IO Unit
+opaque osSetenv : @& String → @& String → IO Unit
 
 /--
 Unsets an environment variable.
 -/
 @[extern "lean_uv_os_unsetenv"]
-opaque osUnsetenv : String → IO Unit
+opaque osUnsetenv : @& String → IO Unit
 
 /--
 Gets the hostname of the machine.
diff --git a/src/runtime/uv/system.cpp b/src/runtime/uv/system.cpp
index c5f6302ca7..f02ee3b4db 100644
--- a/src/runtime/uv/system.cpp
+++ b/src/runtime/uv/system.cpp
@@ -31,7 +31,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title() {
     return lean_io_result_mk_ok(lean_title);
 }
 
-// Std.Internal.UV.System.setProcessTitle : String → IO Unit
+// Std.Internal.UV.System.setProcessTitle : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title) {
     const char* title_str = lean_string_cstr(title);
     if (strlen(title_str) != lean_string_size(title) - 1) {
@@ -124,7 +124,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd() {
     return lean_io_result_mk_ok(lean_cwd);
 }
 
-// Std.Internal.UV.System.chdir : String → IO Unit
+// Std.Internal.UV.System.chdir : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path) {
     const char* path_str = lean_string_cstr(path);
     if (strlen(path_str) != lean_string_size(path) - 1) {
@@ -271,7 +271,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
     return lean_io_result_mk_ok(env_array);
 }
 
-// Std.Internal.UV.System.osGetenv : String → IO (Option String)
+// Std.Internal.UV.System.osGetenv : @& String → IO (Option String)
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
     const char* name_str = lean_string_cstr(name);
     if (strlen(name_str) != lean_string_size(name) - 1) {
@@ -313,7 +313,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
 }
 
 
-// Std.Internal.UV.System.osSetenv : String → String → IO Unit
+// Std.Internal.UV.System.osSetenv : @& String → @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
     const char* name_str = lean_string_cstr(name);
     const char* value_str = lean_string_cstr(value);
@@ -333,7 +333,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-// Std.Internal.UV.System.osUnsetenv : String → IO Unit
+// Std.Internal.UV.System.osUnsetenv : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
     const char* name_str = lean_string_cstr(name);
     if (strlen(name_str) != lean_string_size(name) - 1) {
@@ -641,21 +641,21 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
     );
 }
 
-// Std.Internal.UV.System.osGetenv : String → IO (Option String)
+// Std.Internal.UV.System.osGetenv : @& String → IO (Option String)
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-// Std.Internal.UV.System.osSetenv : String → String → IO Unit
+// Std.Internal.UV.System.osSetenv : @& String → @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-// Std.Internal.UV.System.osUnsetenv : String → IO Unit
+// Std.Internal.UV.System.osUnsetenv : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")