feat: add date and time functionality

[algebraic-dev]

This PR introduces date and time functionality to the Lean 4 Std. It's not complete yet and I need to implement some these things:

• [x] Implement parsing for various date and time formats (In the Format module so I can easily create a format for all the standard formats like ISO8601).
• [x] Improve support for Timezone handling (add timezone Database by reading the Linux /usr/share/zoneinfo/ or using a hardcoded version).
• [x] Introduce macros for date creation e.g %date 2000-01-01.
• [x] Add some native code to retrieve system date and time information.
• [x] Tests

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a845a007ac07350824c0b7773a03302373d8e8f1 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-05 18:32:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-07 20:58:20)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-09 17:53:25)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto f3e7b455bbd4ea39376e0928d0d6cb8d26bd0ba3. (2024-08-14 21:42:05)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto 8c96d213f3089ac2352ed95e79645f4cdbd70ebf. (2024-08-15 19:34:28)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto 0ecbcfdcc3785c155b8f394c655f48f4f7ed0e65. (2024-08-16 18:00:42)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto b486c6748b153bda628575635baa28aeeb38b8c5. (2024-08-19 12:17:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c4de5fea9e083ba09e4e243e04cdff428b7beb --onto 4aa74d9c0b0e9706b819af655dfe3f4954213102. (2024-08-20 15:33:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c45a6a93f98b004d2e10574d25ee5898bdf0ee34 --onto 9305049f1ef7309842806c2a994a2020bb32a71f. (2024-08-26 22:45:51)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c45a6a93f98b004d2e10574d25ee5898bdf0ee34 --onto 9ce15fb0c61e3a1bee17fd81647ed4d02b4f6c6d. (2024-08-28 12:18:02)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c45a6a93f98b004d2e10574d25ee5898bdf0ee34 --onto d31066646dfa7389d818a2e2e1493be6a941924e. (2024-09-02 15:54:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6830f90ab365e14ccb7ca31201de37f8c1e978c --onto d8e0fa425b3225fc0c35c07247ecb11b49bb00ed. (2024-09-20 18:05:17)
• 💥 Mathlib branch lean-pr-testing-4904 build failed against this PR. (2024-09-26 02:55:14) View Log
• 💥 Mathlib branch lean-pr-testing-4904 build failed against this PR. (2024-10-11 22:38:12) View Log
• 💥 Mathlib branch lean-pr-testing-4904 build failed against this PR. (2024-10-14 13:16:23) View Log

[kim-em]

A very minor suggestion for an in-Lean use case: have the @[deprecated (since := "2024-08-09")] attribute complain if the date is not formatting sensibly.

[algebraic-dev]

Ok I accidentally used push force :S.

[eric-wieser]

Would you mind replying to my comment at https://github.com/leanprover/lean4/pull/4904#discussion_r1724020988, which I think has got lost in the diff?

[algebraic-dev]

I agree that handling UTC timestamps may not be necessary. However, I think that it is important to keep the support for leap seconds just to try keep the support for ISO 8601 compliant dates. In the future, If someone requests (that will not be the case I guess given that a lot of libraries don't implement something like that), I think that we can consider deriving a specialized type from the Timestamp type to address these problems.

[TwoFX]

However, I think that it is important to keep the support for leap seconds just to try keep the support for ISO 8601 compliant dates.

If I'm understanding you correctly, this is compatible with my request above, i.e., not reading the leap second information from the time zone database but keeping leap second representation in PlainTime, right?

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbdd77b85c44728e0a749fd224d3ce31770976 --onto f752ce2db94892fe70686730fb594bc6e7da5159. (2024-10-23 04:23:24)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbdd77b85c44728e0a749fd224d3ce31770976 --onto 66dbad911eaaec4cd512662bd5cc67a2a16d2484. (2024-10-23 17:02:46)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbdd77b85c44728e0a749fd224d3ce31770976 --onto 9847923f9be5de968f10ed7c7493e3ca0072abce. (2024-10-28 13:31:38)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbdd77b85c44728e0a749fd224d3ce31770976 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-31 05:39:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbdd77b85c44728e0a749fd224d3ce31770976 --onto 0973ba3e4260327f69587813d6a67e5fade0c977. (2024-11-01 17:04:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbdd77b85c44728e0a749fd224d3ce31770976 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-04 22:39:18)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7f0fe20315dcfc6125dc4fb7faefe181b4741cb1 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 15:06:31)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 680177049f998f8f80f29c39853bc44a96565875 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-08 04:14:38)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 61f7dcb36b43b05903cf02236f85426db6d59365 --onto 456e6d2b791bbc560b304b28a60f35db7072c306. (2024-11-12 13:53:17)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 61f7dcb36b43b05903cf02236f85426db6d59365 --onto 5e01e628b2ef90d8881a5ba10340032eeeabc5d4. (2024-11-13 00:37:38)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 85f25967ea4e7650e7edf877777dcce3b6571795 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 13:48:48)

[TwoFX]

I think the missing DateTime functions indicated in the Google sheet are still missing.

[TwoFX]

You removed the test that called defaultGetLocalZoneRules, but I think the failing test actually highlighted a real issue that I can reproduce when setting time zone on my computer to Etc/UTC: calling defaultGetLocalZoneRules completely fails, which sounds wrong to me. Instead it should return a ZoneRules where the initialLocalTimeType describes UTC and the transitions array is empty.

[TwoFX]

Hi @eric-wieser, thank you for taking the time to read through the PR. Our current priorities are to get the public API right and to get the PR merged. As far as I understand (please correct me if I'm wrong), your comments about UnitVal and the notation module don't affect prospective users of the date/time API, but concern implementation details. If you have comments about the public API, please leave them here, but I would prefer to handle feedback for implementation details in additional RFCs/PRs after this PR is merged.

[eric-wieser]

your comments about [...] the notation module don't affect prospective users of the date/time API,

Agreed

your comments about UnitVal

I don't agree, the Mul instance for Minutes.Offset is derived later on from the UnitVal one, so this provides users with a footgun that allows them to compute 1 hour * 1 hour = 1 hour but 60 minutes * 60 minutes = 3600 minutes = 60 hours. These expressions should just be type errors, which can be fixed by deleting the instance.

[TwoFX]

I don't agree, the Mul instance for Minutes.Offset is derived later

Thanks, I had missed this. I agree that the Offset types should not derive Mul or Div. We can add correct HMul and HDiv instances in a future PR.