feat: add date and time functionality #4904

algebraic-dev · 2024-08-02T21:42:32Z

This PR introduces date and time functionality to the Lean 4 Std.

Breaking Changes:

Lean.Data.Rat is now Std.Internal.Rat because it's used by the DateTime library.

leanprover-community-mathlib4-bot · 2024-08-05T18:32:45Z

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

TwoFX

Please add tests for the various conversion routines that catch all of the interesting cases.

It would be very nice to have a few examples of the library being used in practice to achieve some common things.

src/Std/Time.lean

src/Std/Time/Bounded.lean

src/Std/Time/Date/Unit/Day.lean

src/Std/Time/DateTime/NaiveDateTime.lean

src/Std/Time/Date/Unit/Month.lean

src/Std/Time/Time/HourMarker.lean

src/Std/Time/Date/Unit/Month.lean

src/Std/Time/Time/Unit/Nanosecond.lean

…tation

src/Std/Time.lean

src/Std/Time/Duration.lean

src/Std/Time.lean

kim-em · 2024-08-10T07:14:08Z

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.

src/Std/Time/Date/Unit/Day.lean

TwoFX

Gentle reminder that we will not be able to merge this until there are decent tests for much of the functionality.

src/Std/Time/Zoned/Database/Basic.lean

src/Std/Time/Zoned/ZoneRules.lean

src/Std/Time/Zoned/ZonedDateTime.lean

src/Std/Time/Duration.lean

src/runtime/io.cpp

src/Std/Time/Zoned/ZonedDateTime.lean

src/Std/Time/Time/Unit/Second.lean

src/Std/Time/Format.lean

TwoFX

LGTM!

eric-wieser · 2024-11-12T18:29:46Z

src/Std/Time/Notation/Spec.lean

+private def convertText : Text → MacroM (TSyntax `term)
+  | .short => `(Std.Time.Text.short)
+  | .full => `(Std.Time.Text.full)
+  | .narrow => `(Std.Time.Text.narrow)


Should these be Lean.Quote instances?

I tried once but I saw that I would need a function called Unhygienic.run that I think that is inside Lean.Hygienic. AFAIK I cannot import lean things on std because it would lead to some dependency order problems.

src/Std/Time/Zoned/Offset.lean

src/Std/Time/Internal/UnitVal.lean

eric-wieser · 2024-11-13T09:10:13Z

src/Std/Time/Notation.lean

+private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do
+ `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) $(← convertPlainTime d.time))
+
+private def convertZonedDateTime (d : Std.Time.ZonedDateTime) (identifier := false) : MacroM (TSyntax `term) := do


Thinking one more time about this, I think all this is maybe really Lean.ToExpr instead? Maybe @kmill has some thoughts here.

TwoFX · 2024-11-13T09:26:09Z

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 · 2024-11-13T10:43:48Z

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.

src/runtime/io.cpp

TwoFX · 2024-11-13T11:14:46Z

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.

src/runtime/io.cpp

eric-wieser · 2024-11-13T12:15:15Z

src/Std/Time/DateTime/PlainDateTime.lean

-  let mut quadracentennialCycles := days / daysPer400Y;
-  let mut remDays := days.val % daysPer400Y.val;
+  let mut quadracentennialCycles := days.val / daysPer400Y;
+  let mut remDays := days.val % daysPer400Y;


nit: Adding a Mod operation for UnitVal would be well-typed, and would clean this up a little.

…rs needed with padding

feat: add datetime library

9c1be6c

algebraic-dev added awaiting-review Waiting for someone to review the PR P-low We are not planning to work on this issue labels Aug 2, 2024

algebraic-dev requested a review from TwoFX August 2, 2024 21:42

chore: remove useless piece of code

856f569

TwoFX removed the P-low We are not planning to work on this issue label Aug 5, 2024

feat: format and moved the folder to the right place

a9bf653

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 5, 2024

TwoFX reviewed Aug 6, 2024

View reviewed changes

TwoFX added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Aug 7, 2024

algebraic-dev and others added 3 commits August 7, 2024 14:32

Merge branch 'leanprover:master' into master

36108dd

feat: api docs, parser changes, notation, renames and improve documen…

a2e3a4e

…tation

refactor: rename some functions

21563e8

TwoFX reviewed Aug 8, 2024

View reviewed changes

algebraic-dev added 2 commits August 9, 2024 02:46

feat: zone rules

e0da8a6

fix: wrong import

5e269e2

algebraic-dev added awaiting-review Waiting for someone to review the PR awaiting-author Waiting for PR author to address issues and removed awaiting-author Waiting for PR author to address issues awaiting-review Waiting for someone to review the PR labels Aug 9, 2024

feat: add io functions for timestamp and instant

8d0f196

algebraic-dev marked this pull request as ready for review August 9, 2024 17:54

hargoniX reviewed Aug 10, 2024

View reviewed changes

src/Std/Time/Date/Unit/Day.lean Outdated Show resolved Hide resolved

algebraic-dev requested a review from TwoFX August 10, 2024 13:43

TwoFX reviewed Aug 12, 2024

View reviewed changes

algebraic-dev added 5 commits November 11, 2024 09:58

Merge branch 'master' of github.com:algebraic-dev/lean4

2ca4e23

fix: timezone on windows

4f6b2cd

test: add test

0f6a930

Merge branch 'master' of github.com:leanprover/lean4

89c672c

fix: test for tzif

08310f0

TwoFX approved these changes Nov 12, 2024

View reviewed changes

eric-wieser reviewed Nov 12, 2024

View reviewed changes

src/Std/Time/Zoned/Offset.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 12, 2024

View reviewed changes

src/Std/Time/Internal/UnitVal.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 12, 2024

View reviewed changes

src/Std/Time/Internal/UnitVal.lean Show resolved Hide resolved

algebraic-dev added 3 commits November 12, 2024 19:45

fix: a bunch of small fixes and a huge test

7c60f50

feat: more tests

50a1756

fix: nix ci

97e312d