Generic external C function import

Stream: lean4

[Number Eighteen]

Hello all;

due to the lack of many native IO functions in Lean(e.g. to get current time), for each project I have to write extern declarations, create a C subfolder to get the functions I want from the standard library and write the FFI and compilation instructions (which I am not good at).

Is there a way to import a function from the C standard library without having to go through all this hassle each time? By "way" I mean for example a keyword like extern stdlib to tell the compiler/linker that this is the function from the C standard library? Or at least something that sidesteps the need to create an entire subproject folder just for a function?

[Henrik Böving]

You can use https://github.com/tydeu/lean4-alloy