fix: prioritize TZ and TZDIR over /etc/localtime in TZDB search (#13565)

This PR fixes an issue where the missing /etc/localtime caused a failure
even when TZ and TZDIR were present.

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

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

@@ -23,26 +23,14 @@ Represents a Time Zone Database (TZdb) configuration with paths to local and gen
 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.
+  Static fallback paths to directories containing time zone files. `TZDIR` is not stored here;
+  it is re-read on every lookup via `resolveZonesPaths`.
   -/
-  localPath : System.FilePath := "/etc/localtime"
-
-  /--
-  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 +70,112 @@ 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
+
+/--
+Parsed form of the `TZ` environment variable.
+
+The POSIX proleptic format (e.g. `TZ=EST5EDT,M3.2.0,M11.1.0`) is not supported;
+only file paths and timezone IDs backed by zoneinfo data are recognized.
+-/
+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` with common fallback zoneinfo paths for Linux and macOS.
+Call this once at program startup. The `TZ` and `TZDIR` environment variables
+are re-read on every `getLocalZoneRules`/`getZoneRules` call, so runtime changes
+to those variables are always reflected.
+-/
+def default : TZdb where
+  zonesPaths := #["/usr/share/zoneinfo", "/share/zoneinfo", "/etc/zoneinfo", "/usr/share/lib/zoneinfo"]
+
+/--
+Builds the effective zoneinfo search path by prepending the current `TZDIR` (if set and
+exists on disk) to `db.zonesPaths`. Called on every lookup so that runtime changes to
+`TZDIR` are reflected immediately.
+-/
+def resolveZonesPaths (db : TZdb) : IO (Array System.FilePath) := do
+  match ← IO.getEnv "TZDIR" with
+  | none | some "" => return db.zonesPaths
+  | some d =>
+    if ← System.FilePath.pathExists d then return (#[(d : System.FilePath)] ++ db.zonesPaths)
+    else return db.zonesPaths
+
+/--
+Retrieves the timezone rules for the local timezone, re-reading the `TZ` and `TZDIR`
+environment variables on each call so that runtime changes are reflected immediately.
+-/
+def getLocalZoneRules (db : TZdb) : IO ZoneRules := do
+  let path ← resolveLocalPath (← db.resolveZonesPaths)
+  localRules path
+
+/--
+Retrieves the timezone rules for the given timezone ID, re-reading `TZDIR` on each
+call so that runtime changes are reflected immediately.
+-/
+def getZoneRules (db : TZdb) (id : String) : IO ZoneRules := do
+  for base in ← db.resolveZonesPaths do
+    if ← (base.join id).pathExists then
+      return ← readRulesFromDisk base id
+
+  throw <| IO.userError s!"cannot find {id} in the local timezone database"
 
 instance : Std.Time.Database TZdb where
-  getLocalZoneRules db := localRules db.localPath
-
-  getZoneRules db id := do
-    let env ← IO.getEnv "TZDIR"
-
-    if let some path := env then
-      let result ← readRulesFromDisk path id
-      return result
-
-    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"
+  getLocalZoneRules db := db.getLocalZoneRules
+  getZoneRules db id := db.getZoneRules id