Standard Library: std.time
● Intermediate5 min
Every type, method and function of std.time: what the spec lists, then each declaration in its source, with its examples and the line that declares it.
Spec 14.4 · learn it in Time.
A declaration below shows what a program writes against: a type's fields, a function's parameters, what it gives, its contracts (require, ensure) and its examples. kavach test runs every example, so each one is true of the code.
What the spec lists
| Function | Gives |
|---|---|
time.now_ms() -> Int | Milliseconds since 1970-01-01 UTC |
time.monotonic_ms() -> Int | Milliseconds from a clock that never goes back; use it to measure durations |
time.sleep_ms(ms) | Waits ms milliseconds |
time.sleep(d) | Waits for the Duration d |
time.every_ms(ms) | An interval: a for loop over it runs a round every ms milliseconds, counting 0, 1, 2, …, until the loop ends with break or return |
time.every(d) | The same, every Duration d |
time.after(d, f) | A Task (9.1) that waits for d and then calls f; like any task, it belongs to the function that called time.after, and is cancelled when that function returns (9.2) |
A Duration is a length of time: a record with one field, ms, its milliseconds. A whole number followed by a unit makes one:
| Written | Is |
|---|---|
n.ms | n milliseconds |
n.seconds | n * 1_000 ms |
n.minutes | n * 60_000 ms |
n.hours | n * 3_600_000 ms |
n.days | n * 86_400_000 ms |
| Type | Is |
|---|---|
Date | A day of the calendar, with no time and no zone: year, month (1 to 12), day (1 to the month's last) |
Time | A time of day, with no date and no zone: hour (0 to 23), minute, second, ms |
DateTime | A date and a time, with no zone: what a calendar and a wall clock show |
Weekday | Monday to Sunday |
| Function or method | Gives |
|---|---|
time.today(), time.now() | Today's Date, and the DateTime now, in UTC |
time.utc(ms), dt.utc_ms() | A moment as a DateTime in UTC, and back |
time.parse_date(text) | The Date of 2026-11-04; fails with Invalid(text) for anything else, an impossible date (2026-02-30) too |
time.is_leap_year(year), time.days_in_month(year, month) | As their names say |
d.weekday() | Its Weekday |
d.add_days(n), d.add_months(n) | The date n days or months later (earlier for a negative n); a month too short for the day gives its last day: January 31 and one month is February 28 or 29 |
d.days_until(other) | Days from d to other, negative when other comes first |
d.iso(), t.iso(), dt.iso() | 2026-11-04, 09:05:30 (with .250 when there are milliseconds), 2026-11-04T09:05:30 |
| Function or method | Gives |
|---|---|
time.zone(name) | The Zone named name, or the fixed offset +05:30; fails with UnknownZone(name) for a name the database doesn't have and for an offset that can't be (+24:00, +5:30) |
z.at(ms) | The DateTime the clocks in z show at the moment ms |
z.moment(dt) | The moment the clocks in z show dt; a skipped or repeated time is resolved as below |
z.resolve(dt) | Which moments show dt: Exact(ms), Skipped(earlier, later) or Repeated(earlier, later), a Local |
z.offset_seconds(ms) | How far z is ahead of UTC at the moment ms, in seconds (negative west of Greenwich) |
z.iso(ms) | The moment ms as the clocks in z show it, with the offset: 2026-11-04T14:35:30+05:30, and Z for an offset of zero (see "Times as text") |
time.zone_offset(name, ms) | The same for a named zone of the database, none for any other name: what the others are built on |
| Function | Reads | Gives |
|---|---|---|
time.parse_time(text) | 09:05, 09:05:30, 09:05:30.250 | A Time |
time.parse_datetime(text) | 2026-11-04T09:05:30, with a time as above | A DateTime |
time.parse_moment(text) | 2026-11-04T09:05:30Z, 2026-11-04T14:35:30+05:30 | A moment, in milliseconds |
A test block (11.8) reads the real clock, as a program does. To check code at a chosen moment, it freezes the clock, as Python's freezegun, Ruby's Timecop and Jest's fake timers do:
| Function | Does |
|---|---|
time.freeze(ms) | From now on in this test, the clock is fake: now_ms gives ms (milliseconds since 1970-01-01 UTC), and sleep moves it on at once instead of waiting |
std.time.digits · digits.kav
use std.time.digits: 0 types and 4 functions. stdlib/time/digits.kav
padded function
n as text of at least width digits, with zeros in front.
pub fn padded(n: Int, width: Int) -> String
require n >= -1_000_000_000 and n <= 1_000_000_000
require width >= 1 and width <= 20
example padded(7, 2) == "07"
example padded(2026, 4) == "2026"
example padded(-5, 3) == "-005"read function
The whole number text writes in exactly width digits, with no sign and no spaces: Int(text) takes both.
pub fn read(text: String, width: Int) -> Int?
require width >= 1 and width <= 9
example read("07", 2) == 7
example read("+7", 2) == none
example read("7", 2) == none
example read("a7", 2) == noneoffset function
How many seconds ahead of UTC the offset +05:30 is, if text is one; it may have seconds, +05:21:10.
pub fn offset(text: String) -> Int?
example offset("+05:30") == 19_800
example offset("-08:00") == -28_800
example offset("+05:21:10") == 19_270
example offset("05:30") == none
example offset("+24:00") == none
example offset("+5:30") == none
example offset("Asia/Kolkata") == noneoffset_text function
An offset of seconds as text: +05:30, and Z for none.
pub fn offset_text(seconds: Int) -> String
require seconds > -86_400 and seconds < 86_400
example offset_text(19_800) == "+05:30"
example offset_text(-28_800) == "-08:00"
example offset_text(19_270) == "+05:21:10"
example offset_text(0) == "Z"std.time · time.kav
use std.time: 9 types and 10 functions. stdlib/time/time.kav
Duration type
A length of time, in milliseconds. Written with a unit after a whole number: 200.ms, 5.seconds, 2.minutes, 1.hours, 3.days.
pub type Duration {
pub ms: Int
}Weekday type
A day of the week.
pub type Weekday = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | SundayDateError type
Why text isn't a date or a time.
pub type DateError = Invalid(text: String)Date type
A day of the calendar, with no time and no zone: months 1 to 12, days 1 to the month's last. The calendar is the Gregorian one, for every year, with no exceptions (spec 14.4).
pub type Date {
pub year: Int
pub month: Int
pub day: Int
invariant year >= -1_000_000 and year <= 1_000_000
invariant month >= 1 and month <= 12
invariant day >= 1 and day <= days_in_month(year, month)
}weekday method
The day of the week.
pub fn weekday(self) -> Weekday
example Date(year: 2024, month: 1, day: 31).weekday() == Weekday.Wednesday
example Date(year: 1970, month: 1, day: 1).weekday() == Weekday.Thursdayadd_days method
The date n days later (or earlier, for a negative n).
pub fn add_days(self, n: Int) -> Date
require n >= -730_000_000 and n <= 730_000_000
require days_from_civil(self.year, self.month, self.day) + n >= -365_000_000
require days_from_civil(self.year, self.month, self.day) + n <= 364_000_000
example Date(year: 2024, month: 2, day: 28).add_days(1) == Date(year: 2024, month: 2, day: 29)
example Date(year: 2026, month: 1, day: 1).add_days(-1) == Date(year: 2025, month: 12, day: 31)add_months method
The date n months later (or earlier): the same day, or the month's last when it is shorter (January 31 and one month is February 28 or 29).
pub fn add_months(self, n: Int) -> Date
require n >= -24_000_000 and n <= 24_000_000
require self.year * 12 + n >= -11_990_000 and self.year * 12 + n <= 11_990_000
example Date(year: 2024, month: 1, day: 31).add_months(1) == Date(year: 2024, month: 2, day: 29)
example Date(year: 2026, month: 3, day: 15).add_months(-3) == Date(year: 2025, month: 12, day: 15)days_until method
How many days from this date to other: negative when other comes first.
pub fn days_until(self, other: Date) -> Int
example Date(year: 2024, month: 1, day: 1).days_until(Date(year: 2025, month: 1, day: 1)) == 366
example Date(year: 2026, month: 1, day: 2).days_until(Date(year: 2026, month: 1, day: 1)) == -1iso method
2026-11-04, as ISO 8601 writes it.
pub fn iso(self) -> String
example Date(year: 2026, month: 11, day: 4).iso() == "2026-11-04"Time type
A time of day, with no date and no zone.
pub type Time {
pub hour: Int
pub minute: Int
pub second: Int
pub ms: Int
invariant hour >= 0 and hour <= 23
invariant minute >= 0 and minute <= 59
invariant second >= 0 and second <= 59
invariant ms >= 0 and ms <= 999
}iso method
09:05:30, with .250 when there are milliseconds.
pub fn iso(self) -> String
example Time(hour: 9, minute: 5, second: 30, ms: 0).iso() == "09:05:30"
example Time(hour: 23, minute: 0, second: 0, ms: 250).iso() == "23:00:00.250"DateTime type
A date and a time of day, with no zone: what a wall clock and a calendar show. A moment is a number of milliseconds (time.now_ms()); time.utc turns one into this, as it is in UTC.
pub type DateTime {
pub date: Date
pub time: Time
}iso method
2026-11-04T09:05:30.
pub fn iso(self) -> String
example utc(1_762_247_130_000).iso() == "2025-11-04T09:05:30"utc_ms method
The moment this is in UTC, in milliseconds since 1970-01-01 UTC.
pub fn utc_ms(self) -> Int
example utc(1_762_247_130_250).utc_ms() == 1_762_247_130_250
example utc(-1).utc_ms() == -1ZoneError type
Why a name isn't a time zone.
pub type ZoneError = UnknownZone(name: String)Local type
Which moments show a date and time of day in a zone (spec 14.4): one, none (skipped when daylight saving time began: the moments it would be with the offset after and before the jump), or two (repeated when it ended).
pub type Local = Exact(ms: Int) | Skipped(earlier: Int, later: Int) | Repeated(earlier: Int, later: Int)Zone type
A time zone of the IANA database, by name, or a fixed offset from UTC (+05:30): what the clocks there show at each moment, daylight saving time included (spec 14.4).
pub type Zone {
pub name: String
invariant digits.offset(name) != none or time.zone_offset(name, 0) != none
}offset_seconds method
How many seconds the zone is ahead of UTC at the moment ms.
pub fn offset_seconds(self, ms: Int) -> Int
example Zone(name: "Asia/Kolkata").offset_seconds(0) == 19_800
example Zone(name: "UTC").offset_seconds(0) == 0
example Zone(name: "-08:00").offset_seconds(0) == -28_800at method
The date and time of day the clocks in the zone show at ms.
pub fn at(self, ms: Int) -> DateTime
require ms >= -30_000_000_000_000_000 and ms <= 30_000_000_000_000_000
example Zone(name: "Asia/Kolkata").at(0).iso() == "1970-01-01T05:30:00"iso method
The moment ms as the clocks in the zone show it, with the offset: 2026-11-04T14:35:30+05:30, and Z for an offset of zero.
pub fn iso(self, ms: Int) -> String
require ms >= -30_000_000_000_000_000 and ms <= 30_000_000_000_000_000
example Zone(name: "+05:30").iso(0) == "1970-01-01T05:30:00+05:30"
example Zone(name: "-08:00").iso(0) == "1969-12-31T16:00:00-08:00"
example Zone(name: "UTC").iso(0) == "1970-01-01T00:00:00Z"resolve method
Which moments the clocks in the zone show dt.
pub fn resolve(self, dt: DateTime) -> Local
require dt.date.year >= -100_000 and dt.date.year <= 100_000
example Zone(name: "UTC").resolve(utc(0)) == Local.Exact(ms: 0)moment method
The moment the clocks in the zone show dt: a skipped time moves later by the gap, a repeated one is its earlier moment (RFC 5545, as java.time and jiff do).
pub fn moment(self, dt: DateTime) -> Int
require dt.date.year >= -100_000 and dt.date.year <= 100_000
example Zone(name: "Asia/Kolkata").moment(utc(19_800_000)) == 0zone function
The time zone named name in the IANA database (Asia/Kolkata, Europe/Berlin, UTC), or the fixed offset +05:30.
pub fn zone(name: String) -> Zone ! ZoneError
example zone("Asia/Kolkata") == Zone(name: "Asia/Kolkata")
example zone("+05:30") == Zone(name: "+05:30")
example zone("Mars/Olympus") fails ZoneError.UnknownZone(name: "Mars/Olympus")
example zone("+24:00") fails ZoneError.UnknownZone(name: "+24:00")is_leap_year function
Whether year has a February 29.
pub fn is_leap_year(year: Int) -> Bool
example is_leap_year(2024)
example not is_leap_year(1900)
example is_leap_year(2000)
example not is_leap_year(2026)days_in_month function
How many days month month (1 to 12) of year has.
pub fn days_in_month(year: Int, month: Int) -> Int
require month >= 1 and month <= 12
example days_in_month(2024, 2) == 29
example days_in_month(2026, 2) == 28
example days_in_month(2026, 4) == 30
example days_in_month(2026, 12) == 31utc function
The date and time of day the moment ms (since 1970-01-01 UTC) is in UTC.
pub fn utc(ms: Int) -> DateTime
require ms >= -31_000_000_000_000_000 and ms <= 31_000_000_000_000_000
example utc(0).iso() == "1970-01-01T00:00:00"
example utc(1_762_247_130_250).iso() == "2025-11-04T09:05:30.250"
example utc(-1).iso() == "1969-12-31T23:59:59.999"parse_date function
The date text writes as ISO 8601 does: 2026-11-04. A year before 0 or after 9999 has a sign or more digits, as iso writes it: -0005-01-01, 12345-06-07, +12345-06-07.
pub fn parse_date(text: String) -> Date ! DateError
example parse_date("2026-11-04") == Date(year: 2026, month: 11, day: 4)
example parse_date("-0005-01-01") == Date(year: -5, month: 1, day: 1)
example parse_date("+12345-06-07") == Date(year: 12_345, month: 6, day: 7)
example parse_date("2026-02-30") fails DateError.Invalid(text: "2026-02-30")
example parse_date("4 Nov 2026") fails DateError.Invalid(text: "4 Nov 2026")
example parse_date("2026-+1-04") fails DateError.Invalid(text: "2026-+1-04")
example parse_date("026-01-01") fails DateError.Invalid(text: "026-01-01")
example parse_date("2000000-01-01") fails DateError.Invalid(text: "2000000-01-01")parse_time function
The time of day text writes: 09:05, 09:05:30, 09:05:30.250.
pub fn parse_time(text: String) -> Time ! DateError
example parse_time("09:05") == Time(hour: 9, minute: 5, second: 0, ms: 0)
example parse_time("09:05:30.25") == Time(hour: 9, minute: 5, second: 30, ms: 250)
example parse_time("09:05:30.1239") == Time(hour: 9, minute: 5, second: 30, ms: 123)
example parse_time("24:00") fails DateError.Invalid(text: "24:00")
example parse_time("9:05") fails DateError.Invalid(text: "9:05")
example parse_time("09:05.5") fails DateError.Invalid(text: "09:05.5")parse_datetime function
The date and time of day text writes, with no zone: 2026-11-04T09:05:30.
pub fn parse_datetime(text: String) -> DateTime ! DateError
example parse_datetime("2026-11-04T09:05").iso() == "2026-11-04T09:05:00"
example parse_datetime("2026-11-04T09:05:30Z") fails DateError.Invalid(text: "2026-11-04T09:05:30Z")
example parse_datetime("2026-11-04") fails DateError.Invalid(text: "2026-11-04")parse_moment function
The moment text writes, which must say its offset from UTC: 2026-11-04T09:05:30Z, 2026-11-04T14:35:30+05:30.
pub fn parse_moment(text: String) -> Int ! DateError
example parse_moment("1970-01-01T05:30:00+05:30") == 0
example parse_moment("1969-12-31T16:00:00-08:00") == 0
example parse_moment("1970-01-01T00:00:00.250Z") == 250
example parse_moment("1970-01-01T00:00:00") fails DateError.Invalid(text: "1970-01-01T00:00:00")