Make time.time() return float

[tekktrik]

First real contribution! Still pretty new to C/C++ as opposed to Python, but looking around, I think this is the fix for #3125, by casting it as a float. If I understand correctly, this will default to using float or double depending on the board's implementation.

[tekktrik]

But do let me know if that's not correct, honestly just trying to learn, so the recitation is mostly for me :D

[dhalbert]

The reason not to do this is that single precision floats are only about 5-1/2 digits of accuracy, so we lose resolution if the values are cast to float. Try calling time.time() multiple times from the REPL with this change: I think you will see the value not change very often.

[tekktrik]

You're right, and it's probably better to keep the type consistent between ports. Happy to close since I don't have any obvious solution that. Was fun to try anyway!

[dhalbert]

No problem, and it's great you are seeing how to make changes like this.