Command-line reference
The albite binary carries a large surface, most of which exists to diagnose
the compiler rather than to write programs in it. This page covers the
user-facing subset. Run albite commands --tree for the full listing.
check
albite check <file>
Type-checks and stops — no code generated, no LLVM required. This is the command to run while writing.
✓ hello.tg: 1 definition(s), all OK
Useful options:
| Option | Effect |
|---|---|
--json | Errors as JSON with structured diagnostic hints |
--max-errors <n> | Cap the errors shown; 0 for no limit (default 20) |
--no-cache | Force a full re-elaboration |
--termination <level> | all (default), proofs or report — how hard the termination check is enforced; see Recursion the compiler can see ends. Also on run, test and compile |
run
albite run <file>
Type-checks, then evaluates with the built-in interpreter. No LLVM required.
Prints the value main evaluated to — so a String result appears quoted.
A bare albite <file> is shorthand for albite run <file>.
Two known cases where the interpreter disagrees with compiled output — early
returnand same-named cross-module imports — are listed under Current limitations. Compiled output is correct in both.
compile
albite compile <file> -o <output>
Lowers through LLVM to a native executable. Requires LLVM 18; this is the only command that does.
ALBITE_ARENA — how a compiled program allocates
Since 2.0-alpha
Every natively compiled Albite program reads one environment variable, once, when it starts:
ALBITE_ARENA=off ./myprogram # the default: the system allocator
ALBITE_ARENA=bump ./myprogram # a bump-pointer arena, 4 MiB chunks
ALBITE_ARENA=bump:64 ./myprogram # the same, 64 MiB chunks
It is a run-time setting of the program, not a compiler flag: the same
binary runs either way, and nothing about the program’s behaviour changes —
only how its memory is obtained. Under bump, allocating is a pointer
increment and memory is returned in one go at exit; on the compiler’s own
benchmarks that runs 1.3–1.7× faster, and on the compiler checking itself it
cut peak memory by about a sixth. A value the program does not recognise
prints one line — ALBITE_ARENA not recognised (want off | bump[:chunk_mib]) —
and the program runs with the arena off.
The interpreter (albite run) does not use it, and neither does
albite-bootstrap. The macOS release’s albite is itself a compiled
Albite program — the self-hosted compiler — so it does read the variable.
test
albite test <file>
Discovers and runs top-level test_* functions — arity 0, returning Unit.
| Option | Effect |
|---|---|
--filter <substring> | Run only tests whose name contains the substring |
--module <path> | Scope discovery to one module source file |
--check-only | Compile-time assertions only; skip evaluation |
--watchdog <secs> | Per-test wall-clock limit |
Two assertion forms are checked at elaboration time, so they need no codegen:
expect_type(expr, "Nat") // the expression's inferred type
expect_error(expr, "E0010") // the error code the expression produces
eval
albite eval "2 + 2"
4
Evaluates a single expression. Handy for settling a question about precedence or an operator without creating a file.
explain
albite explain error E0010
Explains an error code, a Core IR type, or a compiler concept:
| Subcommand | Explains |
|---|---|
error <code> | An elaboration error kind |
type <type> | A structural Core IR type, step by step |
recursion-types | Recursion classification categories |
stack-overflow | Stack overflow crashes in Albite programs |
mutual-recursion | Mutual type recursion and its effect on encoding |
keywords [<name>] | The reserved words — or whether one name is free to use |
Diagnostics
Since 2.0-alpha
One mistake, one error. When a definition fails — a type that names
something that does not exist, say — the compiler reports that failure once,
where it happened, and does not go on to report every place that uses the
broken definition. A type with a bad field used from three other modules is
one error, at the field, not four. So the first error in the output is
the one to fix; the compiler’s regression test for this is
tests/golden/error/record_body_fault_reports_once/ in the repository.
Every error has a code, and every code has an explanation. The code is the
bracketed part of the first line — [E0062] Error: …:
albite explain error E0062 # what it means, and how to fix it
albite explain error # every user-facing code
--max-errors <n> caps how many are printed (default 20; 0 for all).
A parse error pointing at something that looks fine usually means the word
before it is reserved. The proof keywords are the ones that catch people —
by, have, show, sym, trans, cong, subst, refl are all reserved,
so fn f(sym: Nat) fails to parse. albite explain keywords <name> answers
whether a name is free.
cache
albite cache status
albite cache clean
Elaboration results are cached to make re-checking fast. clean removes them —
worth doing if you suspect a stale result after upgrading the compiler.
repl
albite repl
An interactive prompt for evaluating expressions.
Beyond this page
albite info, albite doctor, and albite diff are compiler-diagnostic
namespaces — inspecting type encodings, checking internal invariants, comparing
generated IR. They are documented in the repository rather than here, since they
are for working on the compiler rather than with the language.