style: small changes with namespace and end

src/Lean/Server/Logging.lean

@@ -90,11 +90,11 @@ where
     messageMethod? msg <|> (do pending.get? (← messageId? msg))
 
 local instance : ToJson Std.Time.ZonedDateTime where
-  toJson dt := dt.toISO8601String
+  toJson dt := Std.Time.Formats.iso8601.format dt
 
 local instance : FromJson Std.Time.ZonedDateTime where
   fromJson?
-    | .str s => Std.Time.ZonedDateTime.fromISO8601String s
+    | .str s => Std.Time.Formats.iso8601.parse s
     | _ => throw "Expected string when converting JSON to Std.Time.ZonedDateTime"
 
 structure LogEntry where

src/Std/Time.lean

@@ -17,8 +17,7 @@ public import Std.Time.Zoned.Database
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 
 /-!
 # Time
@@ -147,11 +146,16 @@ The supported formats include:
   - `yy`: Displays the year in a two-digit format, showing the last two digits (e.g., "04" for 2004).
   - `yyyy`: Displays the year in a four-digit format (e.g., "2004").
   - `yyyy+`: Extended format for years with more than four digits.
+- `Y`: Represents the week-based year (ISO-like behavior around year boundaries).
+  - `Y`, `YYY`, `YYYY`: Displays the week-based year (e.g., "2017").
+  - `YY`: Displays the last two digits of the week-based year (e.g., "17").
 - `u`: Represents the year.
   - `u`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678").
   - `uu`: Two-digit year format, showing the last two digits (e.g., "04" for 2004).
   - `uuuu`: Displays the year in a four-digit format (e.g., "2004" or "-1000").
   - `uuuu+`: Extended format for handling years with more than four digits (e.g., "12345" or "-12345"). Useful for historical dates far into the past or future!
+- `U`: Alias for extended year formatting in this library (same behavior as `u`).
+- `r`: Alias for Gregorian year formatting in this library (same behavior as `u`).
 - `D`: Represents the day of the year.
 - `M`: Represents the month of the year, displayed as either a number or text.
   - `M`, `MM`: Displays the month as a number, with `MM` zero-padded (e.g., "7" for July, "07" for July with padding).
@@ -165,18 +169,21 @@ The supported formats include:
   - `QQQQ` (full): Displays the full quarter text (e.g., "3rd quarter").
   - `QQQQQ` (narrow): Displays the quarter as a short number (e.g., "3").
 - `w`: Represents the week of the week-based year, each week starts on Monday (e.g., "27").
-- `W`: Represents the week of the month, each week starts on Monday (e.g., "4").
+- `W`: Represents the week of the month in 7-day blocks starting at day 1 (e.g., "1").
 - `E`: Represents the day of the week as text.
   - `E`, `EE`, `EEE`: Displays the abbreviated weekday name (e.g., "Tue").
   - `EEEE`: Displays the full day name (e.g., "Tuesday").
   - `EEEEE`: Displays the narrow day name (e.g., "T" for Tuesday).
+  - `EEEEEE`: Displays a two-letter weekday form (e.g., "Tu").
 - `e`: Represents the weekday as number or text.
   - `e`, `ee`: Displays the weekday as a number, starting from 1 (Monday) to 7 (Sunday).
   - `eee`, `eeee`, `eeeee`: Displays the weekday as text (same format as `E`).
+  - `eeeeee`: Displays a two-letter weekday form (e.g., "Tu").
+- `c`: Standalone weekday; supports the same widths as `e`.
 - `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3").
 - `a`: Represents the AM or PM designation of the day.
-  - `a`, `aa`, `aaa`: Displays AM or PM in a concise format (e.g., "PM").
-  - `aaaa`: Displays the full AM/PM designation (e.g., "Post Meridium").
+  - `a`, `aa`, `aaa`, `aaaa`: Displays AM/PM (e.g., "PM").
+  - `aaaaa`: Displays a narrow form (e.g., "p").
 - `h`: Represents the hour of the AM/PM clock (1-12) (e.g., "12").
   - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `K`: Represents the hour of the AM/PM clock (0-11) (e.g., "0").
@@ -197,30 +204,41 @@ The supported formats include:
   - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
 - `N`: Represents the nanosecond of the day (e.g., "1234000000").
   - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
-- `VV`: Represents the time zone ID, which could be a city-based zone (e.g., "America/Los_Angeles"), a UTC marker (`"Z"`), or a specific offset (e.g., "-08:30").
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `V`: Time zone ID variants.
+  - `V`: Displays `"unk"` (unknown short zone-id form).
+  - `VV`, `VVV`, `VVVV`: Displays the zone identifier/name (UTC-normalized where applicable).
 - `z`: Represents the time zone name.
-  - `z`, `zz`, `zzz`: Shows an abbreviated time zone name (e.g., "PST" for Pacific Standard Time).
-  - `zzzz`: Displays the full time zone name (e.g., "Pacific Standard Time").
+  - `z`, `zz`, `zzz`: Shows a short zone name (e.g., "PST", or `"UTC"` at zero offset).
+  - `zzzz`: Displays the full zone name (e.g., "Pacific Standard Time", or `"Coordinated Universal Time"` at zero offset).
+- `v`: Generic time zone name.
+  - `v`: Displays a short generic name (e.g., "UTC").
+  - `vvvv`: Displays a full generic name (e.g., "Coordinated Universal Time").
 - `O`: Represents the localized zone offset in the format "GMT" followed by the time difference from UTC.
-  - `O`: Displays the GMT offset in a simple format (e.g., "GMT+8").
-  - `OOOO`: Displays the full GMT offset, including hours and minutes (e.g., "GMT+08:00").
+  - `O`: Displays the GMT offset in a short format (e.g., "GMT+8", "GMT+0").
+  - `OOOO`: Displays the full GMT offset with padded hour and minutes (e.g., "GMT+08:00", "GMT+00:00"), and includes seconds when needed.
 - `X`: Represents the zone offset. It uses 'Z' for UTC and can represent any offset (positive or negative).
-  - `X`: Displays the hour offset (e.g., "-08").
+  - `X`: Displays hour and optional minute offset (e.g., "-08", "-0830", or "Z").
   - `XX`: Displays the hour and minute offset without a colon (e.g., "-0830").
   - `XXX`: Displays the hour and minute offset with a colon (e.g., "-08:30").
-  - `XXXX`: Displays the hour, minute, and second offset without a colon (e.g., "-083045").
-  - `XXXXX`: Displays the hour, minute, and second offset with a colon (e.g., "-08:30:45").
-- `x`: Represents the zone offset. Similar to X, but does not display 'Z' for UTC and focuses only on positive offsets.
-  - `x`: Displays the hour offset (e.g., "+08").
+  - `XXXX`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "-0830", "-083045").
+  - `XXXXX`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "-08:30", "-08:30:45").
+- `x`: Represents the zone offset. Similar to `X`, but never displays `'Z'` for UTC.
+  - `x`: Displays hour and optional minute offset (e.g., "+00", "+0530").
   - `xx`: Displays the hour and minute offset without a colon (e.g., "+0830").
   - `xxx`: Displays the hour and minute offset with a colon (e.g., "+08:30").
-  - `xxxx`: Displays the hour, minute, and second offset without a colon (e.g., "+083045").
-  - `xxxxx`: Displays the hour, minute, and second offset with a colon (e.g., "+08:30:45").
-- `Z`: Always includes an hour and minute offset and may use 'Z' for UTC, providing clear differentiation between UTC and other time zones.
-  - `Z`: Displays the hour and minute offset without a colon (e.g., "+0800").
-  - `ZZ`: Displays "GMT" followed by the time offset (e.g., "GMT+08:00" or "Z").
-  - `ZZZ`: Displays the full hour, minute, and second offset with a colon (e.g., "+08:30:45" or "Z").
+  - `xxxx`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "+0830", "+083045").
+  - `xxxxx`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "+08:30", "+08:30:45").
+- `Z`: Represents the zone offset in RFC/CLDR `Z` forms.
+  - `Z`, `ZZ`, `ZZZ`: Displays hour and minute offset without colon, with optional seconds (e.g., "+0800", "+083045").
+  - `ZZZZ`: Displays localized GMT form (e.g., "GMT+08:00").
+  - `ZZZZZ`: Displays hour and minute offset with a colon and optional seconds, and uses `"Z"` for UTC (e.g., "Z", "+08:30", "+08:30:45").
+
+# Runtime Parsing
+
+- `ZonedDateTime.parse` parses common zoned date-time formats with explicit offsets, but does not resolve timezone identifiers like `[Europe/Paris]`.
+- `ZonedDateTime.parseIO` resolves identifier-based inputs via the default timezone database.
+- `ZonedDateTime.fromLeanDateTimeWithIdentifierString` is pure and does not perform timezone database resolution.
+- `ZonedDateTime.fromLeanDateTimeWithIdentifierStringIO` resolves identifiers using the default timezone database.
 
 # Macros
 
@@ -234,8 +252,10 @@ The `.sssssssss` can be omitted in most cases.
 - **`offset("+HH:mm")`**: Represents a timezone offset in the format `+HH:mm`, where `+` or `-` indicates the direction from UTC.
 - **`timezone("NAME/ID ZZZ")`**: Specifies a timezone using a region-based name or ID, along with its associated offset.
 - **`datespec("FORMAT")`**: Defines a compile-time date format based on the provided string.
-- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZ")`**: Represents a `ZonedDateTime` with a fixed timezone and optional nanosecond precision.
+- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZZZ")`**: Represents a `ZonedDateTime` with a fixed timezone and optional nanosecond precision.
 - **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss[IDENTIFIER]")`**: Defines an `IO ZonedDateTime`, where the timezone identifier is dynamically retrieved from the default timezone database.
 - **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss, timezone")`**: Represents an `IO ZonedDateTime`, using a specified `timezone` term and allowing optional nanoseconds.
 
 -/
+
+end Std.Time

src/Std/Time/Date/Basic.lean

@@ -11,11 +11,7 @@ public import Std.Time.Date.ValidDate
 
 public section
 
-namespace Std
-namespace Time
-
-namespace Nanosecond
-namespace Offset
+namespace Std.Time.Nanosecond.Offset
 
 /--
 Convert `Nanosecond.Offset` into `Day.Offset`.
@@ -45,11 +41,9 @@ Convert `Week.Offset` into `Nanosecond.Offset`.
 def ofWeeks (weeks : Week.Offset) : Nanosecond.Offset :=
   weeks.mul 604800000000000 |>.cast (by decide +kernel)
 
-end Offset
-end Nanosecond
+end Nanosecond.Offset
 
-namespace Millisecond
-namespace Offset
+namespace Millisecond.Offset
 
 /--
 Convert `Millisecond.Offset` into `Day.Offset`.
@@ -79,11 +73,8 @@ Convert `Week.Offset` into `Millisecond.Offset`.
 def ofWeeks (weeks : Week.Offset) : Millisecond.Offset :=
   weeks.mul 604800000 |>.cast (by decide +kernel)
 
-end Offset
-end Millisecond
-
-namespace Second
-namespace Offset
+end Millisecond.Offset
+namespace Second.Offset
 
 /--
 Convert `Second.Offset` into `Day.Offset`.
@@ -113,11 +104,9 @@ Convert `Week.Offset` into `Second.Offset`.
 def ofWeeks (weeks : Week.Offset) : Second.Offset :=
   weeks.mul 604800 |>.cast (by decide +kernel)
 
-end Offset
-end Second
+end Second.Offset
 
-namespace Minute
-namespace Offset
+namespace Minute.Offset
 
 /--
 Convert `Minute.Offset` into `Day.Offset`.
@@ -147,11 +136,8 @@ Convert `Week.Offset` into `Minute.Offset`.
 def ofWeeks (weeks : Week.Offset) : Minute.Offset :=
   weeks.mul 10080 |>.cast (by decide +kernel)
 
-end Offset
-end Minute
-
-namespace Hour
-namespace Offset
+end Minute.Offset
+namespace Hour.Offset
 
 /--
 Convert `Hour.Offset` into `Day.Offset`.
@@ -181,8 +167,7 @@ Convert `Week.Offset` into `Hour.Offset`.
 def ofWeeks (weeks : Week.Offset) : Hour.Offset :=
   weeks.mul 168 |>.cast (by decide +kernel)
 
-end Offset
-end Hour
+end Hour.Offset
 
 instance : HAdd Nanosecond.Offset Nanosecond.Offset Nanosecond.Offset where
   hAdd x y := x.add y
@@ -477,3 +462,5 @@ instance : HSub Week.Offset Day.Offset Day.Offset where
 
 instance : HSub Week.Offset Week.Offset Week.Offset where
   hSub x y := x.sub y
+
+end Std.Time

src/Std/Time/Date/PlainDate.lean

@@ -12,11 +12,8 @@ import all Std.Time.Date.Unit.Year
 
 public section
 
-namespace Std
-namespace Time
-open Std.Time
-open Internal
-open Lean
+namespace Std.Time
+open Std.Time Internal Lean
 
 set_option linter.all true
 
@@ -355,6 +352,18 @@ def weekOfYear (date : PlainDate) : Week.Ordinal :=
     let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
     w
 
+/--
+Returns the week-based year for a given `PlainDate`.
+-/
+def weekBasedYear (date : PlainDate) : Year.Offset :=
+  let week := date.weekOfYear
+  if date.month.val = 1 ∧ week.val ≥ 52 then
+    date.year - 1
+  else if date.month.val = 12 ∧ week.val = 1 then
+    date.year + 1
+  else
+    date.year
+
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays
 
@@ -367,6 +376,4 @@ instance : HAdd PlainDate Week.Offset PlainDate where
 instance : HSub PlainDate Week.Offset PlainDate where
   hSub := subWeeks
 
-end PlainDate
-end Time
-end Std
+end Std.Time.PlainDate

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

@@ -20,11 +20,7 @@ The units are organized into types representing these time-related concepts, wit
 to facilitate conversions and manipulations between them.
 -/
 
-namespace Std
-namespace Time
-open Internal
-
-namespace Day.Offset
+namespace Std.Time.Day.Offset
 
 /--
 Convert `Week.Offset` into `Day.Offset`.

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

@@ -10,9 +10,8 @@ public import Std.Time.Time
 
 public section
 
-namespace Std
-namespace Time
-namespace Day
+namespace Std.Time.Day
+
 open Lean Internal
 
 set_option linter.all true
@@ -143,8 +142,7 @@ Converts an `OfYear` ordinal to a `Offset`.
 def toOffset (ofYear : OfYear leap) : Offset :=
   UnitVal.ofInt ofYear.val
 
-end OfYear
-end Ordinal
+end Ordinal.OfYear
 
 namespace Offset
 
@@ -239,7 +237,4 @@ Convert `Hour.Offset` into `Day.Offset`.
 def ofHours (hours : Hour.Offset) : Day.Offset :=
   hours.ediv 24 |>.cast (by decide +kernel)
 
-end Offset
-end Day
-end Time
-end Std
+end Std.Time.Day.Offset

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

@@ -11,9 +11,7 @@ import Init.Data.Fin.Lemmas
 
 public section
 
-namespace Std
-namespace Time
-namespace Month
+namespace Std.Time.Month
 open Internal
 
 set_option linter.all true
@@ -332,7 +330,4 @@ theorem valid_clipDay : Valid leap month (clipDay leap month day) := by
   exact Int.le_refl (days leap month).val
   next h => exact Int.not_lt.mp h
 
-end Ordinal
-end Month
-end Time
-end Std
+end Std.Time.Month.Ordinal

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

@@ -10,9 +10,7 @@ public import Std.Time.Date.Unit.Day
 
 public section
 
-namespace Std
-namespace Time
-namespace Week
+namespace Std.Time.Week
 open Internal
 
 set_option linter.all true
@@ -210,7 +208,4 @@ Convert `Day.Offset` into `Week.Offset`.
 def ofDays (days : Day.Offset) : Week.Offset :=
   days.ediv 7
 
-end Offset
-end Week
-end Time
-end Std
+end Std.Time.Week.Offset

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

@@ -10,8 +10,7 @@ public import Std.Time.Date.Unit.Day
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -158,6 +157,4 @@ def isWeekend : Weekday → Bool
   | .sunday => true
   | _ => false
 
