WEP: Spec Examples Quote Fixtures

Context

The specification is normative: it says how the language should behave. Nothing holds it to that. Its 353 wado code blocks are never compiled or run, so an example can be wrong from the day it is written, or turn wrong when the language moves, and no check notices.

Measured when this WEP was written, wado check over each block as written, and again wrapped in a function body:

Outcome	Blocks	Main causes
Compiles	124
Parse error	101	items and statements mixed at the top level; `...` placeholders (~60)
Name or type error	128	fragments naming what they never declare; examples meant to be errors

The e2e fixtures, by contrast, are checked on every run, and AGENTS.md already names them as where the language's behaviour is stated. Two blocks out of 353 appear in any fixture, and only once indented.

How other ecosystems hold a specification

CommonMark extracts the examples from its specification and runs them as its test suite.
The Rust Reference gives each rule an identifier, and rustc's tests name the rules they cover, so a tool reports the rules no test reaches.
ECMAScript's test262 tags each test with the section it tests, and a proposal reaches Stage 4 only with tests and two implementations.
WebAssembly writes its specification in a DSL that generates the prose, the formal rules and the proof-assistant definitions, beside a reference interpreter and a shared test suite.

The first makes the examples true. The second ties every rule to a test.

Decision

A code block in the specification is a quotation of an e2e fixture.

The rule

Every ```wado block in docs/spec-*.md names a fixture or a source file.
The named file contains the block verbatim: its lines, in order and contiguous, each shifted by one indentation prefix shared by all of them. A blank line matches a blank line.
Any number of blocks may name one file.
A block whose fixture does not expect a compile error contains at least one assert, unless its reference waives the rule. This rule is provisional: the first migrated file decides whether it holds or is absurd, and it is dropped if absurd.

The reference is an HTML comment holding a JSON object, the block directly before the fence in the same container. The formatter puts a blank line between the two, and GitHub does not render the comment, so the reader sees an ordinary code block:

<!-- {"fixture": "cast_fn_type_newtype.wado"} -->

```wado
type Meters = f64;
let double = (|x| x + x) as fn(Meters) -> Meters;
assert double(1.5 as Meters) == 3.0 as Meters;
```

The comment is data, so JSON says what it may hold, and no syntax of its own needs a rule. A comment whose body does not open with { is no reference, which leaves room for a formatter directive. One that does is a reference: it holds exactly one of fixture and source, and may hold "assert": false. A body that fails to parse, holds another key, or gives assert any other value is an error, so a misspelled key is caught rather than read as no reference.

A fixture path is relative to wado-compiler/tests/fixtures/ and is read the way the suite reads it. A file at the top level is a fixture the suite runs, and the block is matched against the code before its __DATA__. A file below it is a helper module, which the suite compiles only through a fixture that imports it, directly, through another helper, or as a dependencies entry. The checker follows those paths from the top level and requires one to reach the helper. The block is matched against the whole file, __DATA__ included, since a helper's data is content that #data reads, not an expectation. The assert rule does not apply, as the fixture importing it states the claims. A two-file example quotes each file.

A source path is relative to the repository root and names a file outside the fixtures: a standard library module, a unit test's input, a package's source. The block is matched against the whole file, and the assert rule does not apply. A source naming a fixture is an error, since it would step around both rules above.

Why a quotation, and not a generated test

A fixture already carries what an example needs: the declarations around it, the expectation in __DATA__, and a run at every optimization level. Quoting it needs no generator, no wrapping rule for fragments, no hidden setup lines and no second expectation syntax. The check is a file lookup and a substring match.

The link is also checked from both sides. Editing the example without the fixture breaks the match, and so does renaming, deleting or rewriting the fixture. A copy with no link drifts silently in either direction.

The reference is the traceability a rule identifier would give: a rule's example names the test that holds it.

What follows from the rule

A ```wado block is always real Wado. A shape sketch with ... placeholders or a grammar outline is ```text.
The indentation allowance is what lets a fragment stand in the specification: let p = …; assert …; sits inside a test { } in its fixture, four spaces in.
A claim an example makes about a value is written as an assert in the block, not as a comment. The claim is then part of the quoted text and runs. A comment such as // 3.14 is checked by nothing, which is what the assert rule targets. A test's #[expect_trap] or #[TODO] is a claim too: the runner holds the body to trapping, so a trap example needs no assert written for the sake of the rule.
An example whose claim is that it compiles has no value to assert: the fixture's run already shows it. Its reference writes "assert": false, as the #[benign] example's does. The waiver is allowed only on a fixture the suite runs, the one place the rule applies.
A compile-error example quotes a fixture declaring compile_error or compile_error_codes. One fixture expects one report, so each rejected example has a fixture of its own.
A fixture is excluded from the formatter ([format] exclude), so its layout stays as the specification quotes it.

The checker

The checker is package-gale-highlight-wado/tools/spec_examples.wado, beside the Wado.g4 grammar it lexes with, so it counts an assert keyword only where the lexer finds one, not in a comment or a string. It reads the Markdown with Marl. scripts/check-spec-examples.sh drives it with wado run, as scripts/check-rust-paths.sh drives package-gale/tools/rust_inline_paths.wado.

A block that breaks any rule, naming nothing among them, fails the check.

A #[TODO] rule was dropped: it asked a WEP to name every fixture marked #[TODO] that a block quotes, as a known gap. A marked fixture is not always a gap. The example of a #[TODO] test is itself marked, by design.

Marl's fenced_code_blocks gives the checker what it reads of each fenced block: its info string, its text, its source line, and the text of the comment block directly before it. Marl's document tree stays internal.

Rollout

During the migration a baseline, scripts/spec-examples.json, counted the blocks of each file that had no reference yet, and CI failed when a count grew. It only shrank, as scripts/rust-inline-paths.json does, and was deleted once empty.

Migrating a block is triage. Each one is exactly one of:

correct, and quoted from an existing or new fixture;
a sketch, and turned into ```text;
meant to be rejected, and quoted from a compile_error fixture;
wrong in the specification, and the specification is fixed;
right, but the compiler disagrees: a #[TODO] fixture and a WEP known gap.

