docs: bring the prose up to 0.5.0, and give CI something to run

[simontreanor]

The 0.5.0 features reached every machine-readable surface (parser, TextMate grammar, all four tree-sitter query sets) and only one prose one, so the documents disagreed with the compiler and with each other.

Prose currency

option {} is the fourth built-in computation expression. DESIGN.md said "exactly three, no more" in its §11 guardrails while saying four in §8.1; RATIONALE.md, README.md and the Marketplace-facing editors/vscode/README.md each said three. §11 now states the closing rule (one per built-in short-circuit type, one per Python control-flow form) rather than a count, and drops the user-defined-CE deferral, which shipped.

Everything below was checked against src/, not against another document:

What it said	What is true
DESIGN.md §8.1: "whitespace-insensitive (no offside rule at all — lexer/mod.rs)"	src/lexer/mod.rs:3 documents the offside rule it implements
INTERNALS.md: desugar/, types/units/, cli/ (clap), prelude/	none exist; Cargo.toml [dependencies] is empty, so there is no clap and no fmt subcommand. src/project/, src/repl.rs, src/kernel.rs and the three lowering/ sub-passes were missing
internals tour: CeItem::LetBang { name, name_span, value }	carries a Pattern since #57
internals tour: build_call partial application	beta_reduce runs first since #52, so (+) 2 is lambda b: 2 + b
examples/interop/README.md: the extern import prefix "mis-reads a lowercase class as a submodule"	since #50 it refuses and names the extern import to add
editors/README.md	told Emacs users to hand-roll a mode we ship, and called the JetBrains plugin aspirational two paragraphs after saying it exists
editors/vscode/DEVELOPMENT.md	recommended vsce publish, the path RELEASING.md and the ROADMAP both record as broken

The VS Code TextMate grammar highlighted in, which is not in Tok::keyword, and did not highlight import, try or as, which are. JetBrains ships that same grammar. editors/nvim/syntax/pyfun.vim had the same two errors, and editors/emacs/pyfun-mode.el had no CE-builder highlighting at all.

RELEASING.md said "all four files" over three bullets, and claimed the Assisted-by: header MELPA asked for was already in pyfun-mode.el. It was not — that would have blocked the resubmission that reopens mid-August. It is now, in MELPA's documented AGENT_NAME:MODEL_VERSION form. The doc also claimed every versioned artifact tracks the compiler; two are deliberately independent, so it now names the tracked set instead.

The CI gap

Nothing ran cargo test, cargo clippy or cargo fmt --check on a PR or on main — the only cargo call in any workflow was a build --release inside the kernel job. That is why a release could ship with the drift above.

ci.yml adds the three commands CLAUDE.md names (tests on all three OSes, since the e2e suite shells out to Python; lint once), plus the lesson verifier, which is executable documentation: every lesson solution runs and its output is compared against what the lesson prints.

docs/verify_lessons.py could not have run in CI — it hardcoded C:\git\Pyfun — and worse, it silently validated against whatever binary happened to be in target/debug. In this working tree that was a 0.4.0 build, so it reported all 23 lessons green against the wrong compiler. It now resolves its own repo, honours PYFUN_BIN (the convention kernel.yml already uses), and refuses a compiler older than Cargo.toml.

Also

examples/hello.pyfun is the showcase file and had no option {} block; it does now. pages.yml was two majors behind on actions/checkout. The tree-sitter README documented tree-sitter parse but not the corpus goldens that are the actual gate.

Verification

cargo test (all suites), cargo clippy --all-targets -- -D warnings, cargo fmt --check, python docs/verify_lessons.py (23/23), and pyfun run examples/hello.pyfun all pass locally.