Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: improve directory fallback on Linux and trim local time identifier #6221

Merged
merged 3 commits into from
Nov 27, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 19 additions & 6 deletions src/Std/Time/Zoned/Database/TZdb.lean
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,10 @@ structure TZdb where
localPath : System.FilePath := "/etc/localtime"

/--
The path to the directory containing all available time zone files. These files define various
All the possible paths to the directories containing all available time zone files. These files define various
time zones and their rules.
-/
zonesPath : System.FilePath := "/usr/share/zoneinfo/"
zonesPaths : Array System.FilePath := #["/usr/share/zoneinfo", "/share/zoneinfo", "/etc/zoneinfo", "/usr/share/lib/zoneinfo"]

namespace TZdb
open TimeZone
Expand All @@ -52,7 +52,7 @@ def parseTZif (bin : ByteArray) (id : String) : Except String ZoneRules := do
Reads a TZif file from disk and retrieves the zone rules for the specified timezone ID.
-/
def parseTZIfFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := do
let binary ← try IO.FS.readBinFile path catch _ => throw <| IO.userError s!"cannot find {id} in the local timezone database"
let binary ← try IO.FS.readBinFile path catch _ => throw <| IO.userError s!"unable to locate {id} in the local timezone database at '{path}'"
IO.ofExcept (parseTZif binary id)

/--
Expand All @@ -64,8 +64,8 @@ def idFromPath (path : System.FilePath) : Option String := do
let last₁ ← res.get? (res.size - 2)

if last₁ = some "zoneinfo"
then last
else last₁ ++ "/" ++ last
then last.trim
else last₁.trim ++ "/" ++ last.trim

/--
Retrieves the timezone rules from the local timezone data file.
Expand All @@ -89,4 +89,17 @@ def readRulesFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := d

instance : Std.Time.Database TZdb where
getLocalZoneRules db := localRules db.localPath
getZoneRules db id := readRulesFromDisk db.zonesPath id

getZoneRules db id := do
algebraic-dev marked this conversation as resolved.
Show resolved Hide resolved
let env ← IO.getEnv "TZDIR"

if let some path := env then
let result ← readRulesFromDisk path id
algebraic-dev marked this conversation as resolved.
Show resolved Hide resolved
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"
Loading