The last two are what this WEP is for. The migration will find them.

Roadmap

[x] Extend Marl with a public read of the fenced code blocks: info string, text, source line, and the HTML block directly preceding each. An HTML comment now ends at -->, not at the next blank line, as CommonMark says.
[x] Write the checker, TDD against small Markdown and fixture cases: the reference, the indented substring match, the assert rule, the #[TODO] rule and the baseline.
[x] Add mise run check-spec-examples and its CI job, and record the baseline of all 353 blocks.
[x] Migrate one file first, spec-types.md, and decide the assert rule from it: keep it, or drop it and say why here. Kept. Its 42 blocks became 55 quotations and one ```text, since a rejected example is now a block of its own; 8 quote a compile_error fixture. In most of the rest the assert replaced a comment that stated a value. A block made only of declarations quotes the test that uses them, which closes the first known gap for that block. The assert was artificial in three: a type-level claim of inference, a field visibility, and a #[cm] name. The migration found one block wrong in the specification: a float vector's comparison mask is the integer vector of the same width, not the float one.
[x] Migrate the other twelve spec files, one change per file. The migration found compiler bugs, fixed on the way: a trait turbofish counting parameters the trait does not write, an associated type's bound pinning a type to Self, the locals of a body other than a function's, and a standard library attribute accepted in a program. It found two gaps, each now a WEP known gap: a CM operation bound by its spelling, and an inline with { path }. A block with no fixture to run could still quote a real file, so a reference may name a source.
[x] Delete the baseline, so the rule holds with no exceptions.

Known gaps

The match proves the quoted text compiles in its fixture, not that the fixture exercises it. A block quoted from a function no test calls passes.
A source quotation is held to its file alone. Nothing asks that the file is compiled or run.
The cheatsheet repeats the specification's examples in a shorter form, and nothing holds it to this rule.