Joseph Ferano
2dd13b5ae0
Nothing in it could. A game got a clock from raylib and a program without a window had none at all, so "how long did that take" was unanswerable in the half of daily use that is a tool rather than a game. Two clocks, because the mistake a single one invites is using it for the other job. monotonic-ns measures: it never goes backwards, nothing adjusts it, and its zero is arbitrary, so it is meaningless alone and correct as a difference. unix-ns dates: nanoseconds since 1970, which is what goes in a save file, and which jumps in either direction when somebody sets the system clock. The names are picked so that reaching for the wrong one reads wrong. This is Odin's shape, from core/time/time.odin and core/time/time_linux.odin: Tick against Time, both an i64 of nanoseconds, over MONOTONIC and REALTIME, with the seconds-valued face derived rather than a second syscall. Three C functions here and six Flan names over them, which is the rule flan_rt.c's own header states -- a primitive is the only thing implemented twice. The monotonic origin is the first read of the clock in the process, not boot, and that is the one decision worth arguing. CLOCK_MONOTONIC counts from boot, so on a machine up a hundred days the raw value is past 2^53 nanoseconds and monotonic-seconds would lose sub-microsecond resolution depending on the machine's uptime rather than on anything the program did. Latched to first read it stays integer-exact for a hundred days of process life, and it also matches what a game already has: raylib's GetTime is seconds since InitWindow, so the two numbers now mix without a conversion at every site. sleep-ns loops on EINTR, because otherwise a signal cuts the wait short and a frame loop wobbles for reasons nothing in the program explains. It is documented as at-least and not as a frame limiter; the shape that actually paces a loop is a deadline recomputed from monotonic-ns each turn, and the comment says so where somebody will read it. getenv answers an (Option [u8]) viewing the process environment, which needs no allocator and no free and is safe precisely because nothing in this language can call setenv or spawn a process. The absent case rides in the length rather than in the pointer: there is no null test to write, since a (Ptr T) here always addresses something, so flan_getenv answers -1 and a pointer at a valid empty string and the Flan side tests arithmetic. The runtime additions are a single block at the end of flan_rt.c, with <time.h> inside it for the reason <errno.h> sits beside the file section. programs/time.flan asserts invariants and never a reading -- t2 >= t1, a sleep that did not return early, a date after 2020 and before 2100 -- because the same file is in the corpus @x86 builds twice and diffs, so a timestamp would fail a correct compiler on its second run.
72 lines
3.4 KiB
Plaintext
72 lines
3.4 KiB
Plaintext
;;;; The clock and the environment.
|
|
;;;;
|
|
;;;; Every line of output here is an invariant and not a reading, and that is
|
|
;;;; forced rather than chosen: this file is in the corpus @x86 builds twice
|
|
;;;; and diffs, and the acceptance table matches its stdout exactly, so a
|
|
;;;; timestamp or an elapsed count would fail a correct compiler on the second
|
|
;;;; run. What is left is what a clock actually has to promise — that it does
|
|
;;;; not go backwards, that a sleep does not return early, that the two faces
|
|
;;;; of one clock describe one instant — and those are the properties worth
|
|
;;;; pinning anyway. A test that asserted "this took under 3ms" would be a
|
|
;;;; test of the machine's load.
|
|
|
|
(defn main [] i32
|
|
;; Monotonic, twice. The whole contract in one line: it never goes
|
|
;; backwards. Equal is allowed and is not a bug — two reads inside one tick
|
|
;; of a coarse timer are the same nanosecond.
|
|
(let [t1 (monotonic-ns)
|
|
t2 (monotonic-ns)]
|
|
(println (>= t2 t1)))
|
|
|
|
;; And the origin is the first read rather than boot, so the first readings
|
|
;; a program takes are small. Bounded rather than pinned: the number is
|
|
;; whatever this process spent between the calls above and this one, which
|
|
;; is not a second on any machine that can run the suite at all.
|
|
(println (< (monotonic-ns) ns-per-second))
|
|
|
|
;; The f64 face is the i64 one divided, and what is checked is that the two
|
|
;; describe the same instant: a later reading in seconds is at or past an
|
|
;; earlier reading in nanoseconds converted the same way. A clock whose two
|
|
;; faces came from different sources fails this.
|
|
(let [a (/ (f64 (monotonic-ns)) 1000000000.0)
|
|
b (monotonic-seconds)]
|
|
(println (>= b a)))
|
|
|
|
;; The wall clock is a date, so the invariant is a date one: it is after
|
|
;; 2020 and before 2100. That pins the epoch and the unit at once — a clock
|
|
;; counting microseconds, or counting from boot, fails both halves.
|
|
(let [now (unix-seconds)]
|
|
(println (and (> now 1577836800.0) (< now 4102444800.0))))
|
|
|
|
;; Sleep is specified as *at least*, so at-least is what is asserted; the
|
|
;; upper bound belongs to the scheduler and not to this language. Two
|
|
;; milliseconds because the shortest sleep a default kernel actually
|
|
;; performs is a timer tick, and a shorter request would make this a test of
|
|
;; how that kernel was configured.
|
|
(let [before (monotonic-ns)]
|
|
(sleep-ns (* 2 ns-per-millisecond))
|
|
(println (>= (- (monotonic-ns) before) (* 2 ns-per-millisecond))))
|
|
|
|
;; Zero and negative return at once rather than being refused, which is what
|
|
;; a deadline already passed produces. That they return at all is the
|
|
;; assertion; nothing here is timed.
|
|
(sleep-ns 0)
|
|
(sleep-ns -1)
|
|
(sleep-seconds 0.0)
|
|
(println "slept")
|
|
|
|
;; ── The environment ──────────────────────────────────────────────
|
|
|
|
;; A variable nothing sets. None is the answer, and it is a different answer
|
|
;; from a variable set to nothing.
|
|
(match (getenv "FLAN_NO_SUCH_VARIABLE_AT_ALL")
|
|
(Some v) (println "unexpectedly set")
|
|
None (println "unset"))
|
|
|
|
;; PATH is set for every process that gets as far as running this, and the
|
|
;; only portable thing about its contents is that there are some.
|
|
(match (getenv "PATH")
|
|
(Some v) (println (> (len v) 0))
|
|
None (println "no PATH"))
|
|
0)
|