fix: adjustments to the datetime library

[algebraic-dev]

This PR fixes the Repr instance of the Timestamp type and changes the PlainTime type so that it always represents a clock time that may be a leap second.

• Fix timestamp Repr.
• The PlainTime type now always represents a clock time that may be a leap second.
• Changed readlink -f to IO.FS.realPath

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-12-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-12-20 23:58:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e46b5f39bf77dffed3af8bfe154c73c2b772107f --onto 8d9d81453bd28aa9799e6bf2ad52def1d75549cb. (2025-01-02 21:03:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e46b5f39bf77dffed3af8bfe154c73c2b772107f --onto 00ef231a6e03398c2ad3b577ab036f901ec88543. (2025-01-08 18:08:02)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e46b5f39bf77dffed3af8bfe154c73c2b772107f --onto dd6445515ddc71826c76b8020fe9e030579b432b. (2025-01-09 22:32:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e46b5f39bf77dffed3af8bfe154c73c2b772107f --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-10 23:11:34)

[tydeu]

Thanks for the leap change! Hopefully, I will eventually be able to swap out Lake's TOML implementation of DateTime for the Std one.

[kim-em]

@algebraic-dev, please remember to add changelog-* labels as needed. It's helpful for reviewers if the green CI check mark is present!

[TwoFX]

I do not like that PlainTime is parameterized now. I think that forcing dependent types on users here makes for bad ergonomics and it's very easy to have inconsistent APIs that are annoying to work around:

import Std.Time

open Std.Time

#eval PlainTime.fromLeanTime24Hour "12:00:00" -- Except.ok ⟨true, time("12:00:00.000000000")⟩
#eval PlainTime.now -- ⟨false, time("15:39:04.310660681")⟩

As far as ISO 8601 is concerned, there is only one kind of clock time -- the one you're calling PlainTime true/LeapTime.

I see two ways forward here:

• carefully review the API, change all functions that currently return a Sigma PlainTime to return PlainTime true or PlainTime false and add conversion functions between PlainTime true and PlainTime false
• Redefine PlainTime to what is called PlainTime true today.

I much prefer the second option, but I'm interested in everyone's opinions.

[algebraic-dev]

I preferred the second option and now the PlainTime makes Second.Offset true without a Sigma.