From 705bd71c34205c503acbb04850b8d1d5eb81e219 Mon Sep 17 00:00:00 2001
From: Sertonix <sertonix@posteo.net>
Date: Mon, 22 Sep 2025 21:28:56 +0200
Subject: [PATCH] feat: expand logic to determine local time

This PR extends TZdb to honor the `TZ` environment variable and fall
back to `UTC` if `/etc/localtime` does not exist.

This is more consistent with C and allows overwriting local time as
unprivileged user.
---
 src/Std/Time/Zoned/Database/TZdb.lean | 31 ++++++++++++++++++---------
 tests/pkg/tzdb_env/Main.lean          |  6 ++++++
 tests/pkg/tzdb_env/lakefile.toml      |  5 +++++
 tests/pkg/tzdb_env/test.sh            | 10 +++++++++
 4 files changed, 42 insertions(+), 10 deletions(-)
 create mode 100644 tests/pkg/tzdb_env/Main.lean
 create mode 100644 tests/pkg/tzdb_env/lakefile.toml
 create mode 100755 tests/pkg/tzdb_env/test.sh

diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean
index 6c56e78745bc..4c5c3a8608ab 100644
--- a/src/Std/Time/Zoned/Database/TZdb.lean
+++ b/src/Std/Time/Zoned/Database/TZdb.lean
@@ -86,19 +86,30 @@ 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
 
-instance : Std.Time.Database TZdb where
-  getLocalZoneRules db := localRules db.localPath
+/--
+Reads timezone rules from disk based on the provided timezone ID.
+-/
+def getZoneRules (id : String) : IO ZoneRules := do
+  let env ← IO.getEnv "TZDIR"
 
-  getZoneRules db id := do
-    let env ← IO.getEnv "TZDIR"
+  if let some path := env then
+    let result ← readRulesFromDisk path id
+    return result
 
-    if let some path := env then
+  for path in default.zonesPaths do
+    if ← System.FilePath.pathExists path 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"
 
-    throw <| IO.userError s!"cannot find {id} in the local timezone database"
+instance : Std.Time.Database TZdb where
+  getLocalZoneRules db := do
+    if let some id ← IO.getEnv "TZ" then
+      getZoneRules id
+    else if ← System.FilePath.pathExists db.localPath then
+      localRules db.localPath
+    else
+      getZoneRules "UTC"
+
+  getZoneRules _ id := TZdb.getZoneRules id
diff --git a/tests/pkg/tzdb_env/Main.lean b/tests/pkg/tzdb_env/Main.lean
new file mode 100644
index 000000000000..a50003cad157
--- /dev/null
+++ b/tests/pkg/tzdb_env/Main.lean
@@ -0,0 +1,6 @@
+import Std.Time
+open Std.Time
+
+def main : IO Unit := do
+  let res ← Database.defaultGetLocalZoneRules
+  println! repr res.initialLocalTimeType.gmtOffset
diff --git a/tests/pkg/tzdb_env/lakefile.toml b/tests/pkg/tzdb_env/lakefile.toml
new file mode 100644
index 000000000000..3819b984d67a
--- /dev/null
+++ b/tests/pkg/tzdb_env/lakefile.toml
@@ -0,0 +1,5 @@
+name = "debug"
+
+[[lean_exe]]
+name = "release"
+root = "Main"
diff --git a/tests/pkg/tzdb_env/test.sh b/tests/pkg/tzdb_env/test.sh
new file mode 100755
index 000000000000..eaf249d7f72b
--- /dev/null
+++ b/tests/pkg/tzdb_env/test.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+if [ "$OS" = "Windows_NT" ]; then
+	exit 0
+fi
+
+rm -rf .lake/build
+[ "$(TZ=UTC lake exe release)" = "{ second := 0 }" ] || exit 1
+[ "$(TZ=America/Sao_Paulo lake exe release)" = "{ second := -11188 }" ] || exit 1
+exit 0