def Std.Internal.UV.Timer : Type

Timers are used to generate IO.Promises that resolve after some time.

A Timer can be in one of 3 states:

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

This together with whether it was set up as repeating with Timer.new determines the behavior of all functions on Timers.

Equations

• Std.Internal.UV.Timer = Std.Internal.UV.TimerImpl✝.type

instance Std.Internal.UV.instNonemptyTimer : Nonempty Timer

@[extern lean_uv_timer_mk]

opaque Std.Internal.UV.Timer.mk (timeout : UInt64) (repeating : Bool) : IO Timer

This creates a Timer in the initial state and doesn't run it yet.

• If repeating is false this constructs a timer that resolves once after timeout milliseconds, counting from when it's run.
• If repeating is true this constructs a timer that resolves after multiples of timeout milliseconds, counting from when it's run. Note that this includes the 0th multiple right after starting the timer. Furthermore a repeating timer will only be freed after Timer.stop is called.

@[extern lean_uv_timer_next]

opaque Std.Internal.UV.Timer.next (timer : Timer) : IO (IO.Promise Unit)

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

• if repeating is false and:
  • it is initial, run it and return a new IO.Promise that is set to resolve once timeout milliseconds have elapsed. After this IO.Promise is resolved the Timer 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, run it and return a new IO.Promise that resolves right away (as it is the 0th multiple of timeout).
  • it is running, check whether the last returned IO.Promise is already resolved:
    • If it is, return a new IO.Promise that resolves upon finishing the next cycle
    • If it is not, return the last IO.Promise This ensures that the returned IO.Promise resolves at the next repetition of the timer.
  • if it is finished, return the last IO.Promise created by next. Notably this could be one that never resolves if the timer was stopped before fulfilling the last one.

@[extern lean_uv_timer_reset]

opaque Std.Internal.UV.Timer.reset (timer : Timer) : IO Unit

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

• If it is initial or finished this is a no-op.
• If it is running and repeating is false this will delay the resolution of the timer until timeout milliseconds after the call of this function.
• Delay the resolution of the next tick of the timer until timeout milliseconds after the call of this function, then continue normal ticking behavior from there.

@[extern lean_uv_timer_stop]

opaque Std.Internal.UV.Timer.stop (timer : Timer) : IO Unit

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

• If it is initial or finished this is a no-op.
• If it is running the execution of the timer 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.