feat: TR35 compatible format

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
@@ -130,23 +129,30 @@ Represents spans of time and the difference between two points in time.
 # Formats
 
 Format strings are used to convert between `String` representations and date/time types, like `yyyy-MM-dd'T'HH:mm:ss.sssZ`.
-The table below shows the available format specifiers. Some specifiers can be repeated to control truncation or offsets.
-When a character is repeated `n` times, it usually truncates the value to `n` characters.
+The table below shows the available format specifiers. Repeating a pattern character may change the
+text style, minimum width, or offset/fraction form, depending on the field.
 
-The `number` type format specifiers, such as `h` and `K`, are parsed based on the number of repetitions.
-If the repetition count is one, the format allows values ranging from 1 up to the maximum capacity of
-the respective data type.
+The current Lean implementation follows Java's pattern language where practical, but it is not fully
+locale-sensitive. Text forms currently use English data, and localized weekday/week-of-month fields use
+the library's fixed Monday-first interpretation.
+
+For numeric fields that accept both one- and two-letter forms, the single-letter form parses a
+non-padded number and the two-letter form parses a zero-padded width of two.
 
 The supported formats include:
-- `G`: Represents the era, such as AD (Anno Domini) or BC (Before Christ).
-  - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "AD").
-  - `GGGG` (full): Displays the era in a full format (e.g., "Anno Domini").
-  - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "A").
+- `G`: Represents the era, such as BCE (Before Common Era) or CE (Common Era).
+  - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "CE").
+  - `GGGG` (full): Displays the era in a full format (e.g., "Common Era").
+  - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "C").
 - `y`: Represents the year of the era.
   - `y`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678").
   - `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").
+  - `YYYYY+`: Extended format for week-based years with more than four digits.
 - `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).
@@ -158,69 +164,94 @@ The supported formats include:
   - `MMM`: Displays the abbreviated month name (e.g., "Jul").
   - `MMMM`: Displays the full month name (e.g., "July").
   - `MMMMM`: Displays the month in a narrow form (e.g., "J" for July).
+- `L`: Represents the standalone month of the year.
+  - Supports the same widths as `M`; in the current English data it formats the same values.
 - `d`: Represents the day of the month.
 - `Q`: Represents the quarter of the year.
   - `Q`, `QQ`: Displays the quarter as a number (e.g., "3", "03").
   - `QQQ` (short): Displays the quarter as an abbreviated text (e.g., "Q3").
   - `QQQQ` (full): Displays the full quarter text (e.g., "3rd quarter").
   - `QQQQQ` (narrow): Displays the quarter as a short number (e.g., "3").
+- `q`: Represents the standalone quarter of the year.
+  - Supports the same widths as `Q`; in the current English data it formats the same values.
 - `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 using the library's fixed Monday-first week model (e.g., "2").
 - `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 the short two-letter weekday name (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`).
-- `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3").
+  - `eeeeee`: Displays the short two-letter weekday name (e.g., "Tu").
+- `c`: Standalone weekday.
+  - `c`: Displays the numeric weekday using the same Monday-to-Sunday numbering as `e`.
+  - `ccc`, `cccc`, `ccccc`: Display standalone text (same values as `e` in the current English data).
+  - `cccccc`: Displays the short two-letter weekday name (e.g., "Tu").
+- `F`: Represents the occurrence of the weekday within the month (e.g., the 2nd Sunday formats as `2`).
 - `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`: Displays AM/PM (e.g., "PM").
+  - `aaaa`: Displays the full form (e.g., "ante meridiem", "post meridiem").
+  - `aaaaa`: Displays the narrow form (e.g., "a", "p").
+- `b`: Represents the day period, extending AM/PM with noon and midnight (TR35 §4, supported in Java 16+). The `B` symbol (flexible day periods) is not supported.
+  - `b`, `bb`, `bbb`: Displays a short form (e.g., "AM", "PM", "noon", "midnight").
+  - `bbbb`: Displays a full form (e.g., "ante meridiem", "post meridiem", "noon", "midnight"); unlike `a`, the AM/PM spellings are lowercase here.
+  - `bbbbb`: Displays a narrow form (e.g., "a", "p", "n", "mi").
 - `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.
+  - `h`, `hh` are supported, matching Java.
 - `K`: Represents the hour of the AM/PM clock (0-11) (e.g., "0").
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+  - `K`, `KK` are supported, matching Java.
 - `k`: Represents the hour of the day in a 1-24 format (e.g., "24").
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+  - `k`, `kk` are supported, matching Java.
 - `H`: Represents the hour of the day in a 0-23 format (e.g., "0").
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+  - `H`, `HH` are supported, matching Java.
 - `m`: Represents the minute of the hour (e.g., "30").
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+  - `m`, `mm` are supported, matching Java.
 - `s`: Represents the second of the minute (e.g., "55").
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+  - `s`, `ss` are supported, matching Java.
 - `S`: Represents a fraction of a second, typically displayed as a decimal number (e.g., "978" for milliseconds).
-  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+  - One or more repetitions of the character truncates to the specified number of most-significant digits; it does not round.
 - `A`: Represents the millisecond of the day (e.g., "1234").
-  - 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 second (e.g., "987654321").
-  - 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.
+  - One or more repetitions of the character indicates zero-padding to the specified number of characters (no truncation is applied).
+- `n`: Represents the nanosecond of the second (e.g., "987654321"). This is a Lean/Java extension, not a TR35 field.
+  - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated.
+- `N`: Represents the nanosecond of the day (e.g., "1234000000"). This is a Lean/Java extension, not a TR35 field.
+  - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated.
+- `V`: Time zone ID.
+  - `VV`: Displays the zone identifier/name.
+  - Other counts are unsupported, matching Java.
 - `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; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "UTC", otherwise the abbreviation (e.g., "PST").
+  - `zzzz`: Displays the full zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "Coordinated Universal Time", otherwise the full zone name (e.g., "Pacific Standard Time").
+- `v`: Generic time zone name.
+  - `v`: In the current Lean timezone data this displays the stored abbreviation; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "UTC".
+  - `vvvv`: In the current Lean timezone data this displays the stored zone name/ID; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "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"), or "GMT" for UTC.
+  - `OOOO`: Displays the full GMT offset with padded hour and minutes (e.g., "GMT+08:00"), or "GMT" for UTC.
 - `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 +265,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/PlainDate.lean

@@ -355,6 +355,28 @@ 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 year := date.year
+  let doy  := date.dayOfYear
+  let dow  := date.weekday.toOrdinal.sub 1
+
+  if doy.val ≤ 3 then
+    if doy.val - dow.val < -2 then
+      year - 1
+    else
+      year
+  else if doy.val ≥ 363 then
+    let leap := if date.inLeapYear then 1 else 0
+    if (doy.val - 363 - leap) - dow.val ≥ 0 then
+      year + 1
+    else
+      year
+  else
+    year
+
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays
 

src/Std/Time/DateTime/PlainDateTime.lean

@@ -502,6 +502,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.