Skip to content

Commit 1355a6b

Browse files
committed
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.
1 parent 20b0bd0 commit 1355a6b

File tree

3 files changed

+34
-10
lines changed

3 files changed

+34
-10
lines changed

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

Lines changed: 21 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -86,19 +86,30 @@ Reads timezone rules from disk based on the provided file path and timezone ID.
8686
def readRulesFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := do
8787
parseTZIfFromDisk (System.FilePath.join path id) id
8888

89-
instance : Std.Time.Database TZdb where
90-
getLocalZoneRules db := localRules db.localPath
89+
/--
90+
Reads timezone rules from disk based on the provided timezone ID.
91+
-/
92+
def getZoneRules (id : String) : IO ZoneRules := do
93+
let env ← IO.getEnv "TZDIR"
9194

92-
getZoneRules db id := do
93-
let env ← IO.getEnv "TZDIR"
95+
if let some path := env then
96+
let result ← readRulesFromDisk path id
97+
return result
9498

95-
if let some path := env then
99+
for path in default.zonesPaths do
100+
if ← System.FilePath.pathExists path then
96101
let result ← readRulesFromDisk path id
97102
return result
98103

99-
for path in db.zonesPaths do
100-
if ← System.FilePath.pathExists path then
101-
let result ← readRulesFromDisk path id
102-
return result
104+
throw <| IO.userError s!"cannot find {id} in the local timezone database"
103105

104-
throw <| IO.userError s!"cannot find {id} in the local timezone database"
106+
instance : Std.Time.Database TZdb where
107+
getLocalZoneRules db := do
108+
if let some id ← IO.getEnv "TZ" then
109+
getZoneRules id
110+
else if ← System.FilePath.pathExists db.localPath then
111+
localRules db.localPath
112+
else
113+
getZoneRules "UTC"
114+
115+
getZoneRules _ id := TZdb.getZoneRules id

tests/pkg/tzdb-env/Main.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
def main : IO Unit := do
2+
let res ← Database.defaultGetLocalZoneRules
3+
println! repr res.initialLocalTimeType.gmtOffset

tests/pkg/tzdb-env/test.sh

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#!/usr/bin/env bash
2+
3+
if [ "$OS" = "Windows_NT" ]; then
4+
exit 0
5+
fi
6+
7+
rm -rf .lake/build
8+
[ "$(TZ=UTC lake exe release)" = "{ second := 0 }" ] || exit 1
9+
[ "$(TZ=America/Sao_Paulo lake exe release)" = "{ second := -11188 }" ] || exit 1
10+
exit 0

0 commit comments

Comments
 (0)