From 14120a519ccfcfa8d3bbc6b2f15a3827fcf580df Mon Sep 17 00:00:00 2001
From: Sofia Rodrigues <sofia@algebraic.dev>
Date: Mon, 11 Aug 2025 10:17:34 -0300
Subject: [PATCH] fix: replace 'D' with 'd' for day representation in long date
 format (#9799)

This PR fixes the #9410 issue.
---
 src/Std/Time/Format.lean             |   4 +-
 tests/lean/run/timeCanonFormats.lean | 140 +++++++++++++++++++++++++++
 2 files changed, 142 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/timeCanonFormats.lean

diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean
index 24f94d1fc5..fa247f2bc2 100644
--- a/src/Std/Time/Format.lean
+++ b/src/Std/Time/Format.lean
@@ -129,10 +129,10 @@ in SQL databases to represent dates.
 def sqlDate : GenericFormat .any := datespec("uuuu-MM-dd")
 
 /--
-The LongDateFormat, which follows the pattern `EEEE, MMMM D, uuuu HH:mm:ss` for
+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 : GenericFormat (.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
diff --git a/tests/lean/run/timeCanonFormats.lean b/tests/lean/run/timeCanonFormats.lean
new file mode 100644
index 0000000000..82fa8ea77f
--- /dev/null
+++ b/tests/lean/run/timeCanonFormats.lean
@@ -0,0 +1,140 @@
+import Std.Time
+open Std.Time
+
+def brTZ : TimeZone := timezone("America/Sao_Paulo -03:00")
+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
+
+def tm := date₁.toTimestamp
+def date₂ := DateTime.ofTimestamp tm brTZ
+
+/--
+info: "2014-06-16T03:03:03-03:00"
+-/
+#guard_msgs in
+#eval Formats.iso8601.format date₂
+
+/--
+info: "06-16-2014"
+-/
+#guard_msgs in
+#eval Formats.americanDate.format date₂
+
+/--
+info: "16-06-2014"
+-/
+#guard_msgs in
+#eval Formats.europeanDate.format date₂
+
+/--
+info: "03:03:03 AM"
+-/
+#guard_msgs in
+#eval Formats.time12Hour.format date₂
+
+/--
+info: "03:03:03"
+-/
+#guard_msgs in
+#eval Formats.time24Hour.format date₂
+
+/--
+info: "2014-06-16:06:03:03.000000000"
+-/
+#guard_msgs in
+#eval Formats.dateTime24Hour.format date₂
+
+/--
+info: "2014-06-16T03:03:03.000000000-0300"
+-/
+#guard_msgs in
+#eval Formats.dateTimeWithZone.format date₂
+
+/--
+info: "03:03:03.000000000"
+-/
+#guard_msgs in
+#eval Formats.leanTime24Hour.format date₂
+
+/--
+info: "03:03:03"
+-/
+#guard_msgs in
+#eval Formats.leanTime24HourNoNanos.format date₂
+
+/--
+info: "2014-06-16T06:03:03.000000000"
+-/
+#guard_msgs in
+#eval Formats.leanDateTime24Hour.format date₂
+
+/--
+info: "2014-06-16T06:03:03"
+-/
+#guard_msgs in
+#eval Formats.leanDateTime24HourNoNanos.format date₂
+
+/--
+info: "2014-06-16T03:03:03.000000000-03:00"
+-/
+#guard_msgs in
+#eval Formats.leanDateTimeWithZone.format date₂
+
+/--
+info: "2014-06-16T03:03:03-03:00"
+-/
+#guard_msgs in
+#eval Formats.leanDateTimeWithZoneNoNanos.format date₂
+
+/--
+info: "2014-06-16T03:03:03[America/Sao_Paulo]"
+-/
+#guard_msgs in
+#eval Formats.leanDateTimeWithIdentifier.format date₂
+
+/--
+info: "2014-06-16T03:03:03.000000000[America/Sao_Paulo]"
+-/
+#guard_msgs in
+#eval Formats.leanDateTimeWithIdentifierAndNanos.format date₂
+
+/--
+info: "2014-06-16"
+-/
+#guard_msgs in
+#eval Formats.leanDate.format date₂
+
+/--
+info: "2014-06-16"
+-/
+#guard_msgs in
+#eval Formats.sqlDate.format date₂
+
+/--
+info: "Monday, June 16, 2014 06:03:03"
+-/
+#guard_msgs in
+#eval Formats.longDateFormat.format date₂
+
+/--
+info: "Mon Jun 16 06:03:03 2014"
+-/
+#guard_msgs in
+#eval Formats.ascTime.format date₂
+
+/--
+info: "Mon, 16 Jun 2014 03:03:03 -0300"
+-/
+#guard_msgs in
+#eval Formats.rfc822.format date₂
+
+/--
+info: "Mon, 16-06-2014 03:03:03 -0300"
+-/
+#guard_msgs in
+#eval Formats.rfc850.format date₂