-end Weekday
-end Time
-end Std
+end Std.Time.Weekday

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

@@ -10,9 +10,7 @@ public import Std.Time.Date.Unit.Month
 
 public section
 
-namespace Std
-namespace Time
-namespace Year
+namespace Std.Time.Year
 open Internal
 
 set_option linter.all true
@@ -128,7 +126,4 @@ Checks if the given date is valid for the specified year, month, and day.
 abbrev Valid (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : Prop :=
   day ≤ month.days year.isLeap
 
-end Offset
-end Year
-end Time
-end Std
+end Std.Time.Year.Offset

src/Std/Time/Date/ValidDate.lean

@@ -12,10 +12,8 @@ import Init.Data.Bool
 
 public section
 
-namespace Std
-namespace Time
-open Internal
-open Month.Ordinal
+namespace Std.Time
+open Internal Month.Ordinal
 
 set_option linter.all true
 
@@ -58,6 +56,7 @@ def dayOfYear (ordinal : ValidDate leap) : Day.Ordinal.OfYear leap :=
   | false, bounded => bounded
 
 set_option backward.isDefEq.respectTransparency false in
+
 /--
 Transforms a `Day.Ordinal.OfYear` into a tuple of a `Month` and a `Day`.
 -/
@@ -103,6 +102,4 @@ def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap :=
 
     go 1 0 (Int.le_trans (by decide) ordinal.property.left) (by cases leap <;> decide)
 
-end ValidDate
-end Time
-end Std
+end Std.Time.ValidDate

src/Std/Time/DateTime.lean

@@ -12,8 +12,7 @@ import all Std.Time.Date.Unit.Month
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 
 namespace Timestamp
 
@@ -106,4 +105,4 @@ def toPlainTime (pdt : PlainDateTime) : PlainTime :=
 instance : HSub PlainDateTime PlainDateTime Duration where
   hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC
 
-end PlainDateTime
+end Std.Time.PlainDateTime

src/Std/Time/DateTime/PlainDateTime.lean

@@ -10,8 +10,7 @@ public import Std.Time.DateTime.Timestamp
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -502,6 +501,11 @@ def weekOfMonth (date : PlainDateTime) : Bounded.LE 1 5 :=
   date.date.weekOfMonth
 
 /--
+Returns the week-based year for a given `PlainDateTime`.
+-/
+def weekBasedYear (date : PlainDateTime) : Year.Offset :=
+  date.date.weekBasedYear
+/--
 Determines the week of the month for the given `PlainDateTime`. The week of the month is calculated based
 on the day of the month and the weekday. Each week starts on Monday because the entire library is
 based on the Gregorian Calendar.
@@ -603,6 +607,4 @@ Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
 def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime :=
   PlainDateTime.mk date time
 
-end PlainTime
-end Time
-end Std
+end Std.Time.PlainTime

src/Std/Time/DateTime/Timestamp.lean

@@ -11,8 +11,7 @@ public import Std.Time.Duration
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -308,4 +307,4 @@ instance : HSub Timestamp Nanosecond.Offset Timestamp where
 instance : HSub Timestamp Timestamp Duration where
   hSub x y := x.val - y.val
 
-end Timestamp
+end Std.Time.Timestamp

src/Std/Time/Duration.lean

@@ -11,8 +11,7 @@ public import Init.Data.String.Basic
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -386,6 +385,4 @@ instance : HAdd PlainTime Duration PlainTime where
 instance : HSub PlainTime Duration PlainTime where
    hSub pt d := PlainTime.ofNanoseconds (pt.toNanoseconds - d.toNanoseconds)
 
-end Duration
-end Time
-end Std
+end Std.Time.Duration

src/Std/Time/Format.lean

@@ -12,10 +12,8 @@ import all Std.Time.Format.Basic
 
 public section
 
-namespace Std
-namespace Time
-namespace Formats
-open Internal
+namespace Std.Time.Formats
+open Std.Time (Format)
 
 set_option linter.all true
 
@@ -23,144 +21,207 @@ set_option linter.all true
 The ISO 8601 format, used for representing date and time in a standardized
 format. The format follows the pattern `uuuu-MM-dd'T'HH:mm:ssXXX`.
 -/
-def iso8601 : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssXXX")
-
+def iso8601 : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssXXX")
 
 /--
 The americanDate format, which follows the pattern `MM-dd-uuuu`.
 -/
-def americanDate : GenericFormat .any := datespec("MM-dd-uuuu")
+def americanDate : Format Awareness.any := datespec("MM-dd-uuuu")
 
 /--
 The europeanDate format, which follows the pattern `dd-MM-uuuu`.
 -/
-def europeanDate : GenericFormat .any := datespec("dd-MM-uuuu")
+def europeanDate : Format Awareness.any := datespec("dd-MM-uuuu")
 
 /--
 The time12Hour format, which follows the pattern `hh:mm:ss aa` for representing time
 in a 12-hour clock format with an upper case AM/PM marker.
 -/
-def time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
+def time12Hour : Format Awareness.any := datespec("hh:mm:ss aa")
 
 /--
 The Time24Hour format, which follows the pattern `HH:mm:ss` for representing time
 in a 24-hour clock format.
 -/
-def time24Hour : GenericFormat .any := datespec("HH:mm:ss")
+def time24Hour : Format Awareness.any := datespec("HH:mm:ss")
 
 /--
 The DateTimeZone24Hour format, which follows the pattern `uuuu-MM-dd:HH:mm:ss.SSSSSSSSS` for
 representing date, time, and time zone.
 -/
-def dateTime24Hour : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd:HH:mm:ss.SSSSSSSSS")
+def dateTime24Hour : Format (.only .GMT) := datespec("uuuu-MM-dd:HH:mm:ss.SSSSSSSSS")
 
 /--
 The DateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ`
 for representing date, time, and time zone.
 -/
-def dateTimeWithZone : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ")
+def dateTimeWithZone : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ")
 
 /--
 The leanTime24Hour format, which follows the pattern `HH:mm:ss.SSSSSSSSS` for representing time
 in a 24-hour clock format. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanTime24Hour : GenericFormat .any := datespec("HH:mm:ss.SSSSSSSSS")
+def leanTime24Hour : Format Awareness.any := datespec("HH:mm:ss.SSSSSSSSS")
 
 /--
 The leanTime24HourNoNanos format, which follows the pattern `HH:mm:ss` for representing time
 in a 24-hour clock format. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanTime24HourNoNanos : GenericFormat .any := datespec("HH:mm:ss")
+def leanTime24HourNoNanos : Format Awareness.any := datespec("HH:mm:ss")
 
 /--
 The leanDateTime24Hour format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS` for
 representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTime24Hour : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS")
+def leanDateTime24Hour : Format (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS")
 
 /--
 The leanDateTime24HourNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss` for
 representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTime24HourNoNanos : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss")
+def leanDateTime24HourNoNanos : Format (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss")
 
 /--
 The leanDateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithZone : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ")
+def leanDateTimeWithZone : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ")
 
 /--
 The leanDateTimeWithZoneNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ssZZZZZ`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithZoneNoNanos : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ")
+def leanDateTimeWithZoneNoNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ")
 
 /--
 The leanDateTimeWithIdentifier format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss[z]`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithIdentifier : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss'['zzzz']'")
+def leanDateTimeWithIdentifier : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss'['VV']'")
 
 /--
 The leanDateTimeWithIdentifierAndNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'[z]'`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithIdentifierAndNanos : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'['zzzz']'")
+def leanDateTimeWithIdentifierAndNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'['VV']'")
+
+/--
+The leanDateTimeWithZoneAndName format, which follows the pattern
+`uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ'['zzzz']'` for representing date, time, timezone offset,
+and timezone identifier. This is the canonical Lean format used in `repr` for named timezones.
+-/
+def leanDateTimeWithZoneAndName : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ'['VV']'")
+
+/--
+The leanDateTimeWithZoneAndNameNoNanos format, which follows the pattern
+`uuuu-MM-dd'T'HH:mm:ssZZZZZ'['zzzz']'` for representing date, time, timezone offset, and timezone
+identifier without nanoseconds.
+-/
+def leanDateTimeWithZoneAndNameNoNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ'['VV']'")
 
 /--
 The Lean Date format, which follows the pattern `uuuu-MM-dd`. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDate : GenericFormat .any := datespec("uuuu-MM-dd")
+def leanDate : Format Awareness.any := datespec("uuuu-MM-dd")
 
 /--
 The SQLDate format, which follows the pattern `uuuu-MM-dd` and is commonly used
 in SQL databases to represent dates.
 -/
-def sqlDate : GenericFormat .any := datespec("uuuu-MM-dd")
+def sqlDate : Format Awareness.any := datespec("uuuu-MM-dd")
 
 /--
 The LongDateFormat, which follows the pattern `EEEE, MMMM d, uuuu HH:mm:ss` for
 representing a full date and time with the day of the week and month name.
 -/
-def longDateFormat : GenericFormat (.only .GMT) := datespec("EEEE, MMMM d, uuuu HH:mm:ss")
+def longDateFormat : Format (.only .GMT) := datespec("EEEE, MMMM d, uuuu HH:mm:ss")
 
 /--
 The AscTime format, which follows the pattern `EEE MMM d HH:mm:ss uuuu`. This format
 is often used in older systems for logging and time-stamping events.
 -/
-def ascTime : GenericFormat (.only .GMT) := datespec("EEE MMM d HH:mm:ss uuuu")
+def ascTime : Format (.only .GMT) := datespec("EEE MMM d HH:mm:ss uuuu")
 
 /--
 The RFC822 format, which follows the pattern `eee, dd MMM uuuu HH:mm:ss ZZZ`.
 This format is used in email headers and HTTP headers.
 -/
-def rfc822 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def rfc822 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
 
 /--
 The RFC850 format, which follows the pattern `eee, dd-MMM-YY HH:mm:ss ZZZ`.
 This format is an older standard for representing date and time in headers.
 -/
-def rfc850 : GenericFormat .any := datespec("eee, dd-MM-uuuu HH:mm:ss ZZZ")
+def rfc850 : Format Awareness.any := datespec("eee, dd-MM-uuuu HH:mm:ss ZZZ")
+
+/--
+A `MultiFormat` that parses `leanDateTimeWithZone` with or without nanoseconds.
+-/
+def leanDateTimeWithZoneAlt : MultiFormat Awareness.any :=
+  .new #[leanDateTimeWithZone, leanDateTimeWithZoneNoNanos]
+
+/--
+A `MultiFormat` that parses `leanDateTimeWithZoneAndName` with or without nanoseconds.
+-/
+def leanDateTimeWithZoneAndNameAlt : MultiFormat Awareness.any :=
+  .new #[leanDateTimeWithZoneAndName, leanDateTimeWithZoneAndNameNoNanos]
+
+/--
+A `MultiFormat` that parses `leanDateTime24Hour` with or without nanoseconds.
+-/
+def leanDateTime24HourAlt : MultiFormat (.only .GMT) :=
+  .new #[leanDateTime24Hour, leanDateTime24HourNoNanos]
+
+/--
+A `MultiFormat` that parses `leanTime24Hour` with or without nanoseconds.
+-/
+def leanTime24HourAlt : MultiFormat Awareness.any :=
+  .new #[leanTime24Hour, leanTime24HourNoNanos]
+
+/--
+A `MultiFormat` that parses `leanDateTimeWithIdentifier` with or without nanoseconds.
+-/
+def leanDateTimeWithIdentifierAlt : MultiFormat Awareness.any :=
+  .new #[leanDateTimeWithIdentifier, leanDateTimeWithIdentifierAndNanos]
 
 end Formats
 
+namespace Format
+
+/--
+Parses the input string, resolving any timezone identifier via the default timezone database.
+For formats with a timezone identifier specifier but no offset specifier (e.g.
+`uuuu-MM-dd'T'HH:mm:ss'['zzzz']'`), this performs a tzdb lookup to find the correct UTC offset.
+For all other formats this behaves identically to `parse`.
+-/
+def parseIO (format : Format Awareness.any) (input : String) : IO ZonedDateTime := do
+  if format.hasIdentifierSpecifier && !format.hasOffsetSpecifier then
+    match format.parseUnchecked input with
+    | .error err => throw <| IO.userError err
+    | .ok zdt =>
+      let rules ← Database.defaultGetZoneRules zdt.timezone.name
+      pure <| ZonedDateTime.ofPlainDateTime zdt.toPlainDateTime rules
+  else
+    IO.ofExcept (format.parse input)
+
+end Format
+
 namespace TimeZone
 
 /--
 Parses a string into a `TimeZone` object. The input string must be in the format `"VV ZZZZZ"`.
 -/
 def fromTimeZone (input : String) : Except String TimeZone := do
-  let spec : GenericFormat .any := datespec("VV ZZZZZ")
+  let spec : Format Awareness.any := datespec("VV ZZZZZ")
   spec.parseBuilder (fun id off => some (TimeZone.mk off id (off.toIsoString true) false)) input
 
 namespace Offset
@@ -169,11 +230,10 @@ namespace Offset
 Parses a string representing an offset into an `Offset` object. The input string must follow the `"xxx"` format.
 -/
 def fromOffset (input : String) : Except String Offset := do
-  let spec : GenericFormat .any := datespec("xxx")
+  let spec : Format Awareness.any := datespec("xxx")
   spec.parseBuilder some input
 
-end Offset
-end TimeZone
+end TimeZone.Offset
 
 namespace PlainDate
 
@@ -181,18 +241,19 @@ namespace PlainDate
 Formats a `PlainDate` using a specific format.
 -/
 def format (date : PlainDate) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
     let res := res.formatGeneric fun
       | .G _ => some date.era
       | .y _ => some date.year
+      | .Y _ => some date.weekBasedYear
       | .u _ => some date.year
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
       | .Qorq _ => some date.quarter
       | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
+      | .W _ => some (date.weekOfMonth.expandTop (by decide))
       | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
@@ -203,54 +264,21 @@ def format (date : PlainDate) (format : String) : String :=
     | some res => res
     | none => "invalid time"
 
-/--
-Parses a date string in the American format (`MM-dd-uuuu`) and returns a `PlainDate`.
--/
-def fromAmericanDateString (input : String) : Except String PlainDate := do
-  Formats.americanDate.parseBuilder (fun m d y => PlainDate.ofYearMonthDay? y m d) input
-
-/--
-Converts a date in the American format (`MM-dd-uuuu`) into a `String`.
--/
-def toAmericanDateString (input : PlainDate) : String :=
-  Formats.americanDate.formatBuilder input.month input.day input.year
-
-/--
-Parses a date string in the SQL format (`uuuu-MM-dd`) and returns a `PlainDate`.
--/
-def fromSQLDateString (input : String) : Except String PlainDate := do
-  Formats.sqlDate.parseBuilder PlainDate.ofYearMonthDay? input
-
-/--
-Converts a date in the SQL format (`uuuu-MM-dd`) into a `String`.
--/
-def toSQLDateString (input : PlainDate) : String :=
-  Formats.sqlDate.formatBuilder input.year input.month input.day
-
-/--
-Parses a date string in the Lean format (`uuuu-MM-dd`) and returns a `PlainDate`.
--/
-def fromLeanDateString (input : String) : Except String PlainDate := do
-  Formats.leanDate.parseBuilder PlainDate.ofYearMonthDay? input
-
-/--
-Converts a date in the Lean format (`uuuu-MM-dd`) into a `String`.
--/
-def toLeanDateString (input : PlainDate) : String :=
-  Formats.leanDate.formatBuilder input.year input.month input.day
-
 /--
 Parses a `String` in the `AmericanDate` or `SQLDate` format and returns a `PlainDate`.
 -/
 def parse (input : String) : Except String PlainDate :=
-  fromAmericanDateString input
-  <|> fromSQLDateString input
+  Formats.americanDate.parseBuilder (fun m d y => PlainDate.ofYearMonthDay? y m d) input
+  <|> Formats.sqlDate.parseBuilder PlainDate.ofYearMonthDay? input
+
+def leanDateString (d : PlainDate) : String :=
+  Formats.leanDate.formatBuilder d.year d.month d.day
 
 instance : ToString PlainDate where
-  toString := toLeanDateString
+  toString := leanDateString
 
 instance : Repr PlainDate where
-  reprPrec data := Repr.addAppParen ("date(\"" ++ toLeanDateString data ++ "\")")
+  reprPrec d := Repr.addAppParen ("date(\"" ++ leanDateString d ++ "\")")
 
 end PlainDate
 
@@ -260,7 +288,7 @@ namespace PlainTime
 Formats a `PlainTime` using a specific format.
 -/
 def format (time : PlainTime) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
@@ -282,58 +310,24 @@ def format (time : PlainTime) (format : String) : String :=
     | none => "invalid time"
 
 /--
-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)) input
-
-/--
-Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
--/
-def toTime24Hour (input : PlainTime) : String :=
-  Formats.time24Hour.formatBuilder input.hour input.minute input.second
-
-/--
-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 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`).
--/
-def toLeanTime24Hour (input : PlainTime) : String :=
-  Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond
-
-/--
-Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`.
--/
-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
-
-  Formats.time12Hour.parseBuilder builder input
-
-/--
-Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`).
--/
-def toTime12Hour (input : PlainTime) : String :=
-  Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute input.second (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am)
-
-/--
-Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`.
+Parses a `String` in the `Time12Hour`, `Time24Hour`, or lean time (with optional nanoseconds) format
+and returns a `PlainTime`.
 -/
 def parse (input : String) : Except String PlainTime :=
