src/ez/timer.bend relies on unsafe/foreign

raw source on the hub · import 0x886223f5c47e4983fe57d887c034bc7f/src/ez/timer.bend as Timer

ez/timer: the clock ez/clock's budget is kept by. date -d works out the deadline at the start and test -gt does the one comparison at the end, both run through snap's foreign effect. This half lives apart from ez/clock because bend 2.0.32 fails a proof whose imports reach foreign code, so a law may import ez/clock but never this.

4 imports

import Base
import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
import ../share/env.bend as Env
import ./clock.bend as Clock

Definitions

def seconds source · line 14 · raw

IO(String)

how many seconds a whole run may take. Five minutes is what the gate is held to; a tree that honestly needs longer says so in EZ_DEADLINE, and "0" turns the budget off for someone bisecting with the cache cold.

def by source · line 19 · raw

@+secs:String -> IO(String)

the second the run must be finished by, worked out once at the start so that nothing later has to add anything up

def start.go source · line 25 · raw

@keep:Bool -> @+secs:String -> IO(String)

the deadline, or "" when there is none

def start source · line 33 · raw

@+secs:String -> IO(String)

the deadline, or "" when there is none

def over.now source · line 37 · raw

@+deadline:String -> IO(Bool)

whether the deadline has gone by

def over.go source · line 45 · raw

@none:Bool -> @+deadline:String -> IO(Bool)

whether the run has outstayed its budget, which a run with no budget never has

def over source · line 54 · raw

@+deadline:String -> IO(Bool)

whether the run has outstayed its budget, which a run with no budget never has