src/ez/timer.bend

ezx@1.4.0.0 · 55 lines · 0 definitions

1# ez/timer: the clock ez/clock's budget is kept by. `date -d` works out the
2# deadline at the start and `test -gt` does the one comparison at the end,
3# both run through snap's foreign effect. This half lives apart from ez/clock
4# because bend 2.0.32 fails a proof whose imports reach foreign code, so a law
5# may import ez/clock but never this.
6import Base
7import snap@1.1.0.0/main.bend as R
8import ezx@1.4.0.0/src/share/env.bend as Env
9import ezx@1.4.0.0/src/ez/clock.bend as Clock
10
11# how many seconds a whole run may take. Five minutes is what the gate is held
12# to; a tree that honestly needs longer says so in EZ_DEADLINE, and "0" turns
13# the budget off for someone bisecting with the cache cold.
14def seconds() -> IO(String):
15  Env.var("EZ_DEADLINE", "300")
16
17# the second the run must be finished by, worked out once at the start so that
18# nothing later has to add anything up
19def by(+secs: String) -> IO(String):
20  do IO<String>:
21    +out : String <- R.exec(["date", "-d", "+" ++ secs ++ " seconds", "+%s"])
22    return String.trim(R.text(out))
23
24# the deadline, or "" when there is none
25def start.go(keep: Bool, +secs: String) -> IO(String):
26  match keep:
27    case False{}:
28      IO.pure(String, "")
29    case True{}:
30      by(secs)
31
32# the deadline, or "" when there is none
33def start(+secs: String) -> IO(String):
34  start.go(Clock.on(secs), secs)
35
36# whether the deadline has gone by
37def over.now(+deadline: String) -> IO(Bool):
38  do IO<Bool>:
39    +now : String <- R.exec(["date", "+%s"])
40    +cmp : String <- R.exec(["test", String.trim(R.text(now)), "-gt", deadline])
41    return R.ok(cmp)
42
43# whether the run has outstayed its budget, which a run with no budget never
44# has
45def over.go(none: Bool, +deadline: String) -> IO(Bool):
46  match none:
47    case True{}:
48      IO.pure(Bool, False{})
49    case False{}:
50      over.now(deadline)
51
52# whether the run has outstayed its budget, which a run with no budget never
53# has
54def over(+deadline: String) -> IO(Bool):
55  over.go(String.is_empty(deadline), deadline)