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. While it listens, a signal that arrives with no promise from next pending resolves the promise of the following next. A repeating signal handler will only be freed after Signal.stop is called, or once nothing references it after cancel.

@[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 after receiving the signal, return the same IO.Promise that the last call to next returned, or a new one if cancel dropped it. A signal received after cancel resolves that promise.
  • it was stopped with stop before receiving the signal, return a new IO.Promise that is never resolved.
• 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, or that is already resolved if signals arrived while no promise was pending. Those signals are reported once, however many arrived.
    • If it is not, return the last IO.Promise This ensures that the returned IO.Promise resolves for a signal that no earlier promise reported.
  • if it is finished, return a new IO.Promise that is never resolved, as stop dropped the last one.

A promise from next may also be resolved by the code holding it; the handler then treats it as fulfilled when the signal arrives. 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, it is put into the finished state and the last IO.Promise generated by next is released. If that promise is still pending it is never resolved; once nothing else references it, its result? resolves to none.

@[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 last IO.Promise generated by next. The handler keeps listening, so a signal that arrives afterwards is reported by the next call to next. Until that call the event loop does not keep the Signal alive, so dropping it stops listening.