Modules and packages

Modules

A module is a unit of scope. A .ar file is a module named for its stem; a directory with a mod.ar is a module whose siblings are its submodules; mod Name { … } nests one inline. A bare mod Name; declares that a sibling Name.ar exists and attaches it — Rust’s child-module declaration, and the only meaning the form carries. A file does not rename itself, and a content-bearing file whose mod Name; resolves to no sibling is refused rather than silently relabeling its own contents.

Visibility follows Rust. A default-visibility item is private to the module that declares it and every descendant, so a private item at the package root is visible package-wide; pub exposes it to dependents, pub(pkg) limits it to the package. use brings names into scope — single, brace-list, glob, and aliased forms — and a pub use re-exports, joining the importer’s public surface. A qualified path walks from a root: pkg:: is the current package’s self-reference, stable across a rename; self:: and super:: step through the module tree; a leading dependency name resolves into that dependency; std:: is always available. Resolution of a bare name tries local scope, then imports and the package prelude, then the language substrate — the primordial types and built-in forms that are always in scope and not a library. Nothing else is ambient: even the type and rel introducers are brought in explicitly, by use std::core::{type, rel} or a package prelude, which is how the language stays vocabulary-neutral.

Packages

A package is a module tree with a manifest. ox.toml is Cargo-flavored — a [package] with a name, version, and edition, a [dependencies] table, an optional [lattice] ceiling that caps the decidability tier the package may reach, and an optional prelude of use-tails auto-prepended to every module. The prelude is empty by default and carries no vocabulary; a package opts its introducers in.

When one module imports another, the elaborator does not pull the whole imported theory in. It extracts a ⊥-locality module: the smallest subset of the imported axioms that stays non-trivial once every concept outside the used signature is reinterpreted as the empty concept. Extraction is a fixpoint, linear per iteration, terminating in a bounded number of steps. Its guarantee is Σ-scoped conservativity: every entailment about the used signature survives. Argon strengthens the classical result for its own semantics — closed-world conclusions are preserved, ghost individuals reachable only through unused concepts are pulled in, defeasible rules drag in their defeaters (a classical extractor is unsound under non-monotone semantics), and extraction composes across an import chain. All of it is mechanized in the Lean’s locality layer. Extraction is also how decidability tiers compose across heterogeneous modules: each extracted module is classified on its own, and conservativity guarantees no entailment is lost in the seam.

A dependency is a path or a registry reference. A path dependency loads a local checkout and folds its pub surface into the workspace under the dependency name; a vocabulary package is consumed exactly this way, with vocab = { path = "../vocab" } in the manifest and use vocab::{ kind, Substantial }; bringing its introducers and categories into scope, so the consumer writes pub kind Person <: Substantial against vocabulary it does not own and a check shipped with that vocabulary fires on the consumer’s catalog. A registry dependency resolves against a content-addressed registry served over the toolchain CDN: blobs are keyed by hash, a package name resolves to a single version across the whole graph — nominal type identity admits no two — and resolution runs PubGrub over the version constraints, reporting an unsolvable conflict with its derivation chain rather than guessing. A registry dependency with no configured index is refused with a diagnostic that names the fix rather than silently resolving to nothing. The reference fixes the manifest and resolution surface under modules and packages.