Compiler details

The pipeline

elfie does every step but Generate and Verify itself, and those steps are deterministic. The two agent steps are the only places a model is involved, and both are checked by the steps after them.

Units and batches

A unit is one definition file compiled for one target: def/main.lfy for hello is the unit main. A unit's name, its stem, is its path under def/ without .lfy. A file that declares nothing to build, such as one holding only targets, traits, or global criteria, gives no unit.

Units are grouped into batches in plan order, by the first segment of their stem: at most six units, or 60,000 characters of source, per batch. One request goes out per batch, so guidance and interfaces are sent once.

Why a unit is planned

Dependencies are compared by interface, meaning each entity's name, kind, description, type, parameters, and output. A change inside a dependency's criteria or body plans only that dependency, not every unit that uses it.

Markers and source maps

The compiler marks every item it writes with a comment that names the entity it comes from, and, for code written to satisfy one criterion or test, that criterion's id.

apps/main/src/components/callout.tsx

// @lfy def/components/callout.lfy:InfoImage
export const InfoImage: string = "/elfie/info.svg";

// @lfy def/components/callout.lfy:Callout#Callout:component:dcdaadb98aeb…
export function Callout({ header, content }: CalloutProps) {

A marker starts with the target language's line comment, then @lfy, the definition file, and the entity. After # comes the id of a criterion: here one that Callout received from the component trait. A marker names an entity, never a line, so markers survive edits that move lines. A region runs from one marker to the line before the next. When a unit is accepted, its regions are recorded in elfie-compile/maps/<target>/<stem>.json. The CLI, the language server, and the agent tools use these maps to trace between definitions and code in both directions.

Outcomes

The compiler ends each run by submitting one of three outcomes.

A batch whose outputs fail acceptance, or whose review finds a violation, is sent back to the compiler once with the problems appended. A second failure stops it. With --continue, batches that don't depend on a stopped one keep going.

Verification

The verifier is a second agent that didn't write the code. It reads each criterion and test, the regions marked for it, and, when it has to, runs the tests.

Reviews are incremental. A verdict carries over while its entity's regions are unchanged, ignoring marker lines. elfie verify --full judges everything again. Global criteria are reviewed once for the whole program, after every merge.

Shortcuts

• Reworded only. When a unit's criteria were only reworded in place, elfie moves the markers to the new ids and sends the batch straight to review, skipping the compiler.
• Dependency only. When every unit of a batch is planned only because a dependency changed, elfie runs the target's build and test first. If both pass, the outputs are accepted as they are.

Running in parallel

With --jobs above 1 in a git repository, each batch runs in its own copy of the project, and a batch can start as soon as everything it depends on is accepted. Batches are merged into your working tree in dependency order, so it only ever holds reviewed work. When a batch is rejected twice, its work is kept under elfie-compile/cache/kept/, and the next compile resumes from it if nothing it was built against has changed.

The agent server

The compiler and the verifier read your program through elfie's agent server rather than raw files, so every answer is resolved and exact.

Language choices

Choice

Ambiguity is a compile error

A compiler that guesses produces code no one asked for. When a criterion reads two ways, the compiler stops and quotes it.

→

Choice

The compiler is a command

elfie embeds no model. elfie.json names any command, so you choose the agent and its harness, and can change them without changing your code.

→

Choice

Criteria are never named

Names drift and collide. A criterion is identified by an id built from what it's for, who wrote it, and what it says, and cited by file and line.

→

Choice

Knowledge is vendored

Knowledge is read from files, never fetched. Every compile reads the same text, and none depends on the network.

→

Choice

Targets live in source

A target is an ace const assembled from packages. Adding a stack never means changing the compiler.

→

Choice

Markers name entities

Markers name the entity, not the line, so they don't drift when definitions move. Lines are derived when output is accepted.

→