Current date in UTC

Stream: lean4

[Michael Rothgang]

I'd like to get the current date for a script running in CI. (Full context: mathlib is writing new tooling in Lean #24861 and it's generally a breeze :tada:) Because CI runners can live in different timezones, using Std.Time.PlainDate.now seems wrong --- if I read the source right, it uses the current timezone. (That would be too brittle for my use case, I don't want to make assumptions about the physical machines used in some github actions runners.)

What's the best way to get the current date, but using UTC? Could there be a function for "now, in a given timezone"? CC @Sofia Rodrigues since I gather you are the code author.

[Michael Rothgang]

(And secondly: would you accept a PR clarifying the docstring of PlainDate.now?)

[Daniel Weber]

docs#Std.Time.PlainDate.now

[Daniel Weber]

You can use (← Timestamp.now).toPlainDateAssumingUTC (docs#Std.Time.Timestamp.toPlainDateAssumingUTC, docs#Std.Time.Timestamp.now)

[Markus Himmel]

I think I would do (← DateTime.now (tz := .UTC)).toPlainDate.

[Markus Himmel]

And yes, we will consider suggestions to improve the docstring. The idea of PlainDate.now is that it is equivalent to looking at your wristwatch.

[Michael Rothgang]

Thanks! I created lean4#8331 with the minimal changes. Perhaps giving advice for "here's how to use UTC instead" would also be useful; I'm happy to include that as well if you deem it useful!