Accessing system date/time

Stream: general

[Jon Eugster]

Is there any way within lean to print the current date/time into a string?

[Henrik Böving]

There does not currently exist a library that does it for you but you should be able to bind the C functions medium easily if you want this to exist.

[Jon Eugster]

Thx! Looks like there is a reasonable example how to bind a C-function at Foreign Function Interface, maybe I give that a try tomorrow.

[Jason Rute]

Also, if you don't need it to be too general, you can have Lean run a command on the command line. Lean 3 for Hackers had an example of calling the command line to generate random numbers. I think the interface is similar in Lean 4.

[Damiano Testa]

Is docs#IO.FS.SystemTime any use? I never tried it myself.

[Eric Rodriguez]

it seems not from a loogle, unless you want to make a new file and then check its created time for the current time, lol

[Damiano Testa]

Oh, is it only used as metadata for a file? :lol:

[Eric Rodriguez]

FS usually stands for file system :b

[Jason Rute]

Similarly, I assume docs#IO.monoMsNow and docs#IO.monoNanosNow are not useful. They are good for timing stuff, but I don't even know if the number itself has an objective interpretation (maybe just the difference between two numbers.)

[Henrik Böving]

You get the result of

    auto now = std::chrono::steady_clock::now();
    auto tm = std::chrono::duration_cast<std::chrono::milliseconds>(now.time_since_epoch());

so whatever C++ stdlib thinks steady_clock semantics is.

[Henrik Böving]

cppreference remarks:

Class std::chrono::steady_clock represents a monotonic clock. The time points of this clock cannot decrease as physical time moves forward and the time between ticks of this clock is constant. This clock is not related to wall clock time (for example, it can be time since last reboot), and is most suitable for measuring intervals.

so you cannot rely on any semantics from the standard's POV

[Jon Eugster]

Thanks for the tips! Actually, FFI wasn't that tricky to use at all, the C++ code looks something like this:

#include <stdio.h>
#include <time.h>
#include <string>

#include <lean/lean.h>

extern "C" lean_obj_res formatLocalTime() {
    time_t rawtime;
    struct tm *timeinfo;
    char buffer[80];
    time(&rawtime);
    timeinfo = localtime(&rawtime);
    strftime(buffer, sizeof(buffer), "%c", timeinfo);
    return lean_io_result_mk_ok(lean_mk_string(buffer));
}

and the Lean code is

/-- Returns the local date/time as a string. -/
@[extern "formatLocalTime"]
opaque Time.getLocalTime : IO String

[Jon Eugster]

(I don't know if it needs to be in IO, but that's the only way I managed to create a function with no arguments without searching too long)

[Patrick Massot]

Getting the local time is certainly interacting with real world so IO is definitely required.

[Thea Brick]

I've been working on a library: https://github.com/T-Brick/DateTime

[Thea Brick]

still a work in progress but it current does some of the stuff described here

[Jürgen Bergmann]

Maybe my port of the haskell time library to lean could help https://github.com/bergmannjg/time