inductive Std.Async.Signal : Type

Unix style signals for Unix and Windows. SIGKILL and SIGSTOP are missing because they cannot be caught. SIGBUS, SIGFPE, SIGILL, and SIGSEGV are missing because they cannot be caught safely. SIGPIPE is not present because the runtime ignores the signal.

• sighup : Signal

  Hangup detected on controlling terminal or death of controlling process.

  On Windows:

  • SIGHUP is generated when the user closes the console window. The program is given ~10 seconds to perform cleanup before Windows unconditionally terminates it.
• sigint : Signal

  Interrupt program.

  Notes:

  • Normally delivered when the user presses CTRL+C. Not generated when terminal raw mode is enabled.
• sigquit : Signal

  Quit program.

• sigtrap : Signal

  Trace/breakpoint trap.

• sigabrt : Signal

  Abort signal.

  Notes:

  • SIGABRT is not catchable if generated by certain runtime functions, such as abort or assertion failure.
  • On Windows, watchers can be created for SIGABRT, but they never receive the signal.
• sigusr1 : Signal

  User-defined signal 1.

• sigusr2 : Signal

  User-defined signal 2.

• sigalrm : Signal

  Real-time timer expired.

• sigterm : Signal

  Termination signal.

  Notes:

  • On Windows, watchers can be created for SIGTERM, but they never receive the signal.
• sigchld : Signal

  Child status has changed.

• sigcont : Signal

  Continue after stop.

• sigtstp : Signal

  Stop typed at terminal.

• sigttin : Signal

  Background read attempted from control terminal.

• sigttou : Signal

  Background write attempted to control terminal.

• sigurg : Signal

  Urgent condition on socket.

• sigxcpu : Signal

  CPU time limit exceeded.

• sigxfsz : Signal

  File size limit exceeded.

• sigvtalrm : Signal

  Virtual alarm clock.

• sigprof : Signal

  Profiling timer expired.

• sigwinch : Signal

  Window size change.

  Notes:

  • SIGWINCH is raised whenever the runtime detects the console has been resized.
  • Under console emulators, or on 32-bit apps on 64-bit systems, SIGWINCH is emulated.
  • In these cases, signals may not be delivered timely.
• sigio : Signal

  I/O now possible.

• sigsys : Signal

  Bad system call.

@[instance_reducible]

instance Std.Async.instReprSignal : Repr Signal

Equations

• Std.Async.instReprSignal = { reprPrec := Std.Async.instReprSignal.repr }

def Std.Async.instReprSignal.repr : Signal → Nat → Format

Equations

• Std.Async.instReprSignal.repr Std.Async.Signal.sighup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sighup")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigint prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigint")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigquit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigquit")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigtrap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigtrap")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigabrt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigabrt")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigusr1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigusr1")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigusr2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigusr2")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigalrm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigalrm")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigterm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigterm")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigchld prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigchld")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigcont prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigcont")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigtstp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigtstp")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigttin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigttin")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigttou prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigttou")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigurg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigurg")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigxcpu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigxcpu")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigxfsz prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigxfsz")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigvtalrm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigvtalrm")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigprof prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigprof")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigwinch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigwinch")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigio prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigio")).group prec✝
• Std.Async.instReprSignal.repr Std.Async.Signal.sigsys prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Async.Signal.sigsys")).group prec✝

@[instance_reducible]

instance Std.Async.instDecidableEqSignal : DecidableEq Signal

Equations

• Std.Async.instDecidableEqSignal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Std.Async.instBEqSignal : BEq Signal

Equations

• Std.Async.instBEqSignal = { beq := Std.Async.instBEqSignal.beq }

def Std.Async.instBEqSignal.beq : Signal → Signal → Bool

Equations

• Std.Async.instBEqSignal.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Std.Async.Signal.Waiter : Type

Signal.Waiter can be used to wait for a specific signal.

• ofNative :: (
• native : Internal.UV.Signal
• )

@[inline]

def Std.Async.Signal.Waiter.mk (signum : Signal) (repeating : Bool) : IO Waiter

Set up a Signal.Waiter that waits for the specified signum. This function only initializes but does not yet start listening for the signal.

While the waiter listens for the signal, the default action of the signal is replaced. A waiter that is no longer referenced can keep listening if the last operation that reached it was wait: a one-shot waiter until the signal arrives, a repeating one for the rest of the process. After a select that checked it, it stops listening once it is dropped. stop stops it in every case.

Equations

• Std.Async.Signal.Waiter.mk signum repeating = do let native ← Std.Internal.UV.Signal.mk (Std.Async.Signal.toInt32✝ signum) repeating pure { native := native }

@[inline]

def Std.Async.Signal.Waiter.wait (s : Waiter) : IO (AsyncTask Int)

If:

• s is not yet running start listening and return an AsyncTask that will resolve once the previously configured signal is received.
• s is running, or is a one-shot s that finished after receiving the signal, return an AsyncTask for the pending signal, which is the one returned by the previous call unless that one resolved (for a repeating s) or a select that did not find the signal already received dropped it. Tasks whose promise was dropped fail.
• s was stopped with stop, and is repeating or had not received the signal, return an AsyncTask that fails.

The resolved AsyncTask contains the number that Signal assigns to the received signal, which is the same on every platform (the x86 Linux numbering).

Equations

• s.wait = do let promise ← s.native.next pure (Std.Async.AsyncTask.ofPurePromise promise)

@[inline]

def Std.Async.Signal.Waiter.stop (s : Waiter) : IO Unit

If:

• s is still running this stops s without resolving any remaining AsyncTasks that were created through wait. Those tasks fail once the last reference to their promise is dropped, rather than producing a value.
• s is not yet or not anymore running this is a no-op.

Equations

• s.stop = s.native.stop

def Std.Async.Signal.Waiter.selector (s : Waiter) : Selector Unit

Create a Selector that resolves once s has received the signal. Calling this function does not start the signal waiter: a select starts it when it checks it, and it may not check it at all if another selector is already ready.

A select that checks s without picking it leaves it listening until stop is called or s is dropped, and a signal that arrives afterwards is kept and reported by the next select that checks s. For a repeating s, a signal that arrives while another selector wins the same select may be lost.

Equations

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