The REPL and editor tools#

Alpha has one implementation of the language, and every interactive tool answers from it: the browser REPL on this site, alpha repl in a terminal, and the language server and debugger adapter behind an editor. None of them models the language separately, so none of them can disagree with alpha check.

The browser REPL#

The REPL takes one module, checks it with the real compiler, and, if you ask it to evaluate, types and normalizes main. Ctrl+Enter (⌘+Enter on a Mac) runs it.

What it is, exactly:

• Reference evaluation, not native execution. main is normalized by the compiler's trusted normalizer. Nothing is compiled to machine code, and nothing runs on a device. The answer's boundary is labelled checked or checked-and-reference-evaluated.
• One isolated module. Your source becomes src/Main.alpha in a fresh, temporary workspace that is deleted afterwards. Choose the alpha-2026 or alpha-2027 edition.
• Bounded. Source is limited to 16,000 characters. The check runs under a compiler budget of 5 seconds and 512 MiB of allocation. Every compiler process runs in a sandbox with no network, all capabilities dropped, a read-only runtime, an 8-second wall-clock limit, 6 seconds of CPU, 2 GiB of address space, 16 MiB files and 64 open files. Output is capped at 64 KiB.
• Shared. One evaluation runs at a time across the whole site, and each visitor may make 12 requests a minute. A busy compiler answers try again in a moment rather than queueing without bound.

The REPL never claims more than it did: it does not imply native emission, hardware execution or physical attestation.

alpha repl#

The terminal REPL loads a root and its whole closure through the incremental engine, then answers questions about terms with the same kernel the compiler uses:

$ alpha repl --edition alpha-2027 --root Hello.alpha
alpha repl — :help for commands, :quit to leave. Evaluation here is reference execution.
loading ./Hello.alpha ...
loaded 1 modules, 2 definitions
alpha> :type double
(pi unrestricted n : Nat . Nat)
alpha> :normalize main
reference evaluation: (nat-literal 42)
alpha> :core (double 21)
(app (Hello.double) (nat-literal 21))
alpha> :erase (succ (succ zero))
3 runtime nodes, digest 030302

(Hello.alpha is the module from Getting startedLearn · startGetting startedBuild the compiler, run a first program, and build a GPU training executable..)

A term that does not check is never evaluated, and effectful terms are refused rather than interpreted on the host. :erase works on closed terms: a term that names a global definition is refused with ALPHA-ERASE-FAILED. --transcript FILE records the session as a transcript that alpha test can replay.

Editors#

alpha lsp is a Language Server Protocol server on stdio, and alpha debug is a Debug Adapter Protocol adapter. Neither contains language knowledge of its own:

The closure check runs when the workspace opens and on save. Editing a document re-indexes only that document, so engine diagnostics reflect saved bytes while lint findings follow the buffer.

VS Code. The extension in editors/vscode starts alpha lsp in the workspace folder and registers the alpha debug type. Build alpha, put it on PATH or set alpha.serverPath, then install the extension from source (cd editors/vscode && npm install, then F5 or vsce package). Its syntax grammar is generated from the edition's feature registry, so its keywords cannot drift from the language.

Other editors. Any LSP client can run alpha lsp from the workspace directory, and any DAP client can run alpha debug.

Debugging. The adapter launches an artifact, reports its exit status, answers debug-console expressions by reference evaluation, and verifies breakpoints against the compiler's source map: a line emitted code came from verifies, and any other line is refused with the lines that would work. Stepping, local values and disassembly are not supported yet, and the adapter says so in its capabilities rather than offering buttons that cannot work.

Read next#

• The language serverTooling · explanationLanguage serveralpha lsp: what each editor request is answered from, what it costs, and the VS Code extension. and the debugger adapterTooling · explanationDebugger adapteralpha debug: launch, evaluate, source-map-verified breakpoints, and what is declared unsupported.: the details.
• Command-line referenceTooling · explanationCommand-line referenceEvery alpha command with its flags, profiles, exit statuses, JSON events, receipts and resource budgets.: every command, profile, exit status and event.
• FormatterTooling · explanationFormatterWhat alpha fmt guarantees: parse, declaration and comment preservation, idempotence, and its one style.: what alpha fmt guarantees.