Hello, `ox.toml`

A single .ar file is fine for hello-world. Anything beyond that wants to be a package: a directory tree with a manifest, a stable public surface, and a lockfile so the same code resolves to the same dependencies tomorrow.

This chapter promotes the Hello-Argon program into a proper package — lease-tutorial — which the rest of the book extends.

We continue to declare metatypes inline (this time in a dedicated metatypes.ar module, shown below). A real project would replace that module with use ufo::prelude::* and pull in UFO’s catalog of kind, subkind, role, phase, relator, etc. Whichever path you take, kind is a metatype declared via Argon’s substrate, not a language built-in; Chapter 2.1 covers the substrate end-to-end.

Setting up a package by hand

The toolchain doesn’t yet ship a cargo new-style scaffolder; you create the two files yourself. From a fresh directory:

$ mkdir -p lease-tutorial/src
$ cd lease-tutorial

The package needs a manifest at the root (ox.toml) and a schema-root directory (src/) holding the .ar source files. The next two sections build them.

The manifest

A working ox.toml for the tutorial:

[project]
name = "lease-tutorial"
version = "0.1.0"
edition = "2025"
entry = "root.ar"
default-world = "open"

[schema]
root = "src"

[package]
name = "lease-tutorial"
version = "0.1.0"
edition = "2025"
description = "Running example for The Argon Programming Language"
license = "CC-BY-4.0"
max_tier = 3

[dependencies]

Four sections. They will accumulate as the package grows. Two of them — [project] and [package] — repeat the package’s identity; that is intentional, and the next subsections explain why.

`[project]` — the perspectival-composition layer

[project] is what ox check, ox build, ox query, and ox mutate read when they need to know how to compose your modules into a world the reasoner can execute over. Required fields:

name and version — the same name and version the package reports.
edition = "2025" — the language edition this source is written in. Editions are parse-time only; no runtime split. "2025" is current.
entry = "root.ar" — the entry-point module under src/. Idiomatic packages name it root.ar; the file lists use … ::* for every submodule the project should see.
default-world = "open" | "closed" — the world assumption applied to every module that does not override it. Open-world is the default for ontology work.

Optional siblings include [modules], [standpoints], [defeat], and [tree-shaking] — covered in Chapter 5.4 and Chapter 4.1 respectively.

`[schema]` — where the source lives

[schema]
root = "src"

Every path under [project] (notably entry) is resolved relative to [schema] root. The default is "." (the manifest’s directory); the convention is "src".

`[package]` — the registry / dependency layer

[package] is what ox install, ox publish, ox audit, ox tree, and ox why read. It is the Cargo-shaped registry surface:

name, version — must match [project] for hybrid manifests.
edition = "2025" — the registry’s view of the edition. Inherited from [workspace.package] via edition.workspace = true when the package belongs to a workspace.
description, license, authors, repository, homepage, documentation, readme, keywords, categories — registry-facing metadata.
max_tier = N — caps the decidability tier the compiler will let your rules sit at. Tier 3 (full Datalog with stratified negation) is the typical cap; lower it to be conservative, raise it if you have invariants in higher tiers that you intend to verify with @[theorem] rather than execute. Chapter 5.3 covers the full ladder.
default_world — the default world assumption for items declared in this package’s modules (overridden by [modules].default-world per-module).

Package names match ^[a-z][a-z0-9_-]*$; hyphens and underscores are both legal at the manifest level and canonicalize to underscores in use paths (so lease-tutorial becomes lease_tutorial).

`[dependencies]`

Empty for now. We will fill this in Chapter 4.1 when we start pulling in foundational vocabulary. A few shapes of dependency entry:

[dependencies]
ufo = "0.2.1"                              # registry, semver
cofris.workspace = true                    # inherit from workspace
my-local = { path = "../my-local" }        # local path

The source tree

Lay down two files under src/. First, the project entry — a root.ar that pulls every submodule into the module graph:

$ tree src
src
├── prelude.ar
└── root.ar

// lease_tutorial::root
//
// Project entry — pulls every submodule into the module graph so
// `ox check`, `ox test`, `ox build`, and `ox diagram` see the full
// project. Add `use foo::*` here when you create `src/foo.ar`.

And a curated prelude.ar — the library surface consumers will reach for:

// lease_tutorial::prelude
//
// Re-export the package's public surface here. Use `pub use foo::*`
// to thread items through. Internal modules left out of the prelude
// stay private — refactor without breaking downstream.

Both are empty for now. We will fill them in shortly.

