Albite

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:

OptionEffect
--jsonErrors as JSON with structured diagnostic hints
--max-errors <n>Cap the errors shown; 0 for no limit (default 20)
--no-cacheForce 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 return and 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.

OptionEffect
--filter <substring>Run only tests whose name contains the substring
--module <path>Scope discovery to one module source file
--check-onlyCompile-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:

SubcommandExplains
error <code>An elaboration error kind
type <type>A structural Core IR type, step by step
recursion-typesRecursion classification categories
stack-overflowStack overflow crashes in Albite programs
mutual-recursionMutual 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.