diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index c0b89eab..3b67ad4a 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -162,6 +162,7 @@ jobs: run: | python scripts/release.py notes \ --version "$VERSION" \ + --repo "$GITHUB_REPOSITORY" \ --output release/RELEASE_NOTES.md python scripts/release.py manifest \ --dist-dir dist \ diff --git a/.gitignore b/.gitignore index 1a9c5f8d..b444b33c 100644 --- a/.gitignore +++ b/.gitignore @@ -72,3 +72,9 @@ node_modules/ # and verifies, so it produces neither; `pytest tests/` leaves the tree clean.) /hello.txt /examples/hello.txt + +# `scripts/check_corpus_differential.py` checks the base revision out here +# by default, keyed by SHA and reused across runs. Output, not source, and +# deliberately repository-local rather than under a shared temporary +# directory (its contents end up on the base side's PYTHONPATH). +/.corpus-differential/ diff --git a/CHANGELOG.md b/CHANGELOG.md index e631af3d..36070cb7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). ### Added - **The examples are now RUN in CI, not only checked, verified and compiled** (`scripts/check_examples_run.py`). `check_examples.py` type-checks and verifies all 42, and `check_e602_clean.py` compiles all 42 as a side effect of policing silent translator skips — but nothing executed them as a set, and an audit of every referencing test found **seventeen examples that no test ran at all**: `array_utilities`, `async_http_fanout`, `collections`, `database`, `fizzbuzz`, `html`, `http`, `inference`, `io_operations`, `json`, `life`, `maximum_syntax`, `modules`, `nested_closures`, `read_char`, `scoreboard` and `string_utilities`, plus `file_io`, which ran only under the browser runtime, where the file IO it demonstrates is a deliberate `Err` stub. Between them they demonstrate `Map`/`Set`, the `` effect, JSON and HTML parsing, module imports and the whole string-utility family, so a runtime regression in any of it could reach a release with every gate green. The gate now runs 34 of the 42 under the native runtime and asserts a trap-free exit; the other 8 carry a documented skip property (`network`, `api-key`, `stdin`, `non-scalar-entry`, `long-running`) which the report prints with its reason on every run. Output pinning deliberately stays in the dedicated tests that already do it, so the gate does not go red on a cosmetic edit to an example. The load-bearing part is not the runs but the **coverage rule**: the script enumerates `examples/*.vera` from disk and requires every name to be in exactly one of its two tables, so an unclassified example is an error and adding one forces the author to decide whether the harness can drive it — and a table key whose file is gone is an error too, so a suppression cannot outlive its example and mask a later program of the same name. The classification is cross-checked against a new execution-coverage table in `TESTING.md` on the `check_doc_counts.py` model, the codebase being the oracle and the documentation having to match it, so the execution model stops living in maintainers' heads. Trap-freedom is asserted on two signals, the discipline `check_examples.py` already applies: the exit code, and an output signal. Either alone accepts a measured failure. Every spec names its entry point rather than relying on `vera run`'s first-export fallback — with `main` privatised, `array_utilities.vera` ran a different function and the gate passed; it now exits 1 on the name. And the three examples that reach outside the process (`sqlitedb.vera` for its committed fixture, `database.vera` for an in-memory database, `file_io.vera` for the filesystem) answer a failure by printing a message and completing normally, so each pins a substring only its success path prints — deleting `examples/sqlitedb.sqlite` left the gate green on the graceful in-memory arm, and now fails on the sentinel. Runs are hermetic: an ambient `VERA_DB_URL` or inference-provider key is stripped from the environment, so a gate run cannot be pointed at a real database or turned into a billed API request, and each example gets a scratch working directory so `file_io.vera` stops dropping `hello.txt` beside the sources. `TESTING.md`'s round-trip section is corrected with them — it claimed all 42 examples were tested through "every pipeline stage ... WASM compilation, and execution", where the directory-globbing parametrised tests in fact stop at verification and canonical form. +- **The grammar-alignment gate now compares terminals and production bodies, not only rule names** ([#1290](https://github.com/aallan/vera/issues/1290)). `scripts/check_grammar_alignment.py` held rule-name headers together and was blind to three drift classes, each demonstrated green on a live file during #1279's review: a fabricated terminal added to spec 10.2 (the header pattern requires a lowercase lead, so no terminal was seen at all), a rule reference restored to a right-hand side, and a production body edited on one side only — the class most grammar edits actually fall into. Three checks close them. A **terminal audit in both directions, within each file**: a terminal declared and never referenced, or referenced and never declared, is now an error — the shapes `SOME`/`NONE`/`OK`/`ERR`/`COLON` and `DOUBLE_COLON` had between them, found by hand and fixed in #1279 with the gate itself unable to see either. A **cross-file terminal-pattern check**: every terminal the chapter publishes as a bare regex must have that pattern in `vera/grammar.lark`, as a named terminal or an `%ignore`, after a semantics-preserving normalisation of Lark's `\\/` and `\\"` escapes — which is the whole of the difference between how the two files spell `STRING_LIT` and `ANNOTATION_COMMENT`, and which `BLOCK_COMMENT` failed. And a **production-body comparison** over the 80 rules both files declare, of the rules and the terminals each right-hand side refers to, with Lark's quoted literals mapped through the chapter's own terminal table rather than a hand-written one. Two notational differences are folded rather than reported: a rule's reference to itself, since Lark spells repetition with left recursion where the chapter uses a Kleene star, and a waived spec-only production, which the existing `ALLOWLIST` already pins to the Lark rule that inlines it. The body comparison needs no waivers of its own, and the six-entry rule-name allowlist is unchanged. +- **`KNOWN_ISSUES.md`'s Bugs table is gated one row per open `bug` issue.** The structural half is pure text and always on: each row's Issue column must hold exactly one `[#N](…/issues/N)` link whose number matches its URL, no two rows may claim one issue, and an empty section must be written `No known bugs.` rather than left as a bare table. The parity half needs the tracker, and a pre-commit hook must not depend on a network call, so it is opt-in through `scripts/check_doc_counts.py --check-bug-issues` for the release PR — mid-burndown the two legitimately disagree, a bug filed against an open PR's branch having an issue before it has a row. +- **TESTING.md's dual-target conformance row is gated against the manifest and a live run.** The row states a run-level total, a tested/skipped split and three category counts, and claims the excluded set "stays accurate as programs are added" — a claim nothing measured. The total now comes from the conformance manifest and the rest from a three-second `-rs` run of the differential itself, with two arithmetic checks the individual figures cannot make: tested plus skipped must be the run-level total, and the three categories must be the skip total. A skip whose reason matches none of the three documented properties fails rather than being folded into one of them. +- **`check_examples_run.py` derives which examples need an output sentinel instead of naming them.** The rule was a hard-coded triple — `database`, `file_io`, `sqlitedb` — so a fourth example reaching outside the process could be added with nothing but an exit code asserted, exactly the gap the sentinel exists to close. The set now comes from each program's own declarations: a resource effect in a function's effect row, or a call to a resource operation, read off the parsed AST rather than the source text so a header comment mentioning `` is prose. Both halves are needed, and the measurement said so: `FileIO` and `Time` are not effects in this language — file and clock operations live under `IO` — so `file_io.vera` declares exactly the bare `` that `hello_world.vera` does, and only the operation it calls separates them. What stays hand-written is a short list of registry *names*, and those are validated against the live effect registry, so a renamed or deleted effect or operation fails loudly rather than silently matching no example. The derived set must equal the specs carrying a sentinel in both directions, so a sentinel on an example with no resource signal is an error too. +- **The corpus differential and the grammar gate are hardened against the platform they run on and the patterns they read** (PR #1329 review). `_first_error` stripped the compiled file's path from a diagnostic by matching `str(path)` alone, which ties the strip to the host's separator: on Windows a diagnostic carrying the POSIX spelling went unstripped and its absolute path pushed the message past the truncation. Both spellings are stripped now, and the parameter is a `PurePath` so a test can render a Windows path on any host rather than waiting for the Windows CI cell. The grammar gate's comment scanner had the same shape of defect with worse consequences: a `/` inside a regex character class was read as the closing delimiter, so the chapter's `ANNOTATION_COMMENT` — which spells the class `[^/*]` where the Lark grammar escapes it `[^\/*]` — was truncated, and a truncated body is not a bare regex, so the terminal was **skipped from the pattern comparison entirely**. That gate was green on it by never looking. Both now have cells that fail on any host. Alongside them: the differential rejects a non-positive `--timeout` (which would fail every compile and report "no movers" over a corpus that never compiled), decodes compiler output leniently (a stray byte otherwise raised out of `subprocess.run` and aborted the whole run), checks the base revision out repository-locally rather than under a predictable shared temporary path whose contents it puts on `PYTHONPATH`, and prints a reproduction command that names the same input it actually compared. `check_doc_counts.py` reads a pytest summary that omits a zero-count category, and its two external calls — the dual-target run and the tracker query — join the script's own error convention instead of ending the run on a traceback. The chapter's `BLOCK_COMMENT` production excludes both delimiters from its character alternative, so `{- {- -}` is no longer derivable from a rule describing a construct the implementation rejects as unterminated. +- **`scripts/check_corpus_differential.py`** promotes the burndown's ad-hoc corpus differential to a first-class instrument: it compiles every corpus program at two revisions and reports the movers, including the programs that compile on one side only. It is deliberately not a pre-commit hook — it compiles the whole corpus twice — and is documented as a CI-optional burndown instrument. ### Fixed @@ -32,6 +38,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). - **The Vera-level type namers join over a conditional instead of reading one branch** ([#1286](https://github.com/aallan/vera/issues/1286)). [#1276](https://github.com/aallan/vera/issues/1276) fixed the WAT result-type deciders to take the first branch that yields a type; their Vera-level siblings kept the one-branch read — `InferenceMixin._infer_vera_type` (the WASM call-rewrite consultor) read `then_branch` only and `arms[0]` only, and `Monomorphizer._infer_vera_type_name` (the instantiation-discovery consultor) read `then_branch` only and had no `MatchExpr` arm at all. A branch whose every path `throw`s names no type, so reading only that branch answered "unknown" for the whole expression, and the issue's latency estimate was wrong in the program's favour: the shape is constructible, and it is loud in two different ways from check-green source. As an **array-literal element** (`[if false then { throw(true) } else { 42 }, 7]`, and the `match` and `String` spellings of the same position) the unknown element type raised `CodegenSkip`, so a declared `public fn main` — `vera check`-green and `vera verify`-green at 2 Tier 1 — was absent from the compiled exports behind an `[E602]` note. As a **generic argument** (`idg(if false then { throw(true) } else { 42 })`, verify-green at 4 Tier 1) the type variable bound nothing and the clone fell to the phantom-var default: the module carried `idg$Bool`, an i32 clone, reached with an i64 argument, and failed to load with `Invalid input WebAssembly code at offset 73: type mismatch: expected i32, found i64`. The same reading through a constructor **field** mis-instantiated the unboxing clone the other way round (`expected i64, found i32`). The repair lands on both consultors together because the `match` case was broken in both directions: with every arm completing and nothing diverging, the rewrite named `idg$Int` from arm 0 while discovery, having no arm for `MatchExpr`, named the phantom default, and the caller was dropped on a dangling target — the clone-name agreement contract ([#772](https://github.com/aallan/vera/issues/772)) makes the pair, not either function, the unit of repair. All 291 pre-existing corpus programs (`examples/` plus `tests/conformance/`, recursive) emit byte-identical WAT, since the join only changes an answer that was previously unknown; `ch02_generic_arg_branch_join` promotes the witness into the conformance suite at level `run`. The review round closed the same divergence in two further shapes, both of them the one gap — the discovery consultor must stay structurally parallel to the rewrite one, arm for arm. It had no `Block` arm, and the transformer leaves a braced match-arm body AS a `Block`, so `idg(match … { Some(@Int) -> { let @Int = @Int.0 + 1; @Int.0 }, None -> throw(true) })` named nothing on the discovery side and `idg$Int` on the rewrite side: a dangling target that dropped `main` from check-green source. A braced `if` branch whose tail is itself braced does the same, and so does a `handle` in argument position, which likewise had no arm. An `IndexExpr` argument is measured to dangle identically and is deliberately left for its own change ([#1327](https://github.com/aallan/vera/issues/1327)): the rewrite's arm resolves chained indexing, aliases and `Future` payloads against codegen tables the monomorphizer does not have, so a partial mirror would replace a shape where both consultors answer "unknown" with one where they disagree. +- **A GitHub Release body that would exceed the 125,000-character limit is condensed instead of failing** ([#1288](https://github.com/aallan/vera/issues/1288)). `release.yml`'s `Tag and create GitHub Release` step 422'd on v0.1.10, whose CHANGELOG section extracts to 147,918 characters, and it failed **after** PyPI had accepted the immutable archives and **after** the tag was cut — the one point in the pipeline where a step must not fail. `scripts/release.py notes` is now total: within budget it publishes the section verbatim, and past it, it regenerates the shape the v0.1.10 release was completed by hand with — the section's `###` subsection headers, one condensed line per bullet carrying its lead-in and its last issue or pull-request reference, and a link to the canonical section in the CHANGELOG at the tag. Run against v0.1.10's section the generated index reproduces the released body's 73 index lines byte for byte. In the pathological case where even the index overflows it is truncated and says so, so the builder cannot be the thing that fails. +- **Four production-level divergences between spec Chapter 10 and the parser are closed** ([#1290](https://github.com/aallan/vera/issues/1290)). Typed holes have been in `grammar.lark` since 2026-03-30 and appeared nowhere in the chapter: 10.2 now declares `HOLE` and `primary_expr` carries the alternative, so the chapter's expression grammar is the parser's. 10.2's `BLOCK_COMMENT` published a non-nesting regex, contradicting 1.3 ("They nest") and the implementation, which counts depth in `vera/lexical.py` because a regular expression cannot; it is now a nesting production with that fact recorded beside it. The other two the new body comparison found: `slot_ref` and `result_ref` admitted an arbitrary `type_expr`, where the parser accepts only `UPPER_IDENT type_args?` — a refinement-typed slot reference is a syntax error, and the published grammar said it was legal; and `effect_list` carried a second alternative ambiguous with the one beside it, `effect_ref` already admitting a bare `UPPER_IDENT`, the same redundancy #1279 removed from `statement`. +- **README's project-status line has every count gated, not just its test count.** The `check_readme` helper returned silently when a pattern matched nothing, and four of its five patterns matched no README text at all — so the conformance count sitting beside the gated test count drifted through two rebases unseen. The line's four countable figures — tests, conformance programs, examples and spec chapters — are now read from that line alone, and a figure that has gone missing is an error rather than a skip. - **A user-defined `fn get` / `fn put` is no longer hijacked by an enclosing handler** ([#1284](https://github.com/aallan/vera/issues/1284)). Three sites answered "does this `get` mean the user's declaration or the effect operation?" independently. The checker answers user-fn-first — `_check_call_with_args` looks a bare name up as a function before it looks it up as an operation, so a declaration named `get` owns every bare `get(...)` in its scope, which an arity or argument-type error at such a call site proves by reporting the *user's* signature (E201/E202). Codegen answered twice more: the declared-effect row in `vera/codegen/functions.py` withheld the intrinsic when `_fn_sigs` already owned the name, and the handler expression in `vera/wasm/calls_handlers.py` installed `get`/`put` unconditionally. From `vera check`-green source that produced, depending on the nesting shape, a **silently wrong value** (`nat_to_int(get(3))` under `handle[State](@Int = 5)` returned the cell's 5 for the function's 4, and the argument was not even emitted), a **module WASM validation rejects** (a `@Bool`-returning user `get` took `state_get_Int`'s i64 into an `i32` position; different-family nesting took the *enclosing* cell's getter at the wrong width), or a **spurious `[E602]`** in which the #1233 unaddressable-cell gate refused `main` outright, naming "a bare or qualified State operation `get`" the program never contained. The repair is one predicate, `vera.slots.bare_call_denotes_user_fn`, stating the checker's rule once and consumed by the bare-call dispatch in `vera/wasm/calls.py` (which now gates the clause-inline registry, the host-cell intrinsics and the addressability gate together), by the three bare-`FnCall` result-type inference sites, and by the monomorphizer's discovery walk — each passing its own name table, so the sites cannot answer differently about the table they share. Gating the *dispatch* rather than the *registries* is what makes it correct rather than merely consistent: the registries record which cell an op name reaches, which is true whatever the program's declarations are called, and withholding an entry answered both questions with one table. That is why the gate-only fix measured during PR #1283's review turned the loud skip into a differently-broken module, and why it also cost the qualified spelling its cell — `State.put(5)` in a function that also declares `fn put` compiled to `call $vera.put` and failed to link, which now lowers to the intrinsic the checker always meant. Discovery's `MonoContext.fn_names` moves to the same lookup-time question, so a `get(())` fixing a generic's type variable under a handler names the clone the rewrite emits. All 256 conformance and example programs emit byte-identical WAT. **The `W002` async-commutativity warning was the same defect in the checker's own file** and is corrected with them: `_collect_expr_effects` asked `lookup_effect_op` before the scoped function lookup — the last op-first consumer — so a user function named after an operation contributed the *operation's* parent effect to the commutativity analysis instead of its own declared row, wrong in both directions. A **pure** `fn get`, in a program containing no `State` at all, drew `async argument performs State effects`; a `fn get` that performs `IO`, under a row naming `Http` first, drew **no warning**, because the walk bound the name to `Http.get`, which is inside the commutative whitelist, and silently withheld the eager-evaluation warning the program is owed. Both are pinned with rename controls — the byte-identical program with the helper called `gett` / `fetch` was correct throughout — beside a control that an unshadowed bare `get(())` under a `State` row still warns, so the fix cannot degenerate into never reporting `State`. The walk's comment claiming it resolves "like the call checker above" is now true. One caveat the predicate did not close on its own: codegen's name table was not scope-accurate, so a name the call site cannot see still answered "user-owned" there — a property of the table rather than of the rule, closed by [#1299](https://github.com/aallan/vera/issues/1299) below. - **A bare call is lowered against the names its call site can see** ([#1299](https://github.com/aallan/vera/issues/1299)). The [#1284](https://github.com/aallan/vera/issues/1284) ownership predicate is one rule read over two tables, and only one of them was a scope. The checker's is a lexical walk; codegen passed `set(_fn_sigs.keys())` — a flat mirror of every symbol the whole compilation absorbed — so a bare `get(())` the checker had resolved to a `State` operation was lowered as a call to a declaration the body cannot name. Four source shapes reach it, all `vera check`-green and all one defect: an imported module's **private** `fn get` (invisible, but still compiled in because the module's own bodies call it), a **public** one a selective import excludes, a `where` helper of a **`forall` parent** (which keeps a bare `_fn_sigs` key beside its clone-qualified one where a non-generic parent's helper does not), and the ability operation `show`, which `E151` does not reserve and which reaches the same table through the *intrinsic* gate rather than the operation one. How it lands is a property of the widths, not of the route: where the invisible declaration and the cell share a WAT type the module loads and returns the wrong value (7007 where the cell holds 42007), where they differ it fails to load (`type mismatch: expected i64, found i32`), and the generic-`where` route is always loud — the bare key exists in the signature table while no bare *symbol* is emitted, so the call dies at WAT assembly on `unknown func: failed to find name $get` with no E-code. The repair splits the two questions the one set was answering. `_known_fns` keeps the flat registry for `_translate_call`'s guard rail, which asks whether a *resolved* target — already mono-mangled, already `mod$…` rerouted — has an implementation, and is flat by nature. A new `_scoped_fns` carries the names visible in the compiling declaration's **lexical** scope, and that is what the ownership predicate reads: its namespace's own declarations plus the public, in-filter names of the imports *that namespace* makes (spec §8.6.4 — imports are never inherited, so a transitively-reached module contributes nothing to the entry program), the prelude, and the `where` helpers of every enclosing function. Module scope alone would not have closed the third route: a generic's helper *is* in the module and still is not in a sibling's scope. The narrowing is a strict subset of the registry by construction — every `$`-bearing key is admitted unconditionally, since `$` cannot occur in a Vera identifier and a mangled name is never what a bare source call spells — so it can only withdraw a name the flat table wrongly claimed. diff --git a/CLAUDE.md b/CLAUDE.md index 442b878d..d218d88b 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -80,6 +80,8 @@ python scripts/build_site.py # Regenerate AI-readable site assets (llms python scripts/check_site_assets.py # Verify site assets are up-to-date + docs/index.html ↔ docs/index.md state coherent facts (#1154) python scripts/check_version_sync.py # Verify version consistency python scripts/check_doc_counts.py # Verify documentation counts match codebase +python scripts/check_doc_counts.py --check-bug-issues # Also check KNOWN_ISSUES' Bugs table against the open `bug` issues (GitHub API; release-PR time, not pre-commit) +python scripts/check_corpus_differential.py --base-ref origin/main # Compile the corpus at two revisions; report programs whose WAT moved (burndown instrument, not a hook) python scripts/check_licenses.py # Verify all package licenses are MIT-compatible python scripts/check_wheel_availability.py # Verify every runtime dep has wheels for all supported platforms (README §Supported platforms) python scripts/check_limitations_sync.py # Verify limitation tables are in sync diff --git a/FAQ.md b/FAQ.md index 716dcd6d..5e920fbc 100644 --- a/FAQ.md +++ b/FAQ.md @@ -279,7 +279,7 @@ The reference compiler is under active development. The current release includes - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute - A 14-chapter formal specification -- 11,786 tests, including a 244-program conformance suite +- 11,940 tests, including a 244-program conformance suite - 42 working example programs - 164 built-in functions covering strings, arrays, math, parsing, and data types - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation diff --git a/KNOWN_ISSUES.md b/KNOWN_ISSUES.md index 7d66d41f..3d7b1f37 100644 --- a/KNOWN_ISSUES.md +++ b/KNOWN_ISSUES.md @@ -21,8 +21,6 @@ Defects in shipped compiler, runtime, or tooling behaviour — this table matche | The checker resolves a bare call to a SIBLING function's `where` helper. Spec §5 makes a helper local to its parent, and the checker's own `_lookup_function_scoped` implements that — it walks the enclosing frame stack and reads each frame's direct helpers — but it then falls back to `env.lookup_function`, and `vera/registration.py` has recursed every helper into that flat `TypeEnv`. So a top-level `other()` calling `helperx(7)`, where `helperx` is a helper of an unrelated `holder`, is **check-green and verify-green** and then refused by codegen (`Function 'helperx' is not defined in this module and was not found in any imported module`) — the helper is emitted as `holder$where$helperx`, so the bare call has no target. Loud, never a wrong answer. The op-name variant is the one that matters for the #1284 ownership predicate: with the helper named `get` and the sibling reading a `State` cell by bare `get(())`, the checker binds the HELPER and reports `[E202] Argument 0 of 'get' has type Unit, expected Int` where spec §7.4 resolves the operation — so the checker rejects a program codegen compiles correctly, the two tables disagreeing in the CHECKER's direction for the first time. Codegen's `_scoped_fns` (#1299) implements the spec rule; the fix here is a checker change, whose new rejections need their own blast-radius pass. | [#1307](https://github.com/aallan/vera/issues/1307) | | `md_parse` diverges between the native and browser runtimes on **211 of 1,471** adversarial inputs (14.3%) and **329 of 4,858** blank-line-separated sections of the project's own documentation (6.8%), measured at [PR #1303](https://github.com/aallan/vera/pull/1303) by comparing the two ADTs directly rather than their renders. The second denominator is the repository's own Markdown, so it moves whenever a document gains or loses a section; 11 of those 4,858 also differ in the rendered output. Nine classes, each with a one-line repro. The largest by a wide margin — 173 of the 211 — is *plain-text run grouping*: the browser emits one `MdText` per scan segment where the reference coalesces adjacent runs, so `**unclosed` is `[MdEmph([]), MdText("unclosed")]` natively and `[MdText("*"), MdText("*unclosed")]` in the browser. That class is invisible to `md_render` (the runs concatenate to the same text) but not to a Vera program that matches on the ADT, which is what makes it a §12.9.3 violation rather than a cosmetic one. The rest are render-visible: emphasis/strong scanning (`***both***` renders `**both****` natively, `***both***` in the browser); list-continuation indent width, where the reference strips exactly two (or three) characters and the browser strips all leading whitespace (`- a\n b` → `- a b` vs `- a b`); a `+` bullet, unrecognised in the browser; an `n)` ordered marker, likewise; a loose list, one list natively and two in the browser (`- a\n\n- b`); nesting past two levels, flattened in the browser (`- a\n - b\n - c`); a thematic break with internal spaces (`* * *`); and a table without a separator row (`\| a \| b \|\n- li`). Neither implementation is the specification — §9.7.3 pins the ADT, not the grammar that produces it — so closing this means choosing a parse for each class and stating it, then mirroring. Successor to [#1294](https://github.com/aallan/vera/issues/1294), which closed the `md_render` half; the parity suite pins the shapes they do agree on, so a regression on one of those goes red. | [#1301](https://github.com/aallan/vera/issues/1301) | | A postcondition may name a `State` the function's effect row never declares, and `vera check` accepts it: `ensures(new(State) == false)` under `effects(>)` reports OK, then `vera compile` fails with **E699** — the internal-compiler-error diagnostic whose own text says the type checker should have rejected the input, which is exactly the situation. Both forms land there for the same reason (no cell of that family exists, so `old()` finds no snapshot local and, since [#1285](https://github.com/aallan/vera/issues/1285), `new()` finds no getter). Loud and never a wrong answer, so this is diagnostic quality rather than soundness — but it is a check-green program that cannot compile, reported against the compiler instead of against the program, with a bug-report request the user should not act on. Before #1285 the `new()` side was worse than loud: the name-keyed lookup found the row's other getter and silently read the wrong cell. Fix direction: validate an `OldExpr`/`NewExpr`'s effect reference against the declared row where the checker already validates the rest of the clause, one rule for both forms; `test_a_family_the_row_does_not_declare_is_loud_on_both_sides` pins today's E699 and is the test to flip. | [#1298](https://github.com/aallan/vera/issues/1298) | -| Spec Chapter 10 is a second, hand-maintained copy of `vera/grammar.lark`, and the rule-name alignment gate `scripts/check_grammar_alignment.py` compares only rule-name headers — three classes of drift pass it unseen. **Terminals, both directions**: the header pattern requires a lowercase lead, so a fabricated terminal added to §10.2 leaves the gate green, and no declared-versus-referenced audit exists in either direction. **Rule references**: restoring a removed ambiguity to a production's right-hand side is invisible, because only headers are compared. **Production bodies**: the class most grammar edits actually fall into. Two instances are live in the chapter on `main` today, both body-level and both this issue's to close: typed holes (`"?" -> hole_expr`, in `grammar.lark` since 2026-03-30) appear nowhere in `primary_expr`, and §10.2's `BLOCK_COMMENT: /\{-[\s\S]*?-\}/` is non-nesting, contradicting both §1.3 ("They nest") and the implementation, which parses `{- a {- b -} c -}` clean. Never a wrong answer from a program — the defect is that the published grammar misdescribes the one the parser has. Fix direction: extend the gate side-aware (terminal audit both ways, reference-set comparison), or fold Chapter 10 toward the DESIGN Grammar row's actual promise of a single-sourced shared grammar rather than a hand-maintained copy held honest by ever-wider cross-checks; the two live instances are fixable independently of which direction wins. | [#1290](https://github.com/aallan/vera/issues/1290) | -| `.github/workflows/release.yml`'s `Tag and create GitHub Release` step fails with `HTTP 422: Validation Failed — body is too long (maximum is 125000 characters)` when the CHANGELOG section `scripts/release.py notes` extracts into `RELEASE_NOTES.md` exceeds GitHub's release-body limit. It fired on v0.1.10, whose notes extract to roughly 148,700 bytes — the #1213 burndown's 44-issue section, some 23,000 characters past the limit — and it fired at the worst point in the pipeline: **after** PyPI had accepted the immutable archives and **after** the tag was created, leaving the release half-cut with no repeatable path back. The v0.1.10 GitHub Release was completed by hand, mirroring the step exactly: the run's artifacts downloaded and hash-verified three ways, then `gh release create --verify-tag --latest` with the wheel, sdist and SHA256SUMS, and a generated body — the section's bold bullet lead-ins as a headline index plus a link to the canonical section at the tag. Rare, since it needs a release this large, but rarity is not the mitigating factor here; the landing point is. Fix direction: make the step total — before `gh release create`, regenerate oversized notes into that index form so the release always carries a body that fits, with the full notes staying in `CHANGELOG.md`, which is already the release notes of record. | [#1288](https://github.com/aallan/vera/issues/1288) | | `ch05_closure_nat_return` (a run-level conformance program in the pre-commit + CI gate) trapped **once** in a full `check_conformance.py` run (`unreachable` in `main` — the sentinel `assert` or a GC shadow-stack guard) and has not reproduced in ~960 attempts across isolated, parallel, eager-GC, and hash-seed-swept executions; the emitted WAT is deterministic and correct. Suspected rare runtime/GC/wasmtime interaction, tracked so a future intermittent CI red resolves here instead of starting fresh. | [#996](https://github.com/aallan/vera/issues/996) | ## Limitations diff --git a/README.md b/README.md index b5f7593e..fe40b36b 100644 --- a/README.md +++ b/README.md @@ -263,7 +263,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md ## Project status -Vera is in **active development** at v0.1.11: 2,000+ commits, 209 releases, 11,786 tests, 95% Python code coverage, 244 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built. +Vera is in **active development** at v0.1.11: 2,000+ commits, 209 releases, 11,940 tests, 95% Python code coverage, 244 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built. The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/). diff --git a/RELEASING.md b/RELEASING.md index ccf3a9e6..66e87416 100644 --- a/RELEASING.md +++ b/RELEASING.md @@ -93,7 +93,16 @@ The release-prep PR must: 2. Turn the accumulated `[Unreleased]` notes into a dated `## [X.Y.Z]` section with at least one bullet and update the CHANGELOG compare links. 3. Add the release's one-line HISTORY entry and regenerate site assets. -4. Pass the ordinary protected-branch CI and review process. +4. Reconcile `KNOWN_ISSUES.md`'s Bugs table with the tracker, by running + `python scripts/check_doc_counts.py --check-bug-issues`. The convention + is one row per open `bug`-labelled issue, and the check needs the GitHub + API — it sends `GH_TOKEN` or `GITHUB_TOKEN` when either is set, and is + rate limited per IP when neither is, so export one before running it — + so it is opt-in rather than part of the pre-commit hook: mid-cycle + the two legitimately disagree, since a bug filed against an open PR's + branch has an issue before it has a row. At release time they should + agree — that is the point at which the file is the published list. +5. Pass the ordinary protected-branch CI and review process. After merge, `release.yml` detects the version increase on `main`. It then: diff --git a/ROADMAP.md b/ROADMAP.md index 1f54b11c..d3e744e5 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati ## Where we are -11,786 tests, 244 conformance programs, 42 examples, 14 spec chapters. [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire. +11,940 tests, 244 conformance programs, 42 examples, 14 spec chapters. [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire. ## Stage 19 — The verification completeness sprint diff --git a/TESTING.md b/TESTING.md index ea569f8d..49724c24 100644 --- a/TESTING.md +++ b/TESTING.md @@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d | Metric | Value | |--------|-------| -| **Tests** | 11,786 across 174 files (~155,000 lines of test code; 11,587 passed + 26 stress, 173 skipped) | +| **Tests** | 11,940 across 175 files (~155,000 lines of test code; 11,741 passed + 26 stress-deselected, 173 skipped) | | **Compiler code coverage** | 95% Python, 87% JavaScript (CI minimum: 80%) | | **Conformance programs** | 244 programs across 9 spec chapters, validating every language feature | | **Example programs** | 42, all validated through `vera check` + `vera verify` | @@ -221,10 +221,11 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_build_site.py` | 46 | 698 | Site-asset tooling — `_abs_links` rewriting (relative links, fenced-block immunity incl. inline backticks and tilde fences, http/https/fragment pass-through, Vera effect syntax not mis-parsed), `build_site` `` stability (preserve/refresh keyed on URL-structure change), `check_site_assets` sitemap staleness (missing / date-only-clean / structural-stale), and the #538 leak guard (vera:skip fence annotations stripped from generated `docs/SKILL.md` / `docs/llms-full.txt`, with a non-vacuous precondition that the source carries annotations); plus the #1154 `check_fact_coherence()` suite — index.html↔index.md fact extraction and divergence detection | | `test_builtin_typevar_collision_970.py` | 61 | 811 | #970 a user `forall` type-var name colliding with a built-in generic's internal name (`T`/`E`/`A`/`B`/`K`/`U`/`V`): focused check/verify pins for the compound-argument shapes (`@Array>`, `@Result>`, `@Map>`) plus a collide-vs-control differential battery over every generic-builtin family and contract/where-helper position. Also pins marker-strip (the `#b` namespacing marker must never reach an E205/E202 diagnostic), a registry-consistency pin (every built-in ability-constraint `type_var` stays a member of its `forall_vars`), the dual completeness-gap pinned in both argument orders, a tier-split equality pin, and the #1069 leaked-placeholder message-rendering sweep (a stripped built-in var renders as `?`, not a bare letter, at every reachable actual-type slot: the mismatch sites plus the operator/index/interpolation family, `assert`/`assume`, `if` condition and branches, and the contract/refinement predicates — one parametrized row per converted render slot, with the provably-unreachable sites documented in the class docstring) | | `test_check_changelog_updated.py` | 68 | 712 | `check_changelog_updated.py` unit + end-to-end tests: file classification (incl. file-style exact-match vs directory-style prefix-match), CHANGELOG diff parsing with `[Unreleased]` section tracking, bare-heading rejection, and full-file context (regression test for bullets far below the heading), `Skip-changelog:` trailer detection, temp-repo integration covering substantive/exempt/label/trailer paths, and `GIT_*`-env hermeticity of the temp-repo fixtures (regression for the pre-commit-hook env leak) | -| `test_release.py` | 47 | 566 | Release policy and registry verification (#481): strict project-name and version parsing/comparison, version-bump/TestPyPI/recovery planning, exact confirmation and immutable-tag guards, first-parent version-introduction discovery, package-change recovery refusal, non-empty CHANGELOG extraction, one-wheel/one-sdist SHA-256 manifests, malformed registry-response handling, missing/filename/hash propagation retries, exact filename/hash verification, and CLI dispatch/GitHub-output wiring. An autouse fixture scrubs hook-exported `GIT_*` variables so the tmp-repo git calls (fixture helpers and `release.py`'s own) never resolve to the developer's repository when the suite runs inside a pre-commit hook. | -| `test_check_doc_counts.py` | 54 | 665 | `check_doc_counts.py`'s pure per-document checks: KNOWN_ISSUES refactoring line counts (±10% tolerance band incl. the exact-boundary case, drift detection, empty-file citation, hyphenated paths, missing file/section/rows, the #419 empty-section sentinel + its cannot-mask-a-malformed-table dual), HISTORY version-row format (issue-link limit, ` — ` separator rejection, dateless-row and prose exemption, line-number reporting), the TESTING.md tests breakdown (parts summing to the collected total, a self-consistent-but-stale row, and the reworded-row error), and vera/README.md's Test Suite counts (all four checked independently — mutation-validated by dropping each citation in turn — plus the reworded-paragraph error, a thousands-separator case pinning that every one of the four counts is read comma-tolerantly, and the two section-anchoring cases — a reworded paragraph with decoy counts in a later section, and a renamed heading, both of which must fail loud rather than match across the section boundary). The reworded case is a test in its own right for both new checks: a pattern that matches nothing must be an error, or rewording the sentence silently switches the gate off. Also the release count (README's status line and HISTORY's total against each other and against `git tag`: the matching case, the one-ahead release cut that `release.yml` has not tagged yet, that +1 being the ONLY slack once the version is tagged, the two-behind drift that actually shipped, per-document reporting, and a tagless checkout standing the oracle down without standing down the cross-check), plus the tag reader itself against real repositories built in `tmp_path` — release tags read, `nightly`/`-rc1` not counted as releases, and both no-evidence answers (`None` rather than `[]`, since an empty list would read as zero releases and make every documented count wrong) for a tagless checkout and a directory that is not a repository at all. CONTRIBUTING.md's pre-commit hook count is checked the same way, reworded-sentence case included; and the CI-pipeline lint row against `ci.yml`'s lint job — a matching row, a step present in CI but absent from the row (the drift that shipped), a row entry CI no longer runs, the same set in a different order, a reworded row and a renamed job (both errors, not skips), that only the lint job is read rather than the whole workflow, and the shipped pair both clean and red with one entry dropped | -| `test_grammar_alignment.py` | 44 | 309 | `check_grammar_alignment.py` gate ([#683](https://github.com/aallan/vera/issues/683)): both extractors (Lark headers with the `?`/`!`/`_` markers stripped, template parameters and rule priorities tolerated, and `-> alias` names deliberately not collected; spec headers from ```ebnf fences only), the allowlist arithmetic in all three directions — unwaived drift, a spent entry both files now have, and an entry whose premise broke — one case per waiver proving the fact it rests on is actually checked, the name-deleted-from-both-files case that must not read as agreement, a mutation restoring the spec's old `assert_stmt` name, non-vacuous extraction, and the false positive the issue itself rested on: `qualified_call` and `module_call` are spec headers Lark expresses as aliases, and must never be reported as drift. Three pin the premise checks against ways they used to pass vacuously: an alias surviving only inside a `//` comment must not hold its waiver up, an alias that moved to another rule must fail the waiver naming `fn_call`, and a spent waiver whose premise also broke must yield one instruction rather than two opposite ones | -| `test_check_examples_run.py` | 59 | 885 | `check_examples_run.py`, the harness gate that RUNS the examples. Five separable parts, each in both directions. **The coverage rule** — the shipped tables cover the shipped corpus exactly, and an unclassified example, a stale `RUN_SPECS` or `SKIPS` key whose file is gone, a name in both tables, and a skip citing an undocumented property are each an error; the empty corpus is an error too, since a glob that stops matching would otherwise report success over zero programs. Plus the specs' own well-formedness: every named entry point is `public` in its example, every no-main example pins one (or `vera run` would fall back to an arbitrary first export), and no skip property is unused. **The runner** — a seeded `tmp_path` corpus proves it goes red on a program that type-checks and compiles but traps at run time, green on one that does not, and reports only the broken member of a mixed pair; a fixture whose first export is clean and whose named one traps proves `spec.fn` is actually honoured rather than ignored; a writer program proves each run gets a scratch working directory, so a gate run leaves nothing beside the examples. **The TESTING.md cross-check** — missing row, extra row, rename (reported naming both sides), wrong disposition and wrong skip property are errors, the parse stops at the next heading so a row-shaped line in a later section is not swept in, and both a reworded heading and a heading whose table has vanished fail loud rather than finding nothing to compare. **The output signal** -- the second half of the two-signal discipline `check_examples.py` established: the fallback note that `vera run` prints when it cannot use the named entry point is a failure even at exit 0, an absent `expect` sentinel is a failure even at exit 0, and a spec without one asserts nothing about output; end to end, a privatised `main` and a program that completed down a graceful arm each go red, and the same program passes once its own output is the sentinel, so the check reads the output rather than always failing. The three environment-dependent specs are required to carry a sentinel, and the runner's use of BOTH streams is pinned structurally -- `vera run` writes the note to stderr and nothing there on a clean exit, so no fixture can distinguish reading both streams from reading stdout alone, and a tripwire wired to the wrong stream is no tripwire. Also the hermetic-environment property: an ambient `VERA_DB_URL` or provider key is stripped so a gate run cannot be pointed at a real database or turned into a billed API call, a fixture spec puts its own URL back, and every neutralised name is checked to be one `vera/runtime/` actually reads | +| `test_release.py` | 61 | 757 | Release policy and registry verification (#481): strict project-name and version parsing/comparison, version-bump/TestPyPI/recovery planning, exact confirmation and immutable-tag guards, first-parent version-introduction discovery, package-change recovery refusal, non-empty CHANGELOG extraction, one-wheel/one-sdist SHA-256 manifests, malformed registry-response handling, missing/filename/hash propagation retries, exact filename/hash verification, and CLI dispatch/GitHub-output wiring. An autouse fixture scrubs hook-exported `GIT_*` variables so the tmp-repo git calls (fixture helpers and `release.py`'s own) never resolve to the developer's repository when the suite runs inside a pre-commit hook. | +| `test_check_doc_counts.py` | 89 | 987 | `check_doc_counts.py`'s pure per-document checks: KNOWN_ISSUES refactoring line counts (±10% tolerance band incl. the exact-boundary case, drift detection, empty-file citation, hyphenated paths, missing file/section/rows, the #419 empty-section sentinel + its cannot-mask-a-malformed-table dual), HISTORY version-row format (issue-link limit, ` — ` separator rejection, dateless-row and prose exemption, line-number reporting), the TESTING.md tests breakdown (parts summing to the collected total, a self-consistent-but-stale row, and the reworded-row error), and vera/README.md's Test Suite counts (all four checked independently — mutation-validated by dropping each citation in turn — plus the reworded-paragraph error, a thousands-separator case pinning that every one of the four counts is read comma-tolerantly, and the two section-anchoring cases — a reworded paragraph with decoy counts in a later section, and a renamed heading, both of which must fail loud rather than match across the section boundary). The reworded case is a test in its own right for both new checks: a pattern that matches nothing must be an error, or rewording the sentence silently switches the gate off. Also the release count (README's status line and HISTORY's total against each other and against `git tag`: the matching case, the one-ahead release cut that `release.yml` has not tagged yet, that +1 being the ONLY slack once the version is tagged, the two-behind drift that actually shipped, per-document reporting, and a tagless checkout standing the oracle down without standing down the cross-check), plus the tag reader itself against real repositories built in `tmp_path` — release tags read, `nightly`/`-rc1` not counted as releases, and both no-evidence answers (`None` rather than `[]`, since an empty list would read as zero releases and make every documented count wrong) for a tagless checkout and a directory that is not a repository at all. CONTRIBUTING.md's pre-commit hook count is checked the same way, reworded-sentence case included; and the CI-pipeline lint row against `ci.yml`'s lint job — a matching row, a step present in CI but absent from the row (the drift that shipped), a row entry CI no longer runs, the same set in a different order, a reworded row and a renamed job (both errors, not skips), that only the lint job is read rather than the whole workflow, and the shipped pair both clean and red with one entry dropped | +| `test_grammar_alignment.py` | 85 | 672 | `check_grammar_alignment.py` gate ([#683](https://github.com/aallan/vera/issues/683)): both extractors (Lark headers with the `?`/`!`/`_` markers stripped, template parameters and rule priorities tolerated, and `-> alias` names deliberately not collected; spec headers from ```ebnf fences only), the allowlist arithmetic in all three directions — unwaived drift, a spent entry both files now have, and an entry whose premise broke — one case per waiver proving the fact it rests on is actually checked, the name-deleted-from-both-files case that must not read as agreement, a mutation restoring the spec's old `assert_stmt` name, non-vacuous extraction, and the false positive the issue itself rested on: `qualified_call` and `module_call` are spec headers Lark expresses as aliases, and must never be reported as drift. Three pin the premise checks against ways they used to pass vacuously: an alias surviving only inside a `//` comment must not hold its waiver up, an alias that moved to another rule must fail the waiver naming `fn_call`, and a spent waiver whose premise also broke must yield one instruction rather than two opposite ones | +| `test_check_examples_run.py` | 77 | 1,280 | `check_examples_run.py`, the harness gate that RUNS the examples. Five separable parts, each in both directions. **The coverage rule** — the shipped tables cover the shipped corpus exactly, and an unclassified example, a stale `RUN_SPECS` or `SKIPS` key whose file is gone, a name in both tables, and a skip citing an undocumented property are each an error; the empty corpus is an error too, since a glob that stops matching would otherwise report success over zero programs. Plus the specs' own well-formedness: every named entry point is `public` in its example, every no-main example pins one (or `vera run` would fall back to an arbitrary first export), and no skip property is unused. **The runner** — a seeded `tmp_path` corpus proves it goes red on a program that type-checks and compiles but traps at run time, green on one that does not, and reports only the broken member of a mixed pair; a fixture whose first export is clean and whose named one traps proves `spec.fn` is actually honoured rather than ignored; a writer program proves each run gets a scratch working directory, so a gate run leaves nothing beside the examples. **The TESTING.md cross-check** — missing row, extra row, rename (reported naming both sides), wrong disposition and wrong skip property are errors, the parse stops at the next heading so a row-shaped line in a later section is not swept in, and both a reworded heading and a heading whose table has vanished fail loud rather than finding nothing to compare. **The output signal** -- the second half of the two-signal discipline `check_examples.py` established: the fallback note that `vera run` prints when it cannot use the named entry point is a failure even at exit 0, an absent `expect` sentinel is a failure even at exit 0, and a spec without one asserts nothing about output; end to end, a privatised `main` and a program that completed down a graceful arm each go red, and the same program passes once its own output is the sentinel, so the check reads the output rather than always failing. Which specs must carry a sentinel is **derived** from what each example declares — a resource effect in a function's effect row, or a call to a resource operation, both validated against the live effect registry so a renamed effect or op fails loudly — and asserted equal to the specs that have one, in both directions; the previous hard-coded triple could not see a fourth such example arriving without one. The runner's use of BOTH streams is pinned structurally -- `vera run` writes the note to stderr and nothing there on a clean exit, so no fixture can distinguish reading both streams from reading stdout alone, and a tripwire wired to the wrong stream is no tripwire. Also the hermetic-environment property: an ambient `VERA_DB_URL` or provider key is stripped so a gate run cannot be pointed at a real database or turned into a billed API call, a fixture spec puts its own URL back, and every neutralised name is checked to be one `vera/runtime/` actually reads | +| `test_check_corpus_differential.py` | 46 | 758 | `check_corpus_differential.py`, the burndown instrument that compiles the corpus at two revisions. The pure pieces only — the real two-revision run costs minutes and is not a test. **Classification**, all four verdicts: identical, WAT differs, and each one-sided compile failure as its own kind, since a compilability reversal reported as a text difference is the mis-description the instrument exists to avoid; failing at both revisions is not a mover and is counted separately, so a green run states how much of it was vacuous. **Enumeration** — recursive, keyed by repo-relative POSIX path, and an empty corpus is an error rather than a clean run over nothing. **The canary** — each side must import the compiler it was pointed at, so a side silently resolving to the venv's editable install cannot compare a revision against itself; an import failure and a foreign compiler are different messages. **Reporting** — every mover named with its reason, the exit code, the `--json` shape, and a program missing from one side reported rather than dropped. One test asserts the instrument is absent from `.pre-commit-config.yaml`, so the docstring's claim cannot rot | | `test_check_editor_grammars.py` | 20 | 249 | `check_editor_grammars.py` gate ([#1156](https://github.com/aallan/vera/issues/1156)): the registry read (every effect in, every ability out, and the four names the grammars actually drifted on present so the set checked is non-vacuous), the word-boundary presence test across all three grammar formats (JSON, plist XML, Vim keyword list) including the prefix pair `Http`/`HttpServer` in both directions, the deliberate comment-mention false pass, a metacharacter pair that only passes when the name is matched literally (`A.B` present, `A0B` not), and the empty registry; the gate's primary path end to end — a listed grammar with an effect stripped out, and a listed README with one stripped out of its prose bullet, each red against an otherwise-clean mirrored tree; the completeness guard — a grammar discovered under `editors/` but absent from `GRAMMARS` fails that same tree, over three discovery routes (`.el` outside a syntax directory, a tree-sitter `.scm` query set, a `.tmLanguage.json` filed anywhere but `syntaxes/`); and the registry's provenance, run as a subprocess against a throwaway checkout whose `vera` package names an effect the grammars do not, which is the only way to see that the list comes from the tree being checked rather than from site-packages. The shipped grammars and READMEs are currently clean | | `test_check_explicit_encoding.py` | 54 | 254 | `check_explicit_encoding.py` gate (#645): flags text-mode `open()` / `read_text()` / `write_text()` **and** `subprocess.run/Popen/check_output(..., text=True)` captures missing an `encoding="utf-8"` literal (rejects non-literal / non-UTF-8 values), skips binary/bytes-mode calls, honours the `# encoding-exempt` opt-out, and asserts the shipped repo is clean | | `test_check_limitations_sync.py` | 6 | 108 | `check_limitations_sync.py` section extraction: table-rows-only issue harvesting, prose-link exemption, bounding at the next second-level heading, `None` for absent or sub-level headings so renamed sections fail loudly; plus the #852 fail-loud rule: an UNKNOWN issue state under `--check-states` (gh missing / auth failure / timeout) is an error, never a silent pass | @@ -995,9 +996,9 @@ Twenty-nine scripts in `scripts/` validate cross-cutting concerns beyond unit te | `check_diagnostic_fields.py` | Every diagnostic in `vera/` carries rationale + spec_ref, and errors also a `fix` (warnings exempt); every present spec_ref resolves to a real spec section; every literal `error_code` is registered in `ERROR_CODES` (#828); `# diag-fields-exempt: ` waives missing/unresolvable fields only — never a wrong-but-resolving spec_ref or an unregistered error_code (#682, #955) | | `check_explicit_encoding.py` | Every text-mode `open()` / `read_text()` / `write_text()`, `subprocess.run/Popen/check_output` text capture, and text-mode `tempfile.NamedTemporaryFile` under `vera/`, `scripts/` and `tests/` passes an explicit `encoding="utf-8"`; `# encoding-exempt: ` opts a deliberate non-UTF-8 site out (#645) | | `check_e602_clean.py` | No unexpected E602/E604 silent-skip sites outside the explicit allowlist | -| `check_examples_run.py` | Every `examples/*.vera` either runs trap-free under the native runtime or carries a documented skip property. Two signals, as in `check_examples.py`: the exit code, and an output signal — every spec names its entry point (so a privatised or renamed `main` exits 1 instead of silently running another export) and the three environment-dependent examples pin a success sentinel (so a vanished fixture fails rather than passing on a graceful arm). An unclassified example is an error, and TESTING.md's execution-coverage table must match the script's own classification | +| `check_examples_run.py` | Every `examples/*.vera` either runs trap-free under the native runtime or carries a documented skip property. Two signals, as in `check_examples.py`: the exit code, and an output signal — every spec names its entry point (so a privatised or renamed `main` exits 1 instead of silently running another export) and every example that declares a resource effect or calls a resource operation pins a success sentinel (so a vanished fixture fails rather than passing on a graceful arm), the set being derived from those declarations rather than named. An unclassified example is an error, and TESTING.md's execution-coverage table must match the script's own classification | | `check_doc_builtin_shadowing.py` | No documentation example defines a function named after an opaque verifier-modelled built-in (would fail `vera check` with E151); the `spec/09` signature reference is exempt ([#819](https://github.com/aallan/vera/issues/819)) | -| `check_grammar_alignment.py` | Every rule header in `spec/10-grammar.md`'s EBNF has a same-named rule in `vera/grammar.lark`, and the reverse. Names only — rule bodies are not compared ([#683](https://github.com/aallan/vera/issues/683)) | +| `check_grammar_alignment.py` | Every rule header in `spec/10-grammar.md`'s EBNF has a same-named rule in `vera/grammar.lark`, and the reverse ([#683](https://github.com/aallan/vera/issues/683)); every terminal is declared and referenced within its own file, every regex-bodied terminal carries the same pattern in both, and each shared production's right-hand side refers to the same rules and terminals ([#1290](https://github.com/aallan/vera/issues/1290)). The *shape* of a right-hand side — alternation, grouping, repetition — is still not compared | | `check_editor_grammars.py` | Every editor grammar under `editors/` (vscode, TextMate, Vim), and the two extension READMEs that repeat the list in prose, carries every built-in effect name from the live registry — read from the checked-out tree, not from whatever `vera` is importable. Word-boundary presence: absence is conclusive, presence is optimistic — the observed failure is omission. A completeness guard fails any grammar discovered under `editors/` that the checked list doesn't name ([#1156](https://github.com/aallan/vera/issues/1156)) | | `check_distribution.py` | The built wheel and sdist carry the project's own name and version, ship the files the installed package needs plus a packaged LICENSE, and exclude `tests/` and generated Python files | | `check_wheel_availability.py` | Every runtime dependency ships wheels for all supported platforms | @@ -1006,6 +1007,8 @@ Twenty-nine scripts in `scripts/` validate cross-cutting concerns beyond unit te Each runs in its configured pre-commit hook or CI job, so issues are caught locally before they reach the remote; `build_site.py` is the generator whose output `check_site_assets.py` verifies. +One script is deliberately outside that set. `check_corpus_differential.py` compiles every corpus program at two revisions and reports the ones whose WAT moved, including the ones that compile on only one side — the measurement behind a "codegen is unchanged" claim, and the scope list when output is meant to change. It costs minutes rather than milliseconds, so it is a burndown instrument run by hand (`--base-ref origin/main`), not a hook and not a CI gate; a test asserts its absence from `.pre-commit-config.yaml` so that claim cannot rot. `check_doc_counts.py --check-bug-issues` is opt-in for the same kind of reason — it needs the GitHub API, which a commit hook must not — and belongs to the release PR (see `RELEASING.md`). + ### Spec validation pipeline `check_spec_examples.py` pushes spec code blocks through three compiler stages. A block that intentionally fails a stage carries an inline annotation on the line before its fence — `` (or `vera:skip-check` / `vera:skip-verify`; see `scripts/doc_annotations.py` and [#538](https://github.com/aallan/vera/issues/538)): @@ -1095,7 +1098,7 @@ The repository configures 36 hooks across two stages: 34 run at the commit stage | `check_pypi_readme_examples.py` | PYPI_README.md code blocks parse, check, and verify | | `check_html_examples.py` | HTML landing page code blocks pass parse + check + verify | | `check_doc_builtin_shadowing.py` | No doc example defines a function named after an opaque built-in (would fail `vera check` with E151); `spec/09` signature reference exempt ([#819](https://github.com/aallan/vera/issues/819)) | -| `check_grammar_alignment.py` | Spec EBNF and Lark grammar agree on every rule name ([#683](https://github.com/aallan/vera/issues/683)) | +| `check_grammar_alignment.py` | Spec EBNF and Lark grammar agree on every rule name ([#683](https://github.com/aallan/vera/issues/683)), every terminal, and the symbols each shared production refers to ([#1290](https://github.com/aallan/vera/issues/1290)) | | `check_editor_grammars.py` | Every editor grammar under `editors/`, and the two extension READMEs, carry every built-in effect name from the live registry ([#1156](https://github.com/aallan/vera/issues/1156)) | | `check_e602_clean.py` | No unexpected `[E602]` (body unsupported) / `[E604]` (param unsupported) silent skips outside the explicit allowlist (Layer 1 of [#626](https://github.com/aallan/vera/issues/626)) | | `check_examples_run.py` | Every example runs trap-free (exit code plus an output signal) or carries a documented skip property, and TESTING.md's execution-coverage table matches | diff --git a/docs/llms-full.txt b/docs/llms-full.txt index bb31edc9..8b6d0be0 100644 --- a/docs/llms-full.txt +++ b/docs/llms-full.txt @@ -3265,7 +3265,7 @@ The reference compiler is under active development. The current release includes - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute - A 14-chapter formal specification -- 11,786 tests, including a 244-program conformance suite +- 11,940 tests, including a 244-program conformance suite - 42 working example programs - 164 built-in functions covering strings, arrays, math, parsing, and data types - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation diff --git a/scripts/check_corpus_differential.py b/scripts/check_corpus_differential.py new file mode 100644 index 00000000..1a6d9847 --- /dev/null +++ b/scripts/check_corpus_differential.py @@ -0,0 +1,777 @@ +#!/usr/bin/env python +"""Burndown instrument: compile every corpus program at two revisions +and report which ones MOVED. + + python scripts/check_corpus_differential.py --base-ref origin/main + +**This is not a pre-commit hook and not a CI gate.** It compiles the +whole corpus twice — once with the working tree's compiler, once with +the compiler at ``--base-ref`` — so a run costs minutes, not the +milliseconds a commit hook may spend. It is deliberately absent from +``.pre-commit-config.yaml``, and `tests/test_check_corpus_differential.py` +asserts that absence so the claim cannot rot. Run it by hand when the +question it answers is the one you have. + +That question is: **did this change move any compiled output, and if so, +exactly which programs?** It has two uses, and they are the same +measurement read in opposite directions: + +- *Proving a change inert.* A refactor, a rename, a whitelist + reshuffle — the claim "codegen is unchanged" is otherwise an argument + from reading the diff. Zero movers over the whole corpus is evidence. + PR #1323 made exactly this claim with an ad-hoc version of this + script; promoting it means the next such claim is reproducible rather + than re-improvised. +- *Enumerating what a change moved.* When output is meant to change, + the mover list is the scope of the change, program by program — + including the programs nobody expected it to reach. + +The comparison surface is the **WAT text** (`vera compile --wat`), which +is what "byte-identical WAT" meant in the PR #1323 record, compared by +SHA-256 digest. Four verdicts per program, from two compiles: + +| base | head | verdict | +|-----------|-----------|-------------------------------| +| same WAT | same WAT | not a mover | +| WAT A | WAT B | mover — `WAT differs` | +| failed | compiled | mover — `compiles only at HEAD` | +| compiled | failed | mover — `compiles only at ` | +| failed | failed | not a mover, counted separately | + +The two one-sided-failure rows are the reason this is not a `diff` over +saved WAT files. A program whose compilability *reverses* has no WAT on +one side, and a comparison that only knows "same text / different text" +reports that as a text difference — which is the class the PR #1323 +record called out as having been mis-described. They are distinct +verdicts here, and each names the direction. + +The both-failed row is counted and printed rather than folded into +agreement. The corpus deliberately contains negative fixtures that fail +to compile at every revision; they agree vacuously, and a reader of a +green run is entitled to know how much of it was actually measured. + +**How the two sides are built.** The corpus is the *working tree's* +`.vera` files, and *both* sides compile those same files — only the +compiler differs. That isolates a compiler change from a corpus change: +a program edited in the working tree is compiled from its edited text on +both sides, so it moves only if the compiler moved under it. A program +using a feature the base compiler lacks shows up as `compiles only at +HEAD`, which is the true verdict. + +The head side is the working tree as it stands, uncommitted edits +included. The base side is materialised with ``git worktree add +--detach`` into ``--work-dir`` and driven through its *own* checkout: the +subprocess runs with ``cwd`` and ``PYTHONPATH`` set to that directory, so +``python -m vera.cli`` there resolves ``vera`` to the base revision's +package. Each side is probed first (`canary_error`) to confirm it +imported the compiler it was supposed to: the venv may carry an editable +install of a *third* checkout, and a side that silently resolved to it +would compare a revision against itself and report zero movers — +a green verdict that measured nothing. + +**The base checkout is left on disk.** It is keyed by the base commit's +SHA and reused by later runs against the same revision, so repeated runs +pay for one checkout per revision rather than one per run. Its path is +printed on every run. Removing it is the caller's business: + + git worktree remove # or: git worktree prune + +Requires the base revision's compiler to run under the *current* venv's +installed dependencies — the base checkout supplies `vera/`, not its own +site-packages. Across a dependency bump this instrument compares what +the current environment can run, which is worth knowing before reading +its verdict. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import os +import re +import subprocess +import sys +from collections.abc import Callable +from concurrent.futures import ThreadPoolExecutor +from pathlib import Path, PurePath +from typing import NamedTuple + + +# The corpus: everything `vera check` can reach under these roots, at any +# depth. `examples/vera/` and `tests/conformance/vera/` hold the modules +# the top-level programs import — a non-recursive glob would compare a +# program while ignoring the source it is built from, the gap +# `scripts/check_corpus_canonical.py` records having had. +_CORPUS_DIRS = ("examples", "tests/conformance") + +# The base checkout's default home. Repository-local rather than under +# `tempfile.gettempdir()`: the path is fully predictable (a fixed directory +# name plus a public commit SHA), `base_checkout` reuses a pre-existing +# directory, and `_side_env` then puts it on PYTHONPATH — so on a shared +# machine another local user could plant a `vera` package there and the base +# side would import it. The canary cannot object, because the planted +# package sits under the expected root (#1329 review). +_DEFAULT_WORK_DIR = Path(__file__).resolve().parent.parent / ".corpus-differential" + + +def _positive_seconds(value: str) -> int: + """An `argparse` type for a budget that must be able to elapse. + + Zero or negative expires before any compile finishes, so both sides + fail every program, `compare` counts them all as `both_failed`, and + the run reports "No movers" over a corpus that never compiled. + """ + seconds = int(value) + if seconds <= 0: + raise argparse.ArgumentTypeError( + f"--timeout must be greater than zero, not {seconds}" + ) + return seconds + + +# Per-file compile budget. Generous — a corpus program compiles in well +# under a second — so this only fires on a genuine hang, and a hang on +# one side is reported as that side failing rather than blocking the run. +DEFAULT_TIMEOUT_SECONDS = 120 + +# The first line of a Vera error diagnostic: `[E154] Error at , +# line N, column M:` — or the same without a code, which a few carry. +# Anchored so a warning's message body, which quotes neither, cannot +# match. +_ERROR_MARKER = re.compile(r"^(\[E\d+\]\s*)?Error\b") + + +# --------------------------------------------------------------------------- +# Data +# --------------------------------------------------------------------------- + +# ``NamedTuple`` rather than ``@dataclass`` throughout: this module is +# loaded by its tests with the bare ``spec_from_file_location`` / +# ``exec_module`` recipe, which leaves the module unregistered in +# ``sys.modules`` — and ``@dataclass`` resolves its annotations through +# ``sys.modules[cls.__module__]``. Same reason as +# `scripts/check_examples_run.py`. + + +class Artifact(NamedTuple): + """One program's compiled output at one revision. + + ``digest`` is the SHA-256 of the WAT text and is ``None`` exactly + when ``ok`` is False — there is no artifact to compare, and the + reason lives in ``error``. + """ + + ok: bool + digest: str | None + size: int + error: str + + +class Mover(NamedTuple): + """A program whose compiled output changed between the revisions.""" + + path: str + kind: str + reason: str + + +class Comparison(NamedTuple): + """The whole corpus, classified. + + ``compared`` counts the programs both sides reported on, and + partitions exactly into ``identical + both_failed + len(movers)``. + ``unreported`` holds programs only one side reported on at all — a + truncated run, which is a failure rather than a quiet shortfall. + """ + + movers: list[Mover] + compared: int + identical: int + both_failed: int + unreported: list[str] + + +class RunInfo(NamedTuple): + """What the run compared, for the report and the JSON envelope.""" + + base_ref: str + base_sha: str + base_root: str + head_root: str + + +# --------------------------------------------------------------------------- +# The corpus +# --------------------------------------------------------------------------- + + +def corpus_files(root: Path) -> list[Path]: + """Every corpus program under `root`, at any depth, in path order.""" + files: list[Path] = [] + for directory in _CORPUS_DIRS: + files.extend(sorted((root / directory).rglob("*.vera"))) + return files + + +def corpus_guard(files: list[Path], root: Path) -> str | None: + """Refuse to run on an empty corpus; ``None`` when there is one. + + A differential over zero programs finds zero movers, and zero movers + is this instrument's success verdict — so an enumeration that stops + matching would report "nothing moved" over nothing at all, which is + the single failure mode most likely to be believed. + """ + if files: + return None + return ( + f"could not find any .vera programs under {root} " + f"({', '.join(_CORPUS_DIRS)}). This is an error rather than a " + f"clean run: a differential over an empty corpus reports zero " + f"movers, which is indistinguishable from a change that moved " + f"nothing." + ) + + +# --------------------------------------------------------------------------- +# Classification +# --------------------------------------------------------------------------- + + +def classify( + base: Artifact, head: Artifact, base_label: str +) -> tuple[str, str] | None: + """``(kind, reason)`` when this program moved, ``None`` when it did + not. + + Compilability is checked before the digests, because a program that + compiles at only one revision has no artifact to compare and must be + named for the *direction* it moved in — reporting it as a text + difference is the mis-description PR #1323's record calls out. + """ + if base.ok and head.ok: + if base.digest == head.digest: + return None + return ( + "wat-differs", + f"WAT differs (at {base_label}: {_short(base.digest)}, " + f"{base.size} bytes; at HEAD: {_short(head.digest)}, " + f"{head.size} bytes)", + ) + + if head.ok and not base.ok: + return ( + "head-only", + f"compiles only at HEAD (at {base_label} it failed: " + f"{base.error})", + ) + + if base.ok and not head.ok: + return ( + "base-only", + f"compiles only at {base_label} (at HEAD it failed: " + f"{head.error})", + ) + + # Neither side produced an artifact — the negative conformance + # fixtures live here. Not a mover; counted separately by `compare` + # so the agreement it contributes is never read as measurement. + return None + + +def _short(digest: str | None) -> str: + return "none" if digest is None else digest[:12] + + +def compare( + base: dict[str, Artifact], head: dict[str, Artifact], base_label: str +) -> Comparison: + """Classify every program both sides reported on.""" + movers: list[Mover] = [] + identical = 0 + both_failed = 0 + compared = 0 + + for path in sorted(set(base) & set(head)): + compared += 1 + verdict = classify(base[path], head[path], base_label) + if verdict is not None: + movers.append(Mover(path=path, kind=verdict[0], reason=verdict[1])) + elif not base[path].ok and not head[path].ok: + both_failed += 1 + else: + identical += 1 + + return Comparison( + movers=movers, + compared=compared, + identical=identical, + both_failed=both_failed, + unreported=sorted(set(base) ^ set(head)), + ) + + +# --------------------------------------------------------------------------- +# Compiling one side +# --------------------------------------------------------------------------- + + +def canary_error(reported: str, root: Path, side: str) -> str | None: + """The load-bearing guard: did this side import the compiler it was + pointed at? + + Both sides run the same ``python -m vera.cli`` and differ only in + ``PYTHONPATH``/``cwd``. The venv also carries an editable install of + whichever checkout was `pip install -e`'d, reachable through a + finder on ``sys.meta_path``. A side that resolved to *that* would + compile with the wrong compiler, and the run would report zero + movers no matter what the change did. + """ + if not reported.strip(): + return ( + f"the {side} side could not import `vera` at all from {root} " + f"— the differential cannot run. Check that the checkout is " + f"intact and that the current environment satisfies its " + f"dependencies." + ) + + resolved = Path(reported.strip()).resolve() + expected = root.resolve() + if resolved == expected or expected in resolved.parents: + return None + + return ( + f"the {side} side imported {reported.strip()}, which is not under " + f"{root} — it is compiling with a different checkout's compiler, " + f"so the differential would compare a revision against itself and " + f"report zero movers. Usually an editable install shadowing the " + f"path, or a stale PYTHONPATH." + ) + + +def _side_env(root: Path) -> dict[str, str]: + """The environment one side's compiles run under. + + ``PYTHONPATH`` is *replaced*, never extended: the caller's own + ``PYTHONPATH`` frequently points at the head checkout (that is how + this repo is driven), and inheriting it on the base side would put + the head compiler first on the path — the exact vacuity + `canary_error` exists to catch. + """ + env = dict(os.environ) + env["PYTHONPATH"] = str(root) + # No .pyc into either checkout: the base one is a scratch worktree, + # and stale bytecode across revisions has bitten this project before. + env["PYTHONDONTWRITEBYTECODE"] = "1" + return env + + +def probe_compiler(python: str, root: Path) -> str: + """Where this side's `vera` package actually resolves to, or ``""``.""" + result = subprocess.run( + [python, "-c", "import vera, sys; sys.stdout.write(vera.__file__)"], + capture_output=True, + text=True, + encoding="utf-8", + cwd=str(root), + env=_side_env(root), + check=False, + ) + return result.stdout if result.returncode == 0 else "" + + +def _first_error(stderr: str, path: PurePath) -> str: + """The compile's reason, in one line. + + A Vera diagnostic is a *block* — marker line, quoted source, caret, + message — and only the first line carries the marker. Skipping + lines that start with ``warning:`` is therefore not enough to skip a + warning: a real run against v0.1.9 reported a warning's quoted + source line (``public fn read_some(@Unit -> @Int)``) as the reason a + program failed to compile. The error's own marker line is what to + look for. + + With no marker anywhere the compile did not produce a diagnostic at + all — it crashed. The informative line of a traceback (and of an + argparse usage error) is the last, not the first. + + The program's own path is stripped back to its name: the reason is + already attached to a named program, and a corpus file's absolute + path under a scratch checkout is long enough on its own to push the + diagnostic past the truncation. + + Both spellings of that path are stripped. Matching on ``str(path)`` + alone ties the strip to the host's separator, and a diagnostic is + free to print the POSIX form on Windows — whereupon the strip + matches nothing, silently, and the truncation eats the message + instead of the path. The parameter is a ``PurePath`` rather than a + ``Path`` for the same reason: nothing here touches the filesystem, + and the wider type lets a test render a Windows path on any host. + """ + lines = [line.strip() for line in stderr.splitlines()] + nonempty = [line for line in lines if line] + + for line in nonempty: + if _ERROR_MARKER.match(line): + reason = line + break + else: + reason = nonempty[-1] if nonempty else "compile failed with no output" + + for rendering in (str(path), path.as_posix()): + reason = reason.replace(rendering, path.name) + return reason[:160] + + +def compile_one( + python: str, compiler_root: Path, timeout: int, path: Path +) -> Artifact: + """Compile one program with one side's compiler. + + Deliberately the CLI rather than the codegen API: ``vera compile + --wat`` is the surface that holds its shape across revisions, and + this script runs unchanged against a compiler whose internals it may + predate. A failure is *data* — the failure-direction verdicts are + half of what the instrument measures — so nothing here raises. + """ + try: + result = subprocess.run( + [python, "-m", "vera.cli", "compile", "--wat", str(path)], + capture_output=True, + text=True, + encoding="utf-8", + # A compiler is free to emit a byte this codec cannot read, and + # strict decoding would raise UnicodeDecodeError out of + # `subprocess.run` — a ValueError that neither handler below + # catches, aborting the whole corpus run through + # `ThreadPoolExecutor.map`. An undecodable diagnostic is data + # like any other failure (#1329 review). + errors="replace", + cwd=str(compiler_root), + env=_side_env(compiler_root), + stdin=subprocess.DEVNULL, + timeout=timeout, + check=False, + ) + except subprocess.TimeoutExpired: + return Artifact( + ok=False, digest=None, size=0, + error=f"compile exceeded the {timeout}s budget", + ) + except OSError as exc: # the interpreter or checkout is not usable + return Artifact( + ok=False, digest=None, size=0, error=f"could not run: {exc}", + ) + + if result.returncode != 0: + return Artifact( + ok=False, digest=None, size=0, + error=_first_error(result.stderr, path), + ) + + wat = result.stdout + digest = hashlib.sha256(wat.encode("utf-8")).hexdigest() + return Artifact(ok=True, digest=digest, size=len(wat), error="") + + +def collect( + files: list[Path], + corpus_root: Path, + compile_fn: Callable[[Path], Artifact], + jobs: int = 1, +) -> dict[str, Artifact]: + """Compile every file, keyed by its path relative to `corpus_root`. + + Both sides compile the *same* files — the working tree's — so both + maps are keyed against the same root and line up by construction. + An absolute key would not: the base compiler runs from a scratch + checkout, and keying by anything side-specific would leave every + program unreported. POSIX form because the key is compared as a + string (CLAUDE.md's cross-platform rule). + """ + keys = [_key(path, corpus_root) for path in files] + if jobs <= 1: + results = [compile_fn(path) for path in files] + else: + with ThreadPoolExecutor(max_workers=jobs) as pool: + # `map` yields in input order, so the zip below cannot + # misattribute a result to the wrong program. + results = list(pool.map(compile_fn, files)) + return dict(zip(keys, results, strict=True)) + + +def _key(path: Path, corpus_root: Path) -> str: + try: + return path.relative_to(corpus_root).as_posix() + except ValueError: + return path.as_posix() + + +# --------------------------------------------------------------------------- +# The base checkout +# --------------------------------------------------------------------------- + + +def resolve_ref(repo_root: Path, ref: str) -> str | None: + """The commit SHA `ref` names, or ``None`` when git cannot resolve it.""" + result = subprocess.run( + ["git", "-C", str(repo_root), "rev-parse", "--verify", f"{ref}^{{commit}}"], + capture_output=True, + text=True, + encoding="utf-8", + check=False, + ) + return result.stdout.strip() if result.returncode == 0 else None + + +def base_checkout( + repo_root: Path, sha: str, work_dir: Path +) -> tuple[Path | None, str]: + """A checkout of `sha`, materialised under `work_dir` if need be. + + Returns ``(path, "")`` or ``(None, error)``. Named by SHA and + reused when it is already there, so a burndown session that runs the + differential repeatedly against one base pays for one checkout. It + is never removed — see the module docstring. + """ + dest = work_dir / f"vera-base-{sha[:12]}" + + if dest.exists(): + current = subprocess.run( + ["git", "-C", str(dest), "rev-parse", "HEAD"], + capture_output=True, + text=True, + encoding="utf-8", + check=False, + ) + if ( + current.returncode == 0 + and current.stdout.strip() == sha + and (dest / "vera" / "__init__.py").is_file() + ): + return dest, "" + return None, ( + f"{dest} already exists but is not a clean checkout of {sha[:12]} " + f"— this script never deletes it. Move it aside, or pass a " + f"different --work-dir." + ) + + work_dir.mkdir(parents=True, exist_ok=True) + result = subprocess.run( + ["git", "-C", str(repo_root), "worktree", "add", "--detach", + str(dest), sha], + capture_output=True, + text=True, + encoding="utf-8", + check=False, + ) + if result.returncode != 0: + return None, ( + f"could not create a worktree for {sha[:12]} at {dest}: " + f"{result.stderr.strip() or result.stdout.strip()}" + ) + return dest, "" + + +# --------------------------------------------------------------------------- +# Reporting +# --------------------------------------------------------------------------- + + +def json_payload(info: RunInfo, comparison: Comparison) -> dict[str, object]: + return { + "ok": not comparison.movers and not comparison.unreported, + "base_ref": info.base_ref, + "base_sha": info.base_sha, + "base_root": info.base_root, + "head_root": info.head_root, + "compared": comparison.compared, + "identical": comparison.identical, + "both_failed": comparison.both_failed, + "movers": [m._asdict() for m in comparison.movers], + "unreported": comparison.unreported, + } + + +def summary_lines(info: RunInfo, comparison: Comparison) -> list[str]: + """The stdout summary — what was compared, and how it partitioned.""" + return [ + f"Corpus differential: {comparison.compared} programs compiled at " + f"both revisions.", + f" base: {info.base_ref} ({info.base_sha[:12]}) -> {info.base_root}", + f" head: working tree -> {info.head_root}", + f" identical WAT: {comparison.identical}", + f" compiled at neither revision: {comparison.both_failed} " + f"(vacuous agreement — nothing was compared for these)", + f" movers: {len(comparison.movers)}", + ] + + +def failure_lines(info: RunInfo, comparison: Comparison) -> list[str]: + """The stderr report: every mover, then what to do about it.""" + lines: list[str] = [] + if comparison.movers: + lines.append(f"MOVERS ({len(comparison.movers)}):") + lines += [f" {m.path}: {m.reason}" for m in comparison.movers] + lines += [ + "", + "Each line is a program whose compiled output changed between " + f"{info.base_ref} and the working tree. If the change under " + "test was meant to be inert, these are its counter-examples; if " + "it was meant to move output, this is the enumeration of what " + "it moved. Reproduce one with:", + "", + " vera compile --wat # working tree", + f" (cd {info.base_root} && vera compile --wat " + f"{info.head_root}/)", + "", + " is the mover's path above, and BOTH commands compile " + "the working tree's copy of it — that is what the differential " + "compared. A relative path in the second command would compile " + "the base checkout's own copy instead, which is a different " + "input whenever the corpus source has changed.", + ] + if comparison.unreported: + if lines: + lines.append("") + lines.append(f"UNREPORTED ({len(comparison.unreported)}):") + lines += [f" {path}" for path in comparison.unreported] + lines += [ + "", + "The two sides did not report on the same set of programs, so " + "the run is truncated rather than clean — its verdict covers " + "less than the corpus. Usually a side that crashed partway.", + ] + return lines + + +def emit(info: RunInfo, comparison: Comparison, *, as_json: bool) -> int: + """Print the verdict; return the exit code (0 clean, 1 moved).""" + payload = json_payload(info, comparison) + if as_json: + print(json.dumps(payload, indent=2)) + return 0 if payload["ok"] else 1 + + for line in summary_lines(info, comparison): + print(line) + + lines = failure_lines(info, comparison) + if lines: + print("", file=sys.stderr) + for line in lines: + print(line, file=sys.stderr) + return 1 + + print( + f"\nNo movers: the working tree's compiled output is identical to " + f"{info.base_ref}'s across the corpus." + ) + return 0 + + +# --------------------------------------------------------------------------- +# Entry point +# --------------------------------------------------------------------------- + + +def _parse_args(argv: list[str] | None) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description=( + "Compile the corpus at two revisions and report which " + "programs moved. Burndown instrument — not a hook." + ), + ) + parser.add_argument( + "--base-ref", default="origin/main", + help="revision to compare the working tree against " + "(default: origin/main)", + ) + parser.add_argument( + "--work-dir", + default=str(_DEFAULT_WORK_DIR), + help="where the base revision is checked out; the checkout is " + "keyed by SHA, reused, and never deleted " + "(default: %(default)s)", + ) + parser.add_argument( + "--jobs", type=int, default=min(8, os.cpu_count() or 1), + help="parallel compiles per side (default: %(default)s)", + ) + parser.add_argument( + "--timeout", type=_positive_seconds, default=DEFAULT_TIMEOUT_SECONDS, + help="per-program compile budget in seconds (default: %(default)s)", + ) + parser.add_argument( + "--json", action="store_true", dest="as_json", + help="emit the verdict as JSON on stdout", + ) + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + args = _parse_args(argv) + repo_root = Path(__file__).resolve().parent.parent + + files = corpus_files(repo_root) + problem = corpus_guard(files, repo_root) + if problem is not None: + print(f"ERROR: {problem}", file=sys.stderr) + return 1 + + sha = resolve_ref(repo_root, args.base_ref) + if sha is None: + print( + f"ERROR: git cannot resolve --base-ref {args.base_ref!r} to a " + f"commit in {repo_root}. Fetch it first (`git fetch origin`), " + f"or name a revision that exists locally.", + file=sys.stderr, + ) + return 1 + + base_root, problem = base_checkout(repo_root, sha, Path(args.work_dir)) + if base_root is None: + print(f"ERROR: {problem}", file=sys.stderr) + return 1 + print(f"Base checkout (left in place): {base_root}", file=sys.stderr) + + # Both canaries before either side's corpus run: a side pointing at + # the wrong compiler makes the whole differential vacuous, and that + # must be a refusal rather than a green run. + for side, root in (("head", repo_root), ("base", base_root)): + problem = canary_error(probe_compiler(sys.executable, root), root, side) + if problem is not None: + print(f"ERROR: {problem}", file=sys.stderr) + return 1 + + info = RunInfo( + base_ref=args.base_ref, + base_sha=sha, + base_root=str(base_root), + head_root=str(repo_root), + ) + + sides: dict[str, dict[str, Artifact]] = {} + for side, root in (("base", base_root), ("head", repo_root)): + print( + f"Compiling {len(files)} programs with the {side} compiler " + f"({root})...", + file=sys.stderr, + ) + sides[side] = collect( + files, + repo_root, + lambda path, root=root: compile_one( + sys.executable, root, args.timeout, path + ), + jobs=args.jobs, + ) + + return emit( + info, + compare(sides["base"], sides["head"], args.base_ref), + as_json=args.as_json, + ) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/check_doc_counts.py b/scripts/check_doc_counts.py index 8d45b8c4..61fd41a0 100644 --- a/scripts/check_doc_counts.py +++ b/scripts/check_doc_counts.py @@ -5,22 +5,29 @@ files, pre-commit hooks, CI jobs) and pytest-collection counts (total tests, per-file test counts and line counts) against the numbers written in TESTING.md, CONTRIBUTING.md, CLAUDE.md, README.md, SKILL.md, AGENTS.md, -FAQ.md, and ROADMAP.md. Also checks TESTING.md's passed/stress/skipped +FAQ.md, and ROADMAP.md. Also checks TESTING.md's passed/stress-deselected/skipped breakdown against the collected total, the KNOWN_ISSUES.md "Refactoring needed" line counts (±10% tolerance), the HISTORY.md version-row format (one issue link max, no " — " separator per row), the vera/README.md module map (#1150) and its Test Suite paragraph's four counts, the project facts hardcoded on the landing page (#528), and the cited corpus-program -count. +count. Three more were added for #1290: every figure on README's +project-status line rather than only its test count; TESTING.md's dual-target +conformance row, whose split and category counts come from a live run of the +differential itself; and the shape of KNOWN_ISSUES.md's Bugs table. Intentionally excludes CHANGELOG.md: its counts are historical records (e.g. "64 programs, was 63") that are frozen snapshots of the project state at each release. Validating them would cause false positives on every new conformance addition, because the old entries are supposed to stay unchanged. -Runs in a couple of seconds — fast enough for a pre-commit hook. +Runs in a few seconds — fast enough for a pre-commit hook. Everything it +does is local: the one check that needs the GitHub API, the Bugs table +against the open `bug`-labelled issues, is opt-in behind --check-bug-issues, +for the release PR. A commit hook must not depend on a network call. """ +import argparse import json import os import re @@ -28,6 +35,8 @@ import sys import tomllib from pathlib import Path +from typing import NamedTuple +from urllib.request import Request, urlopen def check_refactoring_counts(known_issues_text: str, root: Path) -> list[str]: @@ -79,15 +88,24 @@ def check_refactoring_counts(known_issues_text: str, root: Path) -> list[str]: _TESTS_BREAKDOWN = re.compile( r"\*\*Tests\*\*\s*\|\s*[\d,]+\s+across.*?;\s*([\d,]+) passed" - r"\s*\+\s*([\d,]+) stress,\s*([\d,]+) skipped" + r"\s*\+\s*([\d,]+) stress-deselected,\s*([\d,]+) skipped" ) def check_tests_breakdown(testing_text: str, live_total: int) -> list[str]: """Check that TESTING.md's tests breakdown sums to the gated total. + All three parts name a pytest *disposition*, which is what makes the + sum readable: the 26 are deselected before the run by + ``addopts = "-m 'not stress'"``, so they are disjoint from the passed + count rather than a subset of it. Naming the marker alone — "26 + stress" beside "passed" and "skipped" — invited reading them as + stress tests that passed, which would make the sentence's arithmetic + wrong (PR #1329 review). + The overview row states the total *and* its parts, in the shape - "1,306 across 40 files (…; 1,234 passed + 5 stress, 67 skipped)" — + "1,306 across 40 files (…; 1,234 passed + 5 stress-deselected, 67 + skipped)" — illustrative numbers, so this docstring does not itself become a citation to keep in sync. Pinning the total alone leaves the parts free to drift, so a release that moves the parts without moving the @@ -106,7 +124,8 @@ def check_tests_breakdown(testing_text: str, live_total: int) -> list[str]: if m is None: return [ "TESTING.md: no tests breakdown matched" - " ('N passed + N stress, N skipped') — the row moved or was" + " ('N passed + N stress-deselected, N skipped') — the row" + " moved or was" " reworded, so the breakdown is no longer gated" ] parts = [int(g.replace(",", "")) for g in m.groups()] @@ -115,7 +134,8 @@ def check_tests_breakdown(testing_text: str, live_total: int) -> list[str]: passed, stress, skipped = parts return [ f"TESTING.md tests breakdown: {passed:,} passed" - f" + {stress:,} stress + {skipped:,} skipped = {total:,}," + f" + {stress:,} stress-deselected + {skipped:,} skipped" + f" = {total:,}," f" but the collected total is {live_total:,}" ] return [] @@ -825,7 +845,339 @@ def check_module_map(readme_text: str, root: Path) -> list[str]: return errors +# --------------------------------------------------------------------------- +# README's project-status line +# +# One sentence carries six live figures and the oracle read one of them. The +# `check_readme` closure it used returned silently when a pattern matched +# nothing, and four of its five patterns matched nothing at all — so the +# conformance count beside the gated tests count drifted through two rebases +# unseen. Every figure on the line is gated here, and a figure that has gone +# missing is an error rather than a skip. +# --------------------------------------------------------------------------- + +_STATUS_LINE = re.compile(r"^.*?\btests, \d+% Python code coverage.*$", re.M) +_STATUS_FIGURES = ( + (r"([\d,]+) tests,", "tests"), + (r"([\d,]+) conformance programs", "conformance programs"), + (r"([\d,]+) examples", "examples"), + (r"(\d+)-chapter specification", "spec chapters"), +) + + +def check_project_status( + readme_text: str, + live_tests: int, + live_conformance: int, + live_examples: int, + live_chapters: int, +) -> list[str]: + """Check every count on README.md's project-status line.""" + line = _STATUS_LINE.search(readme_text) + if line is None: + return [ + "README.md: could not find the project-status line " + "(`… tests, N% Python code coverage …`)" + ] + expected = (live_tests, live_conformance, live_examples, live_chapters) + errors: list[str] = [] + for (pattern, label), live in zip(_STATUS_FIGURES, expected, strict=True): + found = re.search(pattern, line.group(0)) + if found is None: + errors.append( + f"README.md project-status line: could not find the {label} count" + ) + continue + cited = int(found.group(1).replace(",", "")) + if cited != live: + errors.append( + f"README.md project-status {label}: doc says {cited}, live is {live}" + ) + return errors + + +# --------------------------------------------------------------------------- +# TESTING.md's dual-target conformance row +# +# The row states a run-level total, a tested/skipped split and three category +# counts. The total has an oracle in the conformance manifest; the rest had +# none, and the row explicitly claims the excluded set is "defined by those +# three properties rather than by a filename list, so it stays accurate as +# programs are added" — a claim that only holds if something measures it. The +# split comes from a live `-rs` run of the differential, about three seconds. +# --------------------------------------------------------------------------- + + +class DualTargetSplit(NamedTuple): + """What a live run of the dual-target differential actually did.""" + + tested: int + skipped: int + families: int + no_main: int + nondeterministic: int + + +_DUAL_TARGET_TEST = "tests/test_wasi_target.py::TestDualTargetConformance" +_SKIP_REASONS = ( + ("families", "host famil"), + ("no_main", "zero-argument"), + ("nondeterministic", "nondeterministic ops"), +) +_SKIP_LINE = re.compile(r"^SKIPPED \[(\d+)\] (.*)$", re.M) +# pytest omits a category with a zero count, so "174 passed in 3.1s" and +# "52 skipped in 3.1s" are both well-formed summaries. A pattern +# requiring both made either one unreadable, and an unreadable report is +# a gate failure — a false one (#1329 review). +_PYTEST_TOTALS = re.compile(r"(\d+) (passed|skipped)\b") +_PYTEST_SUMMARY = re.compile(r"\d+ (?:passed|skipped)\b[^\n]*\bin [\d.]+s") +_DUAL_TARGET_FIGURES = ( + ("tested", r"(\d+) are dual-tested"), + ("skipped", r"and (\d+) skip"), + ("families", r"(\d+) whose compiled WAT"), + ("no_main", r"(\d+) with no public zero-argument"), + ("nondeterministic", r"and (\d+) calling a nondeterministic op"), +) + + +def parse_dual_target_report(report: str) -> DualTargetSplit | None: + """Read a split out of pytest's ``-rs`` output, or ``None``. + + ``None`` means the run cannot be read — no summary line, or a skip whose + reason matches none of the three documented properties. A new skip reason + is exactly the case the row's "stays accurate as programs are added" claim + needs to hear about, so it must not be silently folded into a category. + """ + summary = _PYTEST_SUMMARY.search(report) + if summary is None: + return None + totals = {kind: int(n) for n, kind in _PYTEST_TOTALS.findall(summary.group(0))} + counts = dict.fromkeys((name for name, _ in _SKIP_REASONS), 0) + for raw, reason in _SKIP_LINE.findall(report): + for name, marker in _SKIP_REASONS: + if marker in reason: + counts[name] += int(raw) + break + else: + return None + skipped = totals.get("skipped", 0) + if sum(counts.values()) != skipped: + return None + return DualTargetSplit(totals.get("passed", 0), skipped, **counts) + + +def dual_target_split(root: Path) -> DualTargetSplit | None: + """Run the dual-target differential and report what it did.""" + pytest_bin = root / ".venv/bin/pytest" + if not pytest_bin.exists(): + pytest_bin = Path("pytest") + try: + result = subprocess.run( + [str(pytest_bin), _DUAL_TARGET_TEST, "-q", "-rs", "-p", "no:randomly"], + capture_output=True, + text=True, + encoding="utf-8", + cwd=str(root), + timeout=300, + check=False, + ) + except (OSError, subprocess.SubprocessError): + # Every other check here turns a failure into a string in `errors` + # and lets `main` print the whole list. Letting this one raise + # would end the run on a traceback and the other twenty checks + # would never report — and this call is on the default path, so + # the pre-commit hook takes it every time (#1329 review). + return None + if result.returncode != 0: + return None + return parse_dual_target_report(result.stdout) + + +def check_dual_target_row( + testing_text: str, run_level_total: int, split: DualTargetSplit +) -> list[str]: + """Check TESTING.md's dual-target row against the manifest and a run.""" + errors: list[str] = [] + cited_total = re.search(r"all ([\d,]+) run-level", testing_text) + if cited_total is None: + errors.append( + "TESTING.md: could not find the dual-target run-level total " + "(`all N run-level conformance programs`)" + ) + elif int(cited_total.group(1).replace(",", "")) != run_level_total: + errors.append( + f"TESTING.md dual-target run-level total: doc says " + f"{cited_total.group(1)}, manifest has {run_level_total}" + ) + + cited: dict[str, int] = {} + for name, pattern in _DUAL_TARGET_FIGURES: + found = re.search(pattern, testing_text) + if found is None: + errors.append( + f"TESTING.md dual-target row: could not find the {name} count" + ) + continue + cited[name] = int(found.group(1)) + if cited[name] != getattr(split, name): + errors.append( + f"TESTING.md dual-target {name}: doc says {cited[name]}, " + f"a live run has {getattr(split, name)}" + ) + if len(cited) == len(_DUAL_TARGET_FIGURES): + if cited["tested"] + cited["skipped"] != run_level_total: + errors.append( + f"TESTING.md dual-target row does not add up: " + f"{cited['tested']} + {cited['skipped']} is not {run_level_total}" + ) + categories = cited["families"] + cited["no_main"] + cited["nondeterministic"] + if categories != cited["skipped"]: + errors.append( + f"TESTING.md dual-target skip categories do not add up: " + f"{categories} is not {cited['skipped']}" + ) + return errors + + +# --------------------------------------------------------------------------- +# KNOWN_ISSUES' Bugs table against the tracker +# +# The convention is one row per open `bug`-labelled issue. Two halves, and +# they are separated on purpose: the structural half is pure text and runs +# always, while the parity half needs the GitHub API and a pre-commit hook must +# not depend on a network call — it is opt-in via `--check-bug-issues`, for the +# release PR, where the tracker and the file are meant to agree. Mid-burndown +# they legitimately do not: a bug filed on an open PR's branch has an issue +# before it has a row. +# --------------------------------------------------------------------------- + +_BUGS_SECTION = re.compile(r"^## Bugs[ \t]*$(.*?)(?=^## |\Z)", re.M | re.S) +_ISSUE_LINK = re.compile(r"\[#(\d+)\]\(https://github\.com/[\w.-]+/[\w.-]+/issues/(\d+)\)") +_NO_BUGS = "No known bugs." + + +def bug_rows(known_issues_text: str) -> list[int] | None: + """Issue numbers from the Bugs table's Issue column, in order. + + The Issue column is a row's canonical tracker, and it is the only place + read: rows cross-link other issues in their prose, and counting those + would make one bug's context read as another bug's row. + + ``[]`` is the documented empty state — the section body is exactly "No + known bugs." — and ``None`` means the section could not be read at all. + The two are different problems and a caller must not conflate them. + """ + section = _BUGS_SECTION.search(known_issues_text) + if section is None: + return None + body = section.group(1).strip() + if body == _NO_BUGS: + return [] + numbers: list[int] = [] + for line in body.splitlines(): + if not line.startswith("|") or set(line) <= set("|- "): + continue + cells = [cell.strip() for cell in line.strip().strip("|").split("|")] + if cells[-1] == "Issue": + continue + # The last cell, so prose carrying a `|` cannot shift the column. + links = [ + int(number) + for number, url_number in _ISSUE_LINK.findall(cells[-1]) + if number == url_number + ] + if len(links) != 1: + return None + numbers.append(links[0]) + return numbers or None + + +def check_bug_rows(known_issues_text: str) -> list[str]: + """Check the Bugs table's shape: one well-formed, unique issue per row.""" + numbers = bug_rows(known_issues_text) + if numbers is None: + return [ + "KNOWN_ISSUES.md: the `## Bugs` table was not found, or a row's " + "Issue column does not hold exactly one `[#N](…/issues/N)` link. " + "An empty section is written `No known bugs.`" + ] + duplicates = sorted({n for n in numbers if numbers.count(n) > 1}) + return [ + f"KNOWN_ISSUES.md: issue #{number} has a Bugs row twice" + for number in duplicates + ] + + +def check_bug_issue_parity(rows: list[int], open_bugs: list[int]) -> list[str]: + """Check the Bugs table against the open `bug`-labelled issues.""" + if not open_bugs: + return [ + "KNOWN_ISSUES.md: an open `bug`-labelled issue was not found at " + "all, so the Bugs table has nothing to be checked against. An " + "empty query is a failed one, not a clean bill of health." + ] + errors = [ + f"KNOWN_ISSUES.md: issue #{number} is an open bug with no Bugs row" + for number in sorted(set(open_bugs) - set(rows)) + ] + errors += [ + f"KNOWN_ISSUES.md: the Bugs row for #{number} is not an open bug issue" + for number in sorted(set(rows) - set(open_bugs)) + ] + return errors + + +class BugQueryError(RuntimeError): + """The tracker could not be queried — a failed run, not an empty one.""" + + +def open_bug_issues(repo: str = "aallan/vera") -> list[int]: + """Open issue numbers carrying the `bug` label, from the GitHub API. + + Raises `BugQueryError` rather than returning `[]` on a transport or + payload failure. `check_bug_issue_parity` reads an empty list as + "the query failed", so returning one here would reach the right + verdict for the wrong reason — and the caller could no longer tell a + burned-down tracker from an unreachable one (#1329 review). + """ + numbers: list[int] = [] + for page in range(1, 11): + url = ( + f"https://api.github.com/repos/{repo}/issues" + f"?labels=bug&state=open&per_page=100&page={page}" + ) + request = Request(url, headers={"User-Agent": "vera-doc-counts/1"}) + token = os.environ.get("GH_TOKEN") or os.environ.get("GITHUB_TOKEN") + if token: + request.add_header("Authorization", f"Bearer {token}") + try: + # The URL is built from a caller-supplied repository, not input. + with urlopen(request, timeout=30) as response: + payload = json.load(response) + except (OSError, ValueError) as exc: + # URLError and HTTPError are OSError; a socket timeout is too, + # and a malformed body raises JSONDecodeError, a ValueError. + raise BugQueryError(f"could not query {repo} for open bugs: {exc}") from exc + if not payload: + break + numbers += [ + item["number"] for item in payload if "pull_request" not in item + ] + return numbers + + def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--check-bug-issues", + action="store_true", + help=( + "also check KNOWN_ISSUES.md's Bugs table against the open " + "`bug`-labelled issues (needs the GitHub API; for the release PR, " + "not for pre-commit)" + ), + ) + args = parser.parse_args() root = Path(__file__).resolve().parent.parent errors: list[str] = [] @@ -1155,40 +1507,18 @@ def check_testing(pattern: str, expected: int, label: str) -> None: readme_md = (root / "README.md").read_text(encoding="utf-8") - def check_readme(pattern: str, expected: int, label: str) -> None: - m = re.search(pattern, readme_md) - if not m: - return # Pattern absent from README is OK — not all counts appear - doc_val = int(m.group(1).replace(",", "")) - if doc_val != expected: - errors.append( - f"README.md {label}: doc says {doc_val}, live is {expected}" - ) - - check_readme( - r"([\d,]+) tests across", - live_total_tests, - "total tests", - ) - check_readme( - r"([\d,]+) tests, \d+% Python code coverage", - live_total_tests, - "project-status tests", - ) - check_readme( - r"tests across (\d+) files", - live_test_files, - "test file count", - ) - check_readme( - r"(\d+) programs across \d+ spec", - live_conformance, - "conformance programs", - ) - check_readme( - r"(\d+) end-to-end", - live_examples, - "example count", + # One sentence carries six live figures. Its four countable ones are + # gated together, each an error when it goes missing: the four patterns + # that used to sit here beside the tests one matched no README text at + # all, and returned silently rather than saying so. + errors.extend( + check_project_status( + readme_md, + live_total_tests, + live_conformance, + live_examples, + len(list((root / "spec").glob("*.md"))), + ) ) # ------------------------------------------------------------------ @@ -1449,6 +1779,36 @@ def check_readme(pattern: str, expected: int, label: str) -> None: errors.extend(check_corpus_count(root)) errors.extend(check_conformance_skip_total(root)) + # ------------------------------------------------------------------ + # 20. Check TESTING.md's dual-target row against a live run + # ------------------------------------------------------------------ + + split = dual_target_split(root) + if split is None: + errors.append( + f"TESTING.md: the dual-target differential ({_DUAL_TARGET_TEST}) " + f"could not be read — it failed, or it skipped for a reason the " + f"row's three documented properties do not cover" + ) + else: + errors.extend( + check_dual_target_row(testing_md, level_counts.get("run", 0), split) + ) + + # ------------------------------------------------------------------ + # 21. Check KNOWN_ISSUES.md's Bugs table + # ------------------------------------------------------------------ + + known_issues = (root / "KNOWN_ISSUES.md").read_text(encoding="utf-8") + errors.extend(check_bug_rows(known_issues)) + if args.check_bug_issues: + rows = bug_rows(known_issues) + if rows is not None: + try: + errors.extend(check_bug_issue_parity(rows, open_bug_issues())) + except BugQueryError as exc: + errors.append(f"KNOWN_ISSUES.md: {exc}") + # ------------------------------------------------------------------ # Report # ------------------------------------------------------------------ diff --git a/scripts/check_examples_run.py b/scripts/check_examples_run.py index 43debfc1..15c1bc81 100644 --- a/scripts/check_examples_run.py +++ b/scripts/check_examples_run.py @@ -47,10 +47,19 @@ fallback, which runs a different function and exits 0 — so every spec names its entry point and the CLI resolves it by name. An example that reaches outside the process answers a missing resource by printing a -message and completing normally — so the three that do carry an +message and completing normally — so the ones that do carry an ``expect`` substring only their success path prints, which is what makes deleting `examples/sqlitedb.sqlite` fail the gate instead of passing on the graceful in-memory arm. Both signals, per run, always. + +*Which* examples those are is derived rather than listed. +``check_sentinel_coverage`` reads each program's own declarations — the +`DB` effect in a function's effect row, the `IO.read_file` / +`IO.write_file` operations at a call site — and requires that set to +equal the set of specs carrying an ``expect``, in both directions. A +list of filenames would be a snapshot of today's corpus that says +nothing about the next database or filesystem example, which is the only +case the rule exists for. """ from __future__ import annotations @@ -86,6 +95,12 @@ class RunSpec(NamedTuple): deliberately not a full stdout pin; that belongs in the dedicated tests. + Which examples those are is not left to judgement: + ``check_sentinel_coverage`` derives the set from the resources each + program declares and holds it equal to the specs carrying an + ``expect``, so a missing sentinel and a spurious one are both + errors. + A ``NamedTuple`` rather than a frozen dataclass so the module can be loaded by the bare ``spec_from_file_location`` / ``exec_module`` recipe the sibling script tests use: ``@dataclass`` resolves its @@ -301,6 +316,234 @@ def check_coverage( return errors +# --------------------------------------------------------------------------- +# The derived sentinel rule +# --------------------------------------------------------------------------- + + +# The external resources an example can reach, as registry NAMES. Which +# examples must pin a sentinel follows from these by reading what each +# program declares, so one added tomorrow is covered by being written +# rather than by being remembered here — the case a list of filenames +# cannot cover, since it is a snapshot of the corpus it was written +# against. +# +# Both halves are needed because the effect row alone does not +# discriminate. `FileIO` and `Time` are not effects in Vera: file and +# clock operations live under `IO`, so `file_io.vera` declares exactly +# the bare `` that `hello_world.vera` does and only the operation it +# calls tells the two apart. Measured over the corpus, `DB` appears in +# `database.vera` and `sqlitedb.vera` alone, and `IO.read_file` / +# `IO.write_file` in `file_io.vera` alone. +RESOURCE_EFFECTS: tuple[str, ...] = ("DB",) +RESOURCE_OPS: tuple[tuple[str, str], ...] = ( + ("IO", "read_file"), + ("IO", "write_file"), +) + + +def resource_vocabulary() -> str: + """The declared resource names, for the messages that cite them.""" + return ", ".join( + [*RESOURCE_EFFECTS, *(f"{e}.{op}" for e, op in RESOURCE_OPS)] + ) + + +def resource_registry_errors() -> list[str]: + """Every declared resource name, checked against the live registry. + + A name the compiler no longer has would match no example, and with + nothing left requiring a sentinel the rule switches itself off while + still reporting success. Renaming the `DB` effect, or moving + `read_file` out of `IO`, must therefore fail here rather than + quietly empty the derivation — the same reason an empty corpus is an + error in ``check_coverage``. + + The `vera` import is lazy, as `check_doc_counts.check_homepage_facts` + does for the same registry: loading this module for its + classification tables should not drag in the compiler. + """ + from vera.introspect import builtin_effect_names, effects_payload + + live_effects = builtin_effect_names() + live_ops = { + str(item["name"]): {str(op) for op in item.get("ops", ())} + for item in effects_payload()["items"] + if item.get("kind") == "effect" + } + + errors: list[str] = [] + for name in RESOURCE_EFFECTS: + if name not in live_effects: + errors.append( + f"RESOURCE_EFFECTS names {name!r}, which the effect " + f"registry does not have — could not find it among " + f"{sorted(live_effects)}. Re-point it at the current " + f"name, so a renamed effect fails this gate instead of " + f"silently matching no example." + ) + for effect, op in RESOURCE_OPS: + if effect not in live_ops: + errors.append( + f"RESOURCE_OPS names {effect}.{op}, but the effect " + f"registry has no {effect!r} — could not find it among " + f"{sorted(live_ops)}. An operation is only meaningful " + f"under an effect that exists." + ) + elif op not in live_ops[effect]: + errors.append( + f"RESOURCE_OPS names {effect}.{op}, which {effect} does " + f"not have — could not find {op!r} among " + f"{sorted(live_ops[effect])}. Re-point it at the " + f"current operation, so a renamed one fails this gate " + f"instead of silently matching no example." + ) + return errors + + +def resource_signals(path: Path) -> frozenset[str]: + """The external-resource signals one example declares. + + Two sources, since neither alone discriminates: the resource effects + named in a function's effect row, and the resource operations the + source calls. Read off the parsed program rather than the text, so + a comment naming `` is prose and not a declaration — + `examples/sqlitedb.vera`'s first line is exactly such a comment, and + a text scan would agree with the parse there by luck while + disagreeing on the first example whose header describes what it + deliberately does not do. + + Whatever the parse raises propagates; ``check_sentinel_coverage`` + turns it into an error line, because an example whose signals are + *unknown* must not be spelled the same as one that has none. + """ + from vera import ast + from vera.obligations.cache import walk_nodes + from vera.parser import parse_to_ast + + program = parse_to_ast(path.read_text(encoding="utf-8"), file=str(path)) + effects = set(RESOURCE_EFFECTS) + ops = set(RESOURCE_OPS) + + signals: set[str] = set() + for node in walk_nodes(program): + if isinstance(node, ast.FnDecl): + # `walk_nodes` is a generic dataclass-field walk, so a + # `where` helper's row is reached alongside the outer one. + row = node.effect + if isinstance(row, ast.EffectSet): + for ref in row.effects: + # Unqualified refs only: `Mod.DB` names a user + # effect in another module, not the built-in the + # registry check validated. + if isinstance(ref, ast.EffectRef) and ref.name in effects: + signals.add(ref.name) + elif isinstance(node, ast.QualifiedCall): + if (node.qualifier, node.name) in ops: + signals.add(f"{node.qualifier}.{node.name}") + return frozenset(signals) + + +def check_sentinel_coverage( + examples_dir: Path, + run_specs: dict[str, RunSpec], +) -> list[str]: + """The examples that declare an external resource are exactly the + specs that carry an ``expect``. + + Both directions are errors. A resource-touching example with no + sentinel passes on its graceful arm the day its fixture vanishes, + which is the failure the sentinels exist to catch; a sentinel on an + example with no resource re-pins stdout that the dedicated output + tests own, and goes red on a cosmetic edit. + + An empty derived set is an error rather than a vacuous pass: with + nothing required the two sides agree however broken the derivation + is, which is the same failure mode ``check_coverage`` rules out for + a glob that stops matching. + """ + errors = resource_registry_errors() + if errors: + # Without a valid vocabulary the derivation below is + # meaningless — it would match nothing and then report every + # sentinel in the tables as spurious. + return errors + + signals_by_name: dict[str, frozenset[str]] = {} + inspected: set[str] = set() + for name in sorted(run_specs): + path = examples_dir / f"{name}.vera" + if not path.is_file(): + # `check_coverage` and `run_corpus` both report this, each + # naming the table the key came from; a third copy would + # only repeat them. It cannot hide the rule either — with + # the files gone the derivation is empty, which is the + # error below. + continue + inspected.add(name) + try: + signals = resource_signals(path) + except Exception as exc: # noqa: BLE001 — unknown signals are reported, never read as none + errors.append( + f"{name}.vera could not be parsed, so what it reaches " + f"outside the process is unknown — read as 'declares no " + f"resource' it would drop out of this rule silently, " + f"and be diagnosed as carrying a sentinel for nothing: " + f"{exc}" + ) + continue + if signals: + signals_by_name[name] = signals + + if errors: + return errors + + if not signals_by_name: + return [ + f"no example in RUN_SPECS declares any of " + f"[{resource_vocabulary()}] — the derivation matched " + f"nothing, so the sentinel rule is no longer gated. This " + f"is an error rather than a pass: with the required set " + f"empty both sides of the rule agree however broken the " + f"derivation is, and every gate run reports success over " + f"zero examples." + ] + + # Only the specs whose `.vera` the loop above actually read. Building + # this from every entry in `run_specs` put a spec whose file is missing + # into `pinned - signals_by_name`, where it drew the spurious-sentinel + # diagnosis — "declares no external resource" — when the truth is that + # the derivation never opened it. `check_coverage` reports the missing + # file first in `main`, but this is a public function tests call + # directly (#1329 review). + pinned = { + name + for name, spec in run_specs.items() + if spec.expect and name in inspected + } + for name in sorted(set(signals_by_name) - pinned): + errors.append( + f"{name}.vera reaches outside the process " + f"({', '.join(sorted(signals_by_name[name]))}) but its " + f"RUN_SPECS entry sets no `expect` — a program like this " + f"answers a missing resource by printing a message and " + f"completing normally, so exit code alone cannot tell its " + f"success path from that arm. Pin a substring only the " + f"success path prints." + ) + for name in sorted(pinned - set(signals_by_name)): + errors.append( + f"{name}.vera declares no external resource " + f"([{resource_vocabulary()}]) but its RUN_SPECS entry pins " + f"the sentinel {run_specs[name].expect!r} — `expect` is for " + f"programs that answer a missing resource by completing " + f"normally. On any other example it re-pins stdout that " + f"the dedicated output tests own, and goes red on a " + f"cosmetic edit." + ) + return errors + + # --------------------------------------------------------------------------- # Invocation # --------------------------------------------------------------------------- @@ -576,6 +819,7 @@ def _block(title: str, errors: list[str], footer: str = "") -> list[str]: def error_blocks( coverage_errors: list[str], + sentinel_errors: list[str], doc_errors: list[str], failures: list[str], ) -> list[str]: @@ -588,6 +832,13 @@ def error_blocks( """ return [ *_block("COVERAGE ERRORS", coverage_errors), + *_block( + "SENTINEL COVERAGE", sentinel_errors, + "Which examples must pin a success sentinel is derived from " + "the resources each program declares, not from a list of " + "names. Fix the spec — or, if an example genuinely stopped " + "reaching outside the process, drop its `expect`.", + ), *_block( "DOCUMENTATION MISMATCH", doc_errors, "TESTING.md's execution-model table is the documented form of " @@ -628,10 +879,15 @@ def main() -> int: # The coverage rule gates the run: with the tables out of sync with # disk, a green run would be reporting on the wrong set of programs. if coverage_errors: - for line in error_blocks(coverage_errors, doc_errors, []): + for line in error_blocks(coverage_errors, [], doc_errors, []): print(line, file=sys.stderr) return 1 + # Derived from the examples themselves, so it runs only once the + # tables and disk agree: a spec whose file is missing is already + # reported above, and would otherwise be reported twice. + sentinel_errors = check_sentinel_coverage(examples_dir, RUN_SPECS) + with tempfile.TemporaryDirectory(prefix="vera-examples-run-") as td: failures = run_corpus(examples_dir, RUN_SPECS, Path(td)) @@ -645,7 +901,18 @@ def main() -> int: print(f" skip [{prop}]: {', '.join(skipped)}") print(f" {SKIP_PROPERTIES[prop]}") - blocks = error_blocks([], doc_errors, failures) + # With the rule holding, the specs carrying an `expect` ARE the + # derived set, so printing them names it — a reader of a gate run + # sees which examples the sentinel rule covers without opening this + # file, as the skip properties above already do for the skips. + if not sentinel_errors: + pinned = sorted(n for n, s in RUN_SPECS.items() if s.expect) + print( + f" sentinel required [{resource_vocabulary()}]: " + f"{', '.join(pinned)}" + ) + + blocks = error_blocks([], sentinel_errors, doc_errors, failures) if blocks: print("", file=sys.stderr) for line in blocks: diff --git a/scripts/check_grammar_alignment.py b/scripts/check_grammar_alignment.py index 8688ca59..f27e1144 100644 --- a/scripts/check_grammar_alignment.py +++ b/scripts/check_grammar_alignment.py @@ -1,6 +1,7 @@ #!/usr/bin/env python3 -"""Fail if a grammar rule name exists in the spec EBNF but not in the Lark -grammar, or the other way round. +"""Fail when ``spec/10-grammar.md`` and ``vera/grammar.lark`` stop describing +the same language: a rule name, a terminal, or a production body on one side +only. Background (#683): ``spec/10-grammar.md`` and ``vera/grammar.lark`` describe one language, and nothing held their rule names together. They drifted — the spec @@ -12,11 +13,17 @@ the ``with`` form of a handler clause was undocumented). Neither is a compiler bug; both mislead a reader who takes Chapter 10 as the map of the parse tree. -What this compares is **rule headers only**: a line of the form ``name:`` at the -start of a production, in either file. It is a name-level cross-check, not a -grammar equivalence check — two files can agree on every rule name and still -accept different languages. Rule *bodies* are not compared, so a drifted -right-hand side passes here. +The first comparison is **rule headers**: a line of the form ``name:`` at the +start of a production, in either file. That was the whole gate as #683 shipped +it, and it is not a grammar equivalence check — two files can agree on every +rule name and still accept different languages. Three further comparisons, +added for #1290, close the classes it could not see: terminals declared against +terminals referenced, within each file and in both directions; the pattern of +every regex-bodied terminal, across the two files; and the symbols each shared +production's right-hand side refers to. They live under their own banner +further down, with their own reasoning. What remains uncompared is the *shape* +of a right-hand side — alternation, grouping and repetition — so two +productions naming the same symbols in a different arrangement still pass. The two compared *sets* are deliberately blind to Lark's ``-> alias`` names. An alias renames the tree node an alternative produces; it is not a rule header, @@ -53,12 +60,15 @@ them, so the report never asks for two opposite edits at once. What the alias premise does *not* establish is that the Lark alternative still -spells the same construct as the spec production — that is a body-level fact -this header-only gate cannot see. It is worth being concrete about the weakest -two: ``tuple_literal`` and ``tuple_type`` rest on ``constructor_call`` and -``named_type``, general forms that would outlive tuples leaving the language -altogether. For those the premise catches the alternative being renamed or -moved to another rule, and nothing more. +spells the same construct as the spec production. It is worth being concrete +about the weakest two: ``tuple_literal`` and ``tuple_type`` rest on +``constructor_call`` and ``named_type``, general forms that would outlive +tuples leaving the language altogether. For those the premise catches the +alternative being renamed or moved to another rule, and nothing more. The body +comparison narrows that gap without closing it: a waiver naming ``lark_rule`` +is read there as "Lark inlines this production into that rule", so the symbols +the spec's production refers to are checked against the ones Lark's inlining +rule refers to. The allowlist is meant to stay small. If it needs to grow past a handful of entries, the header-only comparison has stopped being the right model and should @@ -109,8 +119,65 @@ def strip_comment(line: str) -> str: The single definition of what a comment is, shared by every scan of either file — a rule header, an alias, or anything added later. Commented-out grammar is deleted grammar; it must not satisfy a check. + + A ``//`` inside a quoted literal or a ``/…/`` regex body is not a comment. + A plain ``line.split("//")[0]`` truncated the annotation-comment terminal in + both files mid-pattern — ``%ignore /\\/\\*…\\*\\//`` ends in ``\\//`` — which + was harmless while only rule headers were scanned and silently wrong the + moment terminal bodies were (#1290). + """ + index = 0 + length = len(line) + while index < length: + char = line[index] + if char == "/" and line.startswith("//", index): + return line[:index] + if char in '"/': + end = _span_end(line, index, char) + if end is not None: + index = end + continue + index += 1 + return line + + +def _span_end(line: str, start: int, quote: str) -> int | None: + """Index just past the literal or regex opened at ``start``, or ``None``. + + Inside a regex, a ``/`` within a ``[…]`` character class is a member + and not the closing delimiter. Ignoring that ended the scan inside + the class of the chapter's annotation-comment terminal — which + spells it ``[^/*]`` where the Lark grammar escapes it ``[^\\/*]`` — + truncating the declaration. A truncated body is not a bare regex, + so ``terminal_patterns`` skipped that terminal altogether: green + because nothing was compared, the failure this gate exists to catch + (#1329). A ``]`` in the first position of a class is a member too, + which is why the class is not closed until at least one has been + consumed. """ - return line.split("//")[0] + index = start + 1 + in_class = False + class_start = -1 + while index < len(line): + char = line[index] + if char == "\\": + index += 2 + continue + if quote == "/" and not in_class and char == "[": + in_class = True + class_start = index + index += 1 + continue + if in_class: + first = class_start + (2 if line[class_start + 1 : class_start + 2] == "^" else 1) + if char == "]" and index > first: + in_class = False + index += 1 + continue + if char == quote: + return index + 1 + index += 1 + return None # Names that appear on one side only, on purpose. Not drift; do not "fix". @@ -254,19 +321,401 @@ def drift( return actionable, stale, unsound +# --------------------------------------------------------------------------- +# Terminals and production bodies (#1290) +# +# The header comparison above is blind to three drift classes, each of which +# was demonstrated on a live file: a fabricated terminal added to §10.2 (the +# header pattern requires a lowercase lead, so no terminal is seen at all); a +# rule reference restored to a right-hand side; and a production body edited on +# one side only — the class most grammar edits actually fall into. The checks +# below close all three, and found two chapter defects beyond the two the issue +# named: `slot_ref`/`result_ref` admitting an arbitrary `type_expr` where the +# parser accepts only `UPPER_IDENT type_args?`, and a redundant `effect_list` +# alternative ambiguous with the one beside it. +# --------------------------------------------------------------------------- + +# A terminal declaration at the start of a line: an uppercase name, Lark's +# optional priority suffix, a colon, a body. +_TERMINAL_DECL = re.compile(r"^([A-Z][A-Z0-9_]*)(?:\.-?\d+)?[ \t]*:[ \t]*(\S.*?)[ \t]*$") +_TERMINAL_REF = re.compile(r"\b([A-Z][A-Z0-9_]*)\b") +_IGNORE_DECL = re.compile(r"^%ignore[ \t]+(\S.*?)[ \t]*$") +_QUOTED = re.compile(r'"((?:[^"\\]|\\.)*)"') +_BARE_REGEX = re.compile(r"^/(.+)/$") +_BARE_STRING = re.compile(r'^"((?:[^"\\]|\\.)*)"$') + +# The §10.2 sub-heading whose terminals the lexer throws away. Those are the +# only spec terminals allowed to go unreferenced by any production; the group +# is located by this marker rather than by a hand-list of names, so a renamed +# heading fails the gate instead of quietly widening it. +_SKIPPED_GROUP = "skipped" + + +def ebnf_fence_lines(text: str) -> list[str]: + """Every line inside a spec chapter's ```ebnf fences, fences excluded.""" + lines: list[str] = [] + in_fence = False + for line in text.splitlines(): + if line.lstrip().startswith("```"): + in_fence = line.lstrip().startswith("```ebnf") + continue + if in_fence: + lines.append(line) + return lines + + +def rule_bodies(lines: list[str]) -> dict[str, list[str]]: + """Map each rule header to its body lines, comments and aliases removed. + + A production spans its header line and the ``| …`` continuations under it, + exactly as ``extract_lark_aliases`` reads them. ``-> alias`` suffixes are + dropped: an alias names a tree node, never a symbol the production refers + to, and leaving them in makes every aliased alternative read as a reference + to a rule that does not exist. + """ + bodies: dict[str, list[str]] = {} + owner: str | None = None + for raw in lines: + line = strip_comment(raw) + header = _HEADER.match(line) + if header: + owner = header.group(2) + bodies.setdefault(owner, []).append(_ALIAS.sub("", line[header.end() :])) + continue + if owner is not None and _CONTINUATION.match(line): + bodies[owner].append(_ALIAS.sub("", line)) + continue + owner = None + return bodies + + +def terminal_declarations(lines: list[str]) -> dict[str, str]: + """Map each declared terminal name to its body.""" + declared: dict[str, str] = {} + for raw in lines: + match = _TERMINAL_DECL.match(strip_comment(raw)) + if match: + declared[match.group(1)] = match.group(2) + return declared + + +def ignore_patterns(lines: list[str]) -> list[str]: + """Bodies of Lark's ``%ignore`` directives — anonymous terminals.""" + return [ + match.group(1) + for match in (_IGNORE_DECL.match(strip_comment(raw)) for raw in lines) + if match + ] + + +def skipped_terminals(lines: list[str]) -> set[str]: + """Spec terminals declared under the ``(skipped)`` group heading. + + A *group* heading is a comment that opens a block — the first line of a + fence, or one following a blank line. A comment sitting between two + declarations is a note about the one below it, not a new group; reading + every comment as a heading ended the skipped group at the first such note + and reported two terminals the lexer discards as unused. + """ + names: set[str] = set() + in_group = False + at_block_start = True + for raw in lines: + stripped = raw.strip() + if not stripped: + # The blank ENDS the group as well as opening a new block. A + # declaration block with no heading of its own would otherwise + # inherit whatever the previous block was, silently widening + # the waiver past the terminals the marker names (#1329 + # review). §10.2 has no blank inside the skipped group today, + # so this narrows the rule without moving the current result. + in_group = False + at_block_start = True + continue + if stripped.startswith("//"): + if at_block_start: + in_group = _SKIPPED_GROUP in stripped.lower() + at_block_start = False + continue + at_block_start = False + match = _TERMINAL_DECL.match(strip_comment(raw)) + if match and in_group: + names.add(match.group(1)) + return names + + +def normalise_pattern(body: str) -> str: + """A regex body with Lark's delimiter and quote escapes removed. + + ``\\/`` and ``\\"`` mean exactly ``/`` and ``"`` to a regex engine; the two + files escape them differently and nothing else, so this is the whole of the + difference between ``STRING_LIT`` and ``ANNOTATION_COMMENT`` as the two + files spell them. ``\\\\`` is copied through, so an escaped backslash is + never mistaken for an escape of the character after it. + """ + out: list[str] = [] + index = 0 + while index < len(body): + if body[index] == "\\" and index + 1 < len(body): + following = body[index + 1] + out.append(following if following in '/"' else body[index : index + 2]) + index += 2 + continue + out.append(body[index]) + index += 1 + return "".join(out) + + +def _referenced_terminals(bodies: dict[str, list[str]]) -> set[str]: + return { + name + for lines in bodies.values() + for line in lines + for name in _TERMINAL_REF.findall(_QUOTED.sub(" ", line)) + } + + +def terminal_audit( + lark_lines: list[str], spec_lines: list[str] +) -> list[str]: + """Declared-versus-referenced, within each file and in both directions. + + A terminal nothing refers to is dead weight the reader has to reconcile — + ``SOME``/``NONE``/``OK``/``ERR``/``COLON`` sat in the Lark grammar that way + while the constructors they claimed to lex went through ``UPPER_IDENT``. A + terminal referred to and never declared is the opposite failure and Lark + had one of those too, ``DOUBLE_COLON`` in ``module_call``. Neither + direction was checked anywhere. + """ + problems: list[str] = [] + for label, lines, allow_unreferenced in ( + (LARK, lark_lines, set[str]()), + (SPEC, spec_lines, skipped_terminals(spec_lines)), + ): + declared = set(terminal_declarations(lines)) + referenced = _referenced_terminals(rule_bodies(lines)) + if label == SPEC and not allow_unreferenced: + problems.append( + f"{label}: no terminal group marked `({_SKIPPED_GROUP})` was " + f"found, so every declared terminal would have to be referenced" + ) + for name in sorted(declared - referenced - allow_unreferenced): + problems.append(f"{label}: terminal {name} is declared and never used") + for name in sorted(referenced - declared): + problems.append(f"{label}: terminal {name} is used and never declared") + return problems + + +def terminal_patterns(lark_lines: list[str], spec_lines: list[str]) -> list[str]: + """Every pattern-bearing terminal must be spelled the same in both files. + + Only terminals whose body is a bare ``/regex/`` are compared: the spec + names each keyword and punctuation mark that Lark writes as an inline + quoted literal, and those have no Lark declaration to compare against. The + regex-bodied ones do, either as a named terminal or as an ``%ignore``, and + ``BLOCK_COMMENT`` was the one that had neither — the spec published a + non-nesting ``/\\{-[\\s\\S]*?-\\}/`` for a construct §1.3 says nests and + ``vera/lexical.py`` resolves by counting depth. + """ + lark_declared = terminal_declarations(lark_lines) + spec_declared = terminal_declarations(spec_lines) + lark_patterns = { + normalise_pattern(match.group(1)) + for match in ( + _BARE_REGEX.match(body) + for body in [*lark_declared.values(), *ignore_patterns(lark_lines)] + ) + if match + } + problems: list[str] = [] + for name, body in sorted(spec_declared.items()): + regex = _BARE_REGEX.match(body) + if regex is None: + continue + if normalise_pattern(regex.group(1)) not in lark_patterns: + problems.append( + f"{SPEC}: terminal {name} publishes a pattern {LARK} does not " + f"have, as a terminal or an %ignore: {body}" + ) + for name, body in sorted(lark_declared.items()): + if name not in spec_declared: + problems.append(f"{SPEC}: terminal {name} is declared only in {LARK}") + elif normalise_pattern(body) != normalise_pattern(spec_declared[name]): + problems.append( + f"{name}: {LARK} has {body}, {SPEC} has {spec_declared[name]}" + ) + return problems + + +def _literal_terminals(spec_lines: list[str]) -> tuple[dict[str, str], list[str]]: + """Map each quoted literal the spec names to its terminal, plus clashes.""" + table: dict[str, str] = {} + clashes: list[str] = [] + for name, body in sorted(terminal_declarations(spec_lines).items()): + match = _BARE_STRING.match(body) + if match is None: + continue + literal = match.group(1) + if literal in table: + clashes.append( + f"{SPEC}: terminals {table[literal]} and {name} both spell {body}" + ) + continue + table[literal] = name + return table, clashes + + +def _symbols(line: str, rules: set[str]) -> tuple[set[str], set[str]]: + """``(rule references, terminal references)`` in one production body line.""" + return ( + {name for name in re.findall(r"\b[a-z][a-z0-9_]*\b", line)} & rules, + set(_TERMINAL_REF.findall(_QUOTED.sub(" ", line))), + ) + + +def _lark_symbols( + rule: str, + bodies: dict[str, list[str]], + rules: set[str], + literals: dict[str, str], +) -> tuple[set[str], set[str], list[str]]: + referenced: set[str] = set() + terminals: set[str] = set() + unmapped: list[str] = [] + for line in bodies[rule]: + rule_refs, terminal_refs = _symbols(line, rules) + referenced |= rule_refs + terminals |= terminal_refs + for raw in _QUOTED.findall(line): + literal = raw.replace('\\"', '"') + if literal in literals: + terminals.add(literals[literal]) + else: + unmapped.append(literal) + return referenced - {rule}, terminals, unmapped + + +def _spec_symbols( + rule: str, bodies: dict[str, list[str]], rules: set[str] +) -> tuple[set[str], set[str], set[str]]: + """``(rules, terminals, inlined)`` for one spec production. + + A waiver saying "Lark expresses this as an alternative of ``lark_rule``" + fixes where the spec's separate production corresponds on the Lark side: + seen from any other rule it *is* ``lark_rule``, and seen from ``lark_rule`` + itself its body is inlined there. Reading the waiver that way is what lets + the body comparison run against the shipped files with no waivers of its + own. + + ``inlined`` names the symbols that arrived by that folding rather than from + the production's own text. Inlining moves a symbol across a rule boundary + and a one-level set comparison cannot say how far it moved — the spec's + ``tuple_type`` contributes ``LT``/``COMMA``/``GT`` that Lark keeps one rule + deeper, inside ``type_args`` — so a folded symbol missing on the Lark side + is not reported. The other direction still is: a symbol Lark refers to and + the chapter does not is drift however the waiver reads. + """ + waived = {name for name, entry in ALLOWLIST.items() if entry.side == "spec"} + referenced: set[str] = set() + terminals: set[str] = set() + for line in bodies[rule]: + rule_refs, terminal_refs = _symbols(line, rules) + referenced |= rule_refs + terminals |= terminal_refs + folded: set[str] = set() + inlined: set[str] = set() + for name in sorted(referenced): + waiver = ALLOWLIST.get(name) if name in waived else None + if waiver is None: + folded.add(name) + elif waiver.lark_rule is None: + continue + elif waiver.lark_rule != rule: + folded.add(waiver.lark_rule) + elif name in bodies: + inner_rules, inner_terminals, _ = _spec_symbols(name, bodies, rules) + folded |= inner_rules + terminals |= inner_terminals + inlined |= inner_rules | inner_terminals + return (folded - waived) - {rule}, terminals, inlined + + +def body_drift(lark_lines: list[str], spec_lines: list[str]) -> list[str]: + """Compare the symbols each shared production refers to. + + Rule references and terminal references, per production, for every rule + both files declare. A rule's reference to *itself* is excluded: Lark + spells repetition with left recursion and the chapter spells it with a + Kleene star, so the eight operator-precedence rules differ there by + notation and not by language. + """ + lark_bodies = rule_bodies(lark_lines) + spec_bodies = rule_bodies(spec_lines) + literals, problems = _literal_terminals(spec_lines) + waived = {name for name, entry in ALLOWLIST.items() if entry.side == "spec"} + shared = sorted(set(lark_bodies) & set(spec_bodies)) + if not shared: + return [*problems, "no rule is a production in both files"] + for rule in shared: + lark_rules, lark_terms, unmapped = _lark_symbols( + rule, lark_bodies, set(lark_bodies), literals + ) + spec_rules, spec_terms, inlined = _spec_symbols( + rule, spec_bodies, set(spec_bodies) + ) + for literal in sorted(set(unmapped)): + problems.append( + f'{rule}: {LARK} matches the literal "{literal}" and no {SPEC} ' + f"terminal declares it" + ) + for label, only_lark, only_spec in ( + ( + "rule", + lark_rules - waived - spec_rules, + spec_rules - lark_rules - inlined, + ), + ("terminal", lark_terms - spec_terms, spec_terms - lark_terms - inlined), + ): + for name in sorted(only_lark): + problems.append(f"{rule}: refers to {label} {name} only in {LARK}") + for name in sorted(only_spec): + problems.append(f"{rule}: refers to {label} {name} only in {SPEC}") + return problems + + +def _report(title: str, problems: list[str], remedy: str) -> None: + print(f"\nERROR: {title}:", file=sys.stderr) + for problem in problems: + print(f" {problem}", file=sys.stderr) + print(f"\n{remedy}", file=sys.stderr) + + def main() -> int: root = Path(__file__).resolve().parent.parent lark = extract_lark_rules(root / LARK) spec = extract_spec_rules(root / SPEC) + lark_text = (root / LARK).read_text(encoding="utf-8") + lark_lines = lark_text.splitlines() + spec_lines = ebnf_fence_lines((root / SPEC).read_text(encoding="utf-8")) + differing = lark ^ spec - actionable, stale, unsound = drift( - lark, spec, (root / LARK).read_text(encoding="utf-8") - ) + actionable, stale, unsound = drift(lark, spec, lark_text) + unused = terminal_audit(lark_lines, spec_lines) + patterns = terminal_patterns(lark_lines, spec_lines) + bodies = body_drift(lark_lines, spec_lines) print(f" {len(lark)} rule headers in {LARK}") print(f" {len(spec)} rule headers in {SPEC}") print(f" {len(differing)} differ, {len(ALLOWLIST)} allowlisted") + print( + f" {len(terminal_declarations(lark_lines))} terminals in {LARK}, " + f"{len(terminal_declarations(spec_lines))} in {SPEC}" + ) + print( + f" {len(set(rule_bodies(lark_lines)) & set(rule_bodies(spec_lines)))} " + f"production bodies compared" + ) if actionable: print("\nERROR: grammar rule names have drifted:", file=sys.stderr) @@ -306,10 +755,34 @@ def main() -> int: "files and delete the entry.", file=sys.stderr, ) - if actionable or stale or unsound: + if unused: + _report( + "terminals declared without a use, or used without a declaration", + unused, + "Delete the terminal, or add the production that refers to it. A " + "terminal nothing refers to is not part of the language.", + ) + if patterns: + _report( + "terminal patterns differ between the two files", + patterns, + f"Make {SPEC} publish the pattern the parser actually has. Where a " + f"construct is not regular — nested block comments are the standing " + f"case — say so in the chapter rather than publishing a regex that " + f"accepts a different language.", + ) + if bodies: + _report( + "production bodies refer to different symbols", + bodies, + f"Bring the two right-hand sides together. If {SPEC} is the one " + f"that is wrong, fix the chapter: it is read as the map of the " + f"parse tree.", + ) + if actionable or stale or unsound or unused or patterns or bodies: return 1 - print(f"OK: {LARK} and {SPEC} agree on every rule name.") + print(f"OK: {LARK} and {SPEC} agree on every rule name, terminal and body.") return 0 diff --git a/scripts/release.py b/scripts/release.py index f7f3e3d7..b4f42437 100644 --- a/scripts/release.py +++ b/scripts/release.py @@ -26,6 +26,7 @@ ROOT = Path(__file__).resolve().parent.parent PROJECT = "veralang" +REPOSITORY = "aallan/vera" INDEX_JSON_URLS = { "pypi": f"https://pypi.org/pypi/{PROJECT}/json", "testpypi": f"https://test.pypi.org/pypi/{PROJECT}/json", @@ -33,6 +34,17 @@ PACKAGE_AFFECTING_PATHS = ("LICENSE", "PYPI_README.md", "pyproject.toml", "vera") _VERSION_RE = re.compile(r"^(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)$") +# GitHub refuses a release body over 125,000 characters with HTTP 422, and the +# release workflow reaches that step AFTER the immutable PyPI upload and AFTER +# the tag is cut (#1288). The builder is therefore total: oversized notes are +# condensed rather than allowed to fail the step. +GITHUB_RELEASE_BODY_LIMIT = 125_000 +RELEASE_BODY_BUDGET = 120_000 +_SECTION_HEADING_RE = re.compile(r"^### .+$") +_BULLET_LEAD_RE = re.compile(r"^- \*\*(?P.+?)\*\*") +_BULLET_RE = re.compile(r"^-\s+(?P\S.*)$") +_ISSUE_LINK_RE = re.compile(r"\[#\d+\]\(https://github\.com/[^\s)]+\)") + class ReleaseError(ValueError): """A release invariant was not satisfied.""" @@ -99,11 +111,20 @@ def version_at_ref(ref: str, root: Path = ROOT) -> str: return version -def changelog_notes(text: str, version: str) -> str: - """Extract a non-empty, bullet-bearing release section.""" +@dataclass(frozen=True) +class ChangelogSection: + """One release section of ``CHANGELOG.md``, with its heading date.""" + + version: str + date: str | None + notes: str + + +def changelog_section(text: str, version: str) -> ChangelogSection: + """Extract a non-empty, bullet-bearing release section and its date.""" parse_version(version) heading = re.compile( - rf"^## \[{re.escape(version)}\](?: - [0-9]{{4}}-[0-9]{{2}}-[0-9]{{2}})?\s*$", + rf"^## \[{re.escape(version)}\](?: - (?P[0-9]{{4}}-[0-9]{{2}}-[0-9]{{2}}))?\s*$", re.MULTILINE, ) match = heading.search(text) @@ -116,12 +137,123 @@ def changelog_notes(text: str, version: str) -> str: raise ReleaseError( f"CHANGELOG.md section [{version}] must contain at least one bullet" ) - return notes + return ChangelogSection(version, match.group("date"), notes) + + +def changelog_notes(text: str, version: str) -> str: + """Extract a non-empty, bullet-bearing release section.""" + return changelog_section(text, version).notes + + +def section_for_version(version: str, root: Path = ROOT) -> ChangelogSection: + """Read one release section from the checkout's changelog.""" + return changelog_section( + (root / "CHANGELOG.md").read_text(encoding="utf-8"), version + ) def notes_for_version(version: str, root: Path = ROOT) -> str: """Extract release notes from the checkout's changelog.""" - return changelog_notes((root / "CHANGELOG.md").read_text(encoding="utf-8"), version) + return section_for_version(version, root).notes + + +def changelog_anchor(version: str, date: str | None) -> str: + """Return GitHub's heading anchor for a ``## [version] - date`` line.""" + heading = f"[{version}]" + (f" - {date}" if date else "") + slug = "".join( + character + for character in heading.lower() + if character.isalnum() or character in "- " + ) + return "#" + slug.replace(" ", "-") + + +def _index_line(bullet: str) -> str: + """Condense one CHANGELOG bullet to its headline-index line. + + The lead-in is the bullet's bold run, de-emphasised, and the reference is + the bullet's LAST issue or pull-request link — the rule that reproduces + the v0.1.10 manual recovery, whose attribution for at least one bullet sat + mid-prose rather than immediately after the bold run. A bullet with no + bold run keeps its own text, so no bullet is ever dropped from the index. + """ + lead_match = _BULLET_LEAD_RE.match(bullet) + if lead_match is not None: + lead = lead_match.group("lead") + else: + plain = _BULLET_RE.match(bullet) + if plain is None: # pragma: no cover - callers filter on _BULLET_RE + raise ReleaseError(f"not a changelog bullet: {bullet!r}") + lead = plain.group("text") + links = _ISSUE_LINK_RE.findall(bullet) + return f"- {lead} ({links[-1]})" if links else f"- {lead}" + + +def condense_notes( + section: ChangelogSection, + *, + repo: str = REPOSITORY, + limit: int = GITHUB_RELEASE_BODY_LIMIT, +) -> str: + """Rewrite a release section as the headline index plus a CHANGELOG link. + + The shape is the one the v0.1.10 release was completed by hand with: the + section's ``###`` subsection headers, one condensed line per bullet, and a + link to the canonical section at the tag — the CHANGELOG being the release + notes of record either way. + """ + anchor = changelog_anchor(section.version, section.date) + dated = f"[{section.version}]" + (f" - {section.date}" if section.date else "") + preamble = ( + f"The full release notes for this version are {len(section.notes):,} " + f"characters — past GitHub's {limit:,}-character release-body limit — so " + "this body carries the headline index and the canonical notes live in the " + f"CHANGELOG at the tag: **[CHANGELOG.md § {dated}]" + f"(https://github.com/{repo}/blob/v{section.version}/CHANGELOG.md{anchor})**" + ) + + lines: list[str] = [] + bullets = 0 + for line in section.notes.splitlines(): + if _SECTION_HEADING_RE.match(line): + lines.append("") + lines.append(line) + elif _BULLET_RE.match(line): + lines.append(_index_line(line)) + bullets += 1 + if not bullets: + raise ReleaseError( + f"release section [{section.version}] condensed to no bullets" + ) + return preamble + "\n" + "\n".join(lines).rstrip() + "\n" + + +def release_body( + section: ChangelogSection, + *, + repo: str = REPOSITORY, + budget: int = RELEASE_BODY_BUDGET, + limit: int = GITHUB_RELEASE_BODY_LIMIT, +) -> str: + """Return a release body that always fits GitHub's limit (#1288). + + Within budget the section is published verbatim. Past it the section is + condensed, and in the pathological case where even the index overflows the + index is truncated — the step must never be the thing that fails after the + immutable archives are already on PyPI. + """ + if len(section.notes) <= budget: + return section.notes + condensed = condense_notes(section, repo=repo, limit=limit) + if len(condensed) <= limit: + return condensed + notice = ( + f"\n\n_This index is truncated at {limit:,} characters; " + "the CHANGELOG link above carries every entry._\n" + ) + kept = condensed[: limit - len(notice)] + cut = kept.rfind("\n") + return (kept[:cut] if cut > 0 else kept.rstrip()) + notice def validate_version_sync(root: Path = ROOT) -> None: @@ -365,9 +497,10 @@ def _parser() -> argparse.ArgumentParser: prepare.add_argument("--confirm-version") prepare.add_argument("--github-output", type=Path, required=True) - notes = commands.add_parser("notes", help="extract a changelog release section") + notes = commands.add_parser("notes", help="build a release body that fits") notes.add_argument("--version", required=True) notes.add_argument("--output", type=Path, required=True) + notes.add_argument("--repo", default=REPOSITORY) manifest = commands.add_parser("manifest", help="write archive SHA-256 values") manifest.add_argument("--dist-dir", type=Path, default=Path("dist")) @@ -398,10 +531,18 @@ def main(argv: list[str] | None = None) -> int: action = f"publish to {plan.target}" if plan.publish else "no release" print(f"Release plan for {plan.version}: {action}.") elif args.command == "notes": + section = section_for_version(args.version) + body = release_body(section, repo=args.repo) args.output.parent.mkdir(parents=True, exist_ok=True) - args.output.write_text( - notes_for_version(args.version) + "\n", encoding="utf-8" - ) + args.output.write_text(body.rstrip("\n") + "\n", encoding="utf-8") + # A pass-through returns the section itself, so length is the + # signal a reader can check against the printed numbers. + if len(body) != len(section.notes): + print( + f"Release notes for {args.version} condensed from " + f"{len(section.notes):,} to {len(body):,} characters " + f"(GitHub's limit is {GITHUB_RELEASE_BODY_LIMIT:,})." + ) elif args.command == "manifest": write_manifest(args.dist_dir, args.output) elif args.command == "assert-absent": diff --git a/spec/10-grammar.md b/spec/10-grammar.md index 4fdde43c..20de2afe 100644 --- a/spec/10-grammar.md +++ b/spec/10-grammar.md @@ -21,7 +21,13 @@ Conventions: // Whitespace and comments (skipped) WS: /\s+/ LINE_COMMENT: /--[^\n]*/ -BLOCK_COMMENT: /\{-[\s\S]*?-\}/ +// Block comments nest (Section 1.3), so they are not a regular language and +// have no regex form. The reference implementation removes them in +// vera/lexical.py, by counting depth, before the parser sees the text. +// The character alternative excludes both delimiters, so a `{-` inside the +// body opens a nested comment and must be closed: `{- {- -}` is not a +// block comment, and the implementation reports it unterminated (E020). +BLOCK_COMMENT: "{-" (BLOCK_COMMENT | /(?!\{-|-\})[\s\S]/)* "-}" ANNOTATION_COMMENT: /\/\*[^*]*\*+([^/*][^*]*\*+)*\// // Keywords @@ -94,6 +100,7 @@ SEMICOLON: ";" DOUBLE_COLON: "::" BAR: "|" UNDERSCORE: "_" +HOLE: "?" // Literals INT_LIT: /0|[1-9][0-9]*/ @@ -182,7 +189,6 @@ pure_effect: PURE effect_set: LT effect_list GT effect_list: effect_ref (COMMA effect_ref)* - | UPPER_IDENT // effect variable effect_ref: UPPER_IDENT type_args? | UPPER_IDENT DOT UPPER_IDENT type_args? // qualified effect @@ -281,6 +287,7 @@ primary_expr: INT_LIT | TRUE | FALSE | LPAREN RPAREN // unit literal + | HOLE // typed hole ? (Section 4.17) | slot_ref // @T.n | result_ref // @T.result | fn_call // function/constructor application @@ -303,9 +310,9 @@ primary_expr: INT_LIT ### 10.3.9 Slot References ```ebnf -slot_ref: AT type_expr DOT INT_LIT +slot_ref: AT UPPER_IDENT type_args? DOT INT_LIT -result_ref: AT type_expr DOT RESULT +result_ref: AT UPPER_IDENT type_args? DOT RESULT ``` ### 10.3.10 Function Calls and Constructors diff --git a/tests/test_check_corpus_differential.py b/tests/test_check_corpus_differential.py new file mode 100644 index 00000000..8a866208 --- /dev/null +++ b/tests/test_check_corpus_differential.py @@ -0,0 +1,758 @@ +"""Tests for scripts/check_corpus_differential.py — the burndown +instrument that compiles the corpus at two revisions and reports which +programs moved. + +The differential itself is far too slow to run from a test: it compiles +every corpus program twice, once per revision, in its own subprocess. +What is tested here is everything *around* those two compiles — the +corpus enumeration, the four-way mover classification, the comparison +and its counts, the report, the exit code, and the ``--json`` shape — +with every compile result injected. + +Injection is not only a speed measure. The one-sided-failure cases +(``compiles only at HEAD`` / ``compiles only at ``) need a +revision pair where a program's compilability *changed*, and the shipped +corpus deliberately has no such pair: at any two revisions CI has passed +on, the same programs compile. Those two cases are exactly the class +the PR #1323 record called out as mis-described, so they are reachable +on demand here rather than left to a lucky revision. + +Two conventions are inherited from ``tests/test_check_examples_run.py`` +and asserted throughout: an enumeration that matches nothing must be an +ERROR rather than a silent pass (otherwise a moved corpus root switches +the instrument off while it still reports success), and each check is +exercised in both directions — a classification that can only ever +answer "identical" would otherwise report a green differential over a +compiler that moved under it. +""" + +from __future__ import annotations + +import argparse +import importlib.util +import io +import json +import subprocess +import threading +from pathlib import Path, PureWindowsPath +from typing import Any + +import pytest + +_SCRIPT = ( + Path(__file__).parent.parent / "scripts" / "check_corpus_differential.py" +) +_ROOT = Path(__file__).parent.parent + + +def _load() -> Any: + spec = importlib.util.spec_from_file_location( + "check_corpus_differential", _SCRIPT + ) + assert spec is not None + module = importlib.util.module_from_spec(spec) + assert spec.loader is not None + spec.loader.exec_module(module) + return module + + +_MOD = _load() + + +# --------------------------------------------------------------------------- +# Injected compile results +# --------------------------------------------------------------------------- + + +def _ok(digest: str, size: int = 512) -> Any: + """A program that compiled, with the given WAT digest.""" + return _MOD.Artifact(ok=True, digest=digest, size=size, error="") + + +def _failed(error: str = "[E101] type mismatch") -> Any: + """A program that did not compile, with the reason the CLI gave.""" + return _MOD.Artifact(ok=False, digest=None, size=0, error=error) + + +def _info() -> Any: + return _MOD.RunInfo( + base_ref="origin/main", + base_sha="0123456789abcdef", + base_root="/scratch/vera-base-0123456789ab", + head_root="/repo", + ) + + +# --------------------------------------------------------------------------- +# Corpus enumeration +# --------------------------------------------------------------------------- + + +class TestCorpusEnumeration: + """What gets compiled, and the refusal to compile nothing.""" + + def test_the_real_corpus_spans_both_roots_and_recurses(self) -> None: + """The corpus is `examples/` plus `tests/conformance/`, at any + depth. The nested `examples/vera/` and `tests/conformance/vera/` + modules are corpus too — `examples/modules.vera` is built from + them, so a non-recursive glob would compare a program whose + inputs the differential never looked at (the same gap + `scripts/check_corpus_canonical.py` records having had).""" + files = _MOD.corpus_files(_ROOT) + rel = {p.relative_to(_ROOT).as_posix() for p in files} + + assert len(rel) > 100 + assert any(r.startswith("examples/") for r in rel) + assert any(r.startswith("tests/conformance/") for r in rel) + assert "examples/vera/math.vera" in rel + assert "tests/conformance/vera/util.vera" in rel + + def test_an_empty_corpus_is_an_error_not_a_skip(self) -> None: + """A differential over zero programs finds zero movers and would + report that as success. The enumeration matching nothing must + fail the run instead.""" + message = _MOD.corpus_guard([], Path("/nowhere")) + assert message is not None + assert "could not find" in message + + def test_a_populated_corpus_passes_the_guard(self) -> None: + """The other direction: the guard must not fail every run.""" + assert _MOD.corpus_guard([Path("/repo/examples/a.vera")], + Path("/repo")) is None + + +# --------------------------------------------------------------------------- +# Mover classification — the four cases +# --------------------------------------------------------------------------- + + +class TestMoverClassification: + """One program, two revisions, four outcomes. + + Both directions of the failure axis are separate cells, and named + separately: a classifier that lumps them together reports a program + that *stopped* compiling as one that *started*, which is the + mis-description the PR #1323 record names. + """ + + def test_identical_wat_is_not_a_mover(self) -> None: + assert _MOD.classify(_ok("abc"), _ok("abc"), "origin/main") is None + + def test_differing_wat_is_a_mover(self) -> None: + verdict = _MOD.classify(_ok("abc"), _ok("def"), "origin/main") + assert verdict is not None + kind, reason = verdict + assert kind == "wat-differs" + assert "WAT differs" in reason + + def test_compiling_only_at_head_is_a_mover(self) -> None: + """Base failed, HEAD succeeded — the working tree made a program + compilable, which is a move even though no WAT can be compared.""" + verdict = _MOD.classify(_failed("[E101] boom"), _ok("abc"), + "origin/main") + assert verdict is not None + kind, reason = verdict + assert kind == "head-only" + assert "compiles only at HEAD" in reason + assert "[E101] boom" in reason + + def test_compiling_only_at_base_is_a_mover(self) -> None: + """The reverse direction, and the one that matters most: the + working tree BROKE a program that used to compile. The reason + must name the base revision, not HEAD.""" + verdict = _MOD.classify(_ok("abc"), _failed("[E620] dropped"), + "origin/main") + assert verdict is not None + kind, reason = verdict + assert kind == "base-only" + assert "compiles only at origin/main" in reason + assert "[E620] dropped" in reason + + def test_failing_at_both_revisions_is_not_a_mover(self) -> None: + """The negative conformance fixtures live here: they fail to + compile at every revision, so they are not movers. They are + counted separately rather than folded into `identical`, because + a run whose corpus was entirely uncompilable would otherwise + report a wall of agreement it never measured.""" + assert _MOD.classify(_failed(), _failed("other"), + "origin/main") is None + + +# --------------------------------------------------------------------------- +# The comparison +# --------------------------------------------------------------------------- + + +class TestComparison: + """The per-program verdicts, rolled up.""" + + def _mixed(self) -> Any: + base = { + "a.vera": _ok("same"), + "b.vera": _ok("same"), + "c.vera": _ok("old"), + "d.vera": _failed("[E101] base"), + "e.vera": _ok("gone"), + "f.vera": _failed("[E101] base"), + } + head = { + "a.vera": _ok("same"), + "b.vera": _ok("same"), + "c.vera": _ok("new"), + "d.vera": _ok("added"), + "e.vera": _failed("[E101] head"), + "f.vera": _failed("[E101] head"), + } + return _MOD.compare(base, head, "origin/main") + + def test_counts_partition_the_corpus(self) -> None: + c = self._mixed() + assert c.compared == 6 + assert c.identical == 2 + assert c.both_failed == 1 + assert len(c.movers) == 3 + assert c.compared == c.identical + c.both_failed + len(c.movers) + + def test_each_mover_keeps_its_own_kind(self) -> None: + """By position, not by count: three movers of three different + kinds are exactly the case a classifier that mislabels one of + them still gets the count right on.""" + c = self._mixed() + assert {m.path: m.kind for m in c.movers} == { + "c.vera": "wat-differs", + "d.vera": "head-only", + "e.vera": "base-only", + } + + def test_movers_are_reported_in_path_order(self) -> None: + c = self._mixed() + assert [m.path for m in c.movers] == sorted(m.path for m in c.movers) + + def test_a_program_missing_from_one_side_is_reported_not_ignored( + self, + ) -> None: + """A program the base side never reported on cannot be compared. + Dropping it silently would shrink the corpus mid-run and still + print a clean verdict; it is surfaced instead, and it is not + counted as agreement.""" + c = _MOD.compare( + {"a.vera": _ok("same")}, + {"a.vera": _ok("same"), "b.vera": _ok("x")}, + "origin/main", + ) + assert c.unreported == ["b.vera"] + assert c.identical == 1 + assert c.compared == 1 + + +# --------------------------------------------------------------------------- +# Report, exit code, JSON +# --------------------------------------------------------------------------- + + +class TestReportAndExitCode: + """What a run prints, and what it exits.""" + + def _clean(self) -> Any: + return _MOD.compare( + {"a.vera": _ok("same"), "b.vera": _failed()}, + {"a.vera": _ok("same"), "b.vera": _failed()}, + "origin/main", + ) + + def _moved(self) -> Any: + return _MOD.compare( + {"a.vera": _ok("old"), "b.vera": _ok("kept")}, + {"a.vera": _ok("new"), "b.vera": _failed("[E620] dropped")}, + "origin/main", + ) + + def test_a_clean_run_exits_zero_and_says_so(self, capsys: Any) -> None: + assert _MOD.emit(_info(), self._clean(), as_json=False) == 0 + out = capsys.readouterr().out + assert "No movers" in out + + def test_a_run_with_movers_exits_one(self, capsys: Any) -> None: + assert _MOD.emit(_info(), self._moved(), as_json=False) == 1 + capsys.readouterr() + + def test_every_mover_is_named_with_its_reason(self, capsys: Any) -> None: + _MOD.emit(_info(), self._moved(), as_json=False) + captured = capsys.readouterr() + report = captured.out + captured.err + assert "a.vera" in report + assert "WAT differs" in report + assert "b.vera" in report + assert "compiles only at origin/main" in report + + def test_the_both_failed_count_is_reported_not_hidden( + self, capsys: Any + ) -> None: + """A corpus where half the programs compile at neither revision + agrees vacuously. The count is printed so a reader of a green + run knows how much of it was measured.""" + _MOD.emit(_info(), self._clean(), as_json=False) + out = capsys.readouterr().out + # The whole line, not just the digit: `identical WAT: 1` and the + # run's SHA both contain a "1", so a bare `"1" in out` stayed green + # on a regression that printed `compiled at neither revision: 0` + # (#1329 review). + assert "compiled at neither revision: 1" in out + + def test_an_unreported_program_exits_one(self, capsys: Any) -> None: + """A truncated run is a failed run, not a clean one — even with + no movers among the programs that did report.""" + comparison = _MOD.compare( + {"a.vera": _ok("same")}, + {"a.vera": _ok("same"), "b.vera": _ok("x")}, + "origin/main", + ) + assert _MOD.emit(_info(), comparison, as_json=False) == 1 + capsys.readouterr() + + def test_json_carries_the_verdict_and_the_run_identity( + self, capsys: Any + ) -> None: + code = _MOD.emit(_info(), self._moved(), as_json=True) + payload = json.loads(capsys.readouterr().out) + + assert code == 1 + assert payload["ok"] is False + assert payload["base_ref"] == "origin/main" + assert payload["base_sha"] == "0123456789abcdef" + assert payload["base_root"] == "/scratch/vera-base-0123456789ab" + assert payload["head_root"] == "/repo" + assert payload["compared"] == 2 + assert payload["identical"] == 0 + assert payload["both_failed"] == 0 + assert payload["unreported"] == [] + assert {m["path"]: m["kind"] for m in payload["movers"]} == { + "a.vera": "wat-differs", + "b.vera": "base-only", + } + assert all("reason" in m for m in payload["movers"]) + + def test_json_flags_a_clean_run_ok(self, capsys: Any) -> None: + code = _MOD.emit(_info(), self._clean(), as_json=True) + payload = json.loads(capsys.readouterr().out) + assert code == 0 + assert payload["ok"] is True + assert payload["movers"] == [] + assert payload["both_failed"] == 1 + + +# --------------------------------------------------------------------------- +# The compiler canary +# --------------------------------------------------------------------------- + + +class TestCompilerCanary: + """Which `vera` each side actually imported. + + The load-bearing guard of the whole instrument. Both sides run the + same CLI under different `PYTHONPATH`s, and the venv carries an + editable install of a *third* checkout whose finder sits on + `sys.meta_path`. If either side resolves `vera` somewhere other + than its own root, the run compares a revision against itself and + reports 0 movers — a green verdict that measured nothing. + """ + + def test_a_compiler_under_the_expected_root_passes(self) -> None: + assert _MOD.canary_error( + "/scratch/base/vera/__init__.py", Path("/scratch/base"), "base" + ) is None + + def test_a_compiler_outside_the_expected_root_is_an_error(self) -> None: + root = Path("/scratch/base") + message = _MOD.canary_error( + "/usr/lib/site-packages/vera/__init__.py", root, "base" + ) + assert message is not None + assert "base" in message + assert "/usr/lib/site-packages/vera/__init__.py" in message + # The root is asserted by the property "it is this path", not by a + # POSIX shape: the message renders it with the host's separators, + # and `\scratch\base` is the correct rendering on Windows. + assert str(root) in message + assert "different checkout" in message + + def test_the_root_in_the_message_is_the_root_it_was_given(self) -> None: + """Non-vacuity for the assertion above: `str(root) in message` + would also hold if the message quoted some other path that + happened to contain it, so a different root must change it.""" + elsewhere = _MOD.canary_error( + "/usr/lib/site-packages/vera/__init__.py", Path("/other/root"), "base" + ) + assert elsewhere is not None + assert str(Path("/other/root")) in elsewhere + assert str(Path("/scratch/base")) not in elsewhere + + def test_an_import_failure_is_an_error_that_says_so(self) -> None: + """A side that could not import `vera` at all reports no path; + that is a failed run, not an absent objection. + + The message must say the import failed. Asserting only that + *some* message came back is satisfied by the wrong branch: an + empty path resolves to the process's own directory, which is not + under the expected root either, so a missing import-failure + check still objects — while claiming the side compiled with + another checkout's compiler, which is not what happened. + """ + message = _MOD.canary_error("", Path("/scratch/base"), "base") + assert message is not None + assert "base" in message + assert "could not import" in message + + +# --------------------------------------------------------------------------- +# Collection +# --------------------------------------------------------------------------- + + +class TestCollection: + """How per-file results are keyed, with the compile injected.""" + + def test_results_are_keyed_by_repo_relative_posix_path(self) -> None: + """Both sides compile the *working tree's* files, so both maps + must be keyed against that one corpus root. An absolute key + would work only by accident — the base compiler runs from a + scratch checkout elsewhere — and a side-specific key would leave + every program unreported. POSIX form because the key is + compared as a string (CLAUDE.md's cross-platform rule).""" + root = Path("/repo") + files = [ + root / "examples" / "a.vera", + root / "tests" / "conformance" / "vera" / "b.vera", + ] + seen: list[Path] = [] + + def fake_compile(path: Path) -> Any: + seen.append(path) + return _ok(f"digest-of-{path.name}") + + results = _MOD.collect(files, root, fake_compile) + + assert set(results) == { + "examples/a.vera", + "tests/conformance/vera/b.vera", + } + assert results["examples/a.vera"].digest == "digest-of-a.vera" + assert seen == files + + +# --------------------------------------------------------------------------- +# The failure reason +# --------------------------------------------------------------------------- + + +class TestFailureReason: + """What a one-sided mover's line says the compile failed of. + + Measured, not imagined: the first version took the first line of + stderr that did not begin with ``warning:``, and a real run against + v0.1.9 reported a *warning's* quoted source line + (``public fn read_some(@Unit -> @Int)``) as the reason a program did + not compile. A diagnostic is a block, and only its first line + carries the marker. + """ + + _WARNING_BLOCK = ( + "warning: [E604] Error at /repo/x.vera, line 3, column 1:\n" + "\n" + " public fn read_some(@Unit -> @Int)\n" + " ^\n" + "\n" + " Function 'read_some' has unsupported parameter type.\n" + ) + + def test_the_reason_is_the_error_not_a_warnings_source_line(self) -> None: + stderr = ( + self._WARNING_BLOCK + + "[E154] Error at /repo/x.vera, line 9, column 8:\n" + "\n public forall fn pick(@VeraFn -> @Int)\n" + ) + reason = _MOD._first_error(stderr, Path("/repo/x.vera")) + assert "[E154]" in reason + assert "read_some" not in reason + + def test_the_compiled_files_path_is_not_repeated_in_the_reason( + self, + ) -> None: + """The reason is already attached to a named program, and the + absolute path of a corpus file under a scratch checkout is long + enough to push the diagnostic out of the truncated line.""" + stderr = "[E154] Error at /repo/x.vera, line 9, column 8:\n" + reason = _MOD._first_error(stderr, Path("/repo/x.vera")) + assert "/repo/x.vera" not in reason + assert "x.vera" in reason + + def test_a_posix_form_path_is_stripped_under_a_windows_renderer(self) -> None: + """The diagnostic's spelling of the path need not be the host's. + + Stripping on ``str(path)`` alone is a separator-shaped match: on + Windows the same path renders `\\repo\\x.vera`, so a diagnostic + carrying the POSIX form goes unstripped and its absolute path + pushes the message past the truncation — the silent + matches-nothing failure, not a loud one. ``PureWindowsPath`` + reproduces that rendering on any host, so this cell fails on + macOS too rather than only in the Windows CI cell. + """ + stderr = "[E154] Error at /repo/x.vera, line 9, column 8:\n" + reason = _MOD._first_error(stderr, PureWindowsPath("/repo/x.vera")) + assert "/repo/x.vera" not in reason + assert "x.vera" in reason + assert "[E154]" in reason + + def test_a_native_form_path_is_stripped_under_a_windows_renderer(self) -> None: + """The complement: the same path as Windows itself would print it.""" + stderr = "[E154] Error at \\repo\\x.vera, line 9, column 8:\n" + reason = _MOD._first_error(stderr, PureWindowsPath("/repo/x.vera")) + assert "\\repo\\x.vera" not in reason + assert "x.vera" in reason + + def test_a_crash_reports_its_exception_not_its_first_line(self) -> None: + """No diagnostic marker at all — a compiler crash. The useful + line is the exception, which is last.""" + stderr = ( + "Traceback (most recent call last):\n" + ' File "/repo/vera/cli.py", line 1, in main\n' + "AssertionError: slot table is empty\n" + ) + reason = _MOD._first_error(stderr, Path("/repo/x.vera")) + assert reason == "AssertionError: slot table is empty" + + def test_silence_still_gives_a_reason(self) -> None: + assert _MOD._first_error("", Path("/repo/x.vera")) != "" + + +# --------------------------------------------------------------------------- +# What the instrument is not +# --------------------------------------------------------------------------- + + +class TestNotAPreCommitHook: + """The module docstring's claim, asserted rather than trusted.""" + + def test_the_instrument_is_not_wired_into_pre_commit(self) -> None: + """It compiles the whole corpus twice. As a commit hook that is + minutes per commit, which is why it is a burndown instrument the + maintainer runs deliberately. If it is ever wired in, the + module docstring saying it is not must change in the same + commit.""" + config = (_ROOT / ".pre-commit-config.yaml").read_text( + encoding="utf-8" + ) + assert "check_corpus_differential" not in config + + +class TestParallelCollection: + """The `jobs > 1` branch, which no cell reached (#1329 review). + + Every other collection cell runs at the default `jobs=1`, so the + sequential branch was covered and the parallel one was not. The + parallel branch pairs keys with results *positionally* — it zips a + list built from `files` against `ThreadPoolExecutor.map`'s output — + so it is correct only while `map` yields in input order. If that + ever stopped holding, every artifact would be attributed to the + wrong program and the run would invent movers out of nothing, which + is the one failure this instrument must not have. + """ + + def test_results_stay_paired_with_their_keys(self) -> None: + root = Path("/repo") + files = [root / "examples" / f"p{index}.vera" for index in range(24)] + + def fake_compile(path: Path) -> Any: + return _ok(f"digest-of-{path.name}") + + results = _MOD.collect(files, root, fake_compile, jobs=4) + + assert len(results) == len(files) + for path in files: + assert results[f"examples/{path.name}"].digest == f"digest-of-{path.name}" + + def test_the_parallel_branch_is_the_one_being_exercised(self) -> None: + """Non-vacuity: `jobs=4` must not quietly fall through to the + sequential path, or this class tests nothing new. + + The property is *where* the work ran, not how many threads the + pool chose to spawn. `ThreadPoolExecutor` creates a worker only + when no idle one is available, so a handful of trivial callables + can be drained by a single worker before `map` finishes + submitting them: measured over 200 trials on a 12-core host the + distinct-thread count came out 2, 3 or 4, and on a 2-core CI + runner it is 1. Asserting `len(threads) > 1` therefore inherited + the host's scheduling — green here, red on every CI cell. What + *is* invariant is that the pool never executes inline: the + calling thread ran work in 0 of those 200 trials, and 0 of any, + because `submit` always hands the callable to a worker. + """ + root = Path("/repo") + files = [root / "examples" / f"p{index}.vera" for index in range(8)] + threads: set[int] = set() + + def fake_compile(path: Path) -> Any: + threads.add(threading.get_ident()) + return _ok(path.name) + + _MOD.collect(files, root, fake_compile, jobs=4) + assert threads, "no compile ran at all" + assert threading.get_ident() not in threads, ( + "a compile ran on the calling thread, so `jobs=4` fell through " + "to the sequential branch" + ) + + def test_the_sequential_branch_runs_inline(self) -> None: + """The complement, and the reason the cell above is not vacuous: + `jobs=1` must run on the caller, so the two branches are told + apart by the same observation rather than by a count.""" + root = Path("/repo") + files = [root / "examples" / f"p{index}.vera" for index in range(8)] + threads: set[int] = set() + + def fake_compile(path: Path) -> Any: + threads.add(threading.get_ident()) + return _ok(path.name) + + _MOD.collect(files, root, fake_compile, jobs=1) + assert threads == {threading.get_ident()} + + def test_both_branches_agree(self) -> None: + root = Path("/repo") + files = [root / "examples" / f"p{index}.vera" for index in range(8)] + + def fake_compile(path: Path) -> Any: + return _ok(f"digest-of-{path.name}") + + assert _MOD.collect(files, root, fake_compile, jobs=1) == _MOD.collect( + files, root, fake_compile, jobs=4 + ) + + +class TestSideEnvironment: + """`_side_env`, which had no test at all (#1329 review).""" + + def test_pythonpath_is_replaced_not_extended( + self, monkeypatch: Any + ) -> None: + """The caller's `PYTHONPATH` usually names the head checkout — + that is how this repo is driven. Inheriting it on the base side + puts the head compiler first on the path, so the differential + compares a revision against itself and reports zero movers: the + vacuity `canary_error` exists to catch, arriving one layer down. + """ + monkeypatch.setenv("PYTHONPATH", "/repo") + env = _MOD._side_env(Path("/scratch/base")) + assert env["PYTHONPATH"] == str(Path("/scratch/base")) + assert "/repo" not in env["PYTHONPATH"] + + def test_bytecode_writing_is_off_for_both_checkouts( + self, monkeypatch: Any + ) -> None: + """Scrubbed from the ambient environment first, deliberately. + + This suite is itself run with `PYTHONDONTWRITEBYTECODE=1`, and + `_side_env` copies `os.environ` — so without the scrub the + assertion is satisfied by the caller's shell and passes with the + line under test deleted. It measures the function only when the + variable is absent to begin with. + """ + monkeypatch.delenv("PYTHONDONTWRITEBYTECODE", raising=False) + env = _MOD._side_env(Path("/scratch/base")) + assert env["PYTHONDONTWRITEBYTECODE"] == "1" + + def test_the_rest_of_the_environment_is_inherited( + self, monkeypatch: Any + ) -> None: + """Only those two keys are the function's business: the base + compiler still needs the venv's interpreter and its PATH.""" + monkeypatch.setenv("VERA_SIDE_ENV_PROBE", "kept") + assert _MOD._side_env(Path("/scratch/base"))["VERA_SIDE_ENV_PROBE"] == "kept" + + +class TestTimeoutValidation: + """`--timeout` must be able to elapse (#1329 review). + + Zero or negative expires before any compile finishes, so both sides + fail every program, `compare` counts them all as `both_failed`, and + `emit` reports "No movers" with exit 0 over a corpus that never + compiled — a green run measuring nothing. + """ + + @pytest.mark.parametrize("value", ["0", "-1"]) + def test_a_non_positive_budget_is_rejected(self, value: str) -> None: + with pytest.raises(argparse.ArgumentTypeError, match="greater than zero"): + _MOD._positive_seconds(value) + + def test_a_positive_budget_is_accepted(self) -> None: + assert _MOD._positive_seconds("120") == 120 + + @pytest.mark.parametrize("value", ["0", "-1"]) + def test_the_parser_refuses_it_too(self, value: str) -> None: + """Wired into `--timeout`, not merely defined beside it.""" + with pytest.raises(SystemExit): + _MOD._parse_args(["--timeout", value]) + + +class TestUndecodableCompilerOutput: + """A compiler byte the codec cannot read must stay data (#1329 review). + + Strict decoding raises `UnicodeDecodeError` out of `subprocess.run` + itself — a `ValueError`, which neither handler in `compile_one` + catches — and `collect` iterates `ThreadPoolExecutor.map`, so that + one program would abort the whole corpus run. + """ + + def test_the_compile_asks_for_lenient_decoding( + self, monkeypatch: Any + ) -> None: + seen: dict[str, Any] = {} + + def fake_run(*args: Any, **kwargs: Any) -> Any: + seen.update(kwargs) + raise subprocess.TimeoutExpired(cmd="x", timeout=1) + + monkeypatch.setattr(_MOD.subprocess, "run", fake_run) + _MOD.compile_one("python", Path("/scratch"), 5, Path("/repo/a.vera")) + assert seen.get("encoding") == "utf-8" + assert seen.get("errors") == "replace" + + def test_strict_decoding_is_what_would_have_raised(self) -> None: + """The reason the kwarg above matters, measured rather than + asserted: the same bytes through the same decoder raise on + strict and survive on replace. + + Measured through `io.TextIOWrapper`, which is not a stand-in — + it is the mechanism. `subprocess.Popen` wraps each captured + pipe in exactly this object with exactly the `encoding` and + `errors` it was given, so this reproduces `compile_one`'s + decode without a child process. + + Spawning one was the previous shape and it made the cell + environment-dependent: what a child puts on a pipe depends on + the OS, and the three Windows cells failed here with "DID NOT + RAISE". The decode itself never varied — both calls named + `encoding="utf-8"` — but the byte reaching them did. Note the + byte is only undecodable in UTF-8: `b"\\x97".decode("cp1252")` + is an em dash, so a decode left to the platform default would + not raise on Windows either. Naming the codec is what makes + this deterministic, and it is the same codec the script names. + """ + undecodable = b"\x97" + + def decode(**kwargs: Any) -> str: + return io.TextIOWrapper( + io.BytesIO(undecodable), encoding="utf-8", **kwargs + ).read() + + with pytest.raises(UnicodeDecodeError): + decode() + assert decode(errors="replace") == "\ufffd" + + def test_the_byte_is_undecodable_in_the_codec_the_script_names(self) -> None: + """Non-vacuity: the fixture must be undecodable in UTF-8 and not + merely unusual, or the cell above proves nothing about the + codec `compile_one` actually passes.""" + with pytest.raises(UnicodeDecodeError): + b"\x97".decode("utf-8") + assert b"\x97".decode("cp1252") == "\u2014" diff --git a/tests/test_check_doc_counts.py b/tests/test_check_doc_counts.py index 8e5f44ba..077f7f0b 100644 --- a/tests/test_check_doc_counts.py +++ b/tests/test_check_doc_counts.py @@ -7,7 +7,7 @@ line counts must stay within ±10% of the measured file sizes. - ``check_history_row_format`` — HISTORY.md version rows carry at most one issue link and no " — " separator. -- ``check_tests_breakdown`` — TESTING.md's passed/stress/skipped parts +- ``check_tests_breakdown`` — TESTING.md's passed/stress-deselected/skipped parts must sum to the collected total. - ``check_vera_readme_test_counts`` — the four counts in vera/README.md's Test Suite paragraph. @@ -26,6 +26,7 @@ from __future__ import annotations import importlib.util +import re from pathlib import Path from typing import Any @@ -207,7 +208,8 @@ def _overview(passed: int, stress: int, skipped: int, total: int) -> str: "| Metric | Value |\n" "|--------|-------|\n" f"| **Tests** | {total:,} across 143 files (~108,000 lines of test" - f" code; {passed:,} passed + {stress} stress, {skipped} skipped) |\n" + f" code; {passed:,} passed + {stress} stress-deselected," + f" {skipped} skipped) |\n" ) @@ -663,3 +665,323 @@ def test_a_directory_that_is_not_a_repository_is_no_evidence( plain = tmp_path / "plain" plain.mkdir() assert _MOD.release_tags(plain) is None + + +# --------------------------------------------------------------------------- +# README's project-status line (#1290 rider): the sentence gated the tests +# figure and nothing else on it. The conformance count beside it drifted +# through two rebases unseen, because `check_readme` returned silently when a +# pattern matched nothing — four of its five patterns matched nothing at all. +# --------------------------------------------------------------------------- + +_STATUS = ( + "Vera is in **active development** at v0.1.11: 2,000+ commits, 209 " + "releases, 11,134 tests, 95% Python code coverage, 229 conformance " + "programs, 42 examples, and a 14-chapter specification.\n" +) + + +class TestProjectStatusLine: + def test_the_shipped_line_is_consistent(self) -> None: + assert _MOD.check_project_status(_STATUS, 11134, 229, 42, 14) == [] + + def test_every_count_on_the_line_is_gated(self) -> None: + """One error per wrong figure, and the conformance one is among them.""" + errors = _MOD.check_project_status(_STATUS, 1, 2, 3, 4) + assert len(errors) == 4 + assert any("conformance" in e for e in errors) + assert any("examples" in e for e in errors) + assert any("chapter" in e for e in errors) + + def test_the_conformance_count_alone_is_caught(self) -> None: + """The measured drift: tests right, conformance stale beside it.""" + errors = _MOD.check_project_status(_STATUS, 11134, 230, 42, 14) + assert len(errors) == 1 + assert "229" in errors[0] and "230" in errors[0] + + def test_a_missing_status_line_is_an_error_not_a_skip(self) -> None: + # Same true numbers, phrasing the pattern cannot see. Returning [] + # here is what let four of the five README gates sit dead. + text = "Vera has 11,134 tests and 229 conformance programs.\n" + errors = _MOD.check_project_status(text, 11134, 229, 42, 14) + assert len(errors) == 1 + assert "could not find" in errors[0] + + def test_a_count_dropped_from_the_line_is_an_error_not_a_skip(self) -> None: + text = _STATUS.replace("229 conformance programs, ", "") + errors = _MOD.check_project_status(text, 11134, 229, 42, 14) + assert len(errors) == 1 + assert "could not find" in errors[0] + + def test_the_counts_are_read_from_the_status_line_only(self) -> None: + """A decoy elsewhere in the file must not satisfy the gate.""" + text = "Elsewhere: 999 conformance programs.\n\n" + _STATUS + assert _MOD.check_project_status(text, 11134, 229, 42, 14) == [] + + +# --------------------------------------------------------------------------- +# TESTING.md's dual-target row (#1290 rider): a run-level total from the +# manifest, and a tested/skipped split with three category counts that no +# oracle read. +# --------------------------------------------------------------------------- + +_DUAL_ROW = ( + "the **dual-target conformance differential** (all 168 run-level " + "conformance programs driven under both targets, byte-identical " + "stdout/stderr required — 118 are dual-tested and 50 skip *loudly* " + "rather than passing silently: 43 whose compiled WAT imports a host " + "family outside `IO`/`Random`, 6 with no public zero-argument `main`, " + "and 1 calling a nondeterministic op.)\n" +) + + +def _split(**overrides: int) -> Any: + values = dict(tested=118, skipped=50, families=43, no_main=6, nondeterministic=1) + values.update(overrides) + return _MOD.DualTargetSplit(**values) + + +class TestDualTargetRow: + def test_the_shipped_row_is_consistent(self) -> None: + assert _MOD.check_dual_target_row(_DUAL_ROW, 168, _split()) == [] + + def test_the_run_level_total_comes_from_the_manifest(self) -> None: + errors = _MOD.check_dual_target_row(_DUAL_ROW, 169, _split()) + assert [e for e in errors if "run-level total" in e] + + def test_each_part_of_the_split_is_gated(self) -> None: + errors = _MOD.check_dual_target_row( + _DUAL_ROW, 168, _split(tested=117, skipped=51) + ) + assert len(errors) == 2 + + def test_each_category_is_gated(self) -> None: + errors = _MOD.check_dual_target_row( + _DUAL_ROW, 168, _split(families=42, no_main=7, nondeterministic=2) + ) + assert len(errors) == 3 + + def test_the_split_must_sum_to_the_run_level_total(self) -> None: + """Three consistent-looking numbers that do not add up is drift.""" + errors = _MOD.check_dual_target_row( + _DUAL_ROW.replace("all 168 run-level", "all 200 run-level"), + 200, + _split(), + ) + assert [e for e in errors if "does not add up" in e] + + def test_the_categories_must_sum_to_the_skip_total(self) -> None: + row = _DUAL_ROW.replace("and 1 calling", "and 2 calling") + errors = _MOD.check_dual_target_row(row, 168, _split(nondeterministic=2)) + assert [e for e in errors if "do not add up" in e] + + def test_a_reworded_row_is_an_error_not_a_skip(self) -> None: + # The same true numbers, phrased so no pattern sees them. + text = "The differential drives 168 programmes, skipping 50 of them.\n" + errors = _MOD.check_dual_target_row(text, 168, _split()) + assert [e for e in errors if "could not find" in e] + + def test_one_reworded_figure_is_an_error_not_a_skip(self) -> None: + """The row still parses; a single category has been reworded away. + + Every other figure agrees, so a silent skip here leaves the row + looking checked while one of its five numbers is unread. + """ + row = _DUAL_ROW.replace("43 whose compiled WAT", "forty-three whose WAT") + errors = _MOD.check_dual_target_row(row, 168, _split()) + assert len(errors) == 1 + assert "could not find" in errors[0] and "families" in errors[0] + + def test_the_live_split_is_read_from_the_test_run(self) -> None: + """Non-vacuity: parsed from real ``-rs`` output, not from the doc.""" + report = ( + "SKIPPED [43] tests/test_wasi_target.py:1130: family gate: " + "--target wasi-p2 does not support the following host family: map\n" + "SKIPPED [6] tests/test_wasi_target.py:1130: family gate: " + "--target wasi-p2 requires a public zero-argument `main` entry point\n" + "SKIPPED [1] tests/test_wasi_target.py:1124: nondeterministic ops " + "['random_int']\n" + "118 passed, 50 skipped in 3.15s\n" + ) + assert _MOD.parse_dual_target_report(report) == _split() + + def test_an_unclassified_skip_is_an_error_not_a_skip(self) -> None: + report = ( + "SKIPPED [50] tests/test_wasi_target.py:1130: some new reason\n" + "118 passed, 50 skipped in 3.15s\n" + ) + assert _MOD.parse_dual_target_report(report) is None + + def test_an_unclassified_skip_beside_a_correct_total_is_still_an_error( + self, + ) -> None: + """The three documented categories already account for every skip. + + Folding a fourth reason into none of them leaves the arithmetic + looking right, so the sum reconciliation alone cannot catch it. + """ + report = ( + "SKIPPED [43] host family: map\n" + "SKIPPED [6] requires a public zero-argument `main`\n" + "SKIPPED [1] nondeterministic ops ['random_int']\n" + "SKIPPED [3] tests/test_wasi_target.py:9: a brand new reason\n" + "118 passed, 50 skipped in 3.15s\n" + ) + assert _MOD.parse_dual_target_report(report) is None + + def test_classified_skips_that_miss_the_summary_total_are_an_error(self) -> None: + """Every reason is known and they still do not account for the run. + + The complement of the case above: the unclassified-reason guard is + satisfied here, so only the sum reconciliation can catch it. + """ + report = ( + "SKIPPED [43] host family: map\n" + "SKIPPED [6] requires a public zero-argument `main`\n" + "SKIPPED [1] nondeterministic ops ['random_int']\n" + "118 passed, 55 skipped in 3.15s\n" + ) + assert _MOD.parse_dual_target_report(report) is None + + def test_a_report_with_no_summary_line_is_an_error_not_a_skip(self) -> None: + assert _MOD.parse_dual_target_report("nothing to see here\n") is None + + def test_a_summary_omitting_the_skipped_category_is_read(self) -> None: + """pytest prints no category with a zero count, so `174 passed in + 3.1s` is a well-formed summary. Requiring both groups made it + unreadable, and an unreadable report is reported as drift — a + false failure (#1329 review).""" + split = _MOD.parse_dual_target_report("174 passed in 3.15s\n") + assert split == _MOD.DualTargetSplit(174, 0, 0, 0, 0) + + def test_a_summary_omitting_the_passed_category_is_read(self) -> None: + """The complement: every run-level programme skipped.""" + report = ( + "SKIPPED [52] host family: map\n" + "52 skipped in 3.15s\n" + ) + assert _MOD.parse_dual_target_report(report) == _MOD.DualTargetSplit( + 0, 52, 52, 0, 0 + ) + + +# --------------------------------------------------------------------------- +# KNOWN_ISSUES' Bugs table (#1290 rider): one row per open `bug` issue. +# +# The parity half needs the GitHub API, which a pre-commit hook must not +# depend on, so it is opt-in: `--check-bug-issues` at release-PR time. The +# structural half is pure text and always on. +# --------------------------------------------------------------------------- + + +def _bugs(*rows: str) -> str: + body = "\n".join(rows) + return f"# Known Issues\n\n## Bugs\n\n| Bug | Issue |\n|-----|-------|\n{body}\n\n## Limitations\n" + + +def _row(number: int, text: str = "Something is wrong.") -> str: + url = f"https://github.com/aallan/vera/issues/{number}" + return f"| {text} | [#{number}]({url}) |" + + +class TestBugRows: + def test_the_shipped_table_parses(self) -> None: + text = (Path(__file__).parent.parent / "KNOWN_ISSUES.md").read_text( + encoding="utf-8" + ) + rows = _MOD.bug_rows(text) + assert rows is not None + # The floor is derived from the file, not a literal: `> 5` would + # fail the day the tracker is burned down to five open bugs, which + # is a project state rather than a regression — and it would not + # catch the parser returning a SHORT list, which is the failure + # worth naming (#1329 review). + section = re.search(r"^## Bugs[ \t]*$(.*?)(?=^## )", text, re.M | re.S) + assert section is not None + table = [ + line + for line in section.group(1).splitlines() + if line.startswith("|") and not set(line) <= set("|- ") + ][1:] # drop the header row + assert table, "the Bugs table is no longer being read" + assert len(rows) == len(table) + assert len(set(rows)) == len(rows) + + def test_a_row_with_no_issue_link_is_an_error(self) -> None: + text = _bugs("| A bug with no tracker. | none |") + errors = _MOD.check_bug_rows(text) + assert len(errors) == 1 and "not found" in errors[0] + + def test_two_rows_for_one_issue_are_an_error(self) -> None: + """One-to-one: two rows citing one issue is a duplicate, not two bugs.""" + text = _bugs(_row(101), _row(101, "The same bug again.")) + errors = _MOD.check_bug_rows(text) + assert len(errors) == 1 and "twice" in errors[0] + + def test_a_link_whose_number_and_url_disagree_is_an_error(self) -> None: + text = _bugs( + "| Mislinked. | [#101](https://github.com/aallan/vera/issues/202) |" + ) + errors = _MOD.check_bug_rows(text) + assert len(errors) == 1 and "not found" in errors[0] + + def test_a_pull_request_link_is_not_an_issue_link(self) -> None: + text = _bugs("| Wrong kind. | [#101](https://github.com/aallan/vera/pull/101) |") + errors = _MOD.check_bug_rows(text) + assert len(errors) == 1 and "not found" in errors[0] + + def test_a_row_carrying_a_pipe_in_its_prose_still_parses(self) -> None: + text = _bugs(_row(101, "The `|>` operator is wrong.")) + assert _MOD.check_bug_rows(text) == [] + + def test_the_no_known_bugs_convention_is_not_an_empty_table(self) -> None: + text = "# Known Issues\n\n## Bugs\n\nNo known bugs.\n\n## Limitations\n" + assert _MOD.bug_rows(text) == [] + assert _MOD.check_bug_rows(text) == [] + + def test_an_empty_bugs_section_is_an_error_not_a_skip(self) -> None: + text = "# Known Issues\n\n## Bugs\n\n## Limitations\n" + errors = _MOD.check_bug_rows(text) + assert len(errors) == 1 and "not found" in errors[0] + + def test_a_renamed_heading_is_an_error_not_a_skip(self) -> None: + text = _bugs(_row(101)).replace("## Bugs", "## Open bugs") + errors = _MOD.check_bug_rows(text) + assert len(errors) == 1 and "not found" in errors[0] + + +class TestBugIssueParity: + def test_a_matching_pair_of_sets_is_clean(self) -> None: + assert _MOD.check_bug_issue_parity([101, 102], [102, 101]) == [] + + def test_an_open_bug_issue_with_no_row_is_reported(self) -> None: + errors = _MOD.check_bug_issue_parity([101], [101, 102]) + assert len(errors) == 1 and "#102" in errors[0] + + def test_a_row_whose_issue_is_not_an_open_bug_is_reported(self) -> None: + errors = _MOD.check_bug_issue_parity([101, 103], [101]) + assert len(errors) == 1 and "#103" in errors[0] + + def test_no_open_bug_issues_is_an_error_not_a_skip(self) -> None: + """An empty fetch is a failed query, not a clean bill of health.""" + errors = _MOD.check_bug_issue_parity([101], []) + assert [e for e in errors if "not found" in e] + + def test_the_parity_check_is_not_wired_into_the_default_run(self) -> None: + """A pre-commit hook must not depend on the GitHub API.""" + source = _SCRIPT.read_text(encoding="utf-8") + assert "--check-bug-issues" in source + # EVERY call site, not just the last one: `rindex` inspected only + # the final occurrence, so an unguarded call added above it would + # leave this green while the pre-commit hook made a network call + # (#1329 review). + calls = [ + index + for index in range(len(source)) + if source.startswith("check_bug_issue_parity(", index) + and not source.startswith("def check_bug_issue_parity(", max(0, index - 4)) + ] + assert calls, "the parity check is no longer called at all" + for index in calls: + guarded = source[max(0, index - 600) : index] + assert "args.check_bug_issues" in guarded diff --git a/tests/test_check_examples_run.py b/tests/test_check_examples_run.py index ff75da35..5980deb7 100644 --- a/tests/test_check_examples_run.py +++ b/tests/test_check_examples_run.py @@ -79,6 +79,79 @@ def _load() -> Any: """ +# A program whose only external-resource signal is its declared effect +# ROW: `DB` is in ``RESOURCE_EFFECTS``, while `DB.execute` is not in +# ``RESOURCE_OPS`` — so a derivation that stopped reading effect rows +# would find nothing here. +_DB_SRC = """\ +public fn main(-> @Int) + requires(true) + ensures(true) + effects() +{ + let @Array> = []; + match DB.execute("CREATE TABLE t (id INTEGER)", @Array>.0) { + Err(@String) -> { + IO.print(@String.0); + 1 + }, + Ok(@Int) -> { + IO.print("created the table"); + 0 + } + } +} +""" + +# The mirror image: the only signal is an operation CALL. `IO` is not in +# ``RESOURCE_EFFECTS`` — sixteen examples declare a bare `` and only +# one touches the filesystem — so a derivation that stopped reading call +# sites would find nothing here. +_FILE_SRC = """\ +public fn main(-> @Unit) + requires(true) + ensures(true) + effects() +{ + match IO.read_file("hello.txt") { + Ok(@String) -> IO.print(@String.0), + Err(@String) -> IO.print(@String.0) + } +} +""" + +# Both shapes in prose only. A text scan would call this a database +# program; the derivation reads the parsed declarations, so it does not. +_COMMENTED_SRC = """\ +-- Names the effect and IO.read_file in prose, and uses neither. +public fn main(-> @Int) + requires(true) + ensures(true) + effects(pure) +{ + -- effects() would go here, and IO.write_file("a", "b") below. + 1 + 1 +} +""" + +# Not Vera at all — the parse must fail rather than yield "no signals". +_UNPARSEABLE_SRC = "public fn main(-> @Int) { this is not Vera at all\n" + + +# A module-qualified effect whose tail is `DB`. `Mod.DB` names a user +# effect in another module, not the built-in the registry check validated, +# so the derivation must not credit it (#1329 review). +_QUALIFIED_DB_SRC = """\ +public fn main(-> @Int) + requires(true) + ensures(true) + effects() +{ + 0 +} +""" + + def _corpus(tmp_path: Path, programs: dict[str, str]) -> Path: d = tmp_path / "examples" d.mkdir(exist_ok=True) @@ -226,14 +299,23 @@ def test_no_spec_relies_on_the_first_export_fallback(self) -> None: def test_environment_dependent_specs_carry_an_output_sentinel( self, ) -> None: - """Three examples reach outside the process — a committed SQLite - fixture, an in-memory database, the filesystem — and each answers a - failure by printing a message and completing normally. Exit code - alone cannot tell their success path from their graceful one, so - each must pin a substring only the success path prints.""" - for name in ("sqlitedb", "database", "file_io"): - spec = _MOD.RUN_SPECS[name] - assert spec.expect, f"{name} has no expected-output sentinel" + """An example that reaches outside the process answers a failure by + printing a message and completing normally, so exit code alone + cannot tell its success path from its graceful one: each must pin a + substring only the success path prints. + + WHICH examples those are is derived from the corpus, not listed + here. A literal `("sqlitedb", "database", "file_io")` asserts the + sentinels the corpus already has and nothing about the next + example of the same kind — the one case the rule exists for. So + the assertion is the two-way equality between the examples that + *declare* an external resource and the specs that carry an + `expect`, which a new database or filesystem example joins by + being written rather than by being remembered. + """ + assert _MOD.check_sentinel_coverage( + _ROOT / "examples", _MOD.RUN_SPECS + ) == [] def test_every_skip_property_is_documented(self) -> None: for name, prop in _MOD.SKIPS.items(): @@ -245,6 +327,299 @@ def test_no_unused_skip_property(self) -> None: assert set(_MOD.SKIP_PROPERTIES) == set(_MOD.SKIPS.values()) +# --------------------------------------------------------------------------- +# The derived sentinel rule +# --------------------------------------------------------------------------- + + +class TestResourceSignalDerivation: + """Which examples must pin a sentinel is read off the examples. + + The declared constants are resource *names* — the `DB` effect, the + `IO.read_file` / `IO.write_file` operations — and the example set + follows from which programs declare them. Names rather than + filenames is the whole point: a filename list is a snapshot of + today's corpus, and the case the rule exists for is tomorrow's + example. + + An effect row alone cannot discriminate, which is why the operations + are read too: `FileIO` and `Time` are not effects in Vera, so + `file_io.vera` declares the same bare `` that `hello_world.vera` + does, and only the `IO.read_file` call tells them apart. + """ + + def test_declared_resource_names_are_all_live(self) -> None: + """Every name in ``RESOURCE_EFFECTS`` / ``RESOURCE_OPS`` still + exists in the effect registry the compiler serves.""" + assert _MOD.resource_registry_errors() == [] + + def test_an_effect_row_signal_is_derived(self, tmp_path: Path) -> None: + """A `` in the effect row is a signal. `DB.execute` is not in + ``RESOURCE_OPS``, so this program's whole signal comes from the + row — an exact-set assertion, so an implementation that credited + the call site instead would not pass.""" + d = _corpus(tmp_path, {"dbish": _DB_SRC}) + assert _MOD.resource_signals(d / "dbish.vera") == frozenset({"DB"}) + + def test_an_operation_call_signal_is_derived( + self, tmp_path: Path + ) -> None: + """The mirror image: `IO` is not a resource effect, so this + program's whole signal comes from the `IO.read_file` call.""" + d = _corpus(tmp_path, {"filish": _FILE_SRC}) + assert _MOD.resource_signals(d / "filish.vera") == frozenset( + {"IO.read_file"} + ) + + def test_a_resource_free_example_declares_no_signal( + self, tmp_path: Path + ) -> None: + """The other direction, without which a derivation that returned + every name for every program would pass the two above.""" + d = _corpus(tmp_path, {"pure": _CLEAN_SRC}) + assert _MOD.resource_signals(d / "pure.vera") == frozenset() + + def test_signals_come_from_the_declarations_not_the_comments( + self, tmp_path: Path + ) -> None: + """The derivation reads the parsed program, so prose naming `` + or `IO.read_file` is not a resource declaration. + + Not hypothetical: `examples/sqlitedb.vera`'s first line is a + comment containing ``, so a text scan would agree with the + parse there by luck and disagree on the first example whose + header describes what it deliberately does *not* do. + """ + d = _corpus(tmp_path, {"prose": _COMMENTED_SRC}) + assert _MOD.resource_signals(d / "prose.vera") == frozenset() + + def test_a_pinned_spec_whose_file_is_gone_is_not_mis_diagnosed( + self, tmp_path: Path + ) -> None: + """The derivation never opened it, so it cannot say what it + declares. Building `pinned` from every entry in `run_specs` put + this spec into `pinned - signals_by_name`, where it drew the + spurious-sentinel wording — "declares no external resource" — + for a file that does not exist (#1329 review). + """ + d = _corpus(tmp_path, {"present": _DB_SRC}) + specs = { + "present": _MOD.RunSpec(expect="created the table"), + "vanished": _MOD.RunSpec(expect="never printed"), + } + errors = _MOD.check_sentinel_coverage(d, specs) + assert not [e for e in errors if "vanished" in e] + + def test_a_module_qualified_effect_is_not_the_builtin( + self, tmp_path: Path + ) -> None: + """`Mod.DB` is another module's effect, not the registry's `DB`. + + `resource_signals` narrows on `isinstance(ref, ast.EffectRef)` + precisely to drop it, and no cell reached that decision: a mutant + dropping the narrowing, or one crediting any reference whose tail + is `DB`, passed every other case here. This is the boundary in + the direction `_COMMENTED_SRC` does not cover — that one is prose, + this one is a real declaration of a different effect (#1329 + review). + """ + d = _corpus(tmp_path, {"qualified": _QUALIFIED_DB_SRC}) + assert _MOD.resource_signals(d / "qualified.vera") == frozenset() + + def test_a_renamed_resource_effect_is_an_error( + self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch + ) -> None: + """A resource effect the registry no longer has must fail loudly. + + Silently, it would match no example — and with nothing left + requiring a sentinel the rule switches itself off. The + *registry* diagnosis is asserted, not merely that an error came + back: the coinciding-message trap, since the matched-nothing + guard also fires on this input and reads as a different fault. + """ + monkeypatch.setattr(_MOD, "RESOURCE_EFFECTS", ("Databayse",)) + d = _corpus(tmp_path, {"dbish": _DB_SRC}) + errors = _MOD.check_sentinel_coverage(d, {"dbish": _MOD.RunSpec()}) + assert len(errors) == 1 + assert "Databayse" in errors[0] + assert "could not find" in errors[0] + assert "no longer gated" not in errors[0] + + def test_a_renamed_resource_op_is_an_error( + self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch + ) -> None: + """The same for an operation: `IO` exists, `read_flie` does not.""" + monkeypatch.setattr( + _MOD, "RESOURCE_OPS", (("IO", "read_flie"),) + ) + d = _corpus(tmp_path, {"filish": _FILE_SRC}) + errors = _MOD.check_sentinel_coverage(d, {"filish": _MOD.RunSpec()}) + assert len(errors) == 1 + assert "read_flie" in errors[0] + assert "could not find" in errors[0] + assert "no longer gated" not in errors[0] + + def test_a_resource_op_under_an_unknown_effect_is_an_error( + self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch + ) -> None: + """An operation is only meaningful under an effect that exists, and + looking its name up under a missing one must not be read as the + operation being absent.""" + monkeypatch.setattr( + _MOD, "RESOURCE_OPS", (("FileIO", "read_file"),) + ) + d = _corpus(tmp_path, {"filish": _FILE_SRC}) + errors = _MOD.check_sentinel_coverage(d, {"filish": _MOD.RunSpec()}) + assert len(errors) == 1 + assert "FileIO" in errors[0] + assert "could not find" in errors[0] + # The discriminating half. BOTH branches say "could not find" and + # both interpolate `{effect}.{op}`, so the three assertions above + # are satisfied by either — including by the operation-missing + # branch, which would have raised KeyError on `live_ops[effect]` + # to get there. This pins the branch that avoids it (#1329 review). + assert "has no 'FileIO'" in errors[0] + assert "read_file" not in errors[0].split("could not find")[1] + + +class TestDerivedSentinelCoverage: + """The two-way equality: the examples that declare an external + resource are exactly the specs that carry an ``expect``. + + Both directions are errors. A resource-touching example with no + sentinel passes on its graceful arm the day its fixture vanishes, + which is the failure the sentinels exist to catch; a sentinel on an + example with no resource re-pins stdout the dedicated tests own and + goes red on a cosmetic edit. + """ + + def test_a_new_database_example_needs_a_sentinel( + self, tmp_path: Path + ) -> None: + """The property a hard-coded triple could not have: an example + under a name no table has ever heard of is required to pin a + sentinel because of what it declares.""" + d = _corpus(tmp_path, {"brand_new_db": _DB_SRC}) + errors = _MOD.check_sentinel_coverage( + d, {"brand_new_db": _MOD.RunSpec()} + ) + assert len(errors) == 1 + assert "brand_new_db" in errors[0] + assert "expect" in errors[0] + + def test_a_new_filesystem_example_needs_a_sentinel( + self, tmp_path: Path + ) -> None: + """The same through the operation half of the derivation, which + the effect row cannot reach: `` is what sixteen examples + declare, and only the `IO.read_file` call marks this one.""" + d = _corpus(tmp_path, {"brand_new_file": _FILE_SRC}) + errors = _MOD.check_sentinel_coverage( + d, {"brand_new_file": _MOD.RunSpec()} + ) + assert len(errors) == 1 + assert "brand_new_file" in errors[0] + assert "expect" in errors[0] + + def test_a_resource_touching_example_with_a_sentinel_passes( + self, tmp_path: Path + ) -> None: + """The green direction, without which a check that always + returned an error would pass the two above.""" + d = _corpus(tmp_path, {"dbish": _DB_SRC, "filish": _FILE_SRC}) + assert _MOD.check_sentinel_coverage( + d, + { + "dbish": _MOD.RunSpec(expect="created the table"), + "filish": _MOD.RunSpec(expect="Hello from Vera!"), + }, + ) == [] + + def test_a_sentinel_on_a_resource_free_example_is_an_error( + self, tmp_path: Path + ) -> None: + """The other direction of the equality. Without it the rule is + one-way and a spec can pin stdout on any example at all — which + is the duplication of the dedicated output tests that the gate's + design deliberately refuses.""" + d = _corpus(tmp_path, {"dbish": _DB_SRC, "pure": _CLEAN_SRC}) + errors = _MOD.check_sentinel_coverage( + d, + { + "dbish": _MOD.RunSpec(expect="created the table"), + "pure": _MOD.RunSpec(expect="2"), + }, + ) + assert len(errors) == 1 + assert "pure" in errors[0] + assert "dbish" not in errors[0] + + def test_an_empty_derived_set_is_an_error_not_a_skip( + self, tmp_path: Path + ) -> None: + """A derivation that matches nothing must fail, not pass. + + The corpus below is resource-free and its specs pin nothing, so + both sides of the equality are empty and the equality *holds* — + a vacuous green that would also be the verdict if the walk + broke, an effect were renamed, or the parse silently returned + nothing. The whole rule would be switched off and every gate + run would report success. + """ + d = _corpus(tmp_path, {"pure": _CLEAN_SRC, "also_pure": _CLEAN_SRC}) + errors = _MOD.check_sentinel_coverage( + d, {"pure": _MOD.RunSpec(), "also_pure": _MOD.RunSpec()} + ) + assert len(errors) == 1 + assert "no longer gated" in errors[0] + + def test_an_unparseable_example_is_an_error_not_an_empty_signal_set( + self, tmp_path: Path + ) -> None: + """A program the parse cannot read has *unknown* signals, and + unknown must not be spelled the same as none. + + Read as none, a file that stopped parsing would silently leave + the sentinel rule — and the diagnosis a reader got would be the + opposite one, that its sentinel covers no resource. + """ + d = _corpus(tmp_path, {"broken": _UNPARSEABLE_SRC, "dbish": _DB_SRC}) + errors = _MOD.check_sentinel_coverage( + d, + { + "broken": _MOD.RunSpec(), + "dbish": _MOD.RunSpec(expect="created the table"), + }, + ) + assert len(errors) == 1 + assert "broken" in errors[0] + assert "could not be parsed" in errors[0] + + def test_main_computes_the_rule_and_reports_it(self) -> None: + """A structural pin on the wiring, the technique + `test_the_runner_hands_both_streams_to_the_output_check` uses and + for the same reason: reaching `main` end to end means running all + 34 examples under the native runtime, which no unit test can + afford, so nothing else here can distinguish a `main` that + computes the sentinel errors from one that drops them on the + floor. That mutant is the most consequential of the lot — the + rule would hold in this file and gate nothing in CI — so it gets + the tripwire. + """ + import inspect + + src = inspect.getsource(_MOD.main) + assert re.search( + r"sentinel_errors\s*=\s*check_sentinel_coverage\(", src + ), src + # And the result reaches the report, rather than being computed + # and discarded: passing `[]` in its place would satisfy a + # presence check on the name alone. + assert re.search( + r"error_blocks\(\s*\[\]\s*,\s*sentinel_errors\s*,", src + ), src + + class TestBuildCommand: def test_default_spec_names_main_explicitly(self) -> None: """No spec leaves the entry point implicit — see @@ -699,6 +1074,7 @@ def test_doc_errors_are_never_filed_under_the_coverage_count( """ blocks = _MOD.error_blocks( coverage_errors=["one coverage problem"], + sentinel_errors=[], doc_errors=["one doc problem", "another doc problem"], failures=[], ) @@ -722,15 +1098,34 @@ def test_doc_errors_are_never_filed_under_the_coverage_count( assert counted == {1, 2} def test_error_blocks_are_empty_when_nothing_is_wrong(self) -> None: - assert _MOD.error_blocks([], [], []) == [] + assert _MOD.error_blocks([], [], [], []) == [] def test_runtime_failures_get_their_own_counted_block(self) -> None: - blocks = _MOD.error_blocks([], [], ["boom: exited 1"]) + blocks = _MOD.error_blocks([], [], [], ["boom: exited 1"]) assert ( _sole_index(blocks, "RUNTIME FAILURES (1)") < _sole_index(blocks, "boom: exited 1") ) + def test_sentinel_errors_get_their_own_counted_block(self) -> None: + """The derived sentinel rule reports under its own header, for the + same reason the other three do: filed under `COVERAGE ERRORS (n)` + its lines would be attributed to a count that excludes them. + + Positional, like the doc-error test above — presence plus counts + is satisfied by a report that emits every header and then every + line. + """ + blocks = _MOD.error_blocks( + ["one coverage problem"], ["one sentinel problem"], [], [], + ) + assert ( + _sole_index(blocks, "COVERAGE ERRORS (1)") + < _sole_index(blocks, "one coverage problem") + < _sole_index(blocks, "SENTINEL COVERAGE (1)") + < _sole_index(blocks, "one sentinel problem") + ) + # --------------------------------------------------------------------------- # The TESTING.md cross-check diff --git a/tests/test_grammar_alignment.py b/tests/test_grammar_alignment.py index 6478775b..41095fe7 100644 --- a/tests/test_grammar_alignment.py +++ b/tests/test_grammar_alignment.py @@ -307,3 +307,366 @@ def test_drift_reports_a_rotted_allowlist_entry() -> None: assert stale == ["program"] assert actionable == [] assert unsound == [] + + +# --------------------------------------------------------------------------- +# Terminals and production bodies (#1290) +# +# Each of these three classes was demonstrated green on a live file before the +# checks existed: a fabricated terminal in §10.2, a rule reference restored to +# a right-hand side, and a production body edited on one side only. +# --------------------------------------------------------------------------- + + +def _lark_lines() -> list[str]: + return _lark_text().splitlines() + + +def _spec_lines() -> list[str]: + return _MOD.ebnf_fence_lines((_ROOT / _MOD.SPEC).read_text(encoding="utf-8")) + + +def _messages(*problems: list[str]) -> str: + return "\n".join(line for group in problems for line in group) + + +class TestTerminalAudit: + def test_the_shipped_files_are_clean(self) -> None: + assert _MOD.terminal_audit(_lark_lines(), _spec_lines()) == [] + + def test_a_fabricated_spec_terminal_is_caught(self) -> None: + """The demonstrated blind spot: `_HEADER` needs a lowercase lead.""" + spec = [*_spec_lines(), 'BOGUS_TERMINAL: "bogus"'] + problems = _MOD.terminal_audit(_lark_lines(), spec) + assert [p for p in problems if "BOGUS_TERMINAL" in p and "never used" in p] + + def test_a_referenced_but_undeclared_terminal_is_caught(self) -> None: + """The `DOUBLE_COLON` shape: used by a production, declared nowhere.""" + lark = [ + line.replace("UPPER_IDENT", "PHANTOM_IDENT") + if line.startswith("slot_ref:") + else line + for line in _lark_lines() + ] + assert "PHANTOM_IDENT" in "\n".join(lark) + problems = _MOD.terminal_audit(lark, _spec_lines()) + assert [p for p in problems if "PHANTOM_IDENT" in p and "never declared" in p] + + def test_deleting_a_terminal_still_in_use_is_caught(self) -> None: + lark = [line for line in _lark_lines() if not line.startswith("INT_LIT:")] + problems = _MOD.terminal_audit(lark, _spec_lines()) + assert [p for p in problems if "INT_LIT" in p and "never declared" in p] + + def test_a_missing_skipped_group_is_an_error_not_a_skip(self) -> None: + """Losing the marker must fail, not silently waive every terminal.""" + spec = [ + line.replace("(skipped)", "(ignored by the lexer)") for line in _spec_lines() + ] + problems = _MOD.terminal_audit(_lark_lines(), spec) + assert [p for p in problems if "no terminal group marked" in p] + + def test_a_note_between_declarations_does_not_end_the_skipped_group(self) -> None: + """A comment after a declaration annotates it; it opens no new group.""" + assert "BLOCK_COMMENT" in _MOD.skipped_terminals(_spec_lines()) + assert "ANNOTATION_COMMENT" in _MOD.skipped_terminals(_spec_lines()) + + def test_a_blank_line_closes_the_skipped_group(self) -> None: + """A block with no heading of its own inherits nothing. + + `in_group` changed only when a comment opened a block, so a + declaration block following a blank line kept whatever the + previous block was — silently waiving terminals the marker never + named (#1329 review). + """ + # Injected directly AFTER the skipped group, which is the only + # placement that distinguishes: appended at the end of the fence + # the block would follow a group that is not the skipped one, so + # it inherits `False` and the cell passes either way. + spec: list[str] = [] + for line in _spec_lines(): + spec.append(line) + if line.startswith("ANNOTATION_COMMENT:"): + spec += ["", 'UNHEADED_TERMINAL: "unheaded"'] + assert 'UNHEADED_TERMINAL: "unheaded"' in spec, "injection point gone" + assert "ANNOTATION_COMMENT" in _MOD.skipped_terminals(spec), ( + "the skipped group itself must still be recognised" + ) + assert "UNHEADED_TERMINAL" not in _MOD.skipped_terminals(spec) + problems = _MOD.terminal_audit(_lark_lines(), spec) + assert [p for p in problems if "UNHEADED_TERMINAL" in p] + + def test_the_skipped_group_does_not_swallow_the_whole_fence(self) -> None: + skipped = _MOD.skipped_terminals(_spec_lines()) + assert "FN" not in skipped and "INT_LIT" not in skipped + + +class TestTerminalPatterns: + def test_the_shipped_files_are_clean(self) -> None: + assert _MOD.terminal_patterns(_lark_lines(), _spec_lines()) == [] + + def test_the_non_nesting_block_comment_regex_is_caught(self) -> None: + """The live drift #1290 named: §1.3 says they nest, the regex did not.""" + spec = [ + line + for line in _spec_lines() + if not line.startswith(("BLOCK_COMMENT:", "// Block comments nest")) + ] + spec.append(r"BLOCK_COMMENT: /\{-[\s\S]*?-\}/") + problems = _MOD.terminal_patterns(_lark_lines(), spec) + assert [p for p in problems if "BLOCK_COMMENT" in p] + + def test_a_lark_terminal_missing_from_the_chapter_is_caught(self) -> None: + spec = [line for line in _spec_lines() if not line.startswith("FLOAT_LIT:")] + problems = _MOD.terminal_patterns(_lark_lines(), spec) + assert [p for p in problems if "FLOAT_LIT" in p and "only in" in p] + + def test_a_pattern_that_drifted_is_caught(self) -> None: + spec = [ + "INT_LIT: /[0-9]+/" if line.startswith("INT_LIT:") else line + for line in _spec_lines() + ] + problems = _MOD.terminal_patterns(_lark_lines(), spec) + assert [p for p in problems if "INT_LIT" in p] + + @pytest.mark.parametrize( + ("body", "expected"), + [ + (r"\"([^\"\\]|\\.)*\"", r'"([^"\\]|\\.)*"'), + (r"\/\*[^*]*\*\/", r"/\*[^*]*\*/"), + (r"[^/*]", r"[^/*]"), + # An escaped backslash is copied whole, so the `\"` after it is + # still an escape of the quote and not part of a `\\"` triple. + (r"\\\"", r"\\" + '"'), + ], + ) + def test_normalise_pattern(self, body: str, expected: str) -> None: + assert _MOD.normalise_pattern(body) == expected + + def test_the_two_files_spell_string_lit_differently_and_still_agree(self) -> None: + """Non-vacuity: the normalisation is doing work, not comparing equals.""" + lark = _MOD.terminal_declarations(_lark_lines())["STRING_LIT"] + spec = _MOD.terminal_declarations(_spec_lines())["STRING_LIT"] + assert lark != spec + assert _MOD.normalise_pattern(lark) == _MOD.normalise_pattern(spec) + + +class TestBodyDrift: + def test_the_shipped_files_are_clean(self) -> None: + assert _MOD.body_drift(_lark_lines(), _spec_lines()) == [] + + def test_the_comparison_is_not_vacuous(self) -> None: + shared = set(_MOD.rule_bodies(_lark_lines())) & set( + _MOD.rule_bodies(_spec_lines()) + ) + assert len(shared) > 50 + assert {"primary_expr", "statement", "type_expr", "fn_call"} <= shared + + def test_a_restored_ambiguity_on_a_right_hand_side_is_caught(self) -> None: + """The #1290 case: `statement` regaining its assert/assume alternatives.""" + spec = [] + for line in _spec_lines(): + spec.append(line) + if line.startswith("statement:"): + spec.append(" | assert_expr SEMICOLON") + problems = _MOD.body_drift(_lark_lines(), spec) + assert [p for p in problems if p.startswith("statement:")] + + def test_an_undocumented_literal_is_caught(self) -> None: + """Typed holes: `"?"` in Lark, no spec terminal declaring it.""" + spec = [line for line in _spec_lines() if not line.startswith("HOLE:")] + problems = _MOD.body_drift(_lark_lines(), spec) + assert [p for p in problems if 'literal "?"' in p] + + def test_a_dropped_alternative_is_caught(self) -> None: + spec = [ + line + for line in _spec_lines() + if "| refinement_type" not in line and "| fn_type" not in line + ] + problems = _MOD.body_drift(_lark_lines(), spec) + assert [p for p in problems if p.startswith("type_expr:")] + + def test_a_terminal_the_chapter_alone_names_is_caught(self) -> None: + """The `effect_list` defect: an alternative adding only a terminal. + + Every rule reference stays identical, so the rule half of the + comparison sees nothing — this cell is the only thing that dies when + the terminal half is deleted. + """ + spec = [] + for line in _spec_lines(): + spec.append(line) + if line.startswith("effect_list:"): + spec.append(" | UPPER_IDENT // effect variable") + problems = _MOD.body_drift(_lark_lines(), spec) + assert [ + p + for p in problems + if p.startswith("effect_list:") and "UPPER_IDENT" in p and _MOD.SPEC in p + ] + + def test_a_terminal_only_lark_names_is_caught(self) -> None: + spec = [ + line.replace(" SEMICOLON", "") + if line.lstrip().startswith("| expr SEMICOLON") + else line + for line in _spec_lines() + ] + assert "| expr SEMICOLON" not in "\n".join(spec) + problems = _MOD.body_drift(_lark_lines(), spec) + assert [ + p + for p in problems + if p.startswith("statement:") and "SEMICOLON" in p and _MOD.LARK in p + ] + + def test_a_rule_referring_to_itself_is_not_drift(self) -> None: + """Lark spells repetition with left recursion, the chapter with `*`. + + Asserted at the symbol level. Re-asserting that `body_drift` + reports nothing only repeats the clean-file cell above and would + stay green if the exclusion were dropped and the chapter grew a + matching self-reference (#1329 review). + """ + lark_bodies = _MOD.rule_bodies(_lark_lines()) + spec_bodies = _MOD.rule_bodies(_spec_lines()) + assert "add_expr" in "".join(lark_bodies["add_expr"]), "not left-recursive" + + rules, _terminals, _inlined = _MOD._spec_symbols( + "add_expr", spec_bodies, set(spec_bodies) + ) + assert "add_expr" not in rules + lark_rules, _t, _u = _MOD._lark_symbols( + "add_expr", lark_bodies, set(lark_bodies), {} + ) + assert "add_expr" not in lark_rules + assert lark_rules, "the extraction returned nothing at all" + + def test_a_waived_production_is_folded_at_the_rule_the_waiver_names(self) -> None: + """`fn_call` inlines what the chapter factors into `module_call`.""" + rules, terminals, inlined = _MOD._spec_symbols( + "fn_call", _MOD.rule_bodies(_spec_lines()), set(_MOD.rule_bodies(_spec_lines())) + ) + assert "module_path" in rules + assert {"DOT", "DOUBLE_COLON"} <= terminals + assert "module_call" not in rules and "qualified_call" not in rules + + def test_an_aliased_alternative_is_not_read_as_a_rule_reference(self) -> None: + """`func_call` is a real alias — `vera/grammar.lark` spells the + first `fn_call` alternative `-> func_call` — so this assertion is + falsifiable, and the mutation that stops `rule_bodies` stripping + aliases kills it. The positive control below is what stops an + empty body from satisfying it. + """ + bodies = _MOD.rule_bodies(_lark_lines()) + aliases = {alias for rule, alias in _MOD.extract_lark_aliases(_lark_text()) + if rule == "fn_call"} + assert "func_call" in aliases, "the alias this cell rests on is gone" + + body = "".join(bodies["fn_call"]) + assert "LOWER_IDENT" in body, "positive control: the body was read" + for alias in aliases: + assert alias not in body + + +class TestCommentStripping: + @pytest.mark.parametrize( + "line", + [ + # Lark's spelling, which escapes the class slash. + r"%ignore /\/\*[^*]*\*+([^\/*][^*]*\*+)*\//", + # The chapter's spelling, which does not — the case that was + # truncated inside the character class (#1329 review). + r"ANNOTATION_COMMENT: /\/\*[^*]*\*+([^/*][^*]*\*+)*\//", + ], + ) + def test_a_regex_body_ending_in_a_slash_is_not_truncated( + self, line: str + ) -> None: + """`line.split("//")[0]` cut the annotation-comment terminal in half.""" + assert _MOD.strip_comment(line) == line + + def test_a_comment_after_a_regex_is_still_removed(self) -> None: + assert _MOD.strip_comment(r"INT_LIT: /0|[1-9]/ // numbers") == ( + r"INT_LIT: /0|[1-9]/ " + ) + + def test_a_double_slash_inside_a_literal_is_not_a_comment(self) -> None: + assert _MOD.strip_comment('sep: "//" name') == 'sep: "//" name' + + def test_a_whole_line_comment_is_still_removed(self) -> None: + assert _MOD.strip_comment("// assert_stmt: gone").strip() == "" + + +class TestCharacterClasses: + """A `/` inside a regex character class is not the delimiter (#1329). + + `strip_comment` scanned a `/…/` body for the next unescaped `/`, and + the chapter spells the annotation-comment terminal `[^/*]` where the + Lark grammar spells it `[^\\/*]`. The scan therefore ended inside + the class, truncating the declaration — and a truncated body is not + a bare regex, so `terminal_patterns` skipped the terminal entirely. + The gate was green on that terminal by never looking at it. + """ + + def test_the_specs_annotation_comment_line_survives_the_scan(self) -> None: + line = next( + raw + for raw in _spec_lines() + if raw.startswith("ANNOTATION_COMMENT:") + ) + assert "[^/*]" in line, "the chapter no longer spells the class bare" + assert _MOD.strip_comment(line) == line + + def test_the_annotation_comment_pattern_is_actually_compared(self) -> None: + """Non-vacuity: the terminal must reach the pattern check at all. + + A truncated body fails `_BARE_REGEX`, and a terminal that is not + a bare regex is skipped by design — so this is the assertion that + separates "compared and equal" from "never compared". + """ + body = _MOD.terminal_declarations(_spec_lines())["ANNOTATION_COMMENT"] + assert _MOD._BARE_REGEX.match(body), f"not a bare regex: {body!r}" + + def test_the_two_files_spell_the_class_differently_and_still_agree(self) -> None: + spec = _MOD.terminal_declarations(_spec_lines())["ANNOTATION_COMMENT"] + lark = next( + body for body in _MOD.ignore_patterns(_lark_lines()) if "\\*" in body + ) + assert spec != lark, "the normalisation would be doing no work" + assert _MOD.normalise_pattern(spec) == _MOD.normalise_pattern(lark) + + def test_a_drifted_annotation_comment_is_now_caught(self) -> None: + """The gate must fail on this terminal, not skip it. + + Before the character-class fix this mutation left the gate green: + the body was truncated, so no pattern was compared at all. + """ + # The drift keeps the bare `[^/*]` class the chapter really uses, + # so this cell exercises the truncation rather than sidestepping + # it: with an escaped class it would be caught either way. + spec = [ + r"ANNOTATION_COMMENT: /\/\*[^/*]XX[^*]*\*+\//" + if line.startswith("ANNOTATION_COMMENT:") + else line + for line in _spec_lines() + ] + problems = _MOD.terminal_patterns(_lark_lines(), spec) + assert [p for p in problems if "ANNOTATION_COMMENT" in p] + + @pytest.mark.parametrize( + "line", + [ + r"T: /[^/*]/", + r"T: /[/]/", + r"T: /[abc/def]x/", + r"T: /[^]/]/", + ], + ) + def test_a_slash_inside_a_character_class_is_not_the_delimiter( + self, line: str + ) -> None: + assert _MOD.strip_comment(line) == line + + def test_a_comment_after_a_class_bearing_regex_is_still_removed(self) -> None: + assert _MOD.strip_comment(r"T: /[^/*]/ // note") == r"T: /[^/*]/ " diff --git a/tests/test_release.py b/tests/test_release.py index 0981dc41..451d2a2d 100644 --- a/tests/test_release.py +++ b/tests/test_release.py @@ -4,6 +4,7 @@ import importlib.util import os +import re from pathlib import Path import subprocess import sys @@ -140,6 +141,151 @@ def test_section_requires_a_bullet(self, body: str) -> None: with pytest.raises(release.ReleaseError, match="at least one bullet"): release.changelog_notes(f"## [0.1.5]{body}", "0.1.5") + def test_section_carries_the_heading_date(self) -> None: + section = release.changelog_section("## [0.1.5] - 2026-07-15\n\n- One.\n", "0.1.5") + assert (section.version, section.date, section.notes) == ( + "0.1.5", + "2026-07-15", + "- One.", + ) + + def test_section_without_a_date_reports_none(self) -> None: + assert release.changelog_section("## [0.1.5]\n\n- One.\n", "0.1.5").date is None + + +def _section(bullets: str, *, version: str = "0.1.5") -> Any: + return release.changelog_section( + f"## [{version}] - 2026-07-15\n\n{bullets}\n", version + ) + + +class TestReleaseBody: + """#1288 — the GitHub Release body must always fit the 125,000 limit. + + The v0.1.10 failure landed *after* PyPI had accepted the immutable + archives and after the tag was cut, so the notes builder is required to + be total: it either passes the section through or condenses it, and the + result never exceeds the limit. + """ + + def test_a_section_within_budget_passes_through_unchanged(self) -> None: + section = _section("### Fixed\n\n- **One.** Detail.\n- **Two.** Detail.") + assert release.release_body(section, repo="aallan/vera") == section.notes + + def test_an_oversized_section_is_condensed_to_fit(self) -> None: + filler = "x" * 4000 + bullets = "### Fixed\n\n" + "\n".join( + f"- **Lead-in {index}.** {filler}" for index in range(50) + ) + section = _section(bullets) + assert len(section.notes) > release.GITHUB_RELEASE_BODY_LIMIT + + body = release.release_body(section, repo="aallan/vera") + assert len(body) <= release.GITHUB_RELEASE_BODY_LIMIT + assert body != section.notes + assert "### Fixed" in body + assert "- Lead-in 0." in body + assert "- Lead-in 49." in body + assert filler not in body + assert ( + "https://github.com/aallan/vera/blob/v0.1.5/CHANGELOG.md#015---2026-07-15" + in body + ) + + def test_the_condensed_body_states_the_measured_length_and_the_limit(self) -> None: + section = _section( + "### Fixed\n\n" + "\n".join(f"- **Lead {n}.** {'y' * 4000}" for n in range(50)) + ) + body = release.release_body(section, repo="aallan/vera") + assert f"{len(section.notes):,} characters" in body + assert f"{release.GITHUB_RELEASE_BODY_LIMIT:,}-character" in body + + def test_the_index_reproduces_the_v0110_recovery_shape(self) -> None: + """The lead-in carries the bullet's LAST issue/PR link, wrapped. + + Pinned because the v0.1.10 manual recovery attributed a bullet whose + only reference sat mid-prose (``(PR [#1282](...) review)``), not + immediately after the bold run. + """ + section = _section( + "### Changed\n\n" + "- **Lead one.** Body citing " + "([#1260](https://github.com/aallan/vera/issues/1260)) and then " + "(PR [#1282](https://github.com/aallan/vera/pull/1282) review).\n" + "- **Lead two.** No reference at all.\n" + ) + assert release.condense_notes(section, repo="aallan/vera").splitlines()[-3:] == [ + "### Changed", + "- Lead one. ([#1282](https://github.com/aallan/vera/pull/1282))", + "- Lead two.", + ] + + def test_a_bullet_without_a_bold_lead_in_still_reaches_the_index(self) -> None: + section = _section("### Fixed\n\n- A plain bullet with no bold lead-in.") + assert ( + "- A plain bullet with no bold lead-in." + in release.condense_notes(section, repo="aallan/vera").splitlines() + ) + + def test_condensing_a_bullet_free_section_is_an_error(self) -> None: + """An index that matches nothing is a failure, never a silent empty body.""" + section = release.ChangelogSection("0.1.5", "2026-07-15", "Prose only.") + with pytest.raises(release.ReleaseError, match="no bullets"): + release.condense_notes(section, repo="aallan/vera") + + def test_an_index_that_still_overflows_is_truncated_and_says_so(self) -> None: + bullets = "### Fixed\n\n" + "\n".join( + f"- **{'lead ' * 400}{index}.** detail" for index in range(400) + ) + section = _section(bullets) + assert ( + len(release.condense_notes(section, repo="aallan/vera")) + > release.GITHUB_RELEASE_BODY_LIMIT + ) + + body = release.release_body(section, repo="aallan/vera") + assert len(body) <= release.GITHUB_RELEASE_BODY_LIMIT + assert "truncated" in body + + @pytest.mark.parametrize( + ("version", "date", "expected"), + [ + ("0.1.10", "2026-08-12", "#0110---2026-08-12"), + ("0.1.5", None, "#015"), + ], + ) + def test_changelog_anchor( + self, version: str, date: str | None, expected: str + ) -> None: + assert release.changelog_anchor(version, date) == expected + + def test_every_shipped_changelog_section_yields_a_body_that_fits(self) -> None: + """The real artefact, not a fixture — and non-vacuously. + + v0.1.10's section is the one that 422'd, so at least one section here + must exercise the condensing path; a suite where none did would pass + with the limit check deleted. + """ + root = Path(__file__).parent.parent + text = (root / "CHANGELOG.md").read_text(encoding="utf-8") + # The canonical heading grammar only; the oldest sections carry a + # trailing PR reference the release extractor has never accepted. + versions = re.findall( + r"^## \[(\d+\.\d+\.\d+)\](?: - \d{4}-\d\d-\d\d)?[ \t]*$", + text, + re.MULTILINE, + ) + assert len(versions) > 100, "CHANGELOG version headings no longer found" + + condensed = [] + for version in versions: + section = release.changelog_section(text, version) + body = release.release_body(section, repo="aallan/vera") + assert len(body) <= release.GITHUB_RELEASE_BODY_LIMIT, version + if body != section.notes: + condensed.append(version) + assert "0.1.10" in condensed + class TestPlanning: def test_recovery_tracks_first_parent_bump_and_package_changes( @@ -506,7 +652,11 @@ def plan(mode: str, **kwargs: Any) -> Any: def test_main_notes(self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: monkeypatch.setattr( - release, "notes_for_version", lambda version: f"- Notes for {version}." + release, + "section_for_version", + lambda version: release.ChangelogSection( + version, "2026-07-15", f"- Notes for {version}." + ), ) output = tmp_path / "release" / "notes.md" assert ( @@ -514,6 +664,47 @@ def test_main_notes(self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> No ) assert output.read_text(encoding="utf-8") == "- Notes for 0.1.5.\n" + def test_main_notes_condenses_an_oversized_section( + self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch + ) -> None: + notes = "### Fixed\n\n" + "\n".join( + f"- **Lead {index}.** {'z' * 4000}" for index in range(50) + ) + monkeypatch.setattr( + release, + "section_for_version", + lambda version: release.ChangelogSection(version, "2026-07-15", notes), + ) + output = tmp_path / "release" / "notes.md" + assert ( + release.main( + [ + "notes", + "--version", + "0.1.5", + "--output", + str(output), + "--repo", + "aallan/vera", + ] + ) + == 0 + ) + written = output.read_text(encoding="utf-8") + assert len(written) <= release.GITHUB_RELEASE_BODY_LIMIT + assert "- Lead 49." in written + assert "z" * 4000 not in written + + def test_the_release_workflow_passes_the_repository_to_the_notes_step(self) -> None: + """The fix is only real if ``release.yml`` consumes the fitted builder.""" + workflow = ( + Path(__file__).parent.parent / ".github" / "workflows" / "release.yml" + ).read_text(encoding="utf-8") + step = "python scripts/release.py notes" + assert step in workflow, "release.yml no longer invokes the notes builder" + tail = workflow[workflow.index(step) : workflow.index(step) + 400] + assert "--repo" in tail + def test_main_manifest(self, tmp_path: Path) -> None: dist = _dist(tmp_path) output = tmp_path / "release" / "SHA256SUMS" diff --git a/vera/README.md b/vera/README.md index 98bdd1c2..33c79773 100644 --- a/vera/README.md +++ b/vera/README.md @@ -753,7 +753,7 @@ The `ERROR_CODES` dict in `errors.py` maps every code to a short description (16 ## Test Suite -Testing spans a **pytest suite** of 11,786 tests across 174 files — compiler-internals unit tests plus a **conformance suite** (244 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (42 end-to-end demos). The conformance suite is the definitive specification artifact — most programs target a single feature, though some (slot references, match, contracts) span several, and each serves as a minimal working example. +Testing spans a **pytest suite** of 11,940 tests across 175 files — compiler-internals unit tests plus a **conformance suite** (244 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (42 end-to-end demos). The conformance suite is the definitive specification artifact — most programs target a single feature, though some (slot references, match, contracts) span several, and each serves as a minimal working example. See **[TESTING.md](../TESTING.md)** for the comprehensive testing reference -- test file table, conformance suite details, compiler code coverage, language feature coverage, helper conventions, validation scripts, CI pipeline, and guidelines for adding tests.