Get system time and other machine data?

Stream: new members

[Ioannis Konstantoulas]

In Core, there is a SystemTime structure. Does Lean have a way to get the current clock time or Unix epoch? I am trying to find a function but cannot see any.

Similarly, is there a way to access other hardware data without reading /proc (which is platform-specific)?

[Alex J. Best]

Are docs#monoMsNow or docs#monoNanosNow useful to you? You can see the implementations here https://github.com/leanprover/lean4/blob/1572e55f06268a87bc82249f7c4c52dec8f5c3cf/stage0/src/runtime/io.cpp#L385

[Ioannis Konstantoulas]

The monotonicity is useful, but I would like the resulting number to be related to the epoch or date. I cannot understand the relation, if any, with the unix epoch (I don't understand all the processing after invoking time_since_epoch()); at least in my system date +%s and #eval IO.monoNanosNow give different results.

[Eric Wieser]

There are a lot of different system times in POSIX most unix systems

[Eric Wieser]

How different are the values you get?

[Ioannis Konstantoulas]

Completely different; for now, I created a project in C with functions like

extern "C" uint64_t system_time_nanoseconds() {
    struct timespec t;
    clock_gettime(CLOCK_REALTIME, &t);
    return (uint64_t)(t.tv_sec) * (uint64_t)1000000000 + (uint64_t)(t.tv_nsec);
}

and bindings like

@[extern "system_time_nanoseconds"]
opaque getSystemTimeNanoseconds : Unit -> UInt64

that did the job (in particular, I can use this value to correctly set IO.FS.SystemTime). It seems I will also need to add date functions from C, since I cannot find such in Lean.

I am sure I am overcomplicating the FFI though, I had to create a different project and require it locally; surely I can incorporate the C code into my existing code with some options in the lakefile, but I have not yet tried.