Every .ar file under src/ is a module. The path under src/ becomes the qualified module path: src/party.ar is lease_tutorial::party, src/prelude.ar is lease_tutorial::prelude, and so on.

Adding a module

Promote our hello-world into a real module. Create src/metatypes.ar:

pub metaxis rigidity for type {
    rigid,
    anti_rigid
}

pub metaxis sortality for type {
    sortal,
    non_sortal
}

pub metatype kind = { rigid, sortal }

Then src/party.ar:

use metatypes::*

pub kind Person {
    id: String,
    name: String,
}

Wire both into the project. Edit src/root.ar to pull them in:

use metatypes::*
use party::*

And expose them through the prelude as the package’s public surface. Edit src/prelude.ar:

pub use metatypes::*
pub use party::*

pub use re-exports — items pass through prelude to consumers as if prelude had defined them itself. This is the canonical pattern: root.ar makes everything reachable for compilation; prelude.ar curates what consumers see.

The directory now looks like this:

src
├── metatypes.ar
├── party.ar
├── prelude.ar
└── root.ar

Type-check it:

$ ox check
ox lease-tutorial v0.1.0 (./ox.toml)
ox 3 modules resolved from entry point
ox 1 standpoints: default
check passed

The package compiles. We have a working skeleton.

What `ox.toml` is doing for you

Three things, mainly.

Resolution. ox install reads [dependencies], walks the dependency graph against the registry, picks compatible versions, and writes ox.lock. The lockfile is bivalent: it records both a content hash (byte-identical fetches) and a Merkle root over construct signatures (semantic identity — what the package actually contains). Chapter 4.2 covers the lockfile in detail.

Visibility. Two-tier: pub exports across module boundaries; the default is module-internal — file-scoped. There is no per-package or per-workspace third tier. The pub use re-export pattern in prelude.ar is how you make a package’s surface intentional rather than accidental.

Direct-dependencies rule. A package can use only items reachable through its own [dependencies], not items reachable transitively through some dependency’s dependencies. If you want to use a transitive package, add it explicitly to your manifest.

Workspace flavor

A workspace is a root ox.toml whose [workspace] section names member packages:

[workspace]
members = ["packages/lease-tutorial", "packages/lease-tests"]
resolver = "1"

[workspace.package]
edition = "2025"
license = "CC-BY-4.0"

[workspace.dependencies]
ufo = "0.2.1"

Workspace members inherit version pins via ufo.workspace = true and shared metadata via edition.workspace = true. The lockfile lives at the workspace root and is shared across members. We will use a workspace once the model has grown enough to want a separate test package.

Running things

Three commands you will use constantly inside a package:

$ ox check                    # Type-check + meta-property + package constraints
$ ox build                    # Compile to kernel types + Datalog
$ ox test                     # Run test blocks (Chapter 3.3)

Two more once there are queries and mutations to run:

$ ox query <name> [--explain]
$ ox mutate <name> --principal <id> [--dry-run] [--explain]

ox check is the fastest of these — it skips reasoning by default. Pass --reason to invoke the saturation engine; you will need it when an invariant depends on the reasoner having classified the TBox.

Edge cases worth knowing

root.ar versus prelude.ar. root.ar is the project entry declared in [project] entry; the toolchain starts module discovery from it. prelude.ar is the library surface — what consumers see when they use lease_tutorial::prelude::*. The convention is for root.ar to use foo::* every internal submodule, and for prelude.ar to pub use foo::* only the curated public surface.
Module names canonicalize. lease-tutorial becomes lease_tutorial for use paths. If you start with hyphens in your package name, expect underscores everywhere else.
Editions are strings. Edition "2025" is current. Editions are parse-time only; no runtime split.

Putting it in the running example

What you have now is the skeleton the rest of the book extends:

lease-tutorial/
├── ox.toml
└── src/
    ├── metatypes.ar       # the small set of metatypes we need
    ├── party.ar           # Person (and soon Tenant, Landlord)
    ├── prelude.ar         # curated re-exports — public surface
    └── root.ar            # project entry — pulls submodules in

Chapter 2.2 extends party.ar and adds lease.ar. By the end of Part 2 the package has rules, queries, computes, mutations, and refinement types. By the end of Part 3 it has a state machine, tests, and diagrams. The complete running version lives in examples/lease-tutorial/ alongside this book.

Summary

A working Argon package is ox.toml plus a src/ tree of .ar files. The manifest names the package, pins dependencies, and configures reasoning. Modules are files; the prelude curates the public surface; pub use re-exports propagate. ox check keeps you honest. The next part teaches what to put into those modules.

Keyboard shortcuts

The Argon Programming Language