def Std.Internal.UV.Signal : Type

Signals are used to generate IO.Promises that resolve when a specific signal is received.

A Signal can be in one of 3 states:

• Right after construction it's initial.
• While it is listening for signals it's running.
• If it has stopped for some reason it's finished.

This together with whether it was set up as repeating with Signal.mk determines the behavior of all functions on Signals.

Equations

• Std.Internal.UV.Signal = Std.Internal.UV.SignalImpl✝.type

instance Std.Internal.UV.instNonemptySignal : Nonempty Signal

@[extern lean_uv_signal_mk]

opaque Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal

This creates a Signal in the initial state and doesn't start listening yet.

• If repeating is false this constructs a signal handler that resolves once when the specified signal signum is received, then automatically stops listening.
• If repeating is true this constructs a signal handler that resolves each time the specified signal signum is received and continues listening. A repeating signal handler will only be freed after Signal.stop is called.

@[extern lean_uv_signal_next]

opaque Std.Internal.UV.Signal.next (signal : Signal) : IO (IO.Promise Int)

This function has different behavior depending on the state and configuration of the Signal:

• if repeating is false and:
  • it is initial, start listening and return a new IO.Promise that is set to resolve once the signal signum is received. After this IO.Promise is resolved the Signal is finished.
  • it is running or finished, return the same IO.Promise that the first call to next returned.
• if repeating is true and:
  • it is initial, start listening and return a new IO.Promise that resolves when the next signal signum is received.
  • it is running, check whether the last returned IO.Promise is already resolved:
    • If it is, return a new IO.Promise that resolves upon receiving the next signal
    • If it is not, return the last IO.Promise This ensures that the returned IO.Promise resolves at the next occurrence of the signal.
  • if it is finished, return the last IO.Promise created by next. Notably this could be one that never resolves if the signal handler was stopped before fulfilling the last one.

The resolved IO.Promise contains the signal number that was received.

@[extern lean_uv_signal_stop]

opaque Std.Internal.UV.Signal.stop (signal : Signal) : IO Unit

This function has different behavior depending on the state of the Signal:

• If it is initial or finished this is a no-op.
• If it is running the signal handler is stopped and it is put into the finished state. Note that if the last IO.Promise generated by next is unresolved and being waited on this creates a memory leak and the waiting task is not going to be awoken anymore.

@[extern lean_uv_signal_cancel]

opaque Std.Internal.UV.Signal.cancel (signal : Signal) : IO Unit

This function has different behavior depending on the state of the Signal:

• If it is initial or finished this is a no-op.
• If it's running then it drops the accept promise and if it's not repeatable it sets the signal handler to the initial state.