source
def Std.Internal.UV.Signal :
Type

`Signal`s are used to generate `IO.Promise`s 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 `Signal`s.

Equations

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

Instances For

source
instance Std.Internal.UV.instNonemptySignal :
Nonempty Signal
source
@[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.

source
@[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.

source
@[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.

source
@[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.