Skip to main content

Module retries

Module retries 

Source
Expand description

How many times a failed call is made again. The part crates/kernel/spec/Retries.lean specifies this module.

One value, one absence. The figure is a value here and its absence is Retries::UntilHalted by construction, so a dispatch, a model-list probe and the form cannot each read a missing figure their own way, and no reader can spell a fourth answer.

It lives in the kernel because two layers read it and neither depends on the other: the gateway, deciding whether to send the request again, and the runtime’s watchdog, deciding whether to freeze the run. One home, or the two drift.

Enums§

Retries
The ceiling a person set on retrying one endpoint.