This module contains all system related functions and environment variables manipulation.

structure Std.Async.System.GroupId : Type

A group identifier, represented by a numeric ID in UNIX systems (e.g. 1000).

• toNat : Nat

  The numeric group ID.

@[implicit_reducible]

instance Std.Async.System.instInhabitedGroupId : Inhabited GroupId

Equations

• Std.Async.System.instInhabitedGroupId = { default := Std.Async.System.instInhabitedGroupId.default }

def Std.Async.System.instDecidableEqGroupId.decEq (x✝ x✝¹ : GroupId) : Decidable (x✝ = x✝¹)

Equations

• Std.Async.System.instDecidableEqGroupId.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Std.Async.System.instDecidableEqGroupId : DecidableEq GroupId

Equations

• Std.Async.System.instDecidableEqGroupId = Std.Async.System.instDecidableEqGroupId.decEq

@[implicit_reducible]

instance Std.Async.System.instOrdGroupId : Ord GroupId

Equations

• Std.Async.System.instOrdGroupId = { compare := Std.Async.System.instOrdGroupId.ord }

def Std.Async.System.instOrdGroupId.ord : GroupId → GroupId → Ordering

Equations

• Std.Async.System.instOrdGroupId.ord { toNat := a } { toNat := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Std.Async.System.instReprGroupId : Repr GroupId

Equations

• Std.Async.System.instReprGroupId = { reprPrec := fun (g : Std.Async.System.GroupId) => Repr.addAppParen (Std.Format.text "GroupId.mk " ++ repr g.toNat) }

structure Std.Async.System.UserId : Type

A user identifier, represented by a numeric ID in UNIX systems (e.g. 1001).

• toNat : Nat

  The numeric user ID.

@[implicit_reducible]

instance Std.Async.System.instInhabitedUserId : Inhabited UserId

Equations

• Std.Async.System.instInhabitedUserId = { default := Std.Async.System.instInhabitedUserId.default }

def Std.Async.System.instDecidableEqUserId.decEq (x✝ x✝¹ : UserId) : Decidable (x✝ = x✝¹)

Equations

• Std.Async.System.instDecidableEqUserId.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Std.Async.System.instDecidableEqUserId : DecidableEq UserId

Equations

• Std.Async.System.instDecidableEqUserId = Std.Async.System.instDecidableEqUserId.decEq

@[implicit_reducible]

instance Std.Async.System.instOrdUserId : Ord UserId

Equations

• Std.Async.System.instOrdUserId = { compare := Std.Async.System.instOrdUserId.ord }

def Std.Async.System.instOrdUserId.ord : UserId → UserId → Ordering

Equations

• Std.Async.System.instOrdUserId.ord { toNat := a } { toNat := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Std.Async.System.instReprUserId : Repr UserId

Equations

• Std.Async.System.instReprUserId = { reprPrec := fun (u : Std.Async.System.UserId) => Repr.addAppParen (Std.Format.text "UserId.mk " ++ repr u.toNat) }

structure Std.Async.System.SystemUser : Type

Information about the current user.

• username : String

  The user's name.

• userId : Option UserId

  The user's ID.

• groupId : Option GroupId

  The group the user belongs to.

• shell : Option String

  The user's login shell.

• homeDir : Option System.FilePath

  The home directory of the user.

@[implicit_reducible]

instance Std.Async.System.instInhabitedSystemUser : Inhabited SystemUser

Equations

• Std.Async.System.instInhabitedSystemUser = { default := Std.Async.System.instInhabitedSystemUser.default }

def Std.Async.System.instDecidableEqSystemUser.decEq (x✝ x✝¹ : SystemUser) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instDecidableEqSystemUser : DecidableEq SystemUser

Equations

• Std.Async.System.instDecidableEqSystemUser = Std.Async.System.instDecidableEqSystemUser.decEq

@[implicit_reducible]

instance Std.Async.System.instReprSystemUser : Repr SystemUser

Equations

• Std.Async.System.instReprSystemUser = { reprPrec := Std.Async.System.instReprSystemUser.repr }

def Std.Async.System.instReprSystemUser.repr : SystemUser → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

structure Std.Async.System.GroupInfo : Type

Information about a group.

• groupName : String

  The name of the group.

• groupId : GroupId

  The ID of the group.

• members : Array String

  The list of users in the group.

@[implicit_reducible]

instance Std.Async.System.instReprGroupInfo : Repr GroupInfo

Equations

• Std.Async.System.instReprGroupInfo = { reprPrec := Std.Async.System.instReprGroupInfo.repr }

def Std.Async.System.instReprGroupInfo.repr : GroupInfo → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instInhabitedGroupInfo : Inhabited GroupInfo

Equations

• Std.Async.System.instInhabitedGroupInfo = { default := Std.Async.System.instInhabitedGroupInfo.default }

structure Std.Async.System.CPUTimes : Type

Represents the breakdown of CPU time usage in milliseconds.

• userTime : Time.Millisecond.Offset

  Time spent in user mode.

• niceTime : Time.Millisecond.Offset

  Time spent on low-priority user processes.

• systemTime : Time.Millisecond.Offset

  time spent in kernel mode.

• idleTime : Time.Millisecond.Offset

  Time the CPU was idle.

• interruptTime : Time.Millisecond.Offset

  Time spent servicing hardware interrupts.

@[implicit_reducible]

instance Std.Async.System.instInhabitedCPUTimes : Inhabited CPUTimes

Equations

• Std.Async.System.instInhabitedCPUTimes = { default := Std.Async.System.instInhabitedCPUTimes.default }

def Std.Async.System.instDecidableEqCPUTimes.decEq (x✝ x✝¹ : CPUTimes) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instDecidableEqCPUTimes : DecidableEq CPUTimes

Equations

• Std.Async.System.instDecidableEqCPUTimes = Std.Async.System.instDecidableEqCPUTimes.decEq

def Std.Async.System.instReprCPUTimes.repr : CPUTimes → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instReprCPUTimes : Repr CPUTimes

Equations

• Std.Async.System.instReprCPUTimes = { reprPrec := Std.Async.System.instReprCPUTimes.repr }

structure Std.Async.System.CPUInfo : Type

Information about a single CPU core.

• model : String

  CPU model name.

• speed : Nat

  The approximate clock speed of the CPU core in MHz.

• times : CPUTimes

  The time spent on the CPU.

@[implicit_reducible]

instance Std.Async.System.instInhabitedCPUInfo : Inhabited CPUInfo

Equations

• Std.Async.System.instInhabitedCPUInfo = { default := Std.Async.System.instInhabitedCPUInfo.default }

@[implicit_reducible]

instance Std.Async.System.instDecidableEqCPUInfo : DecidableEq CPUInfo

Equations

• Std.Async.System.instDecidableEqCPUInfo = Std.Async.System.instDecidableEqCPUInfo.decEq

def Std.Async.System.instDecidableEqCPUInfo.decEq (x✝ x✝¹ : CPUInfo) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instReprCPUInfo : Repr CPUInfo

Equations

• Std.Async.System.instReprCPUInfo = { reprPrec := Std.Async.System.instReprCPUInfo.repr }

def Std.Async.System.instReprCPUInfo.repr : CPUInfo → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

structure Std.Async.System.OSInfo : Type

Gets information about the operating system.

• name : String

  OS name.

• release : String

  OS version.

• version : String

  OS build.

• machine : String

  CPU architecture.

@[implicit_reducible]

instance Std.Async.System.instReprOSInfo : Repr OSInfo

Equations

• Std.Async.System.instReprOSInfo = { reprPrec := Std.Async.System.instReprOSInfo.repr }

def Std.Async.System.instReprOSInfo.repr : OSInfo → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instInhabitedOSInfo : Inhabited OSInfo

Equations

• Std.Async.System.instInhabitedOSInfo = { default := Std.Async.System.instInhabitedOSInfo.default }

structure Std.Async.System.Environment : Type

All the environment variables.

• toHashMap : Std.HashMap String String

@[implicit_reducible]

instance Std.Async.System.instInhabitedEnvironment : Inhabited Environment

Equations

• Std.Async.System.instInhabitedEnvironment = { default := Std.Async.System.instInhabitedEnvironment.default }

def Std.Async.System.instReprEnvironment.repr : Environment → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Async.System.instReprEnvironment : Repr Environment

Equations

• Std.Async.System.instReprEnvironment = { reprPrec := Std.Async.System.instReprEnvironment.repr }

@[inline]

def Std.Async.System.Environment.get? (env : Environment) (key : String) : Option String

Equations

• env.get? key = (Std.Async.System.Environment.toHashMap✝ env)[key]?

def Std.Async.System.getSystemInfo : IO OSInfo

Gets information about the operating system.

Equations

• Std.Async.System.getSystemInfo = do let uname ← Std.Internal.UV.System.osUname pure { name := uname.sysname, release := uname.release, version := uname.version, machine := uname.machine }

def Std.Async.System.getCPUInfo : IO (Array CPUInfo)

Gets information about the CPU cores.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Async.System.getUpTime : IO Time.Second.Offset

Gets the system uptime in seconds.

Equations

• Std.Async.System.getUpTime = do let __do_lift ← Std.Internal.UV.System.uptime pure (Std.Time.Second.Offset.ofNat __do_lift.toNat)

@[inline]

def Std.Async.System.getHighResolutionTime : IO Time.Nanosecond.Offset

The current high-resolution timestamp in nanoseconds. It is relative to an arbitrary time in the past.

Equations

• Std.Async.System.getHighResolutionTime = do let __do_lift ← Std.Internal.UV.System.hrtime pure (Std.Time.Nanosecond.Offset.ofNat __do_lift.toNat)

@[inline]

def Std.Async.System.getHostName : IO String

Gets the hostname of the machine.

Equations

• Std.Async.System.getHostName = Std.Internal.UV.System.osGetHostname

@[inline]

def Std.Async.System.setEnvVar (name value : String) : IO Unit

Sets an environment variable to value.

Equations

• Std.Async.System.setEnvVar name value = Std.Internal.UV.System.osSetenv name value

@[inline]

def Std.Async.System.getEnvVar (name : String) : IO (Option String)

Gets an environment variable.

Equations

• Std.Async.System.getEnvVar name = Std.Internal.UV.System.osGetenv name

@[inline]

def Std.Async.System.unsetEnvVar (name : String) : IO Unit

Unset an environment variable.

Equations

• Std.Async.System.unsetEnvVar name = Std.Internal.UV.System.osUnsetenv name

@[inline]

def Std.Async.System.getEnv : IO Environment

Gets all environment variables.

Equations

• Std.Async.System.getEnv = do let array ← Std.Internal.UV.System.osEnviron pure { toHashMap := (Std.HashMap.emptyWithCapacity array.size).insertMany array }

@[inline]

def Std.Async.System.getHomeDir : IO System.FilePath

Gets the current user's home directory.

Equations

• Std.Async.System.getHomeDir = System.FilePath.mk <$> Std.Internal.UV.System.osHomedir

@[inline]

def Std.Async.System.getTmpDir : IO System.FilePath

Gets the temporary directory.

Equations

• Std.Async.System.getTmpDir = System.FilePath.mk <$> Std.Internal.UV.System.osTmpdir

def Std.Async.System.getCurrentUser : IO SystemUser

Gets the current user by using passwd.

On Windows systems, userId, groupId and shell are set to none

Equations

• One or more equations did not get rendered due to their size.

def Std.Async.System.getGroup (groupId : GroupId) : IO (Option GroupInfo)

Gets the group by its ID.

Equations

• One or more equations did not get rendered due to their size.