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.

Author: sertonix

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

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

tests/pkg/tzdb_env/lakefile.toml

@@ -0,0 +1,5 @@
+name = "debug"
+
+[[lean_exe]]
+name = "release"
+root = "Main"

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