Skip to content

feat: expand logic to determine local time #10509

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.

Sign up for GitHub

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

Open
sertonix wants to merge 1 commit into
base: master
Choose a base branch
from
Open

feat: expand logic to determine local time #10509

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
31 changes: 21 additions & 10 deletions src/Std/Time/Zoned/Database/TZdb.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

@TwoFX TwoFX Dec 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here you're changing the logic by using the default paths instead of the paths given by the database that the user is supplying. This is not correct, we want users to configure their own timezone database location from application code if they are so inclined.

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"
Copy link
Member

@TwoFX TwoFX Dec 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are some subtleties around the paths here that I think we should clear up. The docstring of the zonesPaths field reads

All the possible paths to the directories containing all available time zone files. These files define various time zones and their rules.

To me this reads like getZoneRules should search for the given time zone in all of the supplied paths and return the rules if it finds them in any of the paths.

This is not what currently happens (neither before nor after the PR). The readRulesFromDisk function throws an exception if it does not find the zone rules for the given ID, so the code here only looks for the given time zone in the first directory in zonesPaths that exists. So if we hit this throw clause here, we are actually in the situation that we didn't find any time zone database.

@algebraic-dev, what did you intend the behavior to be here? I see two options:

  • Keep the current behavior where we only search the first path that exists. In that case we should clarify the docstring of zonesPaths and change the error message here to something like did not find a local timezone database in <list of paths>.
  • Change the behavior so that we search all paths and only report an error if we didn't find the rules in any of the paths. This would mean refactoring readRulesFromDisk and getZoneRules (and clarifying the docstring of zonesPaths might still be a good idea).


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
6 changes: 6 additions & 0 deletions tests/pkg/tzdb_env/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
import Std.Time
open Std.Time

def main : IO Unit := do
let res ← Database.defaultGetLocalZoneRules
println! repr res.initialLocalTimeType.gmtOffset
5 changes: 5 additions & 0 deletions tests/pkg/tzdb_env/lakefile.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
name = "debug"

[[lean_exe]]
name = "release"
root = "Main"
10 changes: 10 additions & 0 deletions tests/pkg/tzdb_env/test.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading