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

.github/workflows/ci.yml

@@ -0,0 +1,71 @@
+# The project's own gate: the three commands CLAUDE.md names (test, clippy, fmt)
+# on the pinned toolchain. Everything else in .github/workflows publishes or
+# deploys something; this is the one that decides whether a change is sound.
+#
+# Tests run on all three OSes because the end-to-end suite shells out to a Python
+# interpreter and the emitted code has to run everywhere the wheel installs.
+# Clippy and fmt are toolchain-deterministic, so once is enough for them.
+name: ci
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ci-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  test:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v6
+      # Pyfun targets Python 3.12+ (the emitted code uses `match` and PEP 701
+      # f-strings). Without an interpreter the e2e tests skip rather than fail,
+      # which would quietly hollow out this job.
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.12'
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: '1.97.0'
+      - uses: Swatinem/rust-cache@v2
+      - run: cargo test
+
+  lint:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: '1.97.0'
+          components: clippy, rustfmt
+      - uses: Swatinem/rust-cache@v2
+      - run: cargo clippy --all-targets -- -D warnings
+      - run: cargo fmt --check
+
+  # The learner track is executable documentation: every lesson's solution runs
+  # and its output is compared against what the lesson prints. A compiler change
+  # that alters a diagnostic or a stdlib suggestion shows up here.
+  lessons:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.12'
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: '1.97.0'
+      - uses: Swatinem/rust-cache@v2
+      - run: cargo build
+      - run: python docs/verify_lessons.py

.github/workflows/pages.yml

@@ -33,7 +33,7 @@ jobs:
       name: github-pages
       url: ${{ steps.deploy.outputs.page_url }}
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v6
 
       # Match the toolchain pinned by rust-toolchain.toml, with the wasm target.
       - uses: dtolnay/rust-toolchain@master

.github/workflows/wheels.yml

@@ -125,8 +125,9 @@ jobs:
   # this tag. The Marketplace publish itself stays manual (drag the .vsix into
   # https://marketplace.visualstudio.com/manage/publishers/pyfun). CLI publishing
   # is a dead end here (see the vsce --azure-credential bug). The vsix carries the
-  # version from editors/vscode/package.json, which is independent of the pip tag,
-  # so bump it there before tagging when the extension itself changed.
+  # version from editors/vscode/package.json, not the tag, so bumping it is step 1
+  # of RELEASING.md — every release, whether or not the client itself changed, so
+  # that a user comparing the extension against `pyfun --version` sees one number.
   vscode-extension:
     name: Package VS Code extension
     runs-on: ubuntu-latest

DESIGN.md

@@ -1009,7 +1009,7 @@ Differences from Python that the MVP commits to:
 | Application    | `f(a, b)` n-ary             | `f a b`; `f a` is a partial application       |
 | Pipe           | none                        | `x \|> f \|> g` (= `g(f(x))`)                  |
 | Effects        | untracked                   | tracked in the type (§4)                      |
-| Comp. exprs    | none (ad-hoc `async`/gens)  | `async {}` / `seq {}` / `result {}` (§8)      |
+| Comp. exprs    | none (ad-hoc `async`/gens)  | `async {}` / `seq {}` / `result {}` / `option {}` (§8) |
 | Units          | none                        | units of measure, compile-time only (§8)      |
 
 **Functions are curried by default** (F# style): `let add a b = a + b` has type
@@ -1614,12 +1614,12 @@ case: being indentation-sensitive, it *forbids* blocks in expression position (h
 single-expression `lambda`); an expression-oriented language that went indentation-only for CEs
 would inherit exactly that limitation. So Pyfun keeps the braces deliberately, not by inheritance:
 
-- Pyfun is currently whitespace-insensitive (no offside rule at all — `lexer/mod.rs`), so the `{ }`
-  is the *only* thing delimiting a CE block today.
-- The contextual-keyword scheme (`async`/`seq`/`result` are keywords *only* immediately before `{`)
+- Pyfun's offside rule (`lexer/mod.rs`) delimits *statements and blocks*, not an expression embedded
+  mid-expression, so the `{ }` is what delimits a CE block.
+- The contextual-keyword scheme (`async`/`seq`/`result`/`option` are keywords *only* immediately before `{`)
   depends on the explicit brace as its disambiguator.
-- A future offside rule for `let`/`match`/function bodies is **orthogonal** and composes with this
-  (exactly as in F#): adding it would not require changing CE or record braces. Records (§8.3) reuse
+- The offside rule for `let`/`match`/function bodies proved **orthogonal** and composed with this
+  (exactly as in F#): adding it required no change to CE or record braces. Records (§8.3) reuse
   `{ }` as well, so the brace family stays consistent.
 
 ### 8.2 Units of measure
@@ -1906,10 +1906,14 @@ accreting features. The MVP showcase set (§8) is a *deliberate, fixed* exceptio
 outside it is deferred. Hold the line:
 
 - **Do not fork CPython** — Pyfun is a front end targeting Python, full stop.
-- Beyond the MVP (effects + the three CEs + units), defer **user-defined CE builders**, **unit
-  polymorphism** (if not trivially free), macros, and a package manager until the core is solid.
-- Ship **exactly three** built-in computation expressions (`async`/`seq`/`result`) — no more — and
-  a **small** built-in unit set. Generality comes after the MVP proves out.
+- Beyond the MVP (effects + the CEs + units), defer **unit polymorphism** (if not trivially free),
+  macros, and a package manager until the core is solid. **User-defined CE builders** were on this
+  list and came off it once the core settled: they desugar through machinery that already existed
+  (§8.1), so they cost no new checking rules.
+- The built-in computation expressions are **closed by a rule, not by a count** (§8.1): one per
+  built-in short-circuit type (`Option`, `Result`) and one per Python control-flow form (`async`,
+  `seq`). That is four, and there is no fifth candidate — which is what stops "add one more" from
+  becoming a habit. The built-in unit set stays **small** for the same reason.
 - Syntax is cheap; resist inventing more. Parser quality, error quality, and predictable lowering
   are what make the language usable — spend effort there.
 - Keep the effect lattice small until real programs justify expanding it.

INTERNALS.md

@@ -14,25 +14,35 @@ grow large and must not bleed together.
 
 ```
 src/
-  lexer/           tokenizer, token types, lex errors
-  parser/          recursive-descent + precedence climbing; ast.rs = Expr/Pat/Ty/Stmt
+  lexer/           tokenizer, token types, lex errors, the offside rule
+  parser/          recursive-descent + precedence climbing; ast.rs = span-carrying AST
   ast/             traversal + visitor utilities, pretty-printer
-  desugar/         computation-expression desugaring (DESIGN §8.1): builder{} → bind/return/…
-  types/           HM inference + effect inference/checking, exhaustiveness
-    units/         units-of-measure inference: abelian-group unit unification (DESIGN §8.2)
+  desugar.rs       computation-expression desugaring (DESIGN §8.1): builder{} → bind/return/…
+  types/           HM inference + effect inference/checking, exhaustiveness, units (DESIGN §8.2)
   lowering/        Pyfun AST → Python-AST IR; scope/name-binding analysis; unit erasure
-  python_emitter/  Python-AST IR → readable source
+    fold_loop.rs     hot folds become loops (DESIGN §5.1)
+    decode_spec.rs   statically-known decoders deforest (DESIGN §5.3)
+    self_tail_call.rs a saturated self tail call becomes `while True` (DESIGN §5.4)
+  python_emitter/  Python-AST IR → readable source (py311.rs = the --target 3.11 rewrite)
   diagnostics/     rustc-style errors: codes (E001…), levels, spans, notes
-  cli/             clap-based; subcommands compile/check/fmt/lsp
+  project/         module graph: acyclic import resolution, cross-module checking
   lsp/             front-end-first language server (stdio JSON-RPC)
     json.rs        hand-rolled, dependency-free JSON value + parser + serializer
-prelude/           Pyfun/Python runtime support (Result/Option ADTs, etc.)
+    resolve.rs     AST resolver: symbol_at / find_references / definitions
+  repl.rs          read-eval-print loop over one long-lived Python worker
+  kernel.rs        the REPL session inverted, for the Jupyter kernel
+  main.rs          the CLI: check/compile/run/parse/lsp/repl/kernel-engine
 editors/vscode/    minimal VS Code client that launches `pyfun lsp`
 tests/             parser tests, compile tests, .pyfun fixtures (favor snapshot/golden tests)
 ```
 
-**Build order:** `lexer` + `parser` + `ast` → `desugar` → `types` (incl. `units`) →
-`lowering` + `python_emitter` → `diagnostics` + `cli` → `lsp`.
+The shared Python runtime support (the `Option`/`Result` classes) is not a directory: it is
+generated by `lowering::runtime_module()` into a `_pyfun_rt.py` beside the emitted output.
+There are no dependencies — `Cargo.toml`'s `[dependencies]` is empty, so the CLI is hand-rolled
+argument parsing rather than clap.
+
+**Build order:** `lexer` + `parser` + `ast` → `desugar` → `types` → `lowering` +
+`python_emitter` → `diagnostics` + `main` → `project` → `lsp`.
 
 ## Opaque types (newtype erasure) — implements DESIGN §7.3
 

RATIONALE.md

@@ -102,8 +102,8 @@ know it is safe.
 ## Currying that reads as plain calls
 
 Functions curry by default. A fully applied call compiles straight to a direct call, so `f a b c`
-becomes `f(a, b, c)`. Closures appear only when you partially apply, where they compile to
-`functools.partial`. The `|>` pipe is sugar that resolves at compile time and costs nothing at runtime.
+becomes `f(a, b, c)`. Closures appear only when you partially apply, where a named function compiles
+to `functools.partial` and a lambda closes over the argument directly, so `(+) 2` is `lambda b: 2 + b`. The `|>` pipe is sugar that resolves at compile time and costs nothing at runtime.
 
 The Python side stays n-ary in both directions. You call an imported Python function with normal syntax,
 and a Pyfun function you expose to Python has a plain `def` signature. Python callers work with ordinary
@@ -129,8 +129,8 @@ you handle rather than a crash. The `examples/interop/` cookbook shows the patte
 
 ## A small surface, on purpose
 
-Pyfun keeps a deliberately small surface. There are three computation expressions, `async`, `seq`, and
-`result`, and a fixed set of built-in units. The reason is that parser quality, error quality, and
+Pyfun keeps a deliberately small surface. There are four computation expressions, `async`, `seq`,
+`result` and `option`, and a fixed set of built-in units. The reason is that parser quality, error quality, and
 predictable lowering are where the effort pays off, so the language spends its budget there rather than
 on breadth. User-defined CE builders arrived after the core settled, because they desugar cleanly
 through machinery that already existed.

README.md

@@ -266,7 +266,7 @@ let force = 10<N>
 let side = sqrt 16.0<m^2>       # float<m>, unit-aware roots
 ```
 
-**Computation expressions** (F#'s showcase feature): `result`, `seq`, `async`, plus your own:
+**Computation expressions** (F#'s showcase feature): `result`, `option`, `seq`, `async`, plus your own:
 
 ```fsharp
 let checked ok v =
@@ -289,9 +289,9 @@ let path = r"C:\Users\pyfun"    # raw string, backslashes literal
 ```
 
 And a standard library that reads like F#'s: module-qualified `List` / `Set` / `Map` / `Option` /
-`Result` / `Seq` / `String` (`List.map`, `Map.tryFind`, `Result.bind`, lazy `Seq.take`,
-`String.split`), tuples, active patterns, typed holes for type-driven development, and
-multi-file projects with `import`.
+`Result` / `Seq` / `String` / `Format` (`List.map`, `Map.tryFind`, `Result.bind`, lazy `Seq.take`,
+`String.split`), tuples, destructuring `let` bindings (`let (r, c) = coord`), active patterns,
+typed holes for type-driven development, and multi-file projects with `import`.
 
 ---
 
@@ -468,10 +468,10 @@ to learn Rust on a real codebase), see **[Inside the compiler](https://simontrea
 
 ## Status
 
-MVP showcase complete and runnable: ADTs, records, tuples, computation expressions (including
-user-defined builders), units of measure, mutability, inferred multi-label effects, general Python
-FFI via `extern`, a module-qualified standard library, string interpolation, active patterns,
-typed holes, file-based modules, and a full LSP. See [`ROADMAP.md`](https://github.com/simontreanor/Pyfun/blob/main/ROADMAP.md) for what's next.
+MVP showcase complete and runnable: ADTs, records, tuples, destructuring bindings, computation
+expressions (four built-in, plus user-defined builders), units of measure, mutability, inferred
+multi-label effects, general Python FFI via `extern`, a module-qualified standard library, string
+interpolation, active patterns, typed holes, file-based modules, and a full LSP. See [`ROADMAP.md`](https://github.com/simontreanor/Pyfun/blob/main/ROADMAP.md) for what's next.
 
 This is a solo, actively-developed project: the MVP is feature-complete and runnable, but it's
 pre-1.0. Expect sharp edges; the language surface is stabilizing but not frozen.

RELEASING.md

@@ -1,7 +1,13 @@
 # Releasing Pyfun
 
-The compiler version in `Cargo.toml` is canonical, and **every versioned artifact
-tracks it** — one Pyfun version, the same number everywhere a user can read one.
+The compiler version in `Cargo.toml` is canonical, and **every artifact that carries
+the Pyfun version tracks it** — one Pyfun version, the same number everywhere a user
+can read one. That set is `Cargo.toml`, `editors/vscode/package.json`,
+`editors/jetbrains/build.gradle.kts` and `editors/emacs/pyfun-mode.el`; the wheel and
+the Jupyter kernel derive theirs. Two artifacts are deliberately versioned on their
+own because they change on their own schedule and a user reads them as a grammar
+rather than as a compiler: `editors/zed/extension.toml` and
+`editors/tree-sitter-pyfun/tree-sitter.json`, each bumped when the grammar changes.
 An editor artifact is never left behind because "it didn't change": a user whose
 extension says 0.2.0 while `pyfun --version` says 0.3.0 has no way to tell whether
 that is fine or a broken install. Version numbers are cheap; that doubt is not.
@@ -13,6 +19,7 @@ that is fine or a broken install. Version numbers are cheap; that doubt is not.
    - `editors/vscode/package.json` (+ a `CHANGELOG.md` entry — "no client
      changes" is a fine entry)
    - `editors/jetbrains/build.gradle.kts`
+   - `editors/emacs/pyfun-mode.el` (the `;; Version:` header — MELPA reads it)
 2. Commit, `git tag vX.Y.Z`, push the tag → `wheels.yml` publishes `pyfun-lang`
    to PyPI (Trusted Publishing) and attaches the `.vsix` to the GitHub release.
    **The attached `.vsix` is named from `package.json`, not the tag** — bumping in

ROADMAP.md

@@ -378,7 +378,9 @@ registry (PR to zed-industries/extensions), and consider shipping Helix indent/t
 The mdBook site shipped 2026-07-15 (learner track, educator pack, internals tour, in-page runnable
 code blocks; the playground moved to `/playground/` with `#code=` permalinks). Teaching prose is
 CC BY 4.0. When lessons change, re-verify with `python docs/verify_lessons.py` (checks every deep
-link decodes to its displayed starter and every solution's output matches). Still open:
+link decodes to its displayed starter and every solution's output matches); `ci.yml` runs it on
+every PR, and it refuses a `target/debug` binary older than `Cargo.toml` rather than reporting
+green against a stale compiler. Still open:
 
 - **Notebook-format lessons** (M, demand-gated) — the same lessons as `.ipynb` files riding the
   shipped Jupyter kernel, so instructors can distribute them through existing course
@@ -388,6 +390,30 @@ link decodes to its displayed starter and every solution's output matches). Stil
 - **Printable educator pack** (S, demand-gated) — a PDF export of the five session docs for
   departments that circulate paper.
 
+## Two surface gaps the 0.5.0 documentation audit found (2026-08-02)
+
+Both surfaced while checking what the docs claim against what the compiler does, and neither is a
+documentation problem, so they are recorded here rather than papered over in prose.
+
+1. **An uppercase `let` binding silently defines a function** (S) — `let Some x = Some 1`
+   type-checks. `parser::parse_binding_target` enters the pattern grammar only after `(` or
+   `Ident {`, so a bare constructor name is read as the *function name* of `let f x = …`, and the
+   program defines a function called `Some` that shadows the constructor. The irrefutability rule
+   that exists for exactly this case (`refutable_shape`, which does reject `let (Some x) = …`) never
+   sees it. Nothing downstream can use such a name as a constructor, so the shape is a mistake
+   every time it is written. Fix: reject an uppercase-initial binding name, with a message pointing
+   at the parenthesized pattern form when a constructor pattern was plainly intended. Lesson 8 had
+   to work around it (it quotes the parenthesized spelling), which is how it was found.
+2. **The hole-fit shortlist can hide the answer it exists to name** (S–M) — `hole_fits` ranks by
+   generality, then by qualified-vs-bare, then **by name**, and truncates at `HOLE_FIT_CAP = 6`. For
+   a common shape like `string -> string` the stdlib sweep left far more than six equally specific
+   fits, so the tail is decided alphabetically: `String.upper` now falls off the end of a
+   `string -> string` hole while `String.trimStart` stays. That is arbitrary from the reader's side,
+   and it cost lesson 9 its worked example. Options, in increasing effort: rank the remaining tier
+   by *shortest name* or by prelude-declaration order rather than alphabetically; say "and N more"
+   when the list is truncated; or filter by the hole's own name against candidate names (`?upper`
+   plainly wants `upper`), which is the one that would have kept the lesson working.
+
 ## Non-goals (decided against — with the reason, so they're not re-litigated)
 
 - **Type annotations (`let x : T`, `(x: T)`, return types)** — annotation-free code is a selling point,

bench/README.md

@@ -20,8 +20,7 @@ timings for programs that computed different results.
 
 Deliberately **not** here: I/O-bound workloads. The network-rail example's
 runtime is gzip decompression and long-line scanning, costs every runtime pays
-alike; it measures the shape of that job, not the language (see
-`local/article-draft-leverage-dont-emulate.md`).
+alike; it measures the shape of that job, not the language.
 
 ## Running
 

docs/src/internals/00-orientation.md

@@ -49,7 +49,7 @@ module map; the short version is that each stage of the pipeline is its own dire
 The dependency order among them is the pipeline order:
 
 > **Build order:** `lexer` + `parser` + `ast` -> `desugar` -> `types` (incl. `units`) ->
-> `lowering` + `python_emitter` -> `diagnostics` + `cli` -> `lsp`.
+> `lowering` + `python_emitter` -> `diagnostics` + `main` -> `project` -> `lsp`.
 
 Reading the modules in that order is reading the compiler from front to back, which is exactly
 what this tour does.