timezone example

Stream: lean4

[Patrick Massot]

@Sofia Rodrigues the example from https://github.com/leanprover/lean4/blob/master/src/Std/Time/Notation.lean#L198-L204 doesn’t seem to work:

import Std.Time

open Std.Time

#check timezone("America/Sao_Paulo")

Is there any documentation including working examples for this time library? I couldn’t find it in the reference manual.

[Patrick Massot]

The error message is also not super illuminating, it says error: offset 17: expected:

[Sofia Rodrigues]

That’s weird. I’m going to take a look at what’s wrong :/ it was supposed to be working.

[Patrick Massot]

Do I understand correctly that Lean does not ship with a timezone database and we need to work in IO if we want to get access to the system database?

[Patrick Massot]

About the broken macro, the tests in https://github.com/leanprover/lean4/blob/master/tests/lean/run/timeSet.lean#L19-L20 use a more complicated format including the offset.

[Sofia Rodrigues]

Yes, I took a look, and the example is wrong. This timezone macro isn’t very good for working with timezones because it’s pure :S and you have to combine it with an offset. People will probably get confused when trying to work with it and ZoneRules.

[Sofia Rodrigues]

timezone("America/Sao_Paulo -03:00")

is the correct way to use this macro.

[Sofia Rodrigues]

I recommend using this function instead:

 Std.Time.Database.defaultGetZoneRules "America/Sao_Paulo"

[Patrick Massot]

Is there a strong reason to not include a time zone database? It looks a bit strange to use IO for such a task.

[Patrick Massot]

And I’m a bit confused by the difference between TimeZone and ZoneRules.

[Patrick Massot]

Is this explained somewhere?

[Sofia Rodrigues]

Patrick Massot said:

Is there a strong reason to not include a time zone database? It looks a bit strange to use IO for such a task.

We don’t want to maintain databases or other data that change over time, as that would introduce more things to maintain.

[Sofia Rodrigues]

Patrick Massot said:

And I’m a bit confused by the difference between TimeZone and ZoneRules.

The TimeZone is a fixed offset with an identifier. ZoneRules contains all the offset transitions, such as daylight saving time.

[Sofia Rodrigues]

I’ll probably open a PR to rename these types, they’re not very clear

[Patrick Massot]

Is there any situation where I would want TimeZone and not the full thing?

[Patrick Massot]

And before I forget: thanks a lot for your answers!

[Sofia Rodrigues]

Patrick Massot said:

Is there any situation where I would want TimeZone and not the full thing?

I think that in most cases people actually need ZoneRules, but TimeZone is easier to create and easier to reason about when working with the DateTime type.