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

fix: missing borrow annotations in Std.Internal.UV.System (#13172)

Browse source 
This PR adds borrow annotations in `Std.Internal.UV.System`.
This commit is contained in:
Sofia Rodrigues 2026-03-31 12:10:23 -03:00 • committed by GitHub
parent 48800e438c
commit 17795b02ee
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Std/Internal/UV/System.lean
View file

@ -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.

16
src/runtime/uv/system.cpp
View file

@ -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.")