structure Std.Time.Database.TZdb : Type

Represents a Time Zone Database (TZdb) configuration with paths to local and general timezone data.

• zonesPaths : Array System.FilePath

  Static fallback paths to directories containing time zone files. TZDIR is not stored here; it is re-read on every lookup via resolveZonesPaths.

def Std.Time.Database.TZdb.parseTZif (bin : ByteArray) (id : String) : Except String TimeZone.ZoneRules

Parses binary timezone data into zone rules based on a given timezone ID.

Equations

• Std.Time.Database.TZdb.parseTZif bin id = do let database ← Std.Time.TimeZone.TZif.parse.run bin Std.Time.TimeZone.convertTZif database id

def Std.Time.Database.TZdb.parseTZIfFromDisk (path : System.FilePath) (id : String) : IO TimeZone.ZoneRules

Reads a TZif file from disk and retrieves the zone rules for the specified timezone ID.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.idFromPath (path : System.FilePath) : Option String

Extracts a timezone ID from a file path.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.localRules (path : System.FilePath) : IO TimeZone.ZoneRules

Retrieves the timezone rules from the local timezone data file.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.readRulesFromDisk (path : System.FilePath) (id : String) : IO TimeZone.ZoneRules

Reads timezone rules from disk based on the provided file path and timezone ID.

Equations

• Std.Time.Database.TZdb.readRulesFromDisk path id = Std.Time.Database.TZdb.parseTZIfFromDisk (path.join { toString := id }) id

inductive Std.Time.Database.TZdb.TZSpec : Type

Parsed form of the TZ environment variable.

The POSIX proleptic format (e.g. TZ=EST5EDT,M3.2.0,M11.1.0) is not supported; only file paths and timezone IDs backed by zoneinfo data are recognized.

• filePath (p : String) : TZSpec

  A file path (the part after the leading :), absolute or relative to a zoneinfo directory.

• zoneId (id : String) : TZSpec

  A timezone ID such as America/New_York, looked up in the zoneinfo search paths.

def Std.Time.Database.TZdb.instReprTZSpec.repr : TZSpec → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.Database.TZdb.instReprTZSpec : Repr TZSpec

Equations

• Std.Time.Database.TZdb.instReprTZSpec = { reprPrec := Std.Time.Database.TZdb.instReprTZSpec.repr }

@[implicit_reducible]

instance Std.Time.Database.TZdb.instBEqTZSpec : BEq TZSpec

Equations

• Std.Time.Database.TZdb.instBEqTZSpec = { beq := Std.Time.Database.TZdb.instBEqTZSpec.beq }

def Std.Time.Database.TZdb.instBEqTZSpec.beq : TZSpec → TZSpec → Bool

Equations

• Std.Time.Database.TZdb.instBEqTZSpec.beq (Std.Time.Database.TZdb.TZSpec.filePath a) (Std.Time.Database.TZdb.TZSpec.filePath b) = (a == b)
• Std.Time.Database.TZdb.instBEqTZSpec.beq (Std.Time.Database.TZdb.TZSpec.zoneId a) (Std.Time.Database.TZdb.TZSpec.zoneId b) = (a == b)
• Std.Time.Database.TZdb.instBEqTZSpec.beq x✝¹ x✝ = false

def Std.Time.Database.TZdb.parseTZValue (tz : String) : Option TZSpec

Parses the value of the TZ environment variable. Returns none for empty or : (empty path after the colon) values.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.findInPaths (searchPaths : Array System.FilePath) (rel : String) : IO (Option System.FilePath)

Returns the first path in searchPaths joined with rel that exists on disk, or none.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.resolveLocalPath (zonesPaths : Array System.FilePath) : IO System.FilePath

Resolves the local timezone file path from the TZ environment variable, searching zonesPaths for relative paths and timezone IDs. Falls back to /etc/localtime if TZ is unset. Throws if TZ is set but its value cannot be found on disk.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.default : TZdb

Returns a TZdb with common fallback zoneinfo paths for Linux and macOS. Call this once at program startup. The TZ and TZDIR environment variables are re-read on every getLocalZoneRules/getZoneRules call, so runtime changes to those variables are always reflected.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.resolveZonesPaths (db : TZdb) : IO (Array System.FilePath)

Builds the effective zoneinfo search path by prepending the current TZDIR (if set and exists on disk) to db.zonesPaths. Called on every lookup so that runtime changes to TZDIR are reflected immediately.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.TZdb.getLocalZoneRules (db : TZdb) : IO TimeZone.ZoneRules

Retrieves the timezone rules for the local timezone, re-reading the TZ and TZDIR environment variables on each call so that runtime changes are reflected immediately.

Equations

• db.getLocalZoneRules = do let __do_lift ← db.resolveZonesPaths let path ← Std.Time.Database.TZdb.resolveLocalPath __do_lift Std.Time.Database.TZdb.localRules path

def Std.Time.Database.TZdb.getZoneRules (db : TZdb) (id : String) : IO TimeZone.ZoneRules

Retrieves the timezone rules for the given timezone ID, re-reading TZDIR on each call so that runtime changes are reflected immediately.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.Database.TZdb.inst : Time.Database TZdb

Equations

• One or more equations did not get rendered due to their size.