From bf2e91b6d1afc275bf0cdcfc0d8458d185e79d21 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 27 Jun 2025 13:31:34 -0300 Subject: [PATCH] feat: add system information functions to the standard library (#8109) This PR adds system information functions to the standard library --- src/Std/Internal/Async.lean | 2 + src/Std/Internal/Async/Process.lean | 238 +++++++++ src/Std/Internal/Async/System.lean | 317 +++++++++++ src/Std/Internal/UV.lean | 1 + src/Std/Internal/UV/System.lean | 263 +++++++++ src/runtime/CMakeLists.txt | 2 +- src/runtime/uv/dns.cpp | 4 +- src/runtime/uv/system.cpp | 714 +++++++++++++++++++++++++ src/runtime/uv/system.h | 44 ++ tests/lean/run/async_systems_info.lean | 107 ++++ 10 files changed, 1689 insertions(+), 3 deletions(-) create mode 100644 src/Std/Internal/Async/Process.lean create mode 100644 src/Std/Internal/Async/System.lean create mode 100644 src/Std/Internal/UV/System.lean create mode 100644 src/runtime/uv/system.cpp create mode 100644 src/runtime/uv/system.h create mode 100644 tests/lean/run/async_systems_info.lean diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean index be28420ff2..647b0b0f12 100644 --- a/src/Std/Internal/Async.lean +++ b/src/Std/Internal/Async.lean @@ -10,3 +10,5 @@ import Std.Internal.Async.TCP import Std.Internal.Async.UDP import Std.Internal.Async.DNS import Std.Internal.Async.Select +import Std.Internal.Async.Process +import Std.Internal.Async.System diff --git a/src/Std/Internal/Async/Process.lean b/src/Std/Internal/Async/Process.lean new file mode 100644 index 0000000000..089edc84d2 --- /dev/null +++ b/src/Std/Internal/Async/Process.lean @@ -0,0 +1,238 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +prelude +import Std.Time +import Std.Internal.UV.System +import Std.Data.HashMap + +open Std Time +open System + +namespace Std +namespace Internal +namespace IO +namespace Process + +/-- +Represents resource usage statistics for a process or thread. +All time values are in milliseconds. +-/ +structure ResourceUsageStats where + /-- + CPU time spent in user mode (milliseconds) + -/ + cpuUserTime : Time.Millisecond.Offset + + /-- + CPU time spent in kernel mode (milliseconds) + -/ + cpuSystemTime : Time.Millisecond.Offset + + /-- + Peak resident set size (max physical memory usage) in kilobytes + -/ + peakResidentSetSizeKb : UInt64 + + /-- + Size of shared memory segments (kilobytes) + -/ + sharedMemorySizeKb : UInt64 + + /-- + Size of unshared data segment (kilobytes) + -/ + unsharedDataSizeKb : UInt64 + + /-- + Size of unshared stack segment (kilobytes) + -/ + unsharedStackSizeKb : UInt64 + + /-- + Number of minor (soft) page faults (no disk I/O) + -/ + minorPageFaults : UInt64 + + /-- + Number of major (hard) page faults (disk I/O required) + -/ + majorPageFaults : UInt64 + + /-- + Number of swap ins or swap outs + -/ + swapOperations : UInt64 + + /-- + Number of block input operations (disk reads) + -/ + blockInputOps : UInt64 + + /-- + Number of block output operations (disk writes) + -/ + blockOutputOps : UInt64 + + /-- + Number of IPC messages sent + -/ + messagesSent : UInt64 + + /-- + Number of IPC messages received + -/ + messagesReceived : UInt64 + + /-- + Number of signals received + -/ + signalsReceived : UInt64 + + /-- + Number of voluntary context switches (process yielded CPU) + -/ + voluntaryContextSwitches : UInt64 + + /-- + Number of involuntary context switches (process preempted) + -/ + involuntaryContextSwitches : UInt64 +deriving Repr, Inhabited + + +/-- +A process identifier, represented by a numeric ID in UNIX systems (e.g. 1000). +-/ +structure PId where + /-- + The numeric process ID. + -/ + toUInt64 : UInt64 +deriving Inhabited, DecidableEq, Ord + +instance : Repr PId where + reprPrec u := Repr.addAppParen ("PId.mk " ++ repr u.toUInt64) + +/-- +Gets the title of the current process. +-/ +@[inline] +def getProcessTitle : IO String := + UV.System.getProcessTitle + +/-- +Sets the title of the current process. +-/ +@[inline] +def setProcessTitle (title : String) : IO Unit := + UV.System.setProcessTitle title + +/-- +Gets the current process id. +-/ +@[inline] +def getId : IO PId := + PId.mk <$> UV.System.osGetPid + +/-- +Gets the current process parent id. +-/ +@[inline] +def getParentId : IO PId := + PId.mk <$> UV.System.osGetPpid + +/-- +Gets the current working directory. +-/ +@[inline] +def getCwd : IO System.FilePath := + UV.System.cwd + +/-- +Changes the current working directory to a new one. +-/ +@[inline] +def setCwd (path : System.FilePath) : IO Unit := + UV.System.chdir path.toString + +/-- +Gets the scheduling priority of a process. +-/ +@[inline] +def getPriority (pid : PId) : IO Int64 := + UV.System.osGetPriority pid.toUInt64 + +/-- +Sets the scheduling priority of a process. +-/ +@[inline] +def setPriority (pid : PId) (priority : Int64) : IO Unit := + UV.System.osSetPriority pid.toUInt64 priority + +/-- +Retrieves resource usage statistics. +-/ +@[inline] +def getResourceUsage : IO ResourceUsageStats := + UV.System.getrusage <&> fun rusage => + { + cpuUserTime := .ofNat <| UInt64.toNat rusage.userTime + cpuSystemTime := .ofNat <| UInt64.toNat rusage.systemTime + peakResidentSetSizeKb := rusage.maxRSS + sharedMemorySizeKb := rusage.ixRSS + unsharedDataSizeKb := rusage.idRSS + unsharedStackSizeKb := rusage.isRSS + minorPageFaults := rusage.minFlt + majorPageFaults := rusage.majFlt + swapOperations := rusage.nSwap + blockInputOps := rusage.inBlock + blockOutputOps := rusage.outBlock + messagesSent := rusage.msgSent + messagesReceived := rusage.msgRecv + signalsReceived := rusage.signals + voluntaryContextSwitches := rusage.voluntaryCS + involuntaryContextSwitches := rusage.involuntaryCS + } + +/-- +Returns the absolute path of the current executable. +-/ +@[inline] +def getExecutablePath : IO FilePath := + FilePath.mk <$> UV.System.exePath + +/-- +Returns the amount of free system memory in bytes. +-/ +@[inline] +def freeMemory : IO UInt64 := + UV.System.freeMemory + +/-- +Returns the total system memory in bytes. +-/ +@[inline] +def totalMemory : IO UInt64 := + UV.System.totalMemory + +/-- +Returns the constrained memory limit in bytes. +-/ +@[inline] +def constrainedMemory : IO UInt64 := + UV.System.constrainedMemory + +/-- +Returns the available memory for allocation in bytes. +-/ +@[inline] +def availableMemory : IO UInt64 := + UV.System.availableMemory + +end Process +end IO +end Internal +end Std diff --git a/src/Std/Internal/Async/System.lean b/src/Std/Internal/Async/System.lean new file mode 100644 index 0000000000..9fc6a7e343 --- /dev/null +++ b/src/Std/Internal/Async/System.lean @@ -0,0 +1,317 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +prelude +import Std.Time +import Std.Internal.UV.System +import Std.Data.HashMap + +/-! +This module contains all system related functions and environment variables +manipulation. +-/ + +open Std Time +open System + +namespace Std +namespace Internal +namespace IO +namespace Async +namespace System + +/-- +A group identifier, represented by a numeric ID in UNIX systems (e.g. 1000). +-/ +structure GroupId where + /-- + The numeric group ID. + -/ + toNat : Nat +deriving Inhabited, DecidableEq, Ord + +instance : Repr GroupId where + reprPrec g := Repr.addAppParen ("GroupId.mk " ++ repr g.toNat) + +/-- +A user identifier, represented by a numeric ID in UNIX systems (e.g. 1001). +-/ +structure UserId where + /-- + The numeric user ID. + -/ + toNat : Nat +deriving Inhabited, DecidableEq, Ord + +instance : Repr UserId where + reprPrec u := Repr.addAppParen ("UserId.mk " ++ repr u.toNat) + +/-- +Information about the current user. +-/ +structure SystemUser where + /-- + The user's name. + -/ + username : String + + /-- + The user's ID. + -/ + userId : Option UserId + + /-- + The group the user belongs to. + -/ + groupId : Option GroupId + + /-- + The user's login shell. + -/ + shell : Option String + + /-- + The home directory of the user. + -/ + homeDir : Option System.FilePath +deriving Inhabited, DecidableEq, Repr + +/-- +Information about a group. +-/ +structure GroupInfo where + /-- + The name of the group. + -/ + groupName : String + + /-- + The ID of the group. + -/ + groupId : GroupId + + /-- + The list of users in the group. + -/ + members : Array String + deriving Repr, Inhabited + +/-- +Represents the breakdown of CPU time usage in milliseconds. +-/ +structure CPUTimes where + + /-- + Time spent in user mode. + -/ + userTime : Millisecond.Offset + + /-- + Time spent on low-priority user processes. + -/ + niceTime : Millisecond.Offset + + /-- + time spent in kernel mode. + -/ + systemTime : Millisecond.Offset + + /-- + Time the CPU was idle. + -/ + idleTime : Millisecond.Offset + + /-- + Time spent servicing hardware interrupts. + -/ + interruptTime : Millisecond.Offset +deriving Inhabited, DecidableEq, Repr + +/-- +Information about a single CPU core. +-/ +structure CPUInfo where + /-- + CPU model name. + -/ + model : String + + /-- + The approximate clock speed of the CPU core in MHz. + -/ + speed : Nat + + /-- + The time spent on the CPU. + -/ + times : CPUTimes +deriving Inhabited, DecidableEq, Repr + +/-- +Gets information about the operating system. +-/ +structure OSInfo where + /-- + OS name. + -/ + name : String + + /-- + OS version. + -/ + release : String + + /-- + OS build. + -/ + version : String + + /-- + CPU architecture. + -/ + machine : String +deriving Repr, Inhabited + +/-- +All the environment variables. +-/ +structure Environment where + private mk :: + /-- + The list of all environment variables. + -/ + private toHashMap : HashMap String String +deriving Inhabited, Repr + +@[inline] +def Environment.get? (env : Environment) (key : String) : Option String := + env.toHashMap[key]? + +/-- +Gets information about the operating system. +-/ +def getSystemInfo : IO OSInfo := do + let uname ← UV.System.osUname + return { + name := uname.sysname + release := uname.release + version := uname.version + machine := uname.machine + } + +/-- +Gets information about the CPU cores. +-/ +def getCPUInfo : IO (Array CPUInfo) := do + let cpuinfo ← UV.System.cpuInfo + return cpuinfo.map fun coreInfo => + { + model := coreInfo.model + speed := UInt64.toNat <| coreInfo.speed + times := { + userTime := Millisecond.Offset.ofNat <| UInt64.toNat <| coreInfo.times.user + niceTime := Millisecond.Offset.ofNat <| UInt64.toNat <| coreInfo.times.nice + systemTime := Millisecond.Offset.ofNat <| UInt64.toNat <| coreInfo.times.sys + idleTime := Millisecond.Offset.ofNat <| UInt64.toNat <| coreInfo.times.idle + interruptTime := Millisecond.Offset.ofNat <| UInt64.toNat <| coreInfo.times.irq + } + } + +/-- +Gets the system uptime in seconds. +-/ +@[inline] +def getUpTime : IO Second.Offset := do + return .ofNat <| UInt64.toNat (← UV.System.uptime) + +/-- +Ghe current high-resolution timestamp in nanoseconds. It is relative to an arbitrary time in the past. +-/ +@[inline] +def getHighResolutionTime : IO Nanosecond.Offset := do + return .ofNat <| UInt64.toNat <| (← UV.System.hrtime) + +/-- +Gets the hostname of the machine. +-/ +@[inline] +def getHostName : IO String := + UV.System.osGetHostname + +/-- +Sets an environment variable to `value`. +-/ +@[inline] +def setEnvVar (name : String) (value : String) : IO Unit := do + UV.System.osSetenv name value + +/-- +Gets an environment variable. +-/ +@[inline] +def getEnvVar (name : String) : IO (Option String) := + UV.System.osGetenv name + +/-- +Unset an environment variable. +-/ +@[inline] +def unsetEnvVar (name : String) : IO Unit := do + UV.System.osUnsetenv name + +/-- +Gets all environment variables. +-/ +@[inline] +def getEnv : IO Environment := do + let array ← UV.System.osEnviron + return ⟨HashMap.insertMany (.emptyWithCapacity array.size) array⟩ + +/-- +Gets the current user's home directory. +-/ +@[inline] +def getHomeDir : IO FilePath := + FilePath.mk <$> UV.System.osHomedir + +/-- +Gets the temporary directory. +-/ +@[inline] +def getTmpDir : IO FilePath := do + FilePath.mk <$> UV.System.osTmpdir + +/-- +Gets the current user by using `passwd`. + +On Windows systems, `userId`, `groupId` and `shell` are set to none +-/ +def getCurrentUser : IO SystemUser := do + let passwd ← UV.System.osGetPasswd + return { + userId := (UserId.mk ∘ UInt64.toNat) <$> passwd.uid, + groupId := (GroupId.mk ∘ UInt64.toNat) <$> passwd.gid, + username := passwd.username, + homeDir := passwd.homedir, + shell := passwd.shell + } + +/-- +Gets the group by its ID. +-/ +def getGroup (groupId : GroupId) : IO (Option GroupInfo) := do + let groupInfo ← UV.System.osGetGroup groupId.toNat.toUInt64 + + return groupInfo <&> fun group => { + groupName := group.groupname + groupId := GroupId.mk <| UInt64.toNat group.gid + members := group.members + } + +end System +end Async +end IO +end Internal +end Std diff --git a/src/Std/Internal/UV.lean b/src/Std/Internal/UV.lean index 9082965cef..4509846f69 100644 --- a/src/Std/Internal/UV.lean +++ b/src/Std/Internal/UV.lean @@ -11,4 +11,5 @@ import Std.Internal.UV.Loop import Std.Internal.UV.Timer import Std.Internal.UV.TCP import Std.Internal.UV.UDP +import Std.Internal.UV.System import Std.Internal.UV.DNS diff --git a/src/Std/Internal/UV/System.lean b/src/Std/Internal/UV/System.lean new file mode 100644 index 0000000000..4bdec49f46 --- /dev/null +++ b/src/Std/Internal/UV/System.lean @@ -0,0 +1,263 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving, Sofia Rodrigues +-/ +prelude +import Init.System.IO +import Init.System.Promise +import Init.Data.SInt +import Std.Net + +namespace Std +namespace Internal +namespace UV +namespace System + +open Std.Net + +/-- +Represents resource usage statistics for a process or thread. +All time values are in milliseconds. +-/ +structure RUsage where + userTime : UInt64 + systemTime : UInt64 + maxRSS : UInt64 + ixRSS : UInt64 + idRSS : UInt64 + isRSS : UInt64 + minFlt : UInt64 + majFlt : UInt64 + nSwap : UInt64 + inBlock : UInt64 + outBlock : UInt64 + msgSent : UInt64 + msgRecv : UInt64 + signals : UInt64 + voluntaryCS : UInt64 + involuntaryCS : UInt64 +deriving Repr, Inhabited + +/-- +Represents the breaskdown of CPU time usage in milliseconds. +-/ +structure CPUTimes where + user : UInt64 + nice : UInt64 + sys : UInt64 + idle : UInt64 + irq : UInt64 +deriving Repr, Inhabited + +/-- +Information about a single CPU core. +-/ +structure CPUInfo where + model : String + speed : UInt64 + times : CPUTimes +deriving Repr, Inhabited + +/-- +Information about the current user. +-/ +structure PasswdInfo where + username : String + uid : Option UInt64 + gid : Option UInt64 + shell : Option String + homedir : Option String +deriving Repr, Inhabited + +/-- +Information about the current group, +-/ +structure GroupInfo where + groupname : String + gid : UInt64 + members : Array String +deriving Repr, Inhabited + +/-- +Information about the OS. +-/ +structure UnameInfo where + sysname : String + release : String + version : String + machine : String +deriving Repr, Inhabited + +/-- +Gets the title of the current process. +-/ +@[extern "lean_uv_get_process_title"] +opaque getProcessTitle : IO String + +/-- +Sets the title of the current process. +-/ +@[extern "lean_uv_set_process_title"] +opaque setProcessTitle : @& String → IO Unit + +/-- +Gets the system uptime in seconds. +-/ +@[extern "lean_uv_uptime"] +opaque uptime : IO UInt64 + +/-- +Gets the process ID of the current process. +-/ +@[extern "lean_uv_os_getpid"] +opaque osGetPid : IO UInt64 + +/-- +Gets the parent process ID of the current process. +-/ +@[extern "lean_uv_os_getppid"] +opaque osGetPpid : IO UInt64 + +/-- +Gets information about the system's CPUs. +-/ +@[extern "lean_uv_cpu_info"] +opaque cpuInfo : IO (Array CPUInfo) + +/-- +Gets the current working directory. +-/ +@[extern "lean_uv_cwd"] +opaque cwd : IO String + +/-- +Changes the current working directory. +-/ +@[extern "lean_uv_chdir"] +opaque chdir : String → IO Unit + +/-- +Gets the path to the current user's home directory. +-/ +@[extern "lean_uv_os_homedir"] +opaque osHomedir : IO String + +/-- +Gets the path to the temporary directory. +-/ +@[extern "lean_uv_os_tmpdir"] +opaque osTmpdir : IO String + +/-- +Gets a subset of the password file entry for the current user. +-/ +@[extern "lean_uv_os_get_passwd"] +opaque osGetPasswd : IO PasswdInfo + +/-- +Gets information about the current user's group. +-/ +@[extern "lean_uv_os_get_group"] +opaque osGetGroup : UInt64 → IO (Option GroupInfo) + +/-- +Gets all environment variables. +-/ +@[extern "lean_uv_os_environ"] +opaque osEnviron : IO (Array (String × String)) + +/-- +Gets the value of an environment variable. +-/ +@[extern "lean_uv_os_getenv"] +opaque osGetenv : String → IO (Option String) + +/-- +Sets the value of an environment variable. +-/ +@[extern "lean_uv_os_setenv"] +opaque osSetenv : String → String → IO Unit + +/-- +Unsets an environment variable. +-/ +@[extern "lean_uv_os_unsetenv"] +opaque osUnsetenv : String → IO Unit + +/-- +Gets the hostname of the machine. +-/ +@[extern "lean_uv_os_gethostname"] +opaque osGetHostname : IO String + +/-- +Gets the scheduling priority of a process. +-/ +@[extern "lean_uv_os_getpriority"] +opaque osGetPriority : UInt64 → IO Int64 + +/-- +Sets the scheduling priority of a process. +-/ +@[extern "lean_uv_os_setpriority"] +opaque osSetPriority : UInt64 → Int64 → IO Unit + +/-- +Gets information about the operating system. +-/ +@[extern "lean_uv_os_uname"] +opaque osUname : IO UnameInfo + +/-- +Gets the current high-resolution time in nanoseconds. +-/ +@[extern "lean_uv_hrtime"] +opaque hrtime : IO UInt64 + +/-- +Generates cryptographically secure random bytes. +-/ +@[extern "lean_uv_random"] +opaque random : UInt64 → IO (IO.Promise (Except IO.Error ByteArray)) + +/-- +Retrieves resource usage statistics. +-/ +@[extern "lean_uv_getrusage"] +opaque getrusage : IO RUsage + +/-- +Returns the absolute path of the current executable. +-/ +@[extern "lean_uv_exepath"] +opaque exePath : IO String + +/-- +Returns the amount of free system memory in bytes. +-/ +@[extern "lean_uv_get_free_memory"] +opaque freeMemory : IO UInt64 + +/-- +Returns the total system memory in bytes. +-/ +@[extern "lean_uv_get_total_memory"] +opaque totalMemory : IO UInt64 + +/-- +Returns the constrained memory limit in bytes. +-/ +@[extern "lean_uv_get_constrained_memory"] +opaque constrainedMemory : IO UInt64 + +/-- +Returns the available memory for allocation in bytes. +-/ +@[extern "lean_uv_get_available_memory"] +opaque availableMemory : IO UInt64 + +end System +end UV +end Internal +end Std diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 2dda82f5b3..0185369b01 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -3,7 +3,7 @@ object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp -uv/timer.cpp uv/tcp.cpp uv/dns.cpp uv/udp.cpp) +uv/timer.cpp uv/tcp.cpp uv/udp.cpp uv/dns.cpp uv/system.cpp) if (USE_MIMALLOC) list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c) # Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir diff --git a/src/runtime/uv/dns.cpp b/src/runtime/uv/dns.cpp index d848222bb8..4df1c21181 100644 --- a/src/runtime/uv/dns.cpp +++ b/src/runtime/uv/dns.cpp @@ -80,8 +80,8 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_a for (struct addrinfo* ai = res; ai != NULL; ai = ai->ai_next) { const struct sockaddr* sin_addr = (const struct sockaddr*)ai->ai_addr; - in_addr_storage* s_addr = (in_addr_storage*)sin_addr->sa_data; - lean_object* addr = lean_in_addr_storage_to_ip_addr((short)sin_addr->sa_family, s_addr); + in_addr_storage* storage_addr = (in_addr_storage*)sin_addr->sa_data; + lean_object* addr = lean_in_addr_storage_to_ip_addr((short)sin_addr->sa_family, storage_addr); arr = lean_array_push(arr, addr); } diff --git a/src/runtime/uv/system.cpp b/src/runtime/uv/system.cpp new file mode 100644 index 0000000000..9e9f6e158a --- /dev/null +++ b/src/runtime/uv/system.cpp @@ -0,0 +1,714 @@ +/* +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Sofia Rodrigues +*/ +#include "runtime/uv/system.h" + +namespace lean { +#ifndef LEAN_EMSCRIPTEN + +using namespace std; + +// Stores all the things needed to request a random sequence of bytes. +typedef struct { + uv_random_t req; + lean_object* promise; + lean_object* byte_array; +} random_req_t; + +// Std.Internal.UV.System.getProcessTitle : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) { + char title[512]; + int result = uv_get_process_title(title, sizeof(title)); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_title = lean_mk_string(title); + return lean_io_result_mk_ok(lean_title); +} + +// Std.Internal.UV.System.setProcessTitle : String → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */) { + const char* title_str = lean_string_cstr(title); + int result = uv_set_process_title(title_str); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + return lean_io_result_mk_ok(lean_box(0)); +} + +// Std.Internal.UV.System.uptime : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) { + double uptime; + + int result = uv_uptime(&uptime); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_uptime = lean_box_uint64((uint64_t)uptime); + + return lean_io_result_mk_ok(lean_uptime); +} + +// Std.Internal.UV.System.osGetPid : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */) { + uv_pid_t pid = uv_os_getpid(); + return lean_io_result_mk_ok(lean_box_uint64(pid)); +} + +// Std.Internal.UV.System.osGetPpid : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */) { + uv_pid_t ppid = uv_os_getppid(); + return lean_io_result_mk_ok(lean_box_uint64(ppid)); +} + +// Std.Internal.UV.System.cpuInfo : IO (Array CPUInfo) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) { + uv_cpu_info_t* cpu_infos; + int count; + + int result = uv_cpu_info(&cpu_infos, &count); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_cpu_infos = lean_alloc_array(count, count); + + for (int i = 0; i < count; i++) { + lean_object* times = lean_alloc_ctor(0, 0, 40); + lean_ctor_set_uint64(times, 0, cpu_infos[i].cpu_times.user); + lean_ctor_set_uint64(times, 8, cpu_infos[i].cpu_times.nice); + lean_ctor_set_uint64(times, 16, cpu_infos[i].cpu_times.sys); + lean_ctor_set_uint64(times, 24, cpu_infos[i].cpu_times.idle); + lean_ctor_set_uint64(times, 32, cpu_infos[i].cpu_times.irq); + + lean_object* model = lean_mk_string(cpu_infos[i].model); + + lean_object* cpu_info = lean_alloc_ctor(0, 2, 8); + lean_ctor_set(cpu_info, 0, model); + lean_ctor_set(cpu_info, 1, times); + lean_ctor_set_uint64(cpu_info, sizeof(void*)*2, (uint64_t)cpu_infos[i].speed); + + lean_array_set_core(lean_cpu_infos, i, cpu_info); + } + + uv_free_cpu_info(cpu_infos, count); + + return lean_io_result_mk_ok(lean_cpu_infos); +} + +// Std.Internal.UV.System.cwd : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) { + char buffer[PATH_MAX]; + size_t size = sizeof(buffer); + + int result = uv_cwd(buffer, &size); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_cwd = lean_mk_string(buffer); + return lean_io_result_mk_ok(lean_cwd); +} + +// Std.Internal.UV.System.chdir : String → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */) { + const char* path_str = lean_string_cstr(path); + + int result = uv_chdir(path_str); + + if (result < 0) { + lean_inc(path); + return lean_io_result_mk_error(lean_decode_uv_error(result, path)); + } + + return lean_io_result_mk_ok(lean_box(0)); +} + +// Std.Internal.UV.System.osHomedir : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) { + char buffer[PATH_MAX]; + size_t size = sizeof(buffer); + + int result = uv_os_homedir(buffer, &size); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_homedir = lean_mk_string(buffer); + return lean_io_result_mk_ok(lean_homedir); +} + +// Std.Internal.UV.System.osTmpdir : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) { + char buffer[PATH_MAX]; + size_t size = sizeof(buffer); + + int result = uv_os_tmpdir(buffer, &size); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_tmpdir = lean_mk_string(buffer); + return lean_io_result_mk_ok(lean_tmpdir); +} + +// Std.Internal.UV.System.osGetPasswd : IO PasswdInfo +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) { + uv_passwd_t passwd; + + int result = uv_os_get_passwd(&passwd); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* username = lean_mk_string(passwd.username); + lean_object* uid = passwd.uid != (unsigned long)(-1) ? mk_option_some(lean_box_uint64(passwd.uid)) : mk_option_none(); + lean_object* gid = passwd.uid != (unsigned long)(-1) ? mk_option_some(lean_box_uint64(passwd.gid)) : mk_option_none(); + lean_object* shell = passwd.shell ? mk_option_some(lean_mk_string(passwd.shell)) : mk_option_none(); + lean_object* homedir = passwd.homedir ? mk_option_some(lean_mk_string(passwd.homedir)) : mk_option_none(); + + lean_object* passwd_info = lean_alloc_ctor(0, 5, 0); + lean_ctor_set(passwd_info, 0, username); + lean_ctor_set(passwd_info, 1, uid); + lean_ctor_set(passwd_info, 2, gid); + lean_ctor_set(passwd_info, 3, shell); + lean_ctor_set(passwd_info, 4, homedir); + + uv_os_free_passwd(&passwd); + + return lean_io_result_mk_ok(passwd_info); +} + +// Std.Internal.UV.System.osGetGroup : IO (Option GroupInfo) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /* w */) { + uv_group_t group; + int result = uv_os_get_group(&group, gid); + + if (result == UV_ENOENT) { + return lean_io_result_mk_ok(mk_option_none()); + } + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, lean_mk_string("group"))); + } + + lean_object* groupname = lean_mk_string(group.groupname); + + int count = 0; + char** mem_ptr = group.members; + while (mem_ptr && *mem_ptr != nullptr) { + count++; + mem_ptr++; + } + + lean_object* members = lean_mk_empty_array(); + for (int i = 0; i < count; i++) { + lean_object* member_name = lean_mk_string(group.members[i]); + members = lean_array_push(members, member_name); + } + + lean_object* group_info = lean_alloc_ctor(0, 2, 8); + lean_ctor_set(group_info, 0, groupname); + lean_ctor_set(group_info, 1, members); + lean_ctor_set_uint64(group_info, sizeof(void*)*2, group.gid); + + uv_os_free_group(&group); + + return lean_io_result_mk_ok(mk_option_some(group_info)); +} + +// Std.Internal.UV.System.osEnviron : IO (Array (String × String)) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) { + uv_env_item_t* env; + int count; + int result = uv_os_environ(&env, &count); + + if (result < 0) { + return lean_io_result_mk_error(lean_mk_string(uv_strerror(result))); + } + + lean_object* env_array = lean_mk_empty_array(); + + for (int i = 0; i < count; i++) { + lean_object* name = lean_mk_string(env[i].name); + lean_object* value = lean_mk_string(env[i].value); + + lean_object* pair = lean_alloc_ctor(0, 2, 0); + lean_ctor_set(pair, 0, name); + lean_ctor_set(pair, 1, value); + + env_array = lean_array_push(env_array, pair); + } + + uv_os_free_environ(env, count); + + return lean_io_result_mk_ok(env_array); +} + +// Std.Internal.UV.System.osGetenv : String → IO (Option String) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */) { + const char* name_str = lean_string_cstr(name); + char stack_buffer[1024]; + size_t size = sizeof(stack_buffer); + + int result = uv_os_getenv(name_str, stack_buffer, &size); + + if (result == UV_ENOENT) { + return lean_io_result_mk_ok(lean_box(0)); + } else if (result == UV_ENOBUFS) { + char* heap_buffer = static_cast(malloc(size)); + + result = uv_os_getenv(name_str, heap_buffer, &size); + + if (result == UV_ENOENT) { + free(heap_buffer); + return lean_io_result_mk_ok(lean_box(0)); + } else if (result < 0) { + free(heap_buffer); + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* value = lean_mk_string(heap_buffer); + lean_object* some_value = lean_alloc_ctor(1, 1, 0); + lean_ctor_set(some_value, 0, value); + free(heap_buffer); + return lean_io_result_mk_ok(some_value); + } else if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* value = lean_mk_string(stack_buffer); + lean_object* some_value = lean_alloc_ctor(1, 1, 0); + lean_ctor_set(some_value, 0, value); + return lean_io_result_mk_ok(some_value); +} + + +// 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, obj_arg /* w */) { + const char* name_str = lean_string_cstr(name); + const char* value_str = lean_string_cstr(value); + + int result = uv_os_setenv(name_str, value_str); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + return lean_io_result_mk_ok(lean_box(0)); +} + +// Std.Internal.UV.System.osUnsetenv : String → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */) { + const char* name_str = lean_string_cstr(name); + + int result = uv_os_unsetenv(name_str); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + return lean_io_result_mk_ok(lean_box(0)); +} + +// Std.Internal.UV.System.osGetHostname : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) { + char hostname[256]; + size_t size = sizeof(hostname); + + int result = uv_os_gethostname(hostname, &size); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* lean_hostname = lean_mk_string(hostname); + return lean_io_result_mk_ok(lean_hostname); +} + +// Std.Internal.UV.System.osGetPriority : UInt64 → IO Int64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */) { + int priority; + + int result = uv_os_getpriority(pid, &priority); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + return lean_io_result_mk_ok(lean_box_uint64(priority)); +} + +// Std.Internal.UV.System.osSetPriority : UInt64 → Int → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */) { + int result = uv_os_setpriority(pid, priority); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + return lean_io_result_mk_ok(lean_box(0)); +} + +// Std.Internal.UV.System.osUname : IO UnameInfo +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) { + uv_utsname_t uname_info; + + int result = uv_os_uname(&uname_info); + + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* sysname = lean_mk_string(uname_info.sysname); + lean_object* release = lean_mk_string(uname_info.release); + lean_object* version = lean_mk_string(uname_info.version); + lean_object* machine = lean_mk_string(uname_info.machine); + + lean_object* uname = lean_alloc_ctor(0, 4, 0); + lean_ctor_set(uname, 0, sysname); + lean_ctor_set(uname, 1, release); + lean_ctor_set(uname, 2, version); + lean_ctor_set(uname, 3, machine); + + return lean_io_result_mk_ok(uname); +} + +// Std.Internal.UV.System.hrtime : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */) { + uint64_t time = uv_hrtime(); + return lean_io_result_mk_ok(lean_box_uint64(time)); +} + +// Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error (Array UInt8))) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */) { + lean_object* promise = lean_promise_new(); + mark_mt(promise); + + lean_object* byte_array = lean_alloc_sarray(1, 0, size); + + random_req_t* req = (random_req_t*)malloc(sizeof(random_req_t)); + req->promise = promise; + req->byte_array = byte_array; + + req->req.data = req; + + lean_inc(promise); + + event_loop_lock(&global_ev); + + int result = uv_random( + global_ev.loop, + &req->req, + lean_sarray_cptr(byte_array), + size, + 0, + [](uv_random_t* uv_req, int status, void* buf, size_t buflen) { + random_req_t* req = (random_req_t*)uv_req; + + if (status < 0) { + lean_dec(req->byte_array); + lean_promise_resolve(mk_except_err(lean_decode_uv_error(status, nullptr)), req->promise); + } else { + lean_sarray_set_size(req->byte_array, buflen); + lean_promise_resolve(mk_except_ok(req->byte_array), req->promise); + } + + lean_dec(req->promise); + free(req); + } + ); + + event_loop_unlock(&global_ev); + + if (result < 0) { + lean_dec(byte_array); + lean_dec(promise); + lean_dec(promise); + free(req); + + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + return lean_io_result_mk_ok(promise); +} + +static inline uint64_t timeval_to_millis(uv_timeval_t t) { + return (uint64_t)t.tv_sec * 1000 + (uint64_t)t.tv_usec / 1000; +} + +// Std.Internal.UV.System.getrusage : IO RUsage +extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) { + uv_rusage_t usage; + int result = uv_getrusage(&usage); + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* r = lean_alloc_ctor(0, 0, 16 * sizeof(uint64_t)); + lean_ctor_set_uint64(r, 0 * sizeof(uint64_t), timeval_to_millis(usage.ru_utime)); + lean_ctor_set_uint64(r, 1 * sizeof(uint64_t), timeval_to_millis(usage.ru_stime)); + lean_ctor_set_uint64(r, 2 * sizeof(uint64_t), usage.ru_maxrss); + lean_ctor_set_uint64(r, 3 * sizeof(uint64_t), usage.ru_ixrss); + lean_ctor_set_uint64(r, 4 * sizeof(uint64_t), usage.ru_idrss); + lean_ctor_set_uint64(r, 5 * sizeof(uint64_t), usage.ru_isrss); + lean_ctor_set_uint64(r, 6 * sizeof(uint64_t), usage.ru_minflt); + lean_ctor_set_uint64(r, 7 * sizeof(uint64_t), usage.ru_majflt); + lean_ctor_set_uint64(r, 8 * sizeof(uint64_t), usage.ru_nswap); + lean_ctor_set_uint64(r, 9 * sizeof(uint64_t), usage.ru_inblock); + lean_ctor_set_uint64(r, 10 * sizeof(uint64_t), usage.ru_oublock); + lean_ctor_set_uint64(r, 11 * sizeof(uint64_t), usage.ru_msgsnd); + lean_ctor_set_uint64(r, 12 * sizeof(uint64_t), usage.ru_msgrcv); + lean_ctor_set_uint64(r, 13 * sizeof(uint64_t), usage.ru_nsignals); + lean_ctor_set_uint64(r, 14 * sizeof(uint64_t), usage.ru_nvcsw); + lean_ctor_set_uint64(r, 15 * sizeof(uint64_t), usage.ru_nivcsw); + + return lean_io_result_mk_ok(r); +} + +// Std.Internal.UV.System.exePath : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) { + char buffer[PATH_MAX]; + size_t size = sizeof(buffer); + + int result = uv_exepath(buffer, &size); + if (result < 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr)); + } + + lean_object* path = lean_mk_string(buffer); + return lean_io_result_mk_ok(path); +} + +// Std.Internal.UV.System.freeMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */) { + uint64_t mem = uv_get_free_memory(); + return lean_io_result_mk_ok(lean_box_uint64(mem)); +} + +// Std.Internal.UV.System.totalMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */) { + uint64_t mem = uv_get_total_memory(); + return lean_io_result_mk_ok(lean_box_uint64(mem)); +} + +// Std.Internal.UV.System.constrainedMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */) { + uint64_t mem = uv_get_constrained_memory(); + return lean_io_result_mk_ok(lean_box_uint64(mem)); +} + +// Std.Internal.UV.System.availableMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */) { + uint64_t mem = uv_get_available_memory(); + return lean_io_result_mk_ok(lean_box_uint64(mem)); +} + +#else + +// Std.Internal.UV.System.getProcessTitle : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.setProcessTitle : @& String → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.uptime : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetPid : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetPpid : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.cpuInfo : IO (Array CPUInfo) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.cwd : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.chdir : String → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osHomedir : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osTmpdir : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetPasswd : IO PasswdInfo +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetGroup : IO (Option GroupInfo) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osEnviron : IO (Array (String × String)) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetenv : String → IO (Option String) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// 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, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osUnsetenv : String → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetHostname : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osGetPriority : UInt64 → IO Int +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osSetPriority : UInt64 → Int → IO Unit +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.osUname : IO UnameInfo +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.hrtime : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error (Array UInt8))) +extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +// Std.Internal.UV.System.getrusage : IO RUsage +extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} +// Std.Internal.UV.System.exePath : IO String +extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} +// Std.Internal.UV.System.freeMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} +// Std.Internal.UV.System.totalMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} +// Std.Internal.UV.System.constrainedMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} +// Std.Internal.UV.System.availableMemory : IO UInt64 +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +#endif +} diff --git a/src/runtime/uv/system.h b/src/runtime/uv/system.h new file mode 100644 index 0000000000..07899107cd --- /dev/null +++ b/src/runtime/uv/system.h @@ -0,0 +1,44 @@ +#pragma once +#include +#include "runtime/uv/event_loop.h" + +namespace lean { + +#ifndef LEAN_EMSCRIPTEN +using namespace std; +#include +#endif + +// ======================================= +// System information functions + +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */); + +} diff --git a/tests/lean/run/async_systems_info.lean b/tests/lean/run/async_systems_info.lean new file mode 100644 index 0000000000..6ebe4ce189 --- /dev/null +++ b/tests/lean/run/async_systems_info.lean @@ -0,0 +1,107 @@ +import Std.Internal.Async.System +import Std.Internal.Async.Process + +open Std.Internal.IO.Async.System +open Std.Internal.IO.Process + +#eval do + assert! (← getUpTime) > 0 + +#eval do + assert! (← getHighResolutionTime) > 0 + +#eval do + assert! (← getHostName) != "" + +#eval do + setEnvVar "TEST_LEAN_ASYNC" "hello world" + +#eval do + assert! (← getEnvVar "TEST_LEAN_ASYNC") == (some "hello world") + +#eval do + assert! (← getEnv).get? "TEST_LEAN_ASYNC" == (some "hello world") + +#eval + unsetEnvVar "TEST_LEAN_ASYNC" + +#eval do + assert! (← getEnvVar "TEST_LEAN_ASYNC") == none + +#eval do + assert! (← getSystemInfo).machine != "" + +#eval do + assert! (← getCPUInfo).size > 0 + +#eval do + assert! (← getHomeDir) != "" + +#eval do + assert! (← getTmpDir) != "" + +#eval do + assert! (← getId).toUInt64 != 0 + +#eval do + assert! (← getParentId).toUInt64 != 0 + +#eval do + let cwd ← getCwd + assert! cwd.toString != "" + +#eval do + let cwd ← getCwd + setCwd cwd + +#eval do + if System.Platform.isWindows then + return + + let pid ← getId + setPriority pid 3 + assert! (← getPriority pid) == 3 + +#eval do + if System.Platform.isWindows then + return + + let pid ← getParentId + setPriority pid 3 + assert! (← getPriority pid) == 3 + +#eval do + if System.Platform.isWindows then + return + + let user ← getCurrentUser + if System.Platform.isWindows then + assert! user.userId == none + assert! user.groupId == none + else + assert! user.userId != none + assert! user.username != "" + +#eval do + if System.Platform.isWindows then + return + + assert! (← getGroup (GroupId.mk 240000)).isNone + +#eval do + assert! (← getResourceUsage).peakResidentSetSizeKb > 0 + +#eval do + assert! (← getExecutablePath) != "" + +#eval do + assert! (← freeMemory) > 0 + +#eval do + assert! (← totalMemory) > 0 + +#eval + constrainedMemory + +#eval do + assert! (← availableMemory) > 0