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: adjustments to the datetime library #6431

Merged
merged 22 commits into from
Jan 13, 2025
Merged
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
3e68695
fix: linux fallback directories and trim of the path of localdb in linux
algebraic-dev Nov 26, 2024
41784ab
feat: read TZDIR if it's in the environment
algebraic-dev Nov 26, 2024
7f75830
fix: improve error message of parseTZIfFromDisk
algebraic-dev Nov 26, 2024
262ec2d
Merge branch 'master' of github.com:leanprover/lean4 into datetime-fix
algebraic-dev Dec 17, 2024
1e82e8a
fix: timestamp repr
algebraic-dev Dec 17, 2024
7d9cca4
fix: now PlainTime takes leap seconds as argument
algebraic-dev Dec 18, 2024
9d548b4
fix: change readlink -f to realpath
algebraic-dev Dec 18, 2024
653100b
Merge branch 'leanprover:master' into datetime-fix
algebraic-dev Dec 20, 2024
32a25d8
refactor: update src/Std/Time/Time/PlainTime.lean
algebraic-dev Jan 2, 2025
0afbdd9
Merge branch 'master' of github.com:leanprover/lean4 into datetime-fix
algebraic-dev Jan 2, 2025
3faa88e
Merge branch 'datetime-fix' of github.com:algebraic-dev/lean4 into da…
algebraic-dev Jan 2, 2025
b8630b5
chore: fix type variable names
algebraic-dev Jan 2, 2025
51975f6
feat: update src/Std/Time/Zoned/DateTime.lean
algebraic-dev Jan 8, 2025
6a8831e
feat: update tests/lean/run/timeAPI.lean
algebraic-dev Jan 8, 2025
6e635f1
revert: reverted the changes in the PlainTime structure to a better API
algebraic-dev Jan 9, 2025
d3da587
Merge branch 'datetime-fix' of github.com:algebraic-dev/lean4 into da…
algebraic-dev Jan 9, 2025
e21f70d
feat: remove small diffs
algebraic-dev Jan 9, 2025
ed09e63
fix: small typos
algebraic-dev Jan 9, 2025
77e7d96
fix: representaiton of timestamp
algebraic-dev Jan 10, 2025
572bae9
fix: small corrections to make the code better
algebraic-dev Jan 10, 2025
4870cb1
revert: change in plaindatetime derivings
algebraic-dev Jan 10, 2025
c0a5e5b
chore: remove useless lines
algebraic-dev Jan 10, 2025
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
Next Next commit
fix: linux fallback directories and trim of the path of localdb in linux
algebraic-dev committed Nov 26, 2024
commit 3e68695fd37396357b0f9a2395f30946960f0d5a
17 changes: 12 additions & 5 deletions src/Std/Time/Zoned/Database/TZdb.lean
Original file line number Diff line number Diff line change
@@ -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
@@ -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.
@@ -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"