Struct ClockReading 

pub struct ClockReading(/* private fields */);

The moment a run’s driver read its clock last, shared with the tool faces that report the time (crates/runtime/spec/Clock.lean §8-53).

The driver’s clock hook is the one sampling point of a run, and a tool face receives readings rather than sampling: the hook keeps each reading before handing it on, and a command’s stamp or status’s now: line reads latest. What they report is therefore always some line’s t. Cloned, it is one cell.

“Not read yet” is a state of its own rather than an integer standing for one. The lock holds one Copy value replaced whole, so a thread that panicked while holding it cannot have left half a value behind, and a poisoned lock is read like any other.

Implementations

impl ClockReading

pub fn keep(&self, at: TimeMs)

Records one reading the driver took.

pub fn latest(&self) -> Option<TimeMs>

The last reading kept; None before the driver has read its clock.

Trait Implementations

impl Clone for ClockReading

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ClockReading

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ClockReading

fn default() -> Self

Returns the “default value” for a type.