Skip to content

Commit

Permalink
fix: linux fallback directories and trim of the path of localdb in linux
Browse files Browse the repository at this point in the history
  • Loading branch information
algebraic-dev committed Nov 26, 2024
1 parent 0eca3bd commit 3e68695
Showing 1 changed file with 12 additions and 5 deletions.
17 changes: 12 additions & 5 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 Down Expand Up @@ -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,11 @@ 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
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"

0 comments on commit 3e68695

Please sign in to comment.