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.

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.

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

Extracts a timezone ID from a file path.

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

Retrieves the timezone rules from the local timezone data file.

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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.

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.

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.

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.

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.

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.

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.

@[implicit_reducible]

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