From fe98377e50df5aabdc273f5999e17360e4c1e665 Mon Sep 17 00:00:00 2001
From: Sofia Rodrigues <sofia@algebraic.dev>
Date: Wed, 29 Apr 2026 01:20:18 -0300
Subject: [PATCH] fix: TZDB search for TZ and TZDIR first

---
 src/Std/Time/Zoned/Database.lean      |  10 +--
 src/Std/Time/Zoned/Database/TZdb.lean | 116 +++++++++++++++++++++-----
 2 files changed, 100 insertions(+), 26 deletions(-)

diff --git a/src/Std/Time/Zoned/Database.lean b/src/Std/Time/Zoned/Database.lean
index a78452323c16..70ce4e09b742 100644
--- a/src/Std/Time/Zoned/Database.lean
+++ b/src/Std/Time/Zoned/Database.lean
@@ -26,17 +26,17 @@ Gets the zone rules for a specific time zone identifier, handling Windows and no
 In windows it uses the current `icu.h` in Windows SDK. If it's linux or macos then it will use the `tzdata`
 files.
 -/
-def defaultGetZoneRules : String → IO TimeZone.ZoneRules :=
+def defaultGetZoneRules (name : String) : IO TimeZone.ZoneRules := do
   if System.Platform.isWindows
-    then getZoneRules WindowsDb.default
-    else getZoneRules TZdb.default
+    then getZoneRules WindowsDb.default name
+    else getZoneRules (← TZdb.default) name
 
 /--
 Gets the local zone rules, accounting for platform differences.
 In windows it uses the current `icu.h` in Windows SDK. If it's linux or macos then it will use the `tzdata`
 files.
 -/
-def defaultGetLocalZoneRules : IO TimeZone.ZoneRules :=
+def defaultGetLocalZoneRules : IO TimeZone.ZoneRules := do
   if System.Platform.isWindows
     then getLocalZoneRules WindowsDb.default
-    else getLocalZoneRules TZdb.default
+    else getLocalZoneRules (← TZdb.default)
diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean
index a523f3e0b202..929a8dcf1568 100644
--- a/src/Std/Time/Zoned/Database/TZdb.lean
+++ b/src/Std/Time/Zoned/Database/TZdb.lean
@@ -26,23 +26,17 @@ structure TZdb where
   The path to the local timezone file. This is typically a symlink to a file within the timezone
   database that corresponds to the current local time zone.
   -/
-  localPath : System.FilePath := "/etc/localtime"
+  localPath : System.FilePath
 
   /--
   All the possible paths to the directories containing all available time zone files. These files define various
   time zones and their rules.
   -/
-  zonesPaths : Array System.FilePath := #["/usr/share/zoneinfo", "/share/zoneinfo", "/etc/zoneinfo", "/usr/share/lib/zoneinfo"]
+  zonesPaths : Array System.FilePath
 
 namespace TZdb
 open TimeZone
 
-/--
-Returns a default `TZdb` instance with common timezone data paths for most Linux distributions and macOS.
--/
-@[inline]
-def default : TZdb := {}
-
 /--
 Parses binary timezone data into zone rules based on a given timezone ID.
 -/
@@ -82,21 +76,101 @@ def localRules (path : System.FilePath) : IO ZoneRules := do
 Reads timezone rules from disk based on the provided file path and timezone ID.
 -/
 def readRulesFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := do
-  parseTZIfFromDisk (System.FilePath.join path id) id
+  parseTZIfFromDisk (path.join id) id
 
-instance : Std.Time.Database TZdb where
-  getLocalZoneRules db := localRules db.localPath
+/--
+Parsed form of the `TZ` environment variable.
+-/
+inductive TZSpec
+
+  /--
+  A file path (the part after the leading `:`), absolute or relative to a zoneinfo directory.
+  -/
+  | filePath (p : String)
+
+  /--
+  A timezone ID such as `America/New_York`, looked up in the zoneinfo search paths.
+  -/
+  | zoneId (id : String)
+  deriving Repr, BEq
+
+/--
+Parses the value of the `TZ` environment variable. Returns `none` for empty or
+`:` (empty path after the colon) values.
+-/
+def parseTZValue (tz : String) : Option TZSpec :=
+  if tz.startsWith ":" then
+    let p := (tz.drop 1).toString
+    if p.isEmpty then none else some (.filePath p)
+  else if !tz.isEmpty then
+    some (.zoneId tz)
+  else
+    none
+
+/--
+Returns the first path in `searchPaths` joined with `rel` that exists on disk, or `none`.
+-/
+def findInPaths (searchPaths : Array System.FilePath) (rel : String) : IO (Option System.FilePath) := do
+  for base in searchPaths do
+    let full := base.join rel
+    if ← full.pathExists then
+      return some full
+
+  return none
+
+/--
+Resolves the local timezone file path from the `TZ` environment variable, searching
+`zonesPaths` for relative paths and timezone IDs. Falls back to `/etc/localtime` if
+`TZ` is unset. Throws if `TZ` is set but its value cannot be found on disk.
+-/
+def resolveLocalPath (zonesPaths : Array System.FilePath) : IO System.FilePath := do
+  let some tz := ← IO.getEnv "TZ"
+    | return "/etc/localtime"
+
+  let some spec := parseTZValue tz
+    | return "/etc/localtime"
+
+  match spec with
+  | .filePath p =>
+    if p.startsWith "/" then return p
+    if let some path := ← findInPaths zonesPaths p then return path
+    throw <| IO.userError s!"TZ='{tz}': path '{p}' not found in any zoneinfo directory"
+  | .zoneId id =>
+    if let some path := ← findInPaths zonesPaths id then return path
+    throw <| IO.userError s!"TZ='{tz}': timezone not found in any zoneinfo directory"
+
+/--
+Returns a `TZdb` initialized from the `TZ` and `TZDIR` environment variables, with
+common fallback paths for Linux and macOS. Call this once at program startup.
+-/
+def default : IO TZdb := do
+  let defs : Array System.FilePath := #["/usr/share/zoneinfo", "/share/zoneinfo", "/etc/zoneinfo", "/usr/share/lib/zoneinfo"]
+
+  let zonesPaths ← match ← IO.getEnv "TZDIR" with
+    | none | some "" => pure defs
+    | some d =>
+      if ← System.FilePath.pathExists d then pure #[d]
+      else throw <| IO.userError s!"TZDIR='{d}': directory not found"
 
-  getZoneRules db id := do
-    let env ← IO.getEnv "TZDIR"
+  let localPath ← resolveLocalPath zonesPaths
+  return { localPath, zonesPaths }
+
+/--
+Retrieves the timezone rules for the local timezone using `db.localPath`.
+-/
+def getLocalZoneRules (db : TZdb) : IO ZoneRules :=
+  localRules db.localPath
 
-    if let some path := env then
-      let result ← readRulesFromDisk path id
-      return result
+/--
+Retrieves the timezone rules for the given timezone ID by searching `db.zonesPaths`.
+-/
+def getZoneRules (db : TZdb) (id : String) : IO ZoneRules := do
+  for base in db.zonesPaths do
+    if ← (base.join id).pathExists then
+      return ← readRulesFromDisk base id
 
-    for path in db.zonesPaths do
-      if ← System.FilePath.pathExists path then
-        let result ← readRulesFromDisk path id
-        return result
+  throw <| IO.userError s!"cannot find {id} in the local timezone database"
 
-    throw <| IO.userError s!"cannot find {id} in the local timezone database"
+instance : Std.Time.Database TZdb where
+  getLocalZoneRules db := db.getLocalZoneRules
+  getZoneRules db id := db.getZoneRules id