Version: 1.1.1
Date: 2025-12-16
SPDX-License-Identifier: BSD-3-Clause
License File: See the LICENSE file in the project root
Copyright: © 2025 Michael Gardner, A Bit of Help, Inc.
Status: Released
Zoneinfo is an IANA timezone datetime manipulation library for Ada 2022. Built on the TZif library for IANA database access, it provides a clean, type-safe API for working with timezones, parsing ISO 8601 strings, formatting datetimes, and discovering timezone sources. The library follows hybrid DDD/Clean/Hexagonal architecture with functional error handling and is designed for both desktop and embedded platforms.
- Timezone-Aware Datetimes - Instant, Zoned, and Civil time representations
- ISO 8601 Parsing - Parse datetime strings with timezone offsets and zone IDs
- Datetime Formatting - Format datetimes as ISO 8601 or custom patterns
- Timezone Discovery - Find system timezone, search by pattern/region/regex (bounded arrays)
- Duration Arithmetic - Add/subtract durations, calculate differences
- TZif Integration - Built on the TZif library for IANA timezone database access
- Result Monad Error Handling - No exceptions, functional error handling
- 4-Layer Hexagonal Architecture - Domain -> Application -> Infrastructure -> API
- SPARK Verified - Domain + Application layers formally verified
- Embedded Safety - No implicit heap allocations, bounded types, static dispatch
- Library Standalone - Explicit Library_Interface for ABI stability
| Status | |
| Scope | Domain + Application Layers |
| Mode | gnatprove --mode=prove --level=2 |
| Results | See CHANGELOG for current verification statistics |
The domain and application layers are formally verified using SPARK Ada, ensuring:
- No uninitialized data - All variables properly initialized before use
- Data flow integrity - No aliasing or information flow violations
- Contract consistency - Pre/postconditions are consistent
Infrastructure and API layers use SPARK_Mode => Off as they perform I/O operations and TZif integration.
make spark-check # Run SPARK legality verification
make spark-prove # Run full SPARK proof verification| Layer | SPARK_Mode | Description |
|---|---|---|
| Domain | On | Value objects (Instant, Zoned, Civil, Duration, Zone_ID), 7-operation Result |
| Application | On | Use cases and ports |
| Infrastructure | Off | I/O operations, TZif adapters |
| API | Off | Facade over infrastructure |
This repository uses git submodules for shared tooling. Clone with:
git clone --recurse-submodules https://github.com/abitofhelp/zoneinfo.gitOr if already cloned without submodules:
git submodule update --init --recursive
# Or: make submodule-init+-------------------------------------------------------------+
| Zoneinfo.API |
| (Public Facade - Stable Interface) |
+-------------------------------------------------------------+
| API.Operations | API.Parse | API.Format | API.Discovery|
| (Pure ops) | (ISO 8601) | (Display) | (TZ sources) |
+-------------------------------------------------------------+
| Application Layer |
| Use Cases | Ports (Timezone) | Commands |
+-------------------------------------------------------------+
| Infrastructure Layer |
| Adapters (TZif Integration, Discovery) |
+-------------------------------------------------------------+
| Domain Layer |
| Instant | Zoned | Civil | Duration | Zone_ID | Source_Info |
| Zone_List | Search_Results | 7-operation Result |
+-------------------------------------------------------------+
# Build debug library
make build
# Build release library
make build-release
# Using Alire directly
alr buildAdd to your alire.toml:
[[depends-on]]
zoneinfo = "^1.1.1"In your Ada code:
with Zoneinfo.API;
with Zoneinfo.API.Parse;
with Zoneinfo.API.Format;
use Zoneinfo.API;
procedure Main is
-- Parse ISO 8601 string
Parse_Result : constant Civil_Result.Result :=
Parse.From_ISO_8601 ("2025-12-15T14:30:00");
-- Create a timezone
Zone_Result : constant Zone_ID_Result.Result :=
Zone_ID_Pkg.From_String ("America/New_York");
-- Create duration
One_Hour : constant Duration_Type :=
Duration_Pkg.From_Hours (1);
-- Format datetime
Formatted : constant String :=
Format.To_String (Format.To_ISO_8601 (Some_Civil_Time));
begin
if Civil_Result.Is_Ok (Parse_Result) then
-- Success! Use the parsed Civil time
null;
else
-- Handle error
null;
end if;
end Main;with Zoneinfo.API;
use Zoneinfo.API;
-- UTC is a convenience constant (no Result unwrapping needed)
Zone : constant Zone_ID := UTC;
-- Create instant (epoch nanoseconds)
Now : constant Instant := Instant_Pkg.From_Epoch_Nanos (1700000000);
-- Create zoned datetime
Zoned_Time : constant Zoned := Zoned_Pkg.Create (Now, Zone);
-- Change timezone (preserves instant)
NY_Result : constant Zone_ID_Result.Result :=
Zone_ID_Pkg.From_String ("America/New_York");
if Zone_ID_Result.Is_Ok (NY_Result) then
declare
NY_Zone : constant Zone_ID := Zone_ID_Result.Value (NY_Result);
NY_Time : constant Zoned := Zoned_Pkg.With_Zone (Zoned_Time, NY_Zone);
begin
-- NY_Time has same instant, different timezone context
null;
end;
end if;with Zoneinfo.API.Parse;
-- Parse datetime
Result := Parse.From_ISO_8601 ("2025-12-15T14:30:00");
-- Parse with offset
Result := Parse.From_ISO_8601_With_Offset ("2025-12-15T14:30:00-05:00");
-- Parse with zone
Result := Parse.From_ISO_8601_With_Zone ("2025-12-15T14:30:00[America/New_York]");
-- Parse duration
Duration_Result := Parse.From_ISO_Duration ("PT1H30M");with Zoneinfo.API.Format;
-- Format returns Datetime_String (bounded); use To_String to convert
ISO_Bounded : constant Format.Datetime_String :=
Format.To_ISO_8601 (Civil_Time);
ISO_String : constant String := Format.To_String (ISO_Bounded);
-- Format date portion only
Date_Only : constant Format.Datetime_String := Format.To_ISO_Date (Civil_Time);
-- Format with offset
With_Offset : constant Format.Datetime_String :=
Format.To_ISO_8601_With_Offset (Civil_Time, UTC_Offset);with Zoneinfo.API.Discovery;
-- Find system timezone
My_Zone : constant Zone_ID_Result.Result := Discovery.Find_My_Id;
-- Discover timezone sources
Paths : Path_List (1 .. 1);
Paths (1) := Make_Path ("/usr/share/zoneinfo");
Source_Result : constant Source_Info_Result.Result :=
Discovery.Discover_Sources (Paths);
-- List all zones (returns bounded Zone_List, not callback)
if Source_Info_Result.Is_Ok (Source_Result) then
declare
Source : constant Source_Info := Source_Info_Result.Value (Source_Result);
Zones_Result : constant Zone_List_Result.Result :=
Discovery.List_All_Zones (Source);
begin
if Zone_List_Result.Is_Ok (Zones_Result) then
declare
Zones : constant Zone_List := Zone_List_Result.Value (Zones_Result);
begin
-- Iterate bounded array
for I in 1 .. Zones.Count loop
Process_Zone (Zones.Items (I));
end loop;
end;
end if;
end;
end if;
-- Search by pattern (returns bounded Search_Results)
Pattern_Result : constant Search_Results_Result.Result :=
Discovery.Find_By_Pattern ("York", Source);
if Search_Results_Result.Is_Ok (Pattern_Result) then
declare
Results : constant Search_Results :=
Search_Results_Result.Value (Pattern_Result);
begin
for I in 1 .. Results.Count loop
-- Each result contains the matching Zone_ID
Process_Zone (Results.Items (I));
end loop;
end;
end if;# Run all tests
make test-all
# Build tests
make build-tests
# Run unit tests only
./test/bin/unit_runner
# Run integration tests only
./test/bin/integration_runnerTest Results: All 489 tests passing (335 unit + 154 integration)
- Documentation Index - Complete documentation overview
- Quick Start Guide - Get started in minutes
- Software Requirements Specification
- Software Design Specification
- Software Test Guide
- CHANGELOG - Release history
This project follows:
- Ada Agent (
~/.claude/agents/ada.md) - Ada 2022 standards - Architecture Agent (
~/.claude/agents/architecture.md) - DDD/Clean/Hexagonal - Functional Agent (
~/.claude/agents/functional.md) - Result/Option patterns - SPARK Agent (
~/.claude/agents/spark.md) - Formal verification patterns
This project uses git submodules for shared tooling:
docs/common- Shared documentation templates and guidesscripts/python- Build, release, and architecture scriptstest/python- Shared test fixtures and configuration
# After fresh clone
make submodule-init
# Pull latest from submodule repos
make submodule-update
# Check current submodule commits
make submodule-status| Dependency | Version | Purpose |
|---|---|---|
| gnat | >=13 | Ada 2022 compiler |
| gnatcoll | ^25.0.0 | GNAT components collection |
| functional | ^4.0.0 | Result monad and functional patterns |
| tzif | ^3.0.3 | IANA timezone database access |
This project is not open to external contributions at this time.
This project - including its source code, tests, documentation, and other deliverables - is designed, implemented, and maintained by human developers, with Michael Gardner as the Principal Software Engineer and project lead.
We use AI coding assistants (such as OpenAI GPT models and Anthropic Claude Code) as part of the development workflow to help with:
- drafting and refactoring code and tests,
- exploring design and implementation alternatives,
- generating or refining documentation and examples,
- and performing tedious and error-prone chores.
AI systems are treated as tools, not authors. All changes are reviewed, adapted, and integrated by the human maintainers, who remain fully responsible for the architecture, correctness, and licensing of this project.
Copyright (c) 2025 Michael Gardner, A Bit of Help, Inc.
Licensed under the BSD-3-Clause License. See LICENSE for details.
Michael Gardner
A Bit of Help, Inc.
https://github.com/abitofhelp
Status: Released (v1.1.1)
- Core timezone-aware datetime types (Instant, Zoned, Civil)
- ISO 8601 parsing and formatting
- Timezone discovery with bounded arrays (SPARK-compatible)
- Duration arithmetic and comparisons
- TZif library integration (v3.0.3)
- 4-layer hexagonal architecture
- Full test suite (489 tests)
- Comprehensive documentation
- SPARK legality verification for Domain + Application layers
- Alire publication