-  fromTime12Hour input
-  <|> fromTime24Hour input
+  Formats.time12Hour.parseBuilder (fun h m s a => do
+    let value ← Internal.Bounded.ofInt? h.val
+    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s) input
+  <|> Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
+  <|> Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
+
+def leanTimeString (t : PlainTime) : String :=
+  Formats.leanTime24Hour.formatBuilder t.hour t.minute t.second t.nanosecond
 
 instance : ToString PlainTime where
-  toString := toLeanTime24Hour
+  toString := leanTimeString
 
 instance : Repr PlainTime where
-  reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")")
+  reprPrec data := Repr.addAppParen ("time(\"" ++ leanTimeString data ++ "\")")
 
 end PlainTime
 
@@ -343,99 +337,60 @@ namespace ZonedDateTime
 Formats a `ZonedDateTime` using a specific format.
 -/
 def format (data: ZonedDateTime) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
-  | .ok res => res.format data.toDateTime
+  | .ok res => res.format data
 
 /--
-Parses a `String` in the `ISO8601` format and returns a `ZonedDateTime`.
+Parses a `String` in common zoned date-time formats and returns a `ZonedDateTime`.
+This parser does not resolve timezone identifiers like `[Europe/Paris]`; use `parseIO` for that.
 -/
-def fromISO8601String (input : String) : Except String ZonedDateTime :=
-  Formats.iso8601.parse input
+-- Wraps Format.parse to fix type unification (Awareness.any.type vs ZonedDateTime).
+private def parseFormat (fmt : Format Awareness.any) (input : String) : Except String ZonedDateTime :=
+  fmt.parse input
 
-/--
-Formats a `ZonedDateTime` value into an ISO8601 string.
--/
-def toISO8601String (date : ZonedDateTime) : String :=
-  Formats.iso8601.format date.toDateTime
-
-/--
-Parses a `String` in the rfc822 format and returns a `ZonedDateTime`.
--/
-def fromRFC822String (input : String) : Except String ZonedDateTime :=
-  Formats.rfc822.parse input
-
-/--
-Formats a `ZonedDateTime` value into an RFC822 format string.
--/
-def toRFC822String (date : ZonedDateTime) : String :=
-  Formats.rfc822.format date.toDateTime
-
-/--
-Parses a `String` in the rfc850 format and returns a `ZonedDateTime`.
--/
-def fromRFC850String (input : String) : Except String ZonedDateTime :=
-  Formats.rfc850.parse input
-
-/--
-Formats a `ZonedDateTime` value into an RFC850 format string.
--/
-def toRFC850String (date : ZonedDateTime) : String :=
-  Formats.rfc850.format date.toDateTime
-
-/--
-Parses a `String` in the dateTimeWithZone format and returns a `ZonedDateTime` object in the GMT time zone.
--/
-def fromDateTimeWithZoneString (input : String) : Except String ZonedDateTime :=
-  Formats.dateTimeWithZone.parse input
-
-/--
-Formats a `ZonedDateTime` value into a simple date time with timezone string.
--/
-def toDateTimeWithZoneString (pdt : ZonedDateTime) : String :=
-  Formats.dateTimeWithZone.format pdt.toDateTime
-
-/--
-Parses a `String` in the lean date time format with timezone format and returns a `ZonedDateTime` object.
--/
-def fromLeanDateTimeWithZoneString (input : String) : Except String ZonedDateTime :=
-  Formats.leanDateTimeWithZone.parse input
-  <|> Formats.leanDateTimeWithZoneNoNanos.parse input
-
-/--
-Parses a `String` in the lean date time format with identifier and returns a `ZonedDateTime` object.
--/
-def fromLeanDateTimeWithIdentifierString (input : String) : Except String ZonedDateTime :=
-  Formats.leanDateTimeWithIdentifier.parse input
-  <|> Formats.leanDateTimeWithIdentifierAndNanos.parse input
-
-/--
-Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation.
--/
-def toLeanDateTimeWithZoneString (zdt : ZonedDateTime) : String :=
-  Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset
-/--
-Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier.
--/
-def toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : String :=
-  Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.timezone.name
-
-/--
-Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `ZonedDateTime`.
--/
 def parse (input : String) : Except String ZonedDateTime :=
-  fromISO8601String input
-  <|> fromRFC822String input
-  <|> fromRFC850String input
-  <|> fromDateTimeWithZoneString input
-  <|> fromLeanDateTimeWithIdentifierString input
+  parseFormat Formats.iso8601 input
+  <|> parseFormat Formats.rfc822 input
+  <|> parseFormat Formats.rfc850 input
+  <|> parseFormat Formats.leanDateTimeWithZone input
+  <|> parseFormat Formats.leanDateTimeWithZoneNoNanos input
+  <|> parseFormat Formats.leanDateTimeWithZoneAndName input
+  <|> parseFormat Formats.leanDateTimeWithZoneAndNameNoNanos input
+  <|> parseFormat Formats.dateTimeWithZone input
+  <|> parseFormat Formats.leanDateTimeWithIdentifier input
+  <|> parseFormat Formats.leanDateTimeWithIdentifierAndNanos input
+
+/--
+Parses a `String` in common zoned date-time formats.
+If the input uses a timezone identifier (for example, `[Europe/Paris]`), it resolves it using the default timezone database.
+-/
+def parseIO (input : String) : IO ZonedDateTime := do
+  match parse input with
+  | .ok zdt => pure zdt
+  | .error err =>
+    let identParse : Except String ZonedDateTime :=
+      Formats.leanDateTimeWithIdentifier.parseUnchecked input
+      <|> Formats.leanDateTimeWithIdentifierAndNanos.parseUnchecked input
+    match identParse with
+    | .ok zdt =>
+      let rules ← Database.defaultGetZoneRules zdt.timezone.name
+      pure <| ZonedDateTime.ofPlainDateTime zdt.toPlainDateTime rules
+    | .error _ => throw <| IO.userError err
 
 instance : ToString ZonedDateTime where
-  toString := toLeanDateTimeWithIdentifierString
+  toString data := Formats.leanDateTimeWithIdentifierAndNanos.format data
 
 instance : Repr ZonedDateTime where
-  reprPrec data := Repr.addAppParen ("zoned(\"" ++ toLeanDateTimeWithZoneString data ++ "\")")
+  reprPrec data :=
+    let name := data.timezone.name
+    let str :=
+      if name == data.timezone.offset.toIsoString true then
+        Formats.leanDateTimeWithZone.format data
+      else
+        Formats.leanDateTimeWithZoneAndName.format data
+    Repr.addAppParen ("zoned(\"" ++ str ++ "\")")
 
 end ZonedDateTime
 
@@ -445,18 +400,27 @@ namespace PlainDateTime
 Formats a `PlainDateTime` using a specific format.
 -/
 def format (date : PlainDateTime) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
     let res := res.formatGeneric fun
       | .G _ => some date.era
       | .y _ => some date.year
+      | .Y _ =>
+        let week := date.weekOfYear
+        some <|
+          if date.month.val = 1 ∧ week.val ≥ 52 then
+            date.year - 1
+          else if date.month.val = 12 ∧ week.val = 1 then
+            date.year + 1
+          else
+            date.year
       | .u _ => some date.year
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
       | .Qorq _ => some date.quarter
       | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
+      | .W _ => some (date.weekOfMonth.expandTop (by decide))
       | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
@@ -479,71 +443,22 @@ def format (date : PlainDateTime) (format : String) : String :=
     | none => "invalid time"
 
 /--
-Parses a `String` in the `AscTime` format and returns a `PlainDateTime` object in the GMT time zone.
--/
-def fromAscTimeString (input : String) : Except String PlainDateTime :=
-  Formats.ascTime.parse input
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into an AscTime format string.
--/
-def toAscTimeString (pdt : PlainDateTime) : String :=
-  Formats.ascTime.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC)
-
-/--
-Parses a `String` in the `LongDateFormat` and returns a `PlainDateTime` object in the GMT time zone.
--/
-def fromLongDateFormatString (input : String) : Except String PlainDateTime :=
-  Formats.longDateFormat.parse input
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into a LongDateFormat string.
--/
-def toLongDateFormatString (pdt : PlainDateTime) : String :=
-  Formats.longDateFormat.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC)
-
-/--
-Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
--/
-def fromDateTimeString (input : String) : Except String PlainDateTime :=
-  Formats.dateTime24Hour.parse input
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into a `DateTime` format string.
--/
-def toDateTimeString (pdt : PlainDateTime) : String :=
-  Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
-
-/--
-Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
--/
-def fromLeanDateTimeString (input : String) : Except String PlainDateTime :=
-  (Formats.leanDateTime24Hour.parse input <|> Formats.leanDateTime24HourNoNanos.parse input)
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into a `DateTime` format string.
--/
-def toLeanDateTimeString (pdt : PlainDateTime) : String :=
-  Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
-
-/--
-Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`.
+Parses a `String` in the `AscTime`, `LongDate`, `DateTime`, or `LeanDateTime` format and returns a `PlainDateTime`.
 -/
 def parse (date : String) : Except String PlainDateTime :=
-  fromAscTimeString date
-  <|> fromLongDateFormatString date
-  <|> fromDateTimeString date
-  <|> fromLeanDateTimeString date
+  (Formats.ascTime.parse date).map DateTime.toPlainDateTime
+  <|> (Formats.longDateFormat.parse date).map DateTime.toPlainDateTime
+  <|> (Formats.dateTime24Hour.parse date).map DateTime.toPlainDateTime
+  <|> (Formats.leanDateTime24HourAlt.parse date).map DateTime.toPlainDateTime
+
+def leanPlainDateTimeString (date : PlainDateTime) : String :=
+  Formats.leanDateTime24Hour.formatBuilder date.year date.month date.day date.hour date.minute date.time.second date.nanosecond
 
 instance : ToString PlainDateTime where
-  toString := toLeanDateTimeString
+  toString := leanPlainDateTimeString
 
 instance : Repr PlainDateTime where
-  reprPrec data := Repr.addAppParen ("datetime(\"" ++ toLeanDateTimeString data ++ "\")")
+  reprPrec data := Repr.addAppParen ("datetime(\"" ++ leanPlainDateTimeString data ++ "\")")
 
 end PlainDateTime
 
@@ -553,76 +468,22 @@ namespace DateTime
 Formats a `DateTime` using a specific format.
 -/
 def format (data: DateTime tz) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res => res.format data
 
-/--
-Parses a `String` in the `AscTime` format and returns a `DateTime` object in the GMT time zone.
--/
-def fromAscTimeString (input : String) : Except String (DateTime .GMT) :=
-  Formats.ascTime.parse input
-
-/--
-Formats a `DateTime` value into an AscTime format string.
--/
-def toAscTimeString (datetime : DateTime .GMT) : String :=
-  Formats.ascTime.format datetime
-
-/--
-Parses a `String` in the `LongDateFormat` and returns a `DateTime` object in the GMT time zone.
--/
-def fromLongDateFormatString (input : String) : Except String (DateTime .GMT) :=
-  Formats.longDateFormat.parse input
-
-/--
-Formats a `DateTime` value into a LongDateFormat string.
--/
-def toLongDateFormatString (datetime : DateTime .GMT) : String :=
-  Formats.longDateFormat.format datetime
-
-/--
-Formats a `DateTime` value into an ISO8601 string.
--/
-def toISO8601String (date : DateTime tz) : String :=
-  Formats.iso8601.format date
-
-/--
-Formats a `DateTime` value into an RFC822 format string.
--/
-def toRFC822String (date : DateTime tz) : String :=
-  Formats.rfc822.format date
-
-/--
-Formats a `DateTime` value into an RFC850 format string.
--/
-def toRFC850String (date : DateTime tz) : String :=
-  Formats.rfc850.format date
-
-/--
-Formats a `DateTime` value into a `DateTimeWithZone` format string.
--/
-def toDateTimeWithZoneString (pdt : DateTime tz) : String :=
-  Formats.dateTimeWithZone.format pdt
-
-/--
-Formats a `DateTime` value into a `DateTimeWithZone` format string that can be parsed by `date%`.
--/
-def toLeanDateTimeWithZoneString (pdt : DateTime tz) : String :=
-  Formats.leanDateTimeWithZone.format pdt
-
 /--
 Parses a `String` in the `AscTime` or `LongDate` format and returns a `DateTime`.
 -/
 def parse (date : String) : Except String (DateTime .GMT) :=
-  fromAscTimeString date
-  <|> fromLongDateFormatString date
+  Formats.ascTime.parse date
+  <|> Formats.longDateFormat.parse date
 
 instance : Repr (DateTime tz) where
-  reprPrec data := Repr.addAppParen (toLeanDateTimeWithZoneString data)
+  reprPrec data := Repr.addAppParen (Formats.leanDateTimeWithZone.format data)
 
 instance : ToString (DateTime tz) where
-  toString := toLeanDateTimeWithZoneString
+  toString data := Formats.leanDateTimeWithZone.format data
 
 end DateTime

src/Std/Time/Format/Basic.lean

@@ -16,25 +16,37 @@ public section
 This module defines the `Formatter` types. It is based on the Java's `DateTimeFormatter` format.
 -/
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec Lean PlainTime PlainDate TimeZone DateTime
 
 set_option linter.all true
 
-
 /--
 `Text` represents different text formatting styles.
 -/
 inductive Text
-  /-- Short form (e.g., "Tue") -/
+
+  /--
+  Short form (e.g., "Tue")
+  -/
   | short
-  /-- Full form (e.g., "Tuesday") -/
+
+  /--
+  Full form (e.g., "Tuesday")
+  -/
   | full
-  /-- Narrow form (e.g., "T") -/
+
+  /--
+  Narrow form (e.g., "T")
+  -/
   | narrow
+
+  /--
+  Two-letter short form (e.g., "Tu")
+  -/
+  | twoLetterShort
   deriving Repr, Inhabited
 
 namespace Text
@@ -203,15 +215,30 @@ The output will vary between the number of pattern letters, whether it's the hou
 and whether colons are used.
 -/
 inductive OffsetX
-  /-- Only the hour is output (e.g., "+01") -/
+
+  /--
+  Only the hour is output (e.g., "+01")
+  -/
   | hour
-  /-- Hour and minute without colon (e.g., "+0130") -/
+
+  /--
+  Hour and minute without colon (e.g., "+0130")
+  -/
   | hourMinute
-  /-- Hour and minute with colon (e.g., "+01:30") -/
+
+  /--
+  Hour and minute with colon (e.g., "+01:30")
+  -/
   | hourMinuteColon
-  /-- Hour, minute, and second without colon (e.g., "+013015") -/
+
+  /--
+  Hour, minute, and second without colon (e.g., "+013015")
+  -/
   | hourMinuteSecond
-  /-- Hour, minute, and second with colon (e.g., "+01:30:15") -/
+
+  /--
+  Hour, minute, and second with colon (e.g., "+01:30:15")
+  -/
   | hourMinuteSecondColon
   deriving Repr, Inhabited
 
@@ -240,9 +267,15 @@ end OffsetX
 `OffsetO` represents localized offset text formats based on the number of pattern letters.
 -/
 inductive OffsetO
-  /-- Short form of the localized offset (e.g., "GMT+8") -/
+
+  /--
+  Short form of the localized offset (e.g., "GMT+8")
+  -/
   | short
-  /-- Full form of the localized offset (e.g., "GMT+08:00") -/
+
+  /--
+  Full form of the localized offset (e.g., "GMT+08:00")
+  -/
   | full
   deriving Repr, Inhabited
 
@@ -263,11 +296,20 @@ end OffsetO
 `OffsetZ` represents different offset formats based on the number of pattern letters (capital 'Z').
 -/
 inductive OffsetZ
-  /-- Hour and minute without colon (e.g., "+0130") -/
+
+  /--
+  Hour and minute without colon, with optional seconds (e.g., "+0130", "+013015")
+  -/
   | hourMinute
-  /-- Localized offset text in full form (e.g., "GMT+08:00") -/
+
+  /--
+  Localized offset text in full form (e.g., "GMT+08:00")
+  -/
   | full
-  /-- Hour, minute, and second with colon (e.g., "+01:30:15") -/
+
+  /--
+  Hour and minute with colon, with optional seconds, and "Z" for zero offset (e.g., "+01:30", "+01:30:15", "Z")
+  -/
   | hourMinuteSecondColon
   deriving Repr, Inhabited
 
@@ -301,6 +343,16 @@ inductive Modifier
   -/
   | y (presentation : Year)
 
+  /--
+  `Y`: Week-based year (e.g., 2004, 04, 0002, 2).
+  -/
+  | Y (presentation : Year)
+
+  /--
+  `Q`: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter).
+  -/
+  | Qorq (presentation : Number ⊕ Text)
+
   /--
   `u`: Year (e.g., 2004, 04, -0001, -1).
   -/
@@ -321,11 +373,6 @@ inductive Modifier
   -/
   | d (presentation : Number)
 
-  /--
-  `Q`: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter).
-  -/
-  | Qorq (presentation : Number ⊕ Text)
-
   /--
   `w`: Week of week-based year (e.g., 27).
   -/
@@ -407,15 +454,20 @@ inductive Modifier
   | N (presentation : Number)
 
   /--
-  `V`: Time zone ID (e.g., America/Los_Angeles, Z, -08:30).
+  `V`: Time zone ID variant (e.g., `V`, `VV`, `VVV`, `VVVV`).
   -/
-  | V
+  | V (presentation : Number)
 
   /--
   `z`: Time zone name (e.g., Pacific Standard Time, PST).
   -/
   | z (presentation : ZoneName)
 
+  /--
+  `v`: Generic time zone name, without DST distinction (e.g., Pacific Time, PT).
+  -/
+  | v (presentation : ZoneName)
+
   /--
   `O`: Localized zone offset (e.g., GMT+8, GMT+08:00, UTC-08:00).
   -/
@@ -432,7 +484,10 @@ inductive Modifier
   | x (presentation : OffsetX)
 
   /--
-  `Z`: Zone offset with 'Z' for UTC (e.g., +0000, -0800, -08:00).
+  `Z`: Zone offset.
+  - `Z`, `ZZ`, `ZZZ`: output `±HHMMss` (no colon); parse `±HHMM[ss]`. Does **not** accept the literal `Z` character for UTC — use `ZZZZZ` or `XXX` for that.
+  - `ZZZZ`: outputs/parses localized GMT form (e.g., `GMT+08:00`).
+  - `ZZZZZ`: outputs `±HH:mm[:ss]` and uses `Z` for UTC (e.g., `Z`, `+01:30`).
   -/
   | Z (presentation : OffsetZ)
   deriving Repr, Inhabited
@@ -450,6 +505,13 @@ private def parseMod (constructor : α → Modifier) (classify : Nat → Option
 private def parseText (constructor : Text → Modifier) (p : String) : Parser Modifier :=
   parseMod constructor Text.classify p
 
+private def classifyWeekdayText : Nat → Option Text
+  | 6 => some .twoLetterShort
+  | n => Text.classify n
+
+private def parseWeekdayText (constructor : Text → Modifier) (p : String) : Parser Modifier :=
+  parseMod constructor classifyWeekdayText p
+
 private def parseFraction (constructor : Fraction → Modifier) (p : String) : Parser Modifier :=
   parseMod constructor Fraction.classify p
 
@@ -469,11 +531,38 @@ private def parseOffsetO (constructor : OffsetO → Modifier) (p : String) : Par
   parseMod constructor OffsetO.classify p
 
 private def parseZoneId (p : String) : Parser Modifier :=
-  if p.length = 2 then pure .V else fail s!"invalid quantity of characters for '{p.front}'"
+  if p.length ≥ 2 ∧ p.length ≤ 4 then
+    pure (.V ⟨p.length⟩)
+  else
+    fail s!"invalid quantity of characters for '{p.front}': must be 2–4"
 
 private def parseNumberText (constructor : (Number ⊕ Text) → Modifier) (p : String) : Parser Modifier :=
   parseMod constructor classifyNumberText p
 
+private def classifyWeekdayNumberText : Nat → Option (Number ⊕ Text)
+  | n =>
+    if n < 3 then
+      some (.inl ⟨n⟩)
+    else if n = 6 then
+      some (.inr .twoLetterShort)
+    else
+      .inr <$> Text.classify n
+
+private def parseWeekdayNumberText (constructor : (Number ⊕ Text) → Modifier) (p : String) : Parser Modifier :=
+  parseMod constructor classifyWeekdayNumberText p
+
+private def classifyMarkerText : Nat → Option Text
+  | n =>
+    if n ≤ 4 then
+      some .short
+    else if n = 5 then
+      some .narrow
+    else
+      none
+
+private def parseMarker (constructor : Text → Modifier) (p : String) : Parser Modifier :=
+  parseMod constructor classifyMarkerText p
+
 private def parseZoneName (constructor : ZoneName → Modifier) (p : String) : Parser Modifier :=
   let len := p.length
   match ZoneName.classify (p.front) len with
@@ -483,7 +572,10 @@ private def parseZoneName (constructor : ZoneName → Modifier) (p : String) : P
 private def parseModifier : Parser Modifier
   := (parseText Modifier.G =<< many1Chars (pchar 'G'))
   <|> parseYear Modifier.y =<< many1Chars (pchar 'y')
+  <|> parseYear Modifier.Y =<< many1Chars (pchar 'Y')
   <|> parseYear Modifier.u =<< many1Chars (pchar 'u')
+  <|> (many1Chars (pchar 'U') *> pure (.u .any))
+  <|> (many1Chars (pchar 'r') *> pure (.u .any))
   <|> parseNumber Modifier.D =<< many1Chars (pchar 'D')
   <|> parseNumberText Modifier.MorL =<< many1Chars (pchar 'M')
   <|> parseNumberText Modifier.MorL =<< many1Chars (pchar 'L')
@@ -492,11 +584,11 @@ private def parseModifier : Parser Modifier
   <|> parseNumberText Modifier.Qorq =<< many1Chars (pchar 'q')
   <|> parseNumber Modifier.w =<< many1Chars (pchar 'w')
   <|> parseNumber Modifier.W =<< many1Chars (pchar 'W')
-  <|> parseText Modifier.E =<< many1Chars (pchar 'E')
-  <|> parseNumberText Modifier.eorc =<< many1Chars (pchar 'e')
-  <|> parseNumberText Modifier.eorc =<< many1Chars (pchar 'c')
+  <|> parseWeekdayText Modifier.E =<< many1Chars (pchar 'E')
+  <|> parseWeekdayNumberText Modifier.eorc =<< many1Chars (pchar 'e')
+  <|> parseWeekdayNumberText Modifier.eorc =<< many1Chars (pchar 'c')
   <|> parseNumber Modifier.F =<< many1Chars (pchar 'F')
-  <|> parseText Modifier.a =<< many1Chars (pchar 'a')
+  <|> parseMarker Modifier.a =<< many1Chars (pchar 'a')
   <|> parseNumber Modifier.h =<< many1Chars (pchar 'h')
   <|> parseNumber Modifier.K =<< many1Chars (pchar 'K')
   <|> parseNumber Modifier.k =<< many1Chars (pchar 'k')
@@ -509,6 +601,7 @@ private def parseModifier : Parser Modifier
   <|> parseNumber Modifier.N =<< many1Chars (pchar 'N')
   <|> parseZoneId =<< many1Chars (pchar 'V')
   <|> parseZoneName Modifier.z =<< many1Chars (pchar 'z')
+  <|> parseZoneName Modifier.v =<< many1Chars (pchar 'v')
   <|> parseOffsetO Modifier.O =<< many1Chars (pchar 'O')
   <|> parseOffsetX Modifier.X =<< many1Chars (pchar 'X')
   <|> parseOffsetX Modifier.x =<< many1Chars (pchar 'x')
@@ -589,7 +682,7 @@ deriving Inhabited, Repr
 /--
 A specification on how to format a data or parse some string.
 -/
-structure GenericFormat (awareness : Awareness) where
+structure Format (awareness : Awareness) where
   /--
   Configuration options for formatting behavior.
   -/
@@ -751,11 +844,8 @@ private def formatMarkerLong (marker : HourMarker) : String :=
 
 private def formatMarkerNarrow (marker : HourMarker) : String :=
   match marker with
-  | .am => "A"
-  | .pm => "P"
-
-private def toSigned (data : Int) : String :=
-  if data < 0 then toString data else "+" ++ toString data
+  | .am => "a"
+  | .pm => "p"
 
 private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) : String :=
   let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second)
@@ -768,11 +858,50 @@ private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bo
 
   data
 
+private def toLocalizedGMT (offset : Offset) (full : Bool) : String :=
+  if offset.second.val = 0 then
+    "GMT"
+  else
+    let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second)
+    let time := PlainTime.ofSeconds time
+    let hour :=
+      if full then
+        leftPad 2 '0' (toString time.hour.val)
+      else
+        toString time.hour.val
+    let hasMinute := full ∨ time.minute.val ≠ 0 ∨ time.second.val ≠ 0
+    let withMinute :=
+      if hasMinute then
+        s!"GMT{sign}{hour}:{leftPad 2 '0' (toString time.minute.val)}"
+      else
+        s!"GMT{sign}{hour}"
+    if time.second.val ≠ 0 then
+      s!"{withMinute}:{leftPad 2 '0' (toString time.second.val)}"
+    else
+      withMinute
+
+private def isUTCLabel (input : String) : Bool :=
+  input = "Z"
+  ∨ input = "UTC"
+  ∨ input = "GMT"
+  ∨ input = "+00"
+  ∨ input = "+0000"
+  ∨ input = "+00:00"
+  ∨ input = "GMT+0"
+  ∨ input = "GMT+00:00"
+
+private def normalizeZoneName (input : String) (full : Bool) : String :=
+  if isUTCLabel input then
+    if full then "Coordinated Universal Time" else "UTC"
+  else
+    input
+
 set_option linter.missingDocs false in  -- TODO
 @[expose /- for codegen -/]
 def TypeFormat : Modifier → Type
   | .G _ => Year.Era
   | .y _ => Year.Offset
+  | .Y _ => Year.Offset
   | .u _ => Year.Offset
   | .D _ => Sigma Day.Ordinal.OfYear
   | .MorL _ => Month.Ordinal
@@ -794,8 +923,9 @@ def TypeFormat : Modifier → Type
   | .A _ => Millisecond.Offset
   | .n _ => Nanosecond.Ordinal
   | .N _ => Nanosecond.Offset
-  | .V => String
+  | .V _ => String
   | .z _ => String
+  | .v _ => String
   | .O _ => Offset
   | .X _ => Offset
   | .x _ => Offset
@@ -808,6 +938,7 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .short => formatEraShort data
     | .full => formatEraLong data
     | .narrow => formatEraNarrow data
+    | .twoLetterShort => formatEraShort data
   | .y format =>
     let info := data.toInt
     let info := if info ≤ 0 then -info + 1 else info
@@ -816,6 +947,14 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .twoDigit => pad 2 (info % 100)
     | .fourDigit => pad 4 info
     | .extended n => pad n info
+  | .Y format =>
+    let info := data.toInt
+    let info := if info ≤ 0 then -info + 1 else info
+    match format with
+    | .any => pad 0 (data.toInt)
+    | .twoDigit => pad 2 (info % 100)
+    | .fourDigit => pad 4 info
+    | .extended n => pad n info
   | .u format =>
     match format with
     | .any => pad 0 (data.toInt)
@@ -830,6 +969,7 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .inr .short => formatMonthShort data
     | .inr .full => formatMonthLong data
     | .inr .narrow => formatMonthNarrow data
+    | .inr .twoLetterShort => formatMonthShort data
   | .d format =>
     pad format.padding data.val
   | .Qorq format =>
@@ -838,6 +978,7 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .inr .short => formatQuarterShort data
     | .inr .full => formatQuarterLong data
     | .inr .narrow => formatQuarterNumber data
+    | .inr .twoLetterShort => formatQuarterShort data
   | .w format =>
     pad format.padding data.val
   | .W format =>
@@ -847,12 +988,30 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .short => formatWeekdayShort data
     | .full => formatWeekdayLong data
     | .narrow => formatWeekdayNarrow data
+    | .twoLetterShort =>
+      match data with
+      | .sunday => "Su"
+      | .monday => "Mo"
+      | .tuesday => "Tu"
+      | .wednesday => "We"
+      | .thursday => "Th"
+      | .friday => "Fr"
+      | .saturday => "Sa"
   | .eorc format =>
     match format with
     | .inl format => pad format.padding data.toOrdinal.val
     | .inr .short => formatWeekdayShort data
     | .inr .full => formatWeekdayLong data
     | .inr .narrow => formatWeekdayNarrow data
+    | .inr .twoLetterShort =>
+      match data with
+      | .sunday => "Su"
+      | .monday => "Mo"
+      | .tuesday => "Tu"
+      | .wednesday => "We"
+      | .thursday => "Th"
+      | .friday => "Fr"
+      | .saturday => "Sa"
   | .F format =>
     pad format.padding data.val
   | .a format =>
@@ -860,7 +1019,8 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .short => formatMarkerShort data
     | .full => formatMarkerLong data
     | .narrow => formatMarkerNarrow data
-  | .h format => pad format.padding (data.val % 12)
+    | .twoLetterShort => formatMarkerShort data
+  | .h format => pad format.padding data.val
   | .K format => pad format.padding (data.val % 12)
   | .k format => pad format.padding data.val
   | .H format => pad format.padding data.val
@@ -876,21 +1036,25 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     pad format.padding data.val
   | .N format =>
     pad format.padding data.val
-  | .V => data
+  | .V _ => data
   | .z format =>
     match format with
-    | .short => data
-    | .full => data
+    | .short => normalizeZoneName data false
+    | .full => normalizeZoneName data true
+  | .v format =>
+    match format with
+    | .short => normalizeZoneName data false
+    | .full => normalizeZoneName data true
   | .O format =>
     match format with
-    | .short => s!"GMT{toSigned data.second.toHours.toInt}"
-    | .full => s!"GMT{toIsoString data true false true}"
+    | .short => toLocalizedGMT data false
+    | .full => toLocalizedGMT data true
   | .X format =>
     if data.second == 0 then
       "Z"
     else
       match format with
-        | .hour => toIsoString data false false false
+        | .hour => toIsoString data (data.second.val % 3600 ≠ 0) false false
         | .hourMinute => toIsoString data true false false
         | .hourMinuteColon => toIsoString data true false true
         | .hourMinuteSecond => toIsoString data true true false
@@ -898,11 +1062,11 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
   | .x format =>
     match format with
     | .hour =>
-      toIsoString data (data.second.toMinutes.val % 60 ≠ 0) false false
+      toIsoString data (data.second.val % 3600 ≠ 0) false false
     | .hourMinute =>
       toIsoString data true false false
     | .hourMinuteColon =>
-      toIsoString data true (data.second.val % 60 ≠ 0) true
+      toIsoString data true false true
     | .hourMinuteSecond =>
       toIsoString data true (data.second.val % 60 ≠ 0) false
     | .hourMinuteSecondColon =>
@@ -910,27 +1074,26 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
   | .Z format =>
     match format with
     | .hourMinute =>
-      toIsoString data true false false
+      toIsoString data true true false
     | .full =>
-      if data.second.val = 0
-        then "GMT"
-        else s!"GMT{toIsoString data true false true}"
+      toLocalizedGMT data true
     | .hourMinuteSecondColon =>
       if data.second == 0
         then "Z"
-        else  toIsoString data true (data.second.val % 60 ≠ 0) true
+        else toIsoString data true true true
 
 private def dateFromModifier (date : DateTime tz) : TypeFormat modifier :=
   match modifier with
   | .G _ => date.era
   | .y _ => date.year
+  | .Y _ => weekBasedYear date
   | .u _ => date.year
   | .D _ => Sigma.mk _ date.dayOfYear
   | .MorL _ => date.month
   | .d _ => date.day
   | .Qorq _ => date.quarter
   | .w _ => date.weekOfYear
-  | .W _ => date.alignedWeekOfMonth
+  | .W _ => date.weekOfMonth.expandTop (by decide)
   | .E _ =>  date.weekday
   | .eorc _ => date.weekday
   | .F _ => date.weekOfMonth
@@ -945,9 +1108,11 @@ private def dateFromModifier (date : DateTime tz) : TypeFormat modifier :=
   | .A _ => date.date.get.time.toMilliseconds
   | .n _ => date.nanosecond
   | .N _ => date.date.get.time.toNanoseconds
-  | .V => tz.name
+  | .V _ => tz.name
   | .z .short => tz.abbreviation
   | .z .full => tz.name
+  | .v .short => tz.abbreviation
+  | .v .full => tz.name
   | .O _ => tz.offset
   | .X _ => tz.offset
   | .x _ => tz.offset
@@ -1025,6 +1190,15 @@ private def parseWeekdayNarrow : Parser Weekday
   <|> pstring "F" *> pure Weekday.friday
   <|> pstring "S" *> pure Weekday.saturday
 
+private def parseWeekdaytwoLetterShort : Parser Weekday
+   := pstring "Su" *> pure Weekday.sunday
+  <|> pstring "Mo" *> pure Weekday.monday
+  <|> pstring "Tu" *> pure Weekday.tuesday
+  <|> pstring "We" *> pure Weekday.wednesday
+  <|> pstring "Th" *> pure Weekday.thursday
+  <|> pstring "Fr" *> pure Weekday.friday
+  <|> pstring "Sa" *> pure Weekday.saturday
+
 private def parseEraShort : Parser Year.Era
    := pstring "BCE" *> pure Year.Era.bce
   <|> pstring "CE" *> pure Year.Era.ce
@@ -1065,7 +1239,9 @@ private def parseMarkerLong : Parser HourMarker
 
 private def parseMarkerNarrow : Parser HourMarker
    := pstring "A" *> pure HourMarker.am
+  <|> pstring "a" *> pure HourMarker.am
   <|> pstring "P" *> pure HourMarker.pm
+  <|> pstring "p" *> pure HourMarker.pm
 
 private def exactly (parse : Parser α) (size : Nat) : Parser (Array α) :=
   let rec go (acc : Array α) (count : Nat) : Parser (Array α) :=
@@ -1097,6 +1273,11 @@ private def parseSigned (parser : Parser Nat) : Parser Int := do
 private def parseNum (size : Nat) : Parser Nat :=
   String.toNat! <$> exactlyChars (satisfy Char.isDigit) size
 
+private def parseNum1or2 : Parser Nat := do
+  let first ← exactlyChars (satisfy Char.isDigit) 1
+  let second ← optional (exactlyChars (satisfy Char.isDigit) 1)
+  pure <| String.toNat! (first ++ second.getD "")
+
 private def parseAtLeastNum (size : Nat) : Parser Nat :=
   String.toNat! <$> do
     let start ← exactlyChars (satisfy Char.isDigit) size
@@ -1124,9 +1305,17 @@ private inductive Reason
   | no
   | optional
 
-private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon : Bool) : Parser Offset := do
+private inductive HourDigits
+  | two
+  | oneOrTwo
+
+private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon : Bool) (hourDigits := HourDigits.two) : Parser Offset := do
   let sign ← (pchar '+' *> pure 1) <|> (pchar '-' *> pure (-1))
-  let hours : Hour.Offset ← UnitVal.ofInt <$> parseNum 2
+  let hourParser : Parser Nat :=
+    match hourDigits with
+    | .two => parseNum 2
+    | .oneOrTwo => parseNum1or2
+  let hours : Hour.Offset ← UnitVal.ofInt <$> hourParser
 
   if hours.val < 0 ∨ hours.val > 23 then
     fail s!"invalid hour offset: {hours.val}. Must be between 0 and 23."
@@ -1155,18 +1344,34 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon
 
   return Offset.ofSeconds ⟨hours.val * sign⟩
 
+private def parseLocalizedGMT (full : Bool) : Parser Offset := do
+  skipString "GMT"
+  let parseOff :=
+    match full with
+    | true => parseOffset .yes .optional true
+    | false => parseOffset .optional .optional true (hourDigits := .oneOrTwo)
+  let res ← optional parseOff
+  pure (res.getD Offset.zero)
+
 private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (TypeFormat mod)
   | .G format =>
     match format with
     | .short => parseEraShort
     | .full => parseEraLong
     | .narrow => parseEraNarrow
+    | .twoLetterShort => parseEraShort
   | .y format =>
     match format with
     | .any => Int.ofNat <$> parseAtLeastNum 1
     | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2
     | .fourDigit => Int.ofNat <$> parseNum 4
     | .extended n => Int.ofNat <$> parseNum n
+  | .Y format =>
+    match format with
+    | .any => Int.ofNat <$> parseAtLeastNum 1
+    | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2
+    | .fourDigit => Int.ofNat <$> parseNum 4
+    | .extended n => Int.ofNat <$> parseNum n
   | .u format =>
     match format with
     | .any => parseSigned <| parseAtLeastNum 1
@@ -1180,6 +1385,7 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
     | .inr .short => parseMonthShort
     | .inr .full => parseMonthLong
     | .inr .narrow => parseMonthNarrow
+    | .inr .twoLetterShort => parseMonthShort
   | .d format => parseNatToBounded (parseFlexibleNum format.padding)
   | .Qorq format =>
     match format with
@@ -1187,6 +1393,7 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
     | .inr .short => parseQuarterShort
     | .inr .full => parseQuarterLong
     | .inr .narrow => parseQuarterNumber
+    | .inr .twoLetterShort => parseQuarterShort
   | .w format => parseNatToBounded (parseFlexibleNum format.padding)
   | .W format => parseNatToBounded (parseFlexibleNum format.padding)
   | .E format =>
@@ -1194,18 +1401,21 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
     | .short => parseWeekdayShort
     | .full => parseWeekdayLong
     | .narrow => parseWeekdayNarrow
+    | .twoLetterShort => parseWeekdaytwoLetterShort
   | .eorc format =>
     match format with
     | .inl format => Weekday.ofOrdinal <$> parseNatToBounded (parseFlexibleNum format.padding)
     | .inr .short => parseWeekdayShort
     | .inr .full => parseWeekdayLong
     | .inr .narrow => parseWeekdayNarrow
+    | .inr .twoLetterShort => parseWeekdaytwoLetterShort
   | .F format => parseNatToBounded (parseFlexibleNum format.padding)
   | .a format =>
     match format with
     | .short => parseMarkerShort
     | .full => parseMarkerLong
     | .narrow => parseMarkerNarrow
+    | .twoLetterShort => parseMarkerShort
   | .h format => parseNatToBounded (parseFlexibleNum format.padding)
   | .K format => parseNatToBounded (parseFlexibleNum format.padding)
   | .k format => parseNatToBounded (parseFlexibleNum format.padding)
@@ -1224,23 +1434,27 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
   | .A format => Millisecond.Offset.ofNat <$> (parseFlexibleNum format.padding)
   | .n format => parseNatToBounded (parseFlexibleNum format.padding)
   | .N format => Nanosecond.Offset.ofNat <$> (parseFlexibleNum format.padding)
-  | .V => parseIdentifier
+  | .V _ => parseIdentifier
   | .z format =>
     match format with
     | .short => parseIdentifier
     | .full => parseIdentifier
+  | .v format =>
+    match format with
+    | .short => parseIdentifier
+    | .full => parseIdentifier
   | .O format =>
     match format with
-    | .short => pstring "GMT" *> parseOffset .no .no false
-    | .full => pstring "GMT" *> parseOffset .yes .optional false
+    | .short => parseLocalizedGMT false
+    | .full => parseLocalizedGMT true
   | .X format =>
     let p : Parser Offset :=
       match format with
-        | .hour => parseOffset .no .no false
+        | .hour => parseOffset .optional .no false
         | .hourMinute => parseOffset .yes .no false
         | .hourMinuteColon => parseOffset .yes .no true
-        | .hourMinuteSecond => parseOffset .yes .yes false
-        | .hourMinuteSecondColon => parseOffset .yes .yes true
+        | .hourMinuteSecond => parseOffset .yes .optional false
+        | .hourMinuteSecondColon => parseOffset .yes .optional true
     p <|> (pstring "Z" *> pure (Offset.ofSeconds 0))
   | .x format =>
     match format with
@@ -1249,19 +1463,17 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
     | .hourMinute =>
       parseOffset .yes .no false
     | .hourMinuteColon =>
-      parseOffset .yes .optional true
+      parseOffset .yes .no true
     | .hourMinuteSecond =>
       parseOffset .yes .optional false
     | .hourMinuteSecondColon =>
-      parseOffset .yes .yes true
+      parseOffset .yes .optional true
   | .Z format =>
     match format with
     | .hourMinute =>
-      parseOffset .yes .no false
-    | .full => do
-      skipString "GMT"
-      let res ← optional (parseOffset .yes .no true)
-      return res.getD Offset.zero
+      parseOffset .yes .optional false
+    | .full =>
+      parseLocalizedGMT true
     | .hourMinuteSecondColon =>
       (skipString "Z" *> pure Offset.zero)
       <|> (parseOffset .yes .optional true)
@@ -1278,11 +1490,12 @@ def FormatType (result : Type) : FormatString → Type
   | .string _ :: xs => (FormatType result xs)
   | [] => result
 
-namespace GenericFormat
+namespace Format
 
 private structure DateBuilder where
   G : Option Year.Era := none
   y : Option Year.Offset := none
+  Y : Option Year.Offset := none
   u : Option Year.Offset := none
   D : Option (Sigma Day.Ordinal.OfYear) := none
   MorL : Option Month.Ordinal := none
@@ -1307,6 +1520,8 @@ private structure DateBuilder where
   V : Option String := none
   z : Option String := none
   zabbrev : Option String := none
+  v : Option String := none
+  vabbrev : Option String := none
   O : Option Offset := none
   X : Option Offset := none
   x : Option Offset := none
@@ -1318,6 +1533,7 @@ private def insert (date : DateBuilder) (modifier : Modifier) (data : TypeFormat
   match modifier with
   | .G _ => { date with G := some data }
   | .y _ => { date with y := some data }
+  | .Y _ => { date with Y := some data }
   | .u _ => { date with u := some data }
   | .D _ => { date with D := some data }
   | .MorL _ => { date with MorL := some data }
@@ -1339,9 +1555,11 @@ private def insert (date : DateBuilder) (modifier : Modifier) (data : TypeFormat
   | .A _ => { date with A := some data }
   | .n _ => { date with n := some data }
   | .N _ => { date with N := some data }
-  | .V => { date with V := some data }
+  | .V _ => { date with V := some data }
   | .z .full => { date with z := some data }
   | .z .short => { date with zabbrev := some data }
+  | .v .full => { date with v := some data }
+  | .v .short => { date with vabbrev := some data }
   | .O _ => { date with O := some data }
   | .X _ => { date with X := some data }
   | .x _ => { date with x := some data }
@@ -1356,8 +1574,8 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
 
   let tz : TimeZone := {
     offset,
-    name := builder.V <|> builder.z |>.getD (offset.toIsoString true),
-    abbreviation := builder.zabbrev |>.getD (offset.toIsoString true),
+    name := builder.V <|> builder.z <|> builder.v |>.getD (offset.toIsoString true),
+    abbreviation := builder.zabbrev <|> builder.vabbrev |>.getD (offset.toIsoString true),
     isDST := false,
   }
 
@@ -1367,6 +1585,7 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
 
   let year
     := builder.u
+    <|> builder.Y
     <|> ((convertYearAndEra · era) <$> builder.y)
     |>.getD 0
 
@@ -1414,25 +1633,48 @@ private def parseWithDate (date : DateBuilder) (config : FormatConfig) (mod : Fo
   | .string s => pstring s *> pure date
 
 /--
-Constructs a new `GenericFormat` specification for a date-time string. Modifiers can be combined to create
+Constructs a new `Format` specification for a date-time string. Modifiers can be combined to create
 custom formats, such as "YYYY, MMMM, D".
 -/
-def spec (input : String) (config : FormatConfig := {}) : Except String (GenericFormat tz) := do
+def spec (input : String) (config : FormatConfig := {}) : Except String (Format tz) := do
   let string ← specParser.run input
   return ⟨config, string⟩
 
 /--
-Builds a `GenericFormat` from the input string. If parsing fails, it will panic
+Builds a `Format` from the input string. If parsing fails, it will panic
 -/
-def spec! (input : String) (config : FormatConfig := {}) : GenericFormat tz :=
+def spec! (input : String) (config : FormatConfig := {}) : Format tz :=
   match specParser.run input with
   | .ok res => ⟨config, res⟩
   | .error res => panic! res
 
 /--
-Formats a `DateTime` value into a string using the given `GenericFormat`.
+Type class for types that can be formatted as a `DateTime`.
 -/
-def format (format : GenericFormat aw) (date : DateTime tz) : String :=
+class FormattableTime (α : Type) where
+
+  /--
+  Converts a type `α` to a `DateTime` and a `TimeZone`.
+  -/
+  toDateTime : α → Σ tz, DateTime tz
+
+instance : FormattableTime (DateTime tz) where
+  toDateTime dt := ⟨tz, dt⟩
+
+instance : FormattableTime ZonedDateTime where
+  toDateTime dt := ⟨dt.timezone, dt.toDateTime⟩
+
+instance : FormattableTime (Awareness.any.type) where
+  toDateTime dt := ⟨dt.timezone, dt.toDateTime⟩
+
+instance : FormattableTime (Awareness.only tz |>.type) where
+  toDateTime dt := ⟨tz, by simp at dt; exact dt⟩
+/--
+Formats a `DateTime` value into a string using the given `Format`.
+-/
+def format [FormattableTime t] (format : Format aw) (date : t) : String :=
+  let ⟨_, date⟩ := FormattableTime.toDateTime date
+
   let mapper (part : FormatPart) :=
     match aw with
     | .any => formatPartWithDate date part
@@ -1468,15 +1710,46 @@ def builderParser (format: FormatString) (config : FormatConfig) (func: FormatTy
   go format func
 
 /--
-Parses the input string into a `ZoneDateTime`.
+Returns `true` if this format contains a timezone-offset specifier (`O`, `X`, `x`, or `Z`).
 -/
-def parse (format : GenericFormat aw) (input : String) : Except String aw.type :=
+def hasOffsetSpecifier (format : Format aw) : Bool :=
+  format.string.any fun
+    | .modifier (.O _) | .modifier (.X _) | .modifier (.x _) | .modifier (.Z _) => true
+    | _ => false
+
+/--
+Returns `true` if this format contains a timezone-identifier specifier (`V` or `z`).
+-/
+def hasIdentifierSpecifier (format : Format aw) : Bool :=
+  format.string.any fun
+    | .modifier (.V _) | .modifier (.z _) | .modifier (.v _) => true
+    | _ => false
+
+/--
+Parses the input string without checking for identifier-without-offset.
+Use this only when you will subsequently resolve the identifier via a timezone database lookup.
+For normal parsing, prefer `parse`.
+-/
+def parseUnchecked (format : Format aw) (input : String) : Except String aw.type :=
   (parser format.string format.config aw <* eof).run input
 
+/--
+Parses the input string into a `ZonedDateTime`.
+Fails if the format contains a timezone identifier specifier (`z`/`V`) but no offset specifier
+(`Z`/`X`/`x`/`O`): such formats cannot produce a correct UTC offset without a timezone database
+lookup. Use `parseIO` (on `Format`) or `ZonedDateTime.parseIO` for that case.
+-/
+def parse (format : Format aw) (input : String) : Except String aw.type :=
+  if format.hasIdentifierSpecifier && !format.hasOffsetSpecifier then
+    .error "this format uses a timezone identifier without an offset specifier; \
+            the correct UTC offset requires a timezone database lookup — use parseIO instead"
+  else
+    (parser format.string format.config aw <* eof).run input
+
 /--
 Parses the input string into a `ZoneDateTime` and panics if its wrong.
 -/
-def parse! (format : GenericFormat aw) (input : String) : aw.type :=
+def parse! (format : Format aw) (input : String) : aw.type :=
   match parse format input with
   | .ok res => res
   | .error err => panic! err
@@ -1484,13 +1757,13 @@ def parse! (format : GenericFormat aw) (input : String) : aw.type :=
 /--
 Parses an input string using a builder function to produce a value.
 -/
-def parseBuilder (format : GenericFormat aw)  (builder : FormatType (Option α) format.string) (input : String) : Except String α :=
+def parseBuilder (format : Format aw)  (builder : FormatType (Option α) format.string) (input : String) : Except String α :=
   (builderParser format.string format.config builder).run input
 
 /--
 Parses an input string using a builder function, panicking on errors.
 -/
-def parseBuilder! [Inhabited α] (format : GenericFormat aw)  (builder : FormatType (Option α) format.string) (input : String) : α :=
+def parseBuilder! [Inhabited α] (format : Format aw)  (builder : FormatType (Option α) format.string) (input : String) : α :=
   match parseBuilder format builder input with
   | .ok res => res
   | .error err => panic! err
@@ -1498,7 +1771,7 @@ def parseBuilder! [Inhabited α] (format : GenericFormat aw)  (builder : FormatT
 /--
 Formats the date using the format into a String, using a `getInfo` function to get the information needed to build the `String`.
 -/
-def formatGeneric (format : GenericFormat aw) (getInfo : (typ : Modifier) → Option (TypeFormat typ)) : Option String :=
+def formatGeneric (format : Format aw) (getInfo : (typ : Modifier) → Option (TypeFormat typ)) : Option String :=
   let rec go (data : String) : (format : FormatString) → Option String
     | .modifier x :: xs => do go (data ++ formatWith x (← getInfo x)) xs
     | .string x :: xs => go (data ++ x) xs
@@ -1506,33 +1779,56 @@ def formatGeneric (format : GenericFormat aw) (getInfo : (typ : Modifier) → Op
   go "" format.string
 
 /--
-Constructs a `FormatType` function to format a date into a string using a `GenericFormat`.
+Constructs a `FormatType` function to format a date into a string using a `Format`.
 -/
-def formatBuilder (format : GenericFormat aw) : FormatType String format.string :=
+def formatBuilder (format : Format aw) : FormatType String format.string :=
   let rec go (data : String) : (format : FormatString) → FormatType String format
     | .modifier x :: xs => fun res => go (data ++ formatWith x res) xs
     | .string x :: xs => go (data ++ x) xs
     | [] => data
   go "" format.string
 
-end GenericFormat
+end Format
 
 /--
-Typeclass for formatting and parsing values with the given format type.
+A `MultiFormat` holds a list of `Format` alternatives tried in order when parsing.
+Use it when a value can be represented in several equivalent formats.
 -/
-class Format (f : Type) (typ : Type → f → Type) where
-  /--
-  Converts a format `f` into a string.
-  -/
-  format : (fmt : f) → typ String fmt
+structure MultiFormat (awareness : Awareness) where
+  /-- The list of format alternatives, tried left-to-right. -/
+  formats : { x : Array (Format awareness) // x.size > 0 }
+  deriving Repr
 
-  /--
-  Parses a string into a format using the provided format type `f`.
-  -/
-  parse : (fmt : f) → typ (Option α) fmt → String → Except String α
+instance : Inhabited (MultiFormat aw) where
+  default := ⟨⟨#[default], by simp⟩⟩
 
-instance : Format (GenericFormat aw) (FormatType · ·.string) where
-  format := GenericFormat.formatBuilder
-  parse := GenericFormat.parseBuilder
+namespace MultiFormat
 
-end Time
+/--
+?
+-/
+def new (formats : Array (Format aw)) (proof : formats.size > 0 := by simp) : MultiFormat aw :=
+  ⟨⟨formats, proof⟩⟩
+
+/--
+Parses the input string by trying each format in order, returning the first success.
+-/
+def parse (mf : MultiFormat aw) (input : String) : Except String aw.type :=
+  mf.formats.val.foldl (init := .error s!"no format matched input: {input}")
+    fun acc fmt => acc <|> fmt.parse input
+
+/--
+Parses the input string without timezone awareness checks, trying each format in order.
+-/
+def parseUnchecked (mf : MultiFormat aw) (input : String) : Except String aw.type :=
+  mf.formats.val.foldl (init := .error s!"no format matched input: {input}")
+    fun acc fmt => acc <|> fmt.parseUnchecked input
+
+/--
+Formats a date using the first format in the list.
+-/
+def format (mf : MultiFormat aw) (date : DateTime tz) : String :=
+  let fmt := mf.formats.val[0]'(mf.formats.property)
+  fmt.format date
+
+end Std.Time.MultiFormat

src/Std/Time/Internal/Bounded.lean

@@ -13,9 +13,7 @@ import Init.Ext
 
 @[expose] public section
 
-namespace Std
-namespace Time
-namespace Internal
+namespace Std.Time.Internal
 
 set_option linter.all true in
 
@@ -488,8 +486,4 @@ def max (bounded : Bounded.LE n m) (val : Int) : Bounded.LE (Max.max n val) (Max
     contradiction
   next h h₁ => exact right
 
-end LE
-end Bounded
-end Internal
-end Time
-end Std
+end Std.Time.Internal.Bounded.LE

src/Std/Time/Internal/UnitVal.lean

@@ -11,9 +11,7 @@ public import Init.Data.Rat.Basic
 
 @[expose] public section
 
-namespace Std
-namespace Time
-namespace Internal
+namespace Std.Time.Internal
 open Lean
 
 set_option linter.all true
@@ -150,7 +148,4 @@ instance : ToString (UnitVal n) where toString n := toString n.val
 def cast (_ : a = b) (x : UnitVal a) : UnitVal b :=
   .ofInt (x.val)
 
-end UnitVal
-end Internal
-end Time
-end Std
+end Std.Time.Internal.UnitVal

src/Std/Time/Notation.lean

@@ -11,8 +11,7 @@ public meta import Std.Time.Format
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Lean Parser Command Std
 
 set_option linter.all true
@@ -21,6 +20,7 @@ private meta def convertText : Text → MacroM (TSyntax `term)
   | .short  => `(Std.Time.Text.short)
   | .full   => `(Std.Time.Text.full)
   | .narrow => `(Std.Time.Text.narrow)
+  | .twoLetterShort => `(Std.Time.Text.twoLetterShort)
 
 private meta def convertNumber : Number → MacroM (TSyntax `term)
   | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding))
@@ -58,6 +58,7 @@ private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term)
 private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
+  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
   | .MorL p =>
@@ -88,8 +89,9 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .A p => do `(Std.Time.Modifier.A $(← convertNumber p))
   | .n p => do `(Std.Time.Modifier.n $(← convertNumber p))
   | .N p => do `(Std.Time.Modifier.N $(← convertNumber p))
-  | .V => `(Std.Time.Modifier.V)
+  | .V p => do `(Std.Time.Modifier.V $(← convertNumber p))
   | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p))
+  | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p))
   | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p))
   | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p))
   | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p))
@@ -207,33 +209,40 @@ syntax "timezone(" str ")" : term
 
 macro_rules
   | `(zoned( $date:str )) => do
-      match ZonedDateTime.fromLeanDateTimeWithZoneString date.getString with
+      let s := date.getString
+      match (Formats.leanDateTimeWithZoneAlt.parse s : Except String ZonedDateTime) with
       | .ok res => do return ← convertZonedDateTime res
       | .error _ =>
-        match ZonedDateTime.fromLeanDateTimeWithIdentifierString date.getString with
-        | .ok res => do return ← convertZonedDateTime res (identifier := true)
-        | .error res => Macro.throwErrorAt date s!"error: {res}"
+        match (Formats.leanDateTimeWithZoneAndNameAlt.parse s : Except String ZonedDateTime) with
+        | .ok res => do return ← convertZonedDateTime res
+        | .error _ =>
+          let identParse : Except String ZonedDateTime :=
+            Formats.leanDateTimeWithIdentifier.parseUnchecked s
+            <|> Formats.leanDateTimeWithIdentifierAndNanos.parseUnchecked s
+          match identParse with
+          | .ok res => do return ← convertZonedDateTime res (identifier := true)
+          | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(zoned( $date:str, $timezone )) => do
-      match PlainDateTime.fromLeanDateTimeString date.getString with
+      match (Formats.leanDateTime24HourAlt.parse date.getString).map DateTime.toPlainDateTime with
       | .ok res => do
         let plain ← convertPlainDateTime res
         `(Std.Time.ZonedDateTime.ofPlainDateTime $plain $timezone)
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(datetime( $date:str )) => do
-      match PlainDateTime.fromLeanDateTimeString date.getString with
+      match (Formats.leanDateTime24HourAlt.parse date.getString).map DateTime.toPlainDateTime with
       | .ok res => do
         return ← convertPlainDateTime res
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(date( $date:str )) => do
-      match PlainDate.fromSQLDateString date.getString with
+      match PlainDate.parse date.getString with
       | .ok res => return ← convertPlainDate res
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(time( $time:str )) => do
-      match PlainTime.fromLeanTime24Hour time.getString with
+      match PlainTime.parse time.getString with
       | .ok res => return ← convertPlainTime res
       | .error res => Macro.throwErrorAt time s!"error: {res}"
 
@@ -246,3 +255,5 @@ macro_rules
       match TimeZone.fromTimeZone tz.getString with
       | .ok res => return ← convertTimezone res
       | .error res => Macro.throwErrorAt tz s!"error: {res}"
+
+end Std.Time

src/Std/Time/Notation/Spec.lean

@@ -11,14 +11,14 @@ public meta import Std.Time.Format.Basic
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Lean Parser Command Std
 
 private meta def convertText : Text → MacroM (TSyntax `term)
   | .short => `(Std.Time.Text.short)
   | .full => `(Std.Time.Text.full)
   | .narrow => `(Std.Time.Text.narrow)
+  | .twoLetterShort => `(Std.Time.Text.twoLetterShort)
 
 private meta def convertNumber : Number → MacroM (TSyntax `term)
   | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding))
@@ -56,6 +56,7 @@ private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term)
 private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
+  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
   | .MorL p =>
@@ -86,8 +87,9 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .A p => do `(Std.Time.Modifier.A $(← convertNumber p))
   | .n p => do `(Std.Time.Modifier.n $(← convertNumber p))
   | .N p => do `(Std.Time.Modifier.N $(← convertNumber p))
-  | .V => `(Std.Time.Modifier.V)
+  | .V p => do `(Std.Time.Modifier.V $(← convertNumber p))
   | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p))
+  | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p))
   | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p))
   | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p))
   | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p))
@@ -109,7 +111,7 @@ syntax "datespec(" str "," term ")" : term
 
 private meta def formatStringToFormat (fmt : TSyntax `str) (config : Option (TSyntax `term)) : MacroM (TSyntax `term) := do
   let input := fmt.getString
-  let format : Except String (GenericFormat .any) := GenericFormat.spec input
+  let format : Except String (Format .any) := Format.spec input
   match format with
   | .ok res =>
     let alts ← res.string.mapM convertFormatPart
@@ -122,3 +124,5 @@ private meta def formatStringToFormat (fmt : TSyntax `str) (config : Option (TSy
 macro_rules
   | `(datespec( $fmt:str )) => formatStringToFormat fmt none
   | `(datespec( $fmt:str, $config:term )) => formatStringToFormat fmt (some config)
+
+end Std.Time

src/Std/Time/Time/HourMarker.lean

@@ -10,8 +10,7 @@ public import Std.Time.Time.Basic
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -86,6 +85,4 @@ def toRelative (hour : Hour.Ordinal) : Bounded.LE 1 12 × HourMarker :=
     let t := hour |>.truncateBottom h |>.sub 12
     (t.expandTop (by decide), .pm)
 
-end HourMarker
-end Time
-end Std
+end Std.Time.HourMarker

src/Std/Time/Time/PlainTime.lean

@@ -10,8 +10,7 @@ public import Std.Time.Time.Basic
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -316,6 +315,4 @@ instance : HAdd PlainTime Hour.Offset PlainTime where
 instance : HSub PlainTime Hour.Offset PlainTime where
   hSub := subHours
 
-end PlainTime
-end Time
-end Std
+end Std.Time.PlainTime

src/Std/Time/Time/Unit/Basic.lean

@@ -19,8 +19,7 @@ The units are organized into types representing these time-related concepts, wit
 to facilitate conversions and manipulations between them.
 -/
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -323,7 +322,4 @@ Converts a `Minute.Offset` to an `Hour.Offset`.
 def ofMinutes (offset : Minute.Offset) : Hour.Offset :=
   offset.toHours
 
-end Hour.Offset
-
-end Time
-end Std
+end Std.Time.Hour.Offset

src/Std/Time/Time/Unit/Hour.lean

@@ -10,9 +10,7 @@ public import Std.Time.Time.Unit.Minute
 
 public section
 
-namespace Std
-namespace Time
-namespace Hour
+namespace Std.Time.Hour
 open Internal
 
 set_option linter.all true
@@ -123,7 +121,4 @@ Creates an `Offset` from an integer.
 def ofInt (data : Int) : Offset :=
   UnitVal.ofInt data
 
-end Offset
-end Hour
-end Time
-end Std
+end Std.Time.Hour.Offset

src/Std/Time/Time/Unit/Millisecond.lean

@@ -10,9 +10,7 @@ public import Std.Time.Time.Unit.Nanosecond
 
 public section
 
-namespace Std
-namespace Time
-namespace Millisecond
+namespace Std.Time.Millisecond
 open Internal
 
 set_option linter.all true
@@ -109,7 +107,4 @@ Converts an `Ordinal` to an `Offset`.
 def toOffset (ordinal : Ordinal) : Offset :=
   UnitVal.ofInt ordinal.val
 
-end Ordinal
-end Millisecond
-end Time
-end Std
+end Std.Time.Millisecond.Ordinal

src/Std/Time/Time/Unit/Minute.lean

@@ -10,9 +10,7 @@ public import Std.Time.Time.Unit.Second
 
 public section
 
-namespace Std
-namespace Time
-namespace Minute
+namespace Std.Time.Minute
 open Internal
 
 set_option linter.all true
@@ -109,7 +107,4 @@ Creates an `Offset` from an integer.
 def ofInt (data : Int) : Offset :=
   UnitVal.ofInt data
 
-end Offset
-end Minute
-end Time
-end Std
+end Std.Time.Minute.Offset

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

@@ -10,9 +10,7 @@ public import Std.Time.Internal
 
 public section
 
-namespace Std
-namespace Time
-namespace Nanosecond
+namespace Std.Time.Nanosecond
 open Internal
 
 set_option linter.all true
@@ -161,7 +159,4 @@ Converts an `Ordinal` to an `Offset`.
 def toOffset (ordinal : Ordinal) : Offset :=
   UnitVal.ofInt ordinal.val
 
-end Ordinal
-end Nanosecond
-end Time
-end Std
+end Std.Time.Nanosecond.Ordinal

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

@@ -10,9 +10,7 @@ public import Std.Time.Time.Unit.Nanosecond
 
 @[expose] public section
 
-namespace Std
-namespace Time
-namespace Second
+namespace Std.Time.Second
 open Internal
 
 set_option linter.all true
@@ -126,7 +124,4 @@ Converts an `Ordinal` to an `Second.Offset`.
 def toOffset (ordinal : Ordinal leap) : Second.Offset :=
   UnitVal.ofInt ordinal.val
 
-end Ordinal
-end Second
-end Time
-end Std
+end Std.Time.Second.Ordinal

src/Std/Time/Zoned.lean

@@ -13,13 +13,10 @@ public import Std.Time.Zoned.Database
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time.PlainDateTime
 
 set_option linter.all true
 
-namespace PlainDateTime
-
 /--
 Get the current time, in the local timezone.
 To obtain the current time in a specific timezone, use `DateTime.now` or `ZonedDateTime.nowAt`.
@@ -44,6 +41,7 @@ def now : IO PlainDate :=
   PlainDateTime.date <$> PlainDateTime.now
 
 end PlainDate
+
 namespace PlainTime
 
 /--
@@ -87,6 +85,7 @@ def now : IO (DateTime tz) := do
   return DateTime.ofTimestamp tm tz
 
 end DateTime
+
 namespace ZonedDateTime
 
 /--
@@ -179,4 +178,4 @@ Converts a `PlainDate` to a `Timestamp` using the `TimeZone`.
 def toTimestampWithZone (dt : PlainDate) (tz : TimeZone) : Timestamp :=
   ZonedDateTime.ofPlainDateWithZone dt tz |>.toTimestamp
 
-end PlainDate
+end Std.Time.PlainDate

src/Std/Time/Zoned/Database.lean

@@ -14,9 +14,7 @@ import Init.System.Platform
 
 public section
 
-namespace Std
-namespace Time
-namespace Database
+namespace Std.Time.Database
 open TimeZone.ZoneRules
 
 set_option linter.all true
@@ -40,3 +38,5 @@ def defaultGetLocalZoneRules : IO TimeZone.ZoneRules :=
   if System.Platform.isWindows
     then getLocalZoneRules WindowsDb.default
     else getLocalZoneRules TZdb.default
+
+end Std.Time.Database

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

@@ -11,8 +11,7 @@ public import Std.Time.Zoned.Database.TzIf
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 
 set_option linter.all true
 
@@ -116,3 +115,5 @@ def convertTZif (tz : TZif.TZif) (id : String) : Except String ZoneRules := do
   if let some v2 := tz.v2
     then convertTZifV2 v2 id
     else convertTZifV1 tz.v1 id
+
+end Std.Time.TimeZone

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

@@ -11,9 +11,7 @@ import Init.Data.String.TakeDrop
 
 public section
 
-namespace Std
-namespace Time
-namespace Database
+namespace Std.Time.Database
 
 set_option linter.all true
 
@@ -100,3 +98,5 @@ instance : Std.Time.Database TZdb where
         return result
 
     throw <| IO.userError s!"cannot find {id} in the local timezone database"
+
+end Std.Time.Database.TZdb

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

@@ -13,10 +13,7 @@ public section
 
 -- Based on: https://www.rfc-editor.org/rfc/rfc8536.html
 
-namespace Std
-namespace Time
-namespace TimeZone
-namespace TZif
+namespace Std.Time.TimeZone.TZif
 open Std.Internal.Parsec Std.Internal.Parsec.ByteArray
 
 set_option linter.all true
@@ -328,4 +325,4 @@ def parse : Parser TZif := do
   let v2 ← parseTZifV2
   return { v1, v2 }
 
-end TZif
+end Std.Time.TimeZone.TZif

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

@@ -12,9 +12,7 @@ import Init.While
 
 public section
 
-namespace Std
-namespace Time
-namespace Database
+namespace Std.Time.Database
 
 set_option linter.all true
 
@@ -90,3 +88,5 @@ def default : WindowsDb := {}
 instance : Std.Time.Database WindowsDb where
   getZoneRules _ id := Windows.getZoneRules id
   getLocalZoneRules _ := Windows.getZoneRules =<< Windows.getLocalTimeZoneIdentifierAt (-2147483648)
+
+end Std.Time.Database.WindowsDb

src/Std/Time/Zoned/DateTime.lean

@@ -14,8 +14,7 @@ import all Std.Time.DateTime.PlainDateTime
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 open Internal
 
 set_option linter.all true
@@ -410,9 +409,17 @@ def weekday (dt : DateTime tz) : Weekday :=
 /--
 Determines the era of the given `DateTime` based on its year.
 -/
+@[inline]
 def era (date : DateTime tz) : Year.Era :=
   date.year.era
 
+/--
+Returns the week-based year for a given `DateTime`.
+-/
+@[inline]
+def weekBasedYear (date : DateTime tz) : Year.Offset :=
+  date.date.get.weekBasedYear
+
 /--
 Sets the `DateTime` to the specified `desiredWeekday`.
 -/
@@ -525,6 +532,4 @@ instance : HAdd (DateTime tz) Duration (DateTime tz) where
 instance : HSub (DateTime tz) Duration (DateTime tz) where
   hSub x y := x.subNanoseconds y.toNanoseconds
 
-end DateTime
-end Time
-end Std
+end Std.Time.DateTime

src/Std/Time/Zoned/Offset.lean

@@ -10,9 +10,7 @@ public import Std.Time.Time
 
 public section
 
-namespace Std
-namespace Time
-namespace TimeZone
+namespace Std.Time.TimeZone
 open Internal
 
 set_option linter.all true
@@ -84,7 +82,4 @@ Creates an `Offset` from a given number of hours and minutes.
 def ofHoursAndMinutes (n : Hour.Offset) (m : Minute.Offset) : Offset :=
   ofSeconds (n.toSeconds + m.toSeconds)
 
-end Offset
-end TimeZone
-end Time
-end Std
+end Std.Time.TimeZone.Offset

src/Std/Time/Zoned/TimeZone.lean

@@ -10,8 +10,7 @@ public import Std.Time.Zoned.Offset
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 
 set_option linter.all true
 
@@ -73,3 +72,5 @@ Gets the number of seconds in a timezone offset.
 -/
 def toSeconds (tz : TimeZone) : Second.Offset :=
   tz.offset.second
+
+end Std.Time.TimeZone

src/Std/Time/Zoned/ZoneRules.lean

@@ -11,9 +11,7 @@ public import Std.Time.Zoned.TimeZone
 
 public section
 
-namespace Std
-namespace Time
-namespace TimeZone
+namespace Std.Time.TimeZone
 open Internal
 
 set_option linter.all true
@@ -224,4 +222,4 @@ def ofTimeZone (tz : TimeZone) : ZoneRules :=
   let ltt :=  LocalTimeType.mk tz.offset tz.isDST tz.abbreviation .wall .local tz.name
   ZoneRules.mk ltt #[]
 
-end ZoneRules
+end Std.Time.TimeZone.ZoneRules

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -12,11 +12,9 @@ import all Std.Time.DateTime.PlainDateTime
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 
--- TODO (@kim-em): re-enable this once there is a mechanism to exclude `linter.indexVariables`.
--- set_option linter.all true
+set_option linter.all true
 
 /--
 Represents a date and time with timezone information.
@@ -153,6 +151,13 @@ Getter for the `Year` inside of a `ZonedDateTime`
 def year (zdt : ZonedDateTime) : Year.Offset :=
   zdt.date.get.year
 
+/--
+Returns the week-based year for a given `ZonedDateTime`.
+-/
+@[inline]
+def weekBasedYear (zdt : ZonedDateTime) : Year.Offset :=
+  zdt.date.get.weekBasedYear
+
 /--
 Getter for the `Month` inside of a `ZonedDateTime`
 -/
@@ -588,6 +593,4 @@ instance : HAdd ZonedDateTime Duration ZonedDateTime where
 instance : HSub ZonedDateTime Duration ZonedDateTime where
   hSub x y := x.subNanoseconds y.toNanoseconds
 
-end ZonedDateTime
-end Time
-end Std
+end Std.Time.ZonedDateTime

tests/elab/dateTimeOrd.lean

@@ -45,4 +45,4 @@ example : Std.LawfulBEqOrd (DateTime TimeZone.GMT) := inferInstance
    "Sat Jan 01 02:01:01 2025",
    "Sat Jan 02 01:01:01 2025",
    "Sat Feb 01 01:01:01 2025",
-   "Sat Jan 01 01:01:01 2026"].map (DateTime.fromAscTimeString . |>.toOption.get!)
+   "Sat Jan 01 01:01:01 2026"].map (DateTime.parse · |>.toOption.get!)

tests/elab/timeAPI.lean

@@ -629,9 +629,9 @@ Std.Time.Weekday.friday
   println! repr date.weekOfYear
   println! repr date.weekOfMonth
 
-  println! date.toAmericanDateString
-  println! date.toLeanDateString
-  println! date.toSQLDateString
+  println! (date.format "MM-dd-uuuu")
+  println! (date.format "uuuu-MM-dd")
+  println! (date.format "uuuu-MM-dd")
 
   println! date.toDaysSinceUNIXEpoch
   println! date.toTimestampAssumingUTC

tests/elab/timeCanonFormats.lean

@@ -8,7 +8,7 @@ def date₁ := zoned("2014-06-16T03:03:03-03:00")
 info: "Monday, June 16, 2014 06:03:03"
 -/
 #guard_msgs in
-#eval Formats.longDateFormat.format date₁.toDateTime
+#eval Formats.longDateFormat.format date₁
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ

tests/elab/timeFieldSymbols.lean

@@ -0,0 +1,428 @@
+import Std.Time
+open Std.Time
+
+-- Reference date: Sunday, July 14, 2002 23:13:12.324354679 UTC+09:00 (Q3, week 28, day 195)
+def td := zoned("2002-07-14T23:13:12.324354679+09:00")
+
+-- Same date/time at UTC (for UTC timezone name tests)
+def tdUTC := zoned("2002-07-14T23:13:12.324354679+00:00")
+
+-- AM hour (09:13:12 for AM/PM tests)
+def tdAM := zoned("2002-07-14T09:13:12.000000000+09:00")
+
+-- Named timezone (for z/V name tests)
+def tokyoTZ : TimeZone := { offset := { second := 32400 }, name := "Asia/Tokyo", abbreviation := "JST", isDST := false }
+
+def tdNamed := ZonedDateTime.ofPlainDateTime td.toPlainDateTime (TimeZone.ZoneRules.ofTimeZone tokyoTZ)
+
+-- Week-based year boundary: Dec 31, 2018 is in ISO week 1 of 2019
+def tdWeekBound := ZonedDateTime.ofPlainDateTime datetime("2018-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- G  Era
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "CE CE CE Common Era C"
+-/
+#guard_msgs in
+#eval td.format "G GG GGG GGGG GGGGG"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- y  Year of era
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2002 02 2002 02002 000002002"
+-/
+#guard_msgs in
+#eval td.format "y yy yyyy yyyyy yyyyyyyyy"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Y  Week-based year
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2002 02 2002 02002 000002002"
+-/
+#guard_msgs in
+#eval td.format "Y YY YYYY YYYYY YYYYYYYYY"
+
+-- Boundary: Dec 31, 2018 belongs to ISO week 1 of 2019
+/--
+info: "2019 19 2019"
+-/
+#guard_msgs in
+#eval tdWeekBound.format "Y YY YYYY"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- u  Extended year (signed, no era flip)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2002 02 2002 02002 000002002"
+-/
+#guard_msgs in
+#eval td.format "u uu uuuu uuuuu uuuuuuuuu"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Q / q  Quarter (Q = formatting, q = standalone — same output here)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "3 03 Q3 3rd quarter 3"
+-/
+#guard_msgs in
+#eval td.format "Q QQ QQQ QQQQ QQQQQ"
+
+/--
+info: "3 03 Q3 3rd quarter 3"
+-/
+#guard_msgs in
+#eval td.format "q qq qqq qqqq qqqqq"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- M / L  Month (M = formatting, L = standalone — same output here)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "7 07 Jul July J"
+-/
+#guard_msgs in
+#eval td.format "M MM MMM MMMM MMMMM"
+
+/--
+info: "7 07 Jul July J"
+-/
+#guard_msgs in
+#eval td.format "L LL LLL LLLL LLLLL"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- w  Week of week-based year
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "28 28 028 0028"
+-/
+#guard_msgs in
+#eval td.format "w ww www wwww"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- W  Week of month
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2 02 002 0002"
+-/
+#guard_msgs in
+#eval td.format "W WW WWW WWWW"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- d  Day of month
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "14 14 014 0014 00014"
+-/
+#guard_msgs in
+#eval td.format "d dd ddd dddd ddddd"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- D  Day of year
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "195 195 195"
+-/
+#guard_msgs in
+#eval td.format "D DD DDD"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- F  Day of week in month
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2 02 002 0002"
+-/
+#guard_msgs in
+#eval td.format "F FF FFF FFFF"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- E  Day of week (text only; count 6 = two-letter short)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "Sun Sun Sun Sunday S Su"
+-/
+#guard_msgs in
+#eval td.format "E EE EEE EEEE EEEEE EEEEEE"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- e  Localized day of week (count 1-2 = numeric ordinal, 3-6 = text)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "7 07 Sun Sunday S Su"
+-/
+#guard_msgs in
+#eval td.format "e ee eee eeee eeeee eeeeee"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- c  Standalone day of week (same output as e here)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "7 07 Sun Sunday S Su"
+-/
+#guard_msgs in
+#eval td.format "c cc ccc cccc ccccc cccccc"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- a  AM/PM marker (counts 1-4 = short, 5 = narrow)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "PM PM PM PM p"
+-/
+#guard_msgs in
+#eval td.format "a aa aaa aaaa aaaaa"
+
+/--
+info: "AM AM AM AM a"
+-/
+#guard_msgs in
+#eval tdAM.format "a aa aaa aaaa aaaaa"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- H  Hour of day (0-23)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "23 23 023 0023 00023"
+-/
+#guard_msgs in
+#eval td.format "H HH HHH HHHH HHHHH"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- h  Clock hour of AM/PM (1-12)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "11 11 011 0011 0011"
+-/
+#guard_msgs in
+#eval td.format "h hh hhh hhhh hhhh"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- K  Hour of AM/PM (0-11)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "11 11 011 0011 000011"
+-/
+#guard_msgs in
+#eval td.format "K KK KKK KKKK KKKKKK"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- k  Clock hour of day (1-24)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "23 23 023 0023 000023"
+-/
+#guard_msgs in
+#eval td.format "k kk kkk kkkk kkkkkk"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- m  Minute
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "13 13 013 0013 00013"
+-/
+#guard_msgs in
+#eval td.format "m mm mmm mmmm mmmmm"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- s  Second
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "12 12 012 0012 00012"
+-/
+#guard_msgs in
+#eval td.format "s ss sss ssss sssss"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- S  Fractional seconds (truncated from nanoseconds)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "3 32 324 3243 324354679"
+-/
+#guard_msgs in
+#eval td.format "S SS SSS SSSS SSSSSSSSS"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- A  Milliseconds since midnight
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "83592324 83592324 83592324 83592324 083592324"
+-/
+#guard_msgs in
+#eval td.format "A AA AAA AAAA AAAAAAAAA"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- n  Nanosecond (Lean extension)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "324354679 324354679 324354679 324354679 324354679"
+-/
+#guard_msgs in
+#eval td.format "n nn nnn nnnn nnnnnnnnn"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- N  Nanoseconds since midnight (Lean extension)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "83592324354679 83592324354679 83592324354679 83592324354679 83592324354679"
+-/
+#guard_msgs in
+#eval td.format "N NN NNN NNNN NNNNNNNNN"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- z  Time zone name (short = abbreviation/id, full = long name)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09:00 +09:00 +09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "z zz zzz zzzz"
+
+/--
+info: "UTC UTC UTC Coordinated Universal Time"
+-/
+#guard_msgs in
+#eval tdUTC.format "z zz zzz zzzz"
+
+/--
+info: "JST JST JST Asia/Tokyo"
+-/
+#guard_msgs in
+#eval tdNamed.format "z zz zzz zzzz"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Z  Zone offset
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+0900 +0900 +0900 GMT+09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "Z ZZ ZZZ ZZZZ ZZZZZ"
+
+/--
+info: "+0000 +0000 +0000 GMT Z"
+-/
+#guard_msgs in
+#eval tdUTC.format "Z ZZ ZZZ ZZZZ ZZZZZ"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- O  Localized GMT offset
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "GMT+9 GMT+09:00"
+-/
+#guard_msgs in
+#eval td.format "O OOOO"
+
+/--
+info: "GMT GMT"
+-/
+#guard_msgs in
+#eval tdUTC.format "O OOOO"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- V  Zone ID (VV+ = raw timezone ID; single V unsupported, like Java)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09:00 +09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "VV VVV VVVV"
+
+-- UTC offset-only zone: raw "+00:00", not normalized to "UTC"
+/--
+info: "+00:00 +00:00 +00:00"
+-/
+#guard_msgs in
+#eval tdUTC.format "VV VVV VVVV"
+
+/--
+info: "Asia/Tokyo Asia/Tokyo Asia/Tokyo"
+-/
+#guard_msgs in
+#eval tdNamed.format "VV VVV VVVV"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- v  Generic timezone name (no DST distinction; short = abbreviation, full = name)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- offset-only zone: short = raw offset, full = raw offset (same as z)
+/--
+info: "+09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "v vvvv"
+
+-- UTC offset-only: normalized to "UTC"/"Coordinated Universal Time" (same as z)
+/--
+info: "UTC Coordinated Universal Time"
+-/
+#guard_msgs in
+#eval tdUTC.format "v vvvv"
+
+-- named zone: short = abbreviation, full = IANA name
+/--
+info: "JST Asia/Tokyo"
+-/
+#guard_msgs in
+#eval tdNamed.format "v vvvv"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- X  ISO 8601 offset (uses Z for UTC)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09 +0900 +09:00 +0900 +09:00"
+-/
+#guard_msgs in
+#eval td.format "X XX XXX XXXX XXXXX"
+
+/--
+info: "Z Z Z Z Z"
+-/
+#guard_msgs in
+#eval tdUTC.format "X XX XXX XXXX XXXXX"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- x  ISO 8601 offset (no Z for UTC)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09 +0900 +09:00 +0900 +09:00"
+-/
+#guard_msgs in
+#eval td.format "x xx xxx xxxx xxxxx"
+
+/--
+info: "+00 +0000 +00:00 +0000 +00:00"
+-/
+#guard_msgs in
+#eval tdUTC.format "x xx xxx xxxx xxxxx"

tests/elab/timeFormats.lean

@@ -1,17 +1,17 @@
 import Std.Time
 open Std.Time
 
-def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
-def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
-def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : GenericFormat .any := datespec("MMMM D, uuuu h:mm aa")
-def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
-def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
-def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
-def EraDate : GenericFormat .any := datespec("MM D, uuuu G")
-def DateSmall : GenericFormat .any := datespec("uu-MM-dd")
+def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
+def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
+def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : Format Awareness.any := datespec("MMMM D, uuuu h:mm aa")
+def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def Time12Hour : Format Awareness.any := datespec("hh:mm:ss aa")
+def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
+def EraDate : Format Awareness.any := datespec("MM D, uuuu G")
+def DateSmall : Format Awareness.any := datespec("uu-MM-dd")
 
 -- Dates
 
@@ -27,7 +27,7 @@ def time₂ := time("03:11:01")
 info: "Monday, June 16, 2014 03:03:03 -0300"
 -/
 #guard_msgs in
-#eval FullDayTimeZone.format date₁.toDateTime
+#eval FullDayTimeZone.format date₁
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -197,13 +197,13 @@ info: "03:11:01 AM"
 info: "2024-08-15T14:03:47-03:00"
 -/
 #guard_msgs in
-#eval dateBR₁.toISO8601String
+#eval Formats.iso8601.format dateBR₁
 
 /--
 info: "2024-08-15T14:03:47Z"
 -/
 #guard_msgs in
-#eval dateUTC₁.toISO8601String
+#eval Formats.iso8601.format dateUTC₁
 
 /--
 info: "06/16/2014"
@@ -441,7 +441,7 @@ info: "+09:00 +09:00 +09:00 +09:00"
 #eval zoned₄.format "z zz zzzz zzzz"
 
 /--
-info: "+00:00 +00:00 +00:00 +00:00"
+info: "UTC UTC Coordinated Universal Time Coordinated Universal Time"
 -/
 #guard_msgs in
 #eval zoned₅.format "z zz zzzz zzzz"
@@ -825,7 +825,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 3 0)
-  let s := r.toLeanDateTimeString
+  let s := r.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS"
   let r := PlainDateTime.parse s
   (s, r, datetime("1932-01-02T05:04:03.000000000"))
 
@@ -840,7 +840,7 @@ def tuple6Mk (a : f) (b : g) (c : h) (d : i) (e : j) (k : z) := some (a, b, c, d
 Parsing Length Tests
 -/
 
-def uFormat : GenericFormat .any := datespec("u uu uuuu uuuuu")
+def uFormat : Format Awareness.any := datespec("u uu uuuu uuuuu")
 
 #eval do assert! (uFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk)
 #eval do assert! (uFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk)
@@ -855,7 +855,7 @@ def uFormat : GenericFormat .any := datespec("u uu uuuu uuuuu")
 #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk)
 #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk)
 
-def yFormat : GenericFormat .any := datespec("y yy yyyy yyyyy")
+def yFormat : Format Awareness.any := datespec("y yy yyyy yyyyy")
 
 #eval do assert! (yFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk)
 #eval do assert! (yFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk)
@@ -870,7 +870,7 @@ def yFormat : GenericFormat .any := datespec("y yy yyyy yyyyy")
 #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk)
 #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk)
 
-def dFormat : GenericFormat .any := datespec("D DD DDD")
+def dFormat : Format Awareness.any := datespec("D DD DDD")
 
 #eval do assert! (dFormat.parseBuilder tuple3Mk "1 12 123" |>.isOk)
 #eval do assert! (dFormat.parseBuilder tuple3Mk "323 12 123" |>.isOk)
@@ -879,7 +879,7 @@ def dFormat : GenericFormat .any := datespec("D DD DDD")
 #eval do assert! (not <| dFormat.parseBuilder tuple3Mk "1 123 123" |>.isOk)
 #eval do assert! (not <| dFormat.parseBuilder tuple3Mk "367 12 123" |>.isOk)
 
-def dddFormat : GenericFormat .any := datespec("d dd ddd dddd ddddd")
+def dddFormat : Format Awareness.any := datespec("d dd ddd dddd ddddd")
 
 #eval do assert! (dddFormat.parseBuilder tuple5Mk "1 12 031 0031 00031" |>.isOk)
 #eval do assert! (dddFormat.parseBuilder tuple5Mk "000031 12 031 0031 00031" |>.isOk)
@@ -887,7 +887,7 @@ def dddFormat : GenericFormat .any := datespec("d dd ddd dddd ddddd")
 #eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 12 0031 00031" |>.isOk)
 #eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 031 0031 000031" |>.isOk)
 
-def wFormat : GenericFormat .any := datespec("w ww www wwww")
+def wFormat : Format Awareness.any := datespec("w ww www wwww")
 
 #eval do assert! (wFormat.parseBuilder tuple4Mk "1 01 031 0031" |>.isOk)
 #eval do assert! (wFormat.parseBuilder tuple4Mk "2 01 031 0031" |>.isOk)
@@ -895,7 +895,7 @@ def wFormat : GenericFormat .any := datespec("w ww www wwww")
 #eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 00310" |>.isOk)
 #eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 031" |>.isOk)
 
-def qFormat : GenericFormat .any := datespec("q qq")
+def qFormat : Format Awareness.any := datespec("q qq")
 
 #eval do assert! (qFormat.parseBuilder tuple2Mk "1 02" |>.isOk)
 #eval do assert! (qFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -903,7 +903,7 @@ def qFormat : GenericFormat .any := datespec("q qq")
 #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def WFormat : GenericFormat .any := datespec("W WW")
+def WFormat : Format Awareness.any := datespec("W WW")
 
 #eval do assert! (WFormat.parseBuilder tuple2Mk "1 06" |>.isOk)
 #eval do assert! (WFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -911,7 +911,7 @@ def WFormat : GenericFormat .any := datespec("W WW")
 #eval do assert! (not <| WFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| WFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def eFormat : GenericFormat .any := datespec("e ee")
+def eFormat : Format Awareness.any := datespec("e ee")
 
 #eval do assert! (eFormat.parseBuilder tuple2Mk "1 07" |>.isOk)
 #eval do assert! (eFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -919,7 +919,7 @@ def eFormat : GenericFormat .any := datespec("e ee")
 #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def FFormat : GenericFormat .any := datespec("F FF")
+def FFormat : Format Awareness.any := datespec("F FF")
 
 #eval do assert! (FFormat.parseBuilder tuple2Mk "1 04" |>.isOk)
 #eval do assert! (FFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -927,7 +927,7 @@ def FFormat : GenericFormat .any := datespec("F FF")
 #eval do assert! (not <| FFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| FFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def hFormat : GenericFormat .any := datespec("h hh")
+def hFormat : Format Awareness.any := datespec("h hh")
 
 #eval do assert! (hFormat.parseBuilder tuple2Mk "1 09" |>.isOk)
 #eval do assert! (hFormat.parseBuilder tuple2Mk "12 12" |>.isOk)
@@ -949,16 +949,16 @@ info: zoned("2002-07-14T14:13:12.000000000+23:59")
 info: Except.error "offset 22: invalid hour offset: 24. Must be between 0 and 23."
 -/
 #guard_msgs in
-#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+24:59"
+#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+24:59"
 
 /--
 info: Except.error "offset 25: invalid minute offset: 60. Must be between 0 and 59."
 -/
 #guard_msgs in
-#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+23:60"
+#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+23:60"
 
 /--
 info: Except.ok (zoned("2002-07-14T14:13:12.000000000Z"))
 -/
 #guard_msgs in
-#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+00:00"
+#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+00:00"

tests/elab/timeIO.lean

@@ -40,9 +40,9 @@ info: 2013-10-19T23:59:59.000000000-03:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Sao_Paulo"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-19T23:59:59") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:00") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:01") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-19T23:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:01") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
 
 /-
 Java:
@@ -59,9 +59,9 @@ info: 2019-11-03T01:59:59.000000000-05:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Chicago"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T01:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
 
 /-
 Java:
@@ -78,6 +78,6 @@ info: 2003-10-26T01:59:59.000000000-05:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Monterrey"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"

tests/elab/timeLimits.lean

@@ -2,9 +2,9 @@ import Std.Time
 open Std.Time
 
 
-def ISO8601UTCAllow : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
-def ISO8601UTCNot : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
-def ISO8601UTCDef : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
+def ISO8601UTCAllow : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
+def ISO8601UTCNot : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
+def ISO8601UTCDef : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
 
 /--
 info: Except.ok (zoned("2002-07-14T23:14:00.324354679-23:59"))

tests/elab/timeLocalDateTime.lean

@@ -2,8 +2,8 @@ import Std.Time
 import Init
 open Std.Time
 
-def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss")
-def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu")
+def ShortDateTime : Format Awareness.any := datespec("dd/MM/uuuu HH:mm:ss")
+def ShortDate : Format Awareness.any := datespec("dd/MM/uuuu")
 
 def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second
 def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year

tests/elab/timeParse.lean

@@ -1,18 +1,18 @@
 import Std.Time
 open Std.Time
 
-def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
-def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
-def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
-def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
-def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
-def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
-def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
+def ISO8601UTC : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
+def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
+def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
+def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : Format Awareness.any := datespec("MMMM dd, uuuu hh:mm aa")
+def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def Time12Hour : Format Awareness.any := datespec("hh:mm:ss aa")
+def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
 
-def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
+def Full12HourWrong : Format Awareness.any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
 
 -- Dates
 
@@ -30,7 +30,7 @@ info: "2014-06-16T03:03:03.000000100-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := ISO8601UTC.parse! "2014-06-16T03:03:03.000000100-03:00"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -41,7 +41,7 @@ info: "2014-06-16T03:03:03.000000000-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := RFC1123.parse! "Mon, 16 Jun 2014 03:03:03 -0300"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 def tm₃ := date₁.toTimestamp
 def date₃ := DateTime.ofTimestamp tm₃ brTZ
@@ -52,7 +52,7 @@ info: "2014-06-16T00:00:00.000000000Z"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := ShortDate.parse! "06/16/2014"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 -- the timestamp is always related to UTC.
 
@@ -73,7 +73,7 @@ info: "2024-08-15T13:28:12.000000000-03:00"
 #guard_msgs in
 #eval
     let t := FullDayTimeZone.parse! "Thursday, August 15, 2024 13:28:12 -0300"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 /--
 info: "2024-08-16T01:28:00.000000000Z"
@@ -81,7 +81,7 @@ info: "2024-08-16T01:28:00.000000000Z"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := LongDateTime.parse! "August 16, 2024 01:28 AM"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 /--
 info: "0000-12-31T22:28:12.000000000+09:00"
@@ -105,7 +105,7 @@ info: "Thu 15 Aug 2024 16:28"
 #guard_msgs in
 #eval
     let t2 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 16:28:12 -0000"
-    CustomDayTime.format t2.toDateTime
+    CustomDayTime.format t2
 
 /--
 info: "2024-08-16T13:28:00.000000000Z"
@@ -113,7 +113,7 @@ info: "2024-08-16T13:28:00.000000000Z"
 #guard_msgs in
 #eval
     let t5 : ZonedDateTime := CustomDayTime.parse! "Thu 16 Aug 2024 13:28"
-    ISO8601UTC.format t5.toDateTime
+    ISO8601UTC.format t5
 
 /--
 info: "2024-08-16T01:28:12.000000000+09:00"
@@ -153,7 +153,7 @@ info: "2024-08-15T14:03:47.000000000-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 -0300"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 /--
 info: "2024-08-15T14:03:47.000000000+09:00"
@@ -161,7 +161,7 @@ info: "2024-08-15T14:03:47.000000000+09:00"
 #guard_msgs in
 #eval
     let t1 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 +0900"
-    ISO8601UTC.format t1.toDateTime
+    ISO8601UTC.format t1
 
 /--
 info: "2014-06-16T03:03:03.000000000-03:00"
@@ -169,7 +169,7 @@ info: "2014-06-16T03:03:03.000000000-03:00"
 #guard_msgs in
 #eval
     let t2 : ZonedDateTime := FullDayTimeZone.parse! "Monday, June 16, 2014 03:03:03 -0300"
-    ISO8601UTC.format t2.toDateTime
+    ISO8601UTC.format t2
 
 /--
 info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
@@ -177,7 +177,7 @@ info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 AM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2
 
 /--
 info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
@@ -185,7 +185,7 @@ info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 PM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2
 
 /--
 info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
@@ -193,7 +193,7 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 AM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2
 
 /--
 info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
@@ -201,4 +201,4 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 PM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2

tests/elab/timeSet.lean

@@ -1,18 +1,18 @@
 import Std.Time
 open Std.Time
 
-def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
-def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
-def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
-def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
-def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
-def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
-def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
+def ISO8601UTC : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
+def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
+def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
+def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : Format Awareness.any := datespec("MMMM dd, uuuu hh:mm aa")
+def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def Time12Hour : Format Awareness.any := datespec("hh:mm:ss aa")
+def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
 
-def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
+def Full12HourWrong : Format Awareness.any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
 
 -- Dates
 

tests/elab/timeTzifParse.lean

@@ -98,13 +98,13 @@ info: 0
 #eval code.v1.utLocalIndicators.size
 
 /--
-info: zoned("1969-12-31T21:00:00.000000000-03:00")
+info: zoned("1969-12-31T21:00:00.000000000-03:00[America/Sao_Paulo]")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 0) rules
 
 /--
-info: zoned("2012-12-10T00:35:47.000000000-02:00")
+info: zoned("2012-12-10T00:35:47.000000000-02:00[America/Sao_Paulo]")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 1355106947) rules