fix: adjustments to the datetime library (leanprover#6431)

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`

---------

Co-authored-by: Mac Malone <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>

src/Std/Time/DateTime/PlainDateTime.lean

@@ -29,7 +29,6 @@ structure PlainDateTime where
   The `Time` component of a `PlainTime`
   -/
   time : PlainTime
-
   deriving Inhabited, BEq, Repr
 
 namespace PlainDateTime
@@ -123,7 +122,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
 
   return {
     date := PlainDate.ofYearMonthDayClip year hmon (Day.Ordinal.ofFin (Fin.succ mday))
-    time := PlainTime.ofHourMinuteSecondsNano (leap := false) (hour.expandTop (by decide)) minute second nano
+    time := PlainTime.ofHourMinuteSecondsNano (hour.expandTop (by decide)) minute (second.expandTop (by decide)) nano
   }
 
 /--
@@ -199,7 +198,7 @@ Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to
 -/
 @[inline]
 def withHours (dt : PlainDateTime) (hour : Hour.Ordinal) : PlainDateTime :=
-  { dt with time := { dt.time with hour := hour } }
+  { dt with time := { dt.time with hour } }
 
 /--
 Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value.
@@ -212,7 +211,7 @@ def withMinutes (dt : PlainDateTime) (minute : Minute.Ordinal) : PlainDateTime :
 Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value.
 -/
 @[inline]
-def withSeconds (dt : PlainDateTime) (second : Sigma Second.Ordinal) : PlainDateTime :=
+def withSeconds (dt : PlainDateTime) (second : Second.Ordinal true) : PlainDateTime :=
   { dt with time := { dt.time with second := second } }
 
 /--
@@ -457,8 +456,8 @@ def millisecond (dt : PlainDateTime) : Millisecond.Ordinal :=
 Getter for the `Second` inside of a `PlainDateTime`.
 -/
 @[inline]
-def second (dt : PlainDateTime) : Second.Ordinal dt.time.second.fst :=
-  dt.time.second.snd
+def second (dt : PlainDateTime) : Second.Ordinal true :=
+  dt.time.second
 
 /--
 Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`.

src/Std/Time/DateTime/Timestamp.lean

@@ -37,10 +37,10 @@ instance : OfNat Timestamp n where
   ofNat := ⟨OfNat.ofNat n⟩
 
 instance : ToString Timestamp where
-  toString s := toString s.val.toMilliseconds
+  toString s := toString s.val.toSeconds
 
 instance : Repr Timestamp where
-  reprPrec s := reprPrec (toString s)
+  reprPrec s := Repr.addAppParen ("Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds)
 
 namespace Timestamp
 

src/Std/Time/Format.lean

@@ -280,7 +280,7 @@ def format (time : PlainTime) (format : String) : String :=
 Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`.
 -/
 def fromTime24Hour (input : String) : Except String PlainTime :=
-  Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s.snd)) input
+  Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
 
 /--
 Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
@@ -292,8 +292,8 @@ def toTime24Hour (input : PlainTime) : String :=
 Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`.
 -/
 def fromLeanTime24Hour (input : String) : Except String PlainTime :=
-  Formats.leanTime24Hour.parseBuilder (fun h m s n => some (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input
-  <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input
+  Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
+  <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| PlainTime.ofHourMinuteSecondsNano h m s 0) input
 
 /--
 Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`).
@@ -307,7 +307,7 @@ Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainT
 def fromTime12Hour (input : String) : Except String PlainTime := do
   let builder h m s a : Option PlainTime := do
     let value ← Internal.Bounded.ofInt? h.val
-    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd
+    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s
 
   Formats.time12Hour.parseBuilder builder input
 

src/Std/Time/Format/Basic.lean

@@ -741,7 +741,7 @@ private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bo
 
   let data := s!"{sign}{pad time.hour.val}"
   let data := if withMinutes then s!"{data}{if colon then ":" else ""}{pad time.minute.val}" else data
-  let data := if withSeconds ∧ time.second.snd.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.snd.val}" else data
+  let data := if withSeconds ∧ time.second.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.val}" else data
 
   data
 
@@ -764,7 +764,7 @@ private def TypeFormat : Modifier → Type
   | .k _ => Bounded.LE 1 24
   | .H _ => Hour.Ordinal
   | .m _ => Minute.Ordinal
-  | .s _ => Sigma Second.Ordinal
+  | .s _ => Second.Ordinal true
   | .S _ => Nanosecond.Ordinal
   | .A _ => Millisecond.Offset
   | .n _ => Nanosecond.Ordinal
@@ -835,10 +835,10 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .narrow => formatMarkerNarrow data
   | .h format => pad format.padding (data.val % 12)
   | .K format => pad format.padding (data.val % 12)
-  | .k format => pad format.padding (data.val)
-  | .H format => pad format.padding (data.val)
-  | .m format => pad format.padding (data.val)
-  | .s format => pad format.padding (data.snd.val)
+  | .k format => pad format.padding data.val
+  | .H format => pad format.padding data.val
+  | .m format => pad format.padding data.val
+  | .s format => pad format.padding data.val
   | .S format =>
     match format with
     | .nano => pad 9 data.val
@@ -1167,7 +1167,7 @@ private def parseWith : (mod : Modifier) → Parser (TypeFormat mod)
   | .k format => parseNatToBounded (parseAtLeastNum format.padding)
   | .H format => parseNatToBounded (parseAtLeastNum format.padding)
   | .m format => parseNatToBounded (parseAtLeastNum format.padding)
-  | .s format => Sigma.mk true <$> (parseNatToBounded (parseAtLeastNum format.padding))
+  | .s format => parseNatToBounded (parseAtLeastNum format.padding)
   | .S format =>
     match format with
     | .nano => parseNatToBounded (parseAtLeastNum 9)
@@ -1249,7 +1249,7 @@ private structure DateBuilder where
   k : Option (Bounded.LE 1 24) := none
   H : Option Hour.Ordinal := none
   m : Option Minute.Ordinal := none
-  s : Option (Sigma Second.Ordinal) := none
+  s : Option (Second.Ordinal true) := none
   S : Option Nanosecond.Ordinal := none
   A : Option Millisecond.Offset := none
   n : Option Nanosecond.Ordinal := none
@@ -1335,10 +1335,10 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
       |>.getD ⟨0, by decide⟩
 
   let minute := builder.m |>.getD 0
-  let second := builder.s |>.getD ⟨false, 0⟩
+  let second := builder.s |>.getD 0
   let nano := (builder.n <|> builder.S) |>.getD 0
 
-  let time : PlainTime
+  let time
     :=  PlainTime.ofNanoseconds <$> builder.N
     <|> PlainTime.ofMilliseconds <$> builder.A
     |>.getD (PlainTime.mk hour minute second nano)

src/Std/Time/Notation.lean

@@ -126,7 +126,7 @@ private def convertPlainDate (d : Std.Time.PlainDate) : MacroM (TSyntax `term) :
  `(Std.Time.PlainDate.ofYearMonthDayClip $(← syntaxInt d.year) $(← syntaxBounded d.month.val) $(← syntaxBounded d.day.val))
 
 private def convertPlainTime (d : Std.Time.PlainTime) : MacroM (TSyntax `term) := do
- `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) ⟨true, $(← syntaxBounded d.second.snd.val)⟩ $(← syntaxBounded d.nanosecond.val))
+ `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) $(← syntaxBounded d.second.val) $(← syntaxBounded d.nanosecond.val))
 
 private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do
  `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) $(← convertPlainTime d.time))

src/Std/Time/Time/PlainTime.lean

@@ -30,7 +30,7 @@ structure PlainTime where
   /--
   `Second` component of the `PlainTime`
   -/
-  second : Sigma Second.Ordinal
+  second : Second.Ordinal true
 
   /--
   `Nanoseconds` component of the `PlainTime`
@@ -39,32 +39,32 @@ structure PlainTime where
   deriving Repr
 
 instance : Inhabited PlainTime where
-  default := ⟨0, 0, Sigma.mk false 0, 0, by decide⟩
+  default := ⟨0, 0, 0, 0, by decide⟩
 
 instance : BEq PlainTime where
   beq x y := x.hour.val == y.hour.val && x.minute == y.minute
-          && x.second.snd.val == y.second.snd.val && x.nanosecond == y.nanosecond
+          && x.second.val == y.second.val && x.nanosecond == y.nanosecond
 
 namespace PlainTime
 
 /--
 Creates a `PlainTime` value representing midnight (00:00:00.000000000).
 -/
 def midnight : PlainTime :=
-  ⟨0, 0, ⟨true, 0⟩, 0⟩
+  ⟨0, 0, 0, 0⟩
 
 /--
 Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components.
 -/
 @[inline]
-def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime :=
-  ⟨hour, minute, Sigma.mk leap second, nano⟩
+def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) (nano : Nanosecond.Ordinal) : PlainTime :=
+  ⟨hour, minute, second, nano⟩
 
 /--
 Creates a `PlainTime` value from the provided hours, minutes, and seconds.
 -/
 @[inline]
-def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime :=
+def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : PlainTime :=
   ofHourMinuteSecondsNano hour minute second 0
 
 /--
@@ -73,7 +73,7 @@ Converts a `PlainTime` value to the total number of milliseconds.
 def toMilliseconds (time : PlainTime) : Millisecond.Offset :=
   time.hour.toOffset.toMilliseconds +
   time.minute.toOffset.toMilliseconds +
-  time.second.snd.toOffset.toMilliseconds +
+  time.second.toOffset.toMilliseconds +
   time.nanosecond.toOffset.toMilliseconds
 
 /--
@@ -82,7 +82,7 @@ Converts a `PlainTime` value to the total number of nanoseconds.
 def toNanoseconds (time : PlainTime) : Nanosecond.Offset :=
   time.hour.toOffset.toNanoseconds +
   time.minute.toOffset.toNanoseconds +
-  time.second.snd.toOffset.toNanoseconds +
+  time.second.toOffset.toNanoseconds +
   time.nanosecond.toOffset
 
 /--
@@ -91,15 +91,15 @@ Converts a `PlainTime` value to the total number of seconds.
 def toSeconds (time : PlainTime) : Second.Offset :=
   time.hour.toOffset.toSeconds +
   time.minute.toOffset.toSeconds +
-  time.second.snd.toOffset
+  time.second.toOffset
 
 /--
 Converts a `PlainTime` value to the total number of minutes.
 -/
 def toMinutes (time : PlainTime) : Minute.Offset :=
   time.hour.toOffset.toMinutes +
   time.minute.toOffset +
-  time.second.snd.toOffset.toMinutes
+  time.second.toOffset.toMinutes
 
 /--
 Converts a `PlainTime` value to the total number of hours.
@@ -115,9 +115,12 @@ def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime :=
   have remainingNanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
   have hours := Bounded.LE.byEmod (totalSeconds.val / 3600) 24 (by decide)
   have minutes := (Bounded.LE.byEmod totalSeconds.val 3600 (by decide)).ediv 60 (by decide)
+
   have seconds := Bounded.LE.byEmod totalSeconds.val 60 (by decide)
+  have seconds := seconds.expandTop (by decide)
+
   let nanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
-  PlainTime.mk hours minutes (Sigma.mk false seconds) nanos
+  PlainTime.mk hours minutes seconds nanos
 
 /--
 Creates a `PlainTime` value from a total number of millisecond.
@@ -222,7 +225,7 @@ def subMilliseconds (time : PlainTime) (millisToSub : Millisecond.Offset) : Plai
 Creates a new `PlainTime` by adjusting the `second` component to the given value.
 -/
 @[inline]
-def withSeconds (pt : PlainTime) (second : Sigma Second.Ordinal) : PlainTime :=
+def withSeconds (pt : PlainTime) (second : Second.Ordinal true) : PlainTime :=
   { pt with second := second }
 
 /--

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

@@ -30,7 +30,7 @@ instance : LE (Ordinal leap) where
 instance : LT (Ordinal leap) where
   lt x y := LT.lt x.val y.val
 
-instance : Repr (Ordinal l) where
+instance : Repr (Ordinal leap) where
   reprPrec r := reprPrec r.val
 
 instance : OfNat (Ordinal leap) n := by
@@ -39,10 +39,10 @@ instance : OfNat (Ordinal leap) n := by
   · exact inst
   · exact ⟨inst.ofNat.expandTop (by decide)⟩
 
-instance {x y : Ordinal l} : Decidable (x ≤ y) :=
+instance {x y : Ordinal leap} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance {x y : Ordinal l} : Decidable (x < y) :=
+instance {x y : Ordinal leap} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
 /--

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

@@ -71,12 +71,7 @@ def idFromPath (path : System.FilePath) : Option String := do
 Retrieves the timezone rules from the local timezone data file.
 -/
 def localRules (path : System.FilePath) : IO ZoneRules := do
-  let localTimePath ←
-    try
-      IO.Process.run { cmd := "readlink", args := #["-f", path.toString] }
-    catch _ =>
-      throw <| IO.userError "cannot find the local timezone database"
-
+  let localTimePath ← IO.FS.realPath path
   if let some id := idFromPath localTimePath
     then parseTZIfFromDisk path id
     else throw (IO.userError "cannot read the id of the path.")

src/Std/Time/Zoned/DateTime.lean

@@ -305,7 +305,7 @@ def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz :=
 Creates a new `DateTime tz` by adjusting the `second` component.
 -/
 @[inline]
-def withSeconds (dt : DateTime tz) (second : Sigma Second.Ordinal) : DateTime tz :=
+def withSeconds (dt : DateTime tz) (second : Second.Ordinal true) : DateTime tz :=
   ofPlainDateTime (dt.date.get.withSeconds second) tz
 
 /--
@@ -368,7 +368,7 @@ def minute (dt : DateTime tz) : Minute.Ordinal :=
 Getter for the `Second` inside of a `DateTime`
 -/
 @[inline]
-def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.second.fst :=
+def second (dt : DateTime tz) : Second.Ordinal true :=
   dt.date.get.second
 
 /--

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -179,8 +179,8 @@ def minute (zdt : ZonedDateTime) : Minute.Ordinal :=
 Getter for the `Second` inside of a `ZonedDateTime`
 -/
 @[inline]
-def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.second.fst :=
-  zdt.date.get.time.second.snd
+def second (zdt : ZonedDateTime) : Second.Ordinal true :=
+  zdt.date.get.time.second
 
 /--
 Getter for the `Millisecond` inside of a `ZonedDateTime`.
@@ -491,7 +491,7 @@ def withMinutes (dt : ZonedDateTime) (minute : Minute.Ordinal) : ZonedDateTime :
 Creates a new `ZonedDateTime` by adjusting the `second` component.
 -/
 @[inline]
-def withSeconds (dt : ZonedDateTime) (second : Sigma Second.Ordinal) : ZonedDateTime :=
+def withSeconds (dt : ZonedDateTime) (second : Second.Ordinal true) : ZonedDateTime :=
   let date := dt.date.get
   ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules
 

tests/lean/run/timeAPI.lean

@@ -587,7 +587,7 @@ Std.Time.Weekday.friday
 2023-06-09
 2023-06-09
 19517
-1686268800000
+1686268800
 1970-01-02
 
 -/
@@ -667,7 +667,7 @@ Std.Time.Weekday.tuesday
 12
 3
 9938
-858650584000
+858650584
 1970-01-02T00:00:00.000000000
 
 -/
@@ -741,7 +741,7 @@ Std.Time.Weekday.thursday
 37
 2
 19978
-1726117262000
+1726117262
 1970-01-02T00:00:00.000000000Z
 
 -/
@@ -816,7 +816,7 @@ Std.Time.Weekday.tuesday
 12
 3
 9938
-858661384000
+858661384
 
 -/
 #guard_msgs in

tests/lean/run/timeFormats.lean

@@ -277,7 +277,7 @@ Format
 
 def time₄ := time("23:13:12.324354679")
 def date₄ := date("2002-07-14")
-def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 ⟨false, 12⟩ 0)
+def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 12 0)
 def datetime₄ := datetime("2002-07-14T23:13:12.324354679")
 def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00")
 def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00")
@@ -806,7 +806,7 @@ info: ("19343232432-01-04T01:04:03.000000000",
 -/
 #guard_msgs in
 #eval
-  let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 ⟨true, 3⟩ 0))
+  let r := PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 3 0)
   let s := r.toLeanDateTimeString
   let r := PlainDateTime.parse s
   (s, r, datetime("1932-01-02T05:04:03.000000000"))