feat: expand logic to determine local time

[sertonix]

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.

I would kindly ask for help with writing a test for the TZ environment variable since I am very new to lean. More specifically: How should I set an environment variable for a test?

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 20b0bd0a2018295db19d3dabb5905841fd16a679 --onto 9fc18b8ab462cb9100d37a23814ebbac330e8577. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-22 20:42:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 20b0bd0a2018295db19d3dabb5905841fd16a679 --onto 0807f73171ca8f765c11ef37d69fd95e6613a878. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-24 13:04:35)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 20b0bd0a2018295db19d3dabb5905841fd16a679 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-22 20:42:04)

[TwoFX]

Thanks for the PR!

I would kindly ask for help with writing a test for the TZ environment variable since I am very new to lean. More specifically: How should I set an environment variable for a test?

You can add a new test directory to tests/pkg/. These tests are just small Lean projects together with a script test.sh that can invoke lake build, run the resulting executable with different environment variables, etc.

[sertonix]

Thanks! I think the test works now

[sertonix]

Is there anything blocking this MR?

[TwoFX]

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.

[TwoFX]

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).

[TwoFX]

Is there anything blocking this MR?

Just a lack of review capacity :)