From cdbe94c957dcc1b51effd5ea5d9ab9d4314eb6c3 Mon Sep 17 00:00:00 2001 From: Alasdair Allan Date: Mon, 3 Aug 2026 10:32:20 +0100 Subject: [PATCH 1/2] Gate the facts docs/index.html and docs/index.md both state MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/index.md is not derived from the landing page: it is written out by build_index_md() in scripts/build_site.py, which holds the HTML's substance as a hand-maintained f-string. check_site_assets.py verified it by calling that generator and comparing the result against the committed file, putting the generator on both sides of the comparison — so a generator that missed an edit to the hand-designed HTML produced a committed asset stale in exactly the same way, and the gate passed. A v0.0.7-era benchmark section survived every intervening release that way. check_fact_coherence() extracts the load-bearing facts from each file independently and fails when they diverge, naming the fact, both values and both paths. A fact that cannot be located is itself a failure rather than a silent skip, so a reworded sentence cannot switch its own check off. Co-Authored-By: Claude --- CHANGELOG.md | 6 + CLAUDE.md | 2 +- CONTRIBUTING.md | 2 + KNOWN_ISSUES.md | 1 - README.md | 2 +- ROADMAP.md | 2 +- TESTING.md | 6 +- scripts/check_site_assets.py | 352 ++++++++++++++++++++++++++++++++++- tests/test_build_site.py | 306 ++++++++++++++++++++++++++++++ 9 files changed, 664 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0ca5ead6..b525b892 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). ## [Unreleased] +### Fixed + +- **`scripts/check_site_assets.py` gates the facts `docs/index.html` and `docs/index.md` both state** ([#1154](https://github.com/aallan/vera/issues/1154)). The Markdown companion agents fetch via `rel="alternate"` and `llms.txt` is emitted by `build_index_md()` in `scripts/build_site.py`, which holds the landing page's substance as a hand-maintained f-string. The staleness check called that generator and compared the result against the committed file — the generator on both sides of the comparison — so a generator that missed an edit to the hand-designed HTML produced a committed asset stale in exactly the same way, and the gate passed. A v0.0.7-era benchmark section survived every intervening release that way. + + `check_fact_coherence()` now extracts the load-bearing facts from each file independently and fails when they diverge: the VeraBench version and the Vera release it was measured against, the landing-page version badge, the problem/tier/model/provider counts, the headline perfect-Vera count, the nine-row results table (model name, tier and all three figures per row, plus each file's row count against its own stated model count), and the three editor names. An error names the fact, both values and both paths. A fact that cannot be located is itself a failure rather than a silent skip, so a reworded sentence cannot switch its own check off. + ### Documentation - **The VeraBench section carries the v0.0.18 sweep** ([#1169](https://github.com/aallan/vera/pull/1169)), the first in which all 60 problems are graded — v0.0.17 took the gradeable set from 36 to 46 and v0.0.18 closed it. One problem is now worth 1.7 percentage points rather than 2.8. Six of the nine models solve every Vera problem, and Vera is highest or level with it for six of the nine. Measured against [Vera v0.1.8](https://github.com/aallan/vera/releases/tag/v0.1.8). The section also gains the reading the wider gradeable set supports: Python is dynamically typed and TypeScript is not, Vera sits with TypeScript and goes further, and sorting the three by how much they constrain the model rather than by how much of them it has read puts the two constraining languages ahead — TypeScript with training data behind it, Vera without. diff --git a/CLAUDE.md b/CLAUDE.md index 574ffd05..0bb182d8 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -73,7 +73,7 @@ python scripts/check_doc_builtin_shadowing.py # Verify no doc example redefines python scripts/check_diagnostic_fields.py # Verify every diagnostic carries rationale + spec_ref (+ fix for errors; warnings exempt) or a # diag-fields-exempt reason — waives missing/unresolvable fields only, never a factually wrong spec_ref/error_code (#682) python scripts/check_explicit_encoding.py # Verify every text-mode open()/read_text()/write_text() passes explicit encoding='utf-8' (#645) python scripts/build_site.py # Regenerate AI-readable site assets (llms.txt, etc.) -python scripts/check_site_assets.py # Verify site assets are up-to-date +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_licenses.py # Verify all package licenses are MIT-compatible diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index f839b5ef..87a7e816 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -112,6 +112,8 @@ The **commit-stage** hooks (30, each gated to relevant files) include: If you modify documentation sources (SKILL.md, AGENTS.md, FAQ.md, `vera/errors.py`, `vera/grammar.lark`, or `docs/index.html`), the `site-assets` hook will regenerate `docs/` files via `scripts/build_site.py`. The CI also runs `scripts/check_site_assets.py` to verify freshness. +`docs/index.md` is a special case: it is not derived from `docs/index.html` but written out by `build_index_md()` in `scripts/build_site.py`, so an edit to the landing page's substance has to be made in both places. `check_site_assets.py` compares the load-bearing facts across the pair — benchmark version strings, problem and model counts, the results table, the editor names — and fails when they diverge or when one of them can no longer be located. + ### Pre-push hook: CHANGELOG enforcement A separate `pre-push` hook runs once before each `git push` (not per-commit — which would be too noisy on feature branches). It verifies that any PR touching a non-exempt top-level path adds a new entry to `CHANGELOG.md`. The same check also runs in CI, so pushes without the local hook installed are still caught before merge. diff --git a/KNOWN_ISSUES.md b/KNOWN_ISSUES.md index 98851315..d54c881e 100644 --- a/KNOWN_ISSUES.md +++ b/KNOWN_ISSUES.md @@ -11,7 +11,6 @@ Defects in shipped compiler, runtime, or tooling behaviour — this table matche | Cross-module type-alias namespaces merge flatly in codegen (`setdefault` on bare name, first module wins), so two imported modules defining the same alias name with different targets corrupt one module's function signatures — check-clean (the checker is module-correct), then an invalid WASM module or wrong values at run time. The fix preserves per-module alias maps keyed by module path; the workaround is unique alias names across a program's module graph. | [#1111](https://github.com/aallan/vera/issues/1111) | | A codegen `[E602]` skip drops the function from the emitted module but leaves its callers' `call`/`return_call` in place, so a check- and verify-clean program whose skipped construct sits in a *called helper* fails at `run`/`compile` with a raw wasmtime `unknown func` error instead of a source-located diagnostic. Loud, not silent (never a wrong answer); the fix propagates the skip to callers or diagnoses the dropped callee at the call site. | [#1100](https://github.com/aallan/vera/issues/1100) | | `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) | -| `docs/index.md` — the Markdown companion agents fetch via `rel="alternate"` instead of the landing page — is generated by `build_index_md()` in `scripts/build_site.py`, which mirrors `docs/index.html`'s substance as hand-maintained prose rather than deriving it. An edit to the HTML does not propagate, and `check_site_assets.py` cannot detect the drift: it regenerates from that same function and compares against the committed file, so a stale generator and a stale asset agree and the gate passes. Silent and unbounded — a v0.0.7-era benchmark section survived every intervening release until it was caught by hand. Fix options: derive the Markdown from the HTML, gate the load-bearing facts across the pair, or extract the shared substance to a data file both read. | [#1154](https://github.com/aallan/vera/issues/1154) | | A user `effect { … }` block overriding a built-in host effect (`IO` / `DB` / `Http` / …) — which spec §9.5.1 explicitly permits "for backward compatibility" — with an operation signature that diverges from the built-in passes **both `vera check` and `vera compile`** (exit 0, no diagnostic), yet emits structurally invalid WASM that traps at `run`. The override is checker-level only (§9.5.1 makes only the declared ops available); codegen ignores it and routes a qualified `Effect.op(...)` to the fixed-arity host import, so a divergent signature mismatches. Loud (a wasmtime validator error, never a wrong answer), reachable by an ordinary typo in the (optional-but-idiomatic) declaration; pre-existing and general, orthogonal to the #309 SQL-provenance gate. Fix: either validate an override's op signatures against the host ABI (reject divergence, keeping §9.5.1), or amend §9.5.1 to forbid the block outright (an E151-analogue, per design goal 3 — also closing the #309 shadow surface). | [#1149](https://github.com/aallan/vera/issues/1149) | ## Limitations diff --git a/README.md b/README.md index fc854ac1..353989a9 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.8: 2,000+ commits, 204 releases, 8,568 tests, 95% code coverage, 169 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.8: 2,000+ commits, 204 releases, 8,587 tests, 95% code coverage, 169 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/ROADMAP.md b/ROADMAP.md index 2c0f9c18..7af9a70d 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 -8,568 tests, 169 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. +8,587 tests, 169 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 4ab1933d..ac5ddea1 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** | 8,568 across 131 files (~106,000 lines of test code; 8,452 passed + 26 stress, 90 skipped) | +| **Tests** | 8,587 across 131 files (~106,000 lines of test code; 8,471 passed + 26 stress, 90 skipped) | | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) | | **Conformance programs** | 169 programs across 9 spec chapters, validating every language feature | | **Example programs** | 42, all validated through `vera check` + `vera verify` | @@ -174,7 +174,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_html.py` | 4 | 167 | HTML landing page code samples: parse, check, verify (vera:skip-annotation aware, #538) | | `test_float64_fp.py` | 10 | 260 | #797 — `@Float64` contracts via Z3's IEEE-754 FloatingPoint sort: unsound relational / reflexive contracts (rounding at 2^53, `NaN`, `Inf`) flip from proved to violated/Tier-3, NaN-guarded contracts still verify at Tier 1, `==`/`!=` use IEEE `fpEQ`/`fpNEQ` (incl. `+0.0 == -0.0`), `%` matches codegen truncated remainder (not `fp.rem`; NaN-by-zero + large-magnitude edges), and `float_is_nan` / `float_is_infinite` / `nan()` / `infinity()` translate to FP predicates / constants. Also guards mixed `@Float64`/`@Int` ordering as a clean E142 (not a Z3 crash) | | `test_float64_builtins_807.py` | 81 | 491 | #807 — Tier-1 modeling of the modelable `@Float64` builtins. `float_clamp` modeled unconditionally as faithful WASM `f64.min(f64.max(v,lo),hi)` (the NaN-propagation soundness guard distinguishes it from a naive `z3.fpMin`/`fpMax`); `int_to_float` / `float_to_int` concrete-gated (symbolic args defer to Tier 3 — Z3's symbolic FP↔Real reasoning returns spurious counterexamples); `float_to_int` domain obligation (E529) for concrete NaN/Inf/out-of-range args. Verify-vs-run differentials confirm each model agrees with wasmtime bit-for-bit (±0, ±inf, NaN, ties, lo>hi, the 2^53 rounding boundary, i64 max, and the trap cases) | -| `test_build_site.py` | 25 | 341 | 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) | +| `test_build_site.py` | 44 | 647 | 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), 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), and the #1154 `check_fact_coherence` gate on `docs/index.html` ↔ `docs/index.md` (committed pair clean, then tmp_path-copy mutations for each drift class: a bumped percentage, version string, problem/model count, a removed/renamed table row, a changed tier, a dropped editor — plus extraction failure as gate failure for a restructured table, a deleted caveat, a missing editor claim, a missing file, and one file stating a fact two ways) | | `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. | @@ -664,7 +664,7 @@ Twenty-two scripts in `scripts/` validate cross-cutting concerns beyond unit tes | `check_pypi_readme_examples.py` | All Vera code blocks in PYPI_README.md parse, check, and verify | | `check_examples_doc.py` | All Vera code blocks in EXAMPLES.md parse correctly | | `check_html_examples.py` | All Vera code blocks in docs/index.html pass parse + check + verify | -| `check_site_assets.py` | Generated site assets under `docs/` are up-to-date | +| `check_site_assets.py` | Generated site assets under `docs/` are up-to-date, and `docs/index.html` and `docs/index.md` state coherent facts (benchmark version, counts, results table, editor names) | | `check_version_sync.py` | `pyproject.toml`, `vera/__init__.py`, and the docs badge carry the same version | | `check_doc_counts.py` | Counts cited in the docs match the live codebase, KNOWN_ISSUES refactoring counts within ±10%, HISTORY version-row format | | `check_limitations_sync.py` | Limitation tables consistent across KNOWN_ISSUES.md, vera/README.md, spec chapters, SKILL.md, and LSP_SERVER.md | diff --git a/scripts/check_site_assets.py b/scripts/check_site_assets.py index 61ccbf09..a953c3c4 100644 --- a/scripts/check_site_assets.py +++ b/scripts/check_site_assets.py @@ -1,21 +1,39 @@ #!/usr/bin/env python3 """Verify that docs/ site assets are up-to-date with source documentation. -Regenerates all site assets in memory and compares against the committed -files. Exits non-zero if any file is stale, printing which ones need -rebuilding. +Two independent checks, because they fail differently: + +* **Staleness** — regenerate every site asset in memory and compare against + the committed file. Exits non-zero if any is stale, printing which ones + need rebuilding. +* **Fact coherence** — compare the load-bearing facts stated in + ``docs/index.html`` against the ones stated in ``docs/index.md`` + (:func:`check_fact_coherence`). The staleness check cannot see this + class of drift: ``docs/index.md`` is emitted by ``build_index_md()``, + which holds the landing page's substance as a hand-maintained f-string, + so the staleness comparison puts that generator on *both* sides. When + the generator misses an edit to the hand-designed HTML, the committed + Markdown is stale in exactly the same way and the comparison is + satisfied (#1154). Usage: python scripts/check_site_assets.py Fix stale assets by running: python scripts/build_site.py + +Fix a coherence failure by hand, in ``build_index_md()`` — the Markdown +companion is what agents fetch via ``rel="alternate"`` and ``llms.txt``, +so a fact that has moved on in the HTML has to move on there too. """ from __future__ import annotations +import re import sys +from html import unescape from pathlib import Path +from typing import NamedTuple # Add project root to path so we can import the build script ROOT = Path(__file__).resolve().parent.parent @@ -50,6 +68,310 @@ def sitemap_stale_reason(sitemap_path: Path, expected: str) -> str | None: return None +# --------------------------------------------------------------------------- +# Landing-page fact coherence: docs/index.html vs docs/index.md +# --------------------------------------------------------------------------- +# +# Every fact below is stated in *both* files. The two are written in +# deliberately different registers — the HTML is a designed page, the +# Markdown is a plain companion — so only facts are compared, never +# wording: version strings, counts, the benchmark table, the editor names. +# +# A pattern that matches *nothing* is an error in its own right, the same +# rule `scripts/check_doc_counts.py` applies to the landing page's own +# counts. Silently skipping a fact whose sentence was reworded would +# reinstate exactly the blind spot this check exists to close. + + +class _Fact(NamedTuple): + """A single fact, and how to find it in each file. + + ``md_pattern`` defaults to ``html_pattern``: most facts read the same + in both files, and the ones that do not (the version badge) say so. + Each pattern must have exactly one capturing group — the value. + """ + + label: str + html_pattern: str + md_pattern: str | None = None + + +_PROSE_FACTS: tuple[_Fact, ...] = ( + _Fact("VeraBench version", r"VeraBench v(\d+\.\d+\.\d+)"), + _Fact("tested Vera version", r"\bVera v(\d+\.\d+\.\d+)\b"), + # The badge is the one fact written differently in each file. This is + # not a second copy of `check_version_sync.py`'s gate: that one pins + # the HTML badge to pyproject.toml and never reads docs/index.md. + _Fact( + "landing-page version badge", + r'v(\d+\.\d+\.\d+)', + r"\*\*Current version:\*\* \[(\d+\.\d+\.\d+)\]", + ), + _Fact("benchmark problem count", r"\b(\d+)-problem benchmark\b"), + _Fact("benchmark difficulty tiers", r"benchmark across (\d+) difficulty tiers"), + _Fact("benchmark model count", r"\b(\w+) models, \w+ providers\b"), + _Fact("benchmark provider count", r"\b\w+ models, (\w+) providers\b"), + _Fact("models writing perfect Vera", r"\b(\w+) of \w+ frontier models\b"), +) + +# Editor names, and every spelling each file uses for them. Compared as a +# set: the page names the editors it supports, and the Markdown companion +# has to name the same ones. +_EDITORS: tuple[tuple[str, str], ...] = ( + ("VS Code", r"Visual Studio Code|VS Code"), + ("Vim", r"\bVim\b"), + ("TextMate", r"TextMate"), +) + +_NUMBER_WORDS = { + "one": "1", "two": "2", "three": "3", "four": "4", "five": "5", + "six": "6", "seven": "7", "eight": "8", "nine": "9", "ten": "10", + "eleven": "11", "twelve": "12", "thirteen": "13", "fourteen": "14", + "fifteen": "15", "sixteen": "16", "seventeen": "17", "eighteen": "18", + "nineteen": "19", "twenty": "20", +} + +_HTML_BENCH_TABLE = re.compile(r'(.*?)
', re.DOTALL) +_HTML_BENCH_ROW = re.compile( + r'(?P.*?)\s*(?P[^<]*)' + r"\s*" + r"\s*]*>(?P[^<]*)" + r"\s*]*>(?P[^<]*)" + r"\s*]*>(?P[^<]*)", + re.DOTALL, +) +_MD_BENCH_HEADER = re.compile( + r"^\|\s*Model\s*\|\s*Tier\s*\|\s*Vera\s*\|\s*Python\s*\|\s*TypeScript\s*\|\s*$" +) +_COLUMNS = ("tier", "Vera", "Python", "TypeScript") + + +def _normalize(raw: str) -> str: + """Collapse whitespace and fold a number word onto its digits. + + The two files are allowed to differ in register, so "Nine models" and + "9 models" are the same fact. Percentages and version strings pass + through untouched, and compare as strings. + """ + value = " ".join(raw.split()) + return _NUMBER_WORDS.get(value.lower(), value) + + +def _text_of_html(raw: str) -> str: + """Strip presentational markup from a table cell and normalize it.""" + return _normalize(unescape(re.sub(r"<[^>]+>", "", raw))) + + +def _text_of_md(raw: str) -> str: + """Strip Markdown emphasis from a table cell and normalize it. + + ``**100%**`` and ``_97%_`` carry the same win/loss marking the HTML + puts in a CSS class, so the emphasis is presentation, not fact. + """ + return _normalize(re.sub(r"^[*_]+|[*_]+$", "", raw.strip())) + + +def _bench_rows_html(text: str, path: Path) -> tuple[list[tuple[str, ...]], list[str]]: + """Parse the HTML benchmark table into ``(model, tier, …figures)`` rows.""" + table = _HTML_BENCH_TABLE.search(text) + if table is None: + return [], [ + f'benchmark table: no `` found in' + f" {path} — the table moved or was restructured, so it is no" + f" longer gated" + ] + rows = [ + ( + _text_of_html(m.group("model")), + _text_of_html(m.group("tier")), + _text_of_html(m.group("vera")), + _text_of_html(m.group("python")), + _text_of_html(m.group("typescript")), + ) + for m in _HTML_BENCH_ROW.finditer(table.group(1)) + ] + if not rows: + return [], [ + f"benchmark table: found in {path} but no rows parsed — the row" + f" markup changed, so the figures are no longer gated" + ] + return rows, [] + + +def _bench_rows_md(text: str, path: Path) -> tuple[list[tuple[str, ...]], list[str]]: + """Parse the Markdown benchmark table into the same row shape.""" + lines = text.splitlines() + start = next( + (i for i, line in enumerate(lines) if _MD_BENCH_HEADER.match(line)), None + ) + if start is None: + return [], [ + f"benchmark table: no `| Model | Tier | Vera | Python |" + f" TypeScript |` table found in {path} — the table moved or was" + f" restructured, so it is no longer gated" + ] + rows: list[tuple[str, ...]] = [] + errors: list[str] = [] + for line in lines[start + 1 :]: + if not line.startswith("|"): + break + cells = [c.strip() for c in line.strip().strip("|").split("|")] + if all(c and set(c) <= {"-", ":"} for c in cells): + continue # the |---|---| separator row + if len(cells) != len(_COLUMNS) + 1: + errors.append( + f"benchmark table: {path} row {line.strip()!r} has" + f" {len(cells)} cells, expected {len(_COLUMNS) + 1}" + ) + continue + rows.append(tuple(_text_of_md(c) for c in cells)) + if not rows and not errors: + errors.append( + f"benchmark table: header found in {path} but no rows follow it" + ) + return rows, errors + + +def _index_rows( + rows: list[tuple[str, ...]], path: Path +) -> tuple[dict[str, tuple[str, ...]], list[str]]: + """Key rows by model name, reporting any model listed twice.""" + indexed: dict[str, tuple[str, ...]] = {} + errors: list[str] = [] + for row in rows: + if row[0] in indexed: + errors.append(f"benchmark table: {path} lists model {row[0]!r} twice") + continue + indexed[row[0]] = row[1:] + return indexed, errors + + +def _describe(figures: tuple[str, ...]) -> str: + return ", ".join(f"{c}={v}" for c, v in zip(_COLUMNS, figures, strict=True)) + + +def _compare_bench_tables( + html_rows: list[tuple[str, ...]], + md_rows: list[tuple[str, ...]], + html_path: Path, + md_path: Path, +) -> list[str]: + """Compare the two tables by model-name set and per-model figures.""" + html_by, errors = _index_rows(html_rows, html_path) + md_by, md_errors = _index_rows(md_rows, md_path) + errors += md_errors + + only_html = sorted(set(html_by) - set(md_by)) + only_md = sorted(set(md_by) - set(html_by)) + if only_html or only_md: + errors.append( + f"benchmark table model set differs — in {html_path} only:" + f" {only_html or 'none'}; in {md_path} only: {only_md or 'none'}" + ) + for model in sorted(set(html_by) & set(md_by)): + if html_by[model] != md_by[model]: + errors.append( + f"benchmark table row {model!r} differs: {html_path} says" + f" ({_describe(html_by[model])}), {md_path} says" + f" ({_describe(md_by[model])})" + ) + return errors + + +def _read(path: Path) -> tuple[str | None, list[str]]: + if not path.is_file(): + return None, [ + f"{path}: missing — cannot check landing-page fact coherence" + ] + return path.read_text(encoding="utf-8"), [] + + +def check_fact_coherence(html_path: Path, md_path: Path) -> list[str]: + """Compare the facts docs/index.html and docs/index.md both state. + + Returns one message per divergence, each naming the fact, both values + and both file paths. A fact that cannot be located in either file is + reported the same way — an extraction failure is a gate failure, not a + silent skip, because a reworded sentence would otherwise switch its own + check off (#1154). + """ + html, errors = _read(html_path) + md, md_errors = _read(md_path) + errors += md_errors + if html is None or md is None: + return errors + + # --- prose facts ------------------------------------------------------ + claimed: dict[str, dict[Path, str]] = {} + for fact in _PROSE_FACTS: + per_file: dict[Path, str] = {} + for path, text, pattern in ( + (html_path, html, fact.html_pattern), + (md_path, md, fact.md_pattern or fact.html_pattern), + ): + found = {_normalize(v) for v in re.findall(pattern, text)} + if not found: + errors.append( + f"{fact.label}: not found in {path} (pattern" + f" /{pattern}/) — the sentence moved or was reworded, so" + f" it is no longer gated" + ) + elif len(found) > 1: + errors.append( + f"{fact.label}: {path} states conflicting values" + f" {sorted(found)}" + ) + else: + per_file[path] = found.pop() + if len(per_file) == 2 and per_file[html_path] != per_file[md_path]: + errors.append( + f"{fact.label} differs: {html_path} says" + f" {per_file[html_path]!r}, {md_path} says" + f" {per_file[md_path]!r}" + ) + claimed[fact.label] = per_file + + # --- benchmark results table ----------------------------------------- + html_rows, row_errors = _bench_rows_html(html, html_path) + errors += row_errors + md_rows, row_errors = _bench_rows_md(md, md_path) + errors += row_errors + if html_rows and md_rows: + errors += _compare_bench_tables(html_rows, md_rows, html_path, md_path) + + # Each file's own prose states how many models were benchmarked; the + # table it sits next to has to have that many rows. This is the half + # the cross-file comparison cannot do — both files agreeing on nine + # models says nothing about either table having nine rows. + for path, rows in ((html_path, html_rows), (md_path, md_rows)): + stated = claimed["benchmark model count"].get(path) + if rows and stated is not None and stated != str(len(rows)): + errors.append( + f"benchmark table rows: {path} has {len(rows)} rows but its" + f" prose states {stated} models" + ) + + # --- editor support --------------------------------------------------- + editors: dict[Path, set[str]] = {} + for path, text in ((html_path, html), (md_path, md)): + editors[path] = {n for n, pattern in _EDITORS if re.search(pattern, text)} + if not editors[path]: + errors.append( + f"editor support: no editor names found in {path} (looked" + f" for {', '.join(n for n, _ in _EDITORS)}) — the claim moved" + f" or was reworded, so it is no longer gated" + ) + if all(editors.values()) and editors[html_path] != editors[md_path]: + errors.append( + f"editor support differs — in {html_path} only:" + f" {sorted(editors[html_path] - editors[md_path]) or 'none'};" + f" in {md_path} only:" + f" {sorted(editors[md_path] - editors[html_path]) or 'none'}" + ) + + return errors + + def main() -> int: version = _version() expected = { @@ -74,13 +396,27 @@ def main() -> int: if reason is not None: stale.append(f" sitemap.xml: {reason}") - if stale: - print(f"ERROR: {len(stale)} site asset(s) out of date:") - for s in stale: - print(s) + # The landing page and its Markdown companion state the same facts in + # two hand-maintained places; the staleness loop above cannot see them + # drift apart, because both its sides come from build_index_md(). + incoherent = check_fact_coherence(DOCS / "index.html", DOCS / "index.md") + + if stale or incoherent: + if stale: + print(f"ERROR: {len(stale)} site asset(s) out of date:") + for s in stale: + print(s) + if incoherent: + print( + f"ERROR: {len(incoherent)} landing-page fact(s) diverge" + f" between docs/index.html and docs/index.md" + f" (fix build_index_md() in scripts/build_site.py):" + ) + for i in incoherent: + print(f" {i}") return 1 - print("Site assets are up-to-date.") + print("Site assets are up-to-date and landing-page facts are coherent.") return 0 diff --git a/tests/test_build_site.py b/tests/test_build_site.py index 05c106b7..e7bc421f 100644 --- a/tests/test_build_site.py +++ b/tests/test_build_site.py @@ -3,6 +3,7 @@ from __future__ import annotations import importlib.util +import re from datetime import date from pathlib import Path @@ -339,3 +340,308 @@ def test_sitemap_stale_reason_structural_diff_is_stale(tmp_path): reason = _check.sitemap_stale_reason(tmp_path / "sitemap.xml", _SITEMAP) assert reason is not None assert "stale" in reason + + +# --------------------------------------------------------------------------- +# check_site_assets.check_fact_coherence — docs/index.html ↔ docs/index.md +# +# The staleness check above compares `build_index_md()` against the committed +# `docs/index.md`, i.e. the generator against itself; it cannot see the HTML. +# These tests drive the coherence gate that can (#1154). Every case works on +# tmp_path copies — the committed pair is never mutated. +# --------------------------------------------------------------------------- + +_DOCS = Path(__file__).parent.parent / "docs" + + +def _landing_pair(tmp_path): + """Copy the committed landing-page pair into tmp_path. + + Returns ``(html_path, md_path)``. Mutating a copy and re-running the + check is how each drift class below is proved to be caught. + """ + html = tmp_path / "index.html" + md = tmp_path / "index.md" + html.write_text( + (_DOCS / "index.html").read_text(encoding="utf-8"), encoding="utf-8" + ) + md.write_text((_DOCS / "index.md").read_text(encoding="utf-8"), encoding="utf-8") + return html, md + + +def _edit(path, old, new): + """Replace a *unique* anchor in ``path``, asserting it occurs exactly once. + + The uniqueness assertion is load-bearing: if the landing page is reworded + so an anchor no longer matches, the mutation would silently become a + no-op and the test would pass while proving nothing. + """ + text = path.read_text(encoding="utf-8") + assert text.count(old) == 1, f"anchor not unique ({text.count(old)}x): {old!r}" + path.write_text(text.replace(old, new), encoding="utf-8") + + +def _sub(path, pattern, replacement, flags=0): + """Regex-replace one occurrence in ``path``, asserting the edit landed.""" + text = path.read_text(encoding="utf-8") + mutated, count = re.subn(pattern, replacement, text, count=1, flags=flags) + assert count == 1, f"pattern matched {count} times: {pattern!r}" + path.write_text(mutated, encoding="utf-8") + + +def _joined(errors): + return "\n".join(errors) + + +def test_fact_coherence_committed_pair_is_clean(): + """The committed landing page and its Markdown companion agree today. + + Runs against the real files, not copies — this is the assertion the CI + gate makes, and it must hold on a clean tree. + """ + assert _check.check_fact_coherence(_DOCS / "index.html", _DOCS / "index.md") == [] + + +def test_fact_coherence_html_percentage_bump_is_caught(tmp_path): + """A single changed benchmark figure in the HTML names the model.""" + html, md = _landing_pair(tmp_path) + _sub( + html, + r'(Claude Fable 5 ceiling\s*]*>)100%', + r"\g<1>42%", + ) + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a changed Vera figure must fail the gate" + assert "Claude Fable 5" in joined + assert "42%" in joined + assert "100%" in joined + assert str(html) in joined + assert str(md) in joined + + +def test_fact_coherence_md_percentage_bump_is_caught(tmp_path): + """The mirror case: the Markdown side drifts instead.""" + html, md = _landing_pair(tmp_path) + _edit( + md, + "| Claude Fable 5 | ceiling | **100%** |", + "| Claude Fable 5 | ceiling | **42%** |", + ) + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a changed Vera figure must fail the gate" + assert "Claude Fable 5" in joined + assert "42%" in joined + assert str(html) in joined + assert str(md) in joined + + +def test_fact_coherence_html_verabench_version_bump_is_caught(tmp_path): + """The exact class that bit in #1153: the benchmark version string.""" + html, md = _landing_pair(tmp_path) + _sub(html, r"VeraBench v\d+\.\d+\.\d+", "VeraBench v9.9.9") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a bumped VeraBench version must fail the gate" + assert "VeraBench version" in joined + assert "9.9.9" in joined + assert str(html) in joined + assert str(md) in joined + + +def test_fact_coherence_md_tested_vera_version_bump_is_caught(tmp_path): + """The Vera release the sweep ran against is gated too.""" + html, md = _landing_pair(tmp_path) + _sub(md, r"Vera v\d+\.\d+\.\d+\]", "Vera v9.9.9]") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a bumped tested-Vera version must fail the gate" + assert "tested Vera version" in joined + assert "9.9.9" in joined + + +def test_fact_coherence_version_badge_divergence_is_caught(tmp_path): + """The headline version badge vs the Markdown "Current version" line. + + ``check_version_sync.py`` pins the HTML badge to pyproject.toml; nothing + pinned it to ``index.md``, which states the same version in its own shape. + """ + html, md = _landing_pair(tmp_path) + _edit(md, "**Current version:** [0.1", "**Current version:** [9.9") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a diverged version badge must fail the gate" + assert "version badge" in joined + assert str(html) in joined + assert str(md) in joined + + +def test_fact_coherence_md_problem_count_bump_is_caught(tmp_path): + """The benchmark's problem count is a load-bearing fact.""" + html, md = _landing_pair(tmp_path) + _sub(md, r"A \d+-problem benchmark", "A 61-problem benchmark") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a changed problem count must fail the gate" + assert "problem count" in joined + assert "61" in joined + + +def test_fact_coherence_html_model_count_bump_is_caught(tmp_path): + """A prose model count that no longer matches its own table, or the pair. + + Bumping "Nine models" to "Ten models" in the HTML must trip both the + HTML↔MD comparison and the within-file rows-vs-prose cross-check. + """ + html, md = _landing_pair(tmp_path) + _edit(html, "Nine models, three providers", "Ten models, three providers") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a changed model count must fail the gate" + assert "model count" in joined + assert any("rows" in e for e in errors), ( + f"prose count must be cross-checked against the table rows: {errors}" + ) + + +def test_fact_coherence_removed_html_table_row_is_caught(tmp_path): + """Dropping a model from the HTML table names the missing model.""" + html, md = _landing_pair(tmp_path) + _sub( + html, + r'\s*\s*', + "", + flags=re.DOTALL, + ) + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a removed table row must fail the gate" + assert "Kimi K3" in joined + assert str(html) in joined + assert str(md) in joined + + +def test_fact_coherence_removed_md_table_row_is_caught(tmp_path): + """The mirror case: the Markdown table loses a row.""" + html, md = _landing_pair(tmp_path) + _sub(md, r"\n\| Kimi K3 \|[^\n]*", "") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a removed table row must fail the gate" + assert "Kimi K3" in joined + + +def test_fact_coherence_renamed_model_is_caught(tmp_path): + """A model renamed on one side only shows up in both directions.""" + html, md = _landing_pair(tmp_path) + _edit(md, "| Kimi K3 |", "| Kimi K4 |") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a renamed model must fail the gate" + assert "Kimi K3" in joined + assert "Kimi K4" in joined + + +def test_fact_coherence_tier_change_is_caught(tmp_path): + """The per-model tier label is stated in both files, so it is gated.""" + html, md = _landing_pair(tmp_path) + _edit(md, "| Kimi K3 | flagship |", "| Kimi K3 | workhorse |") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a changed tier must fail the gate" + assert "Kimi K3" in joined + assert "workhorse" in joined + + +def test_fact_coherence_dropped_editor_is_caught(tmp_path): + """Editor support: three names on the page, three in the Markdown.""" + html, md = _landing_pair(tmp_path) + _edit( + md, + "a [Vim package](https://github.com/aallan/vera/tree/main/editors/" + "vim-veralang) for Vim 8+ and Neovim, and ", + "", + ) + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "an editor dropped from one side must fail the gate" + assert "editor support" in joined + assert "Vim" in joined + assert str(html) in joined + assert str(md) in joined + + +# --- Extraction failure is gate failure ------------------------------------ + + +def test_fact_coherence_missing_html_table_is_extraction_failure(tmp_path): + """A restructured HTML table must fail loudly, not silently skip.""" + html, md = _landing_pair(tmp_path) + _sub(html, r'
Kimi K3 .*?
.*?
', "", flags=re.DOTALL) + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "an unlocatable benchmark table must fail the gate" + assert "benchmark table" in joined + assert str(html) in joined + + +def test_fact_coherence_missing_md_table_is_extraction_failure(tmp_path): + """The Markdown table header is the anchor; losing it fails the gate.""" + html, md = _landing_pair(tmp_path) + _edit(md, "| Model | Tier | Vera | Python | TypeScript |", "") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "an unlocatable benchmark table must fail the gate" + assert "benchmark table" in joined + assert str(md) in joined + + +def test_fact_coherence_missing_md_prose_fact_is_extraction_failure(tmp_path): + """Deleting the results caveat removes two facts; both must be named.""" + html, md = _landing_pair(tmp_path) + _sub(md, r"Results from \[VeraBench[^\n]*\n", "") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "an unlocatable fact must fail the gate" + assert "VeraBench version" in joined + assert "tested Vera version" in joined + assert "not found" in joined + assert str(md) in joined + + +def test_fact_coherence_missing_editor_claim_is_extraction_failure(tmp_path): + """No editor names at all in a file is an extraction failure, not a pass.""" + html, md = _landing_pair(tmp_path) + _sub(md, r"Editor support: [^\n]*\n", "") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "an unlocatable editor claim must fail the gate" + assert "editor support" in joined + assert str(md) in joined + + +def test_fact_coherence_missing_file_is_gate_failure(tmp_path): + """A missing half of the pair fails loudly rather than passing vacuously.""" + html, md = _landing_pair(tmp_path) + md.unlink() + errors = _check.check_fact_coherence(html, md) + assert errors, "a missing companion file must fail the gate" + assert str(md) in _joined(errors) + + +def test_fact_coherence_conflicting_values_within_one_file_is_caught(tmp_path): + """One file stating a fact twice, differently, is drift in its own right.""" + html, md = _landing_pair(tmp_path) + _edit( + md, + "Full source and data:", + "Results from [VeraBench v9.9.9](https://github.com/aallan/vera-bench" + "#results).\n\nFull source and data:", + ) + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "conflicting values inside one file must fail the gate" + assert "VeraBench version" in joined + assert "9.9.9" in joined + assert str(md) in joined From 68c4cd64638cff76dc6673215d470bdd0f6c275b Mon Sep 17 00:00:00 2001 From: Alasdair Allan Date: Mon, 3 Aug 2026 10:48:21 +0100 Subject: [PATCH 2/2] Cover the two remaining fact-coherence error branches; un-pin the badge mutation Review round: the duplicate-model-row (_index_rows) and wrong-cell-count (_bench_rows_md) error paths had no exercising test. Two tests now mutate the Markdown benchmark table located via the checker's own header regex, asserting the "twice" / "cells" messages name the row and the file. The version-badge mutation anchored on a literal "[0.1" prefix that would go stale at the next minor release; it is digit-anchored via _sub like its sibling tests. Per-file and headline test counts move 8,587 -> 8,589. Co-Authored-By: Claude --- README.md | 2 +- ROADMAP.md | 2 +- TESTING.md | 4 +-- tests/test_build_site.py | 53 +++++++++++++++++++++++++++++++++++++++- 4 files changed, 56 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 353989a9..6f87ebfe 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.8: 2,000+ commits, 204 releases, 8,587 tests, 95% code coverage, 169 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.8: 2,000+ commits, 204 releases, 8,589 tests, 95% code coverage, 169 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/ROADMAP.md b/ROADMAP.md index 7af9a70d..8057ee45 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 -8,587 tests, 169 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. +8,589 tests, 169 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 ac5ddea1..8ce7b151 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** | 8,587 across 131 files (~106,000 lines of test code; 8,471 passed + 26 stress, 90 skipped) | +| **Tests** | 8,589 across 131 files (~106,000 lines of test code; 8,473 passed + 26 stress, 90 skipped) | | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) | | **Conformance programs** | 169 programs across 9 spec chapters, validating every language feature | | **Example programs** | 42, all validated through `vera check` + `vera verify` | @@ -174,7 +174,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_html.py` | 4 | 167 | HTML landing page code samples: parse, check, verify (vera:skip-annotation aware, #538) | | `test_float64_fp.py` | 10 | 260 | #797 — `@Float64` contracts via Z3's IEEE-754 FloatingPoint sort: unsound relational / reflexive contracts (rounding at 2^53, `NaN`, `Inf`) flip from proved to violated/Tier-3, NaN-guarded contracts still verify at Tier 1, `==`/`!=` use IEEE `fpEQ`/`fpNEQ` (incl. `+0.0 == -0.0`), `%` matches codegen truncated remainder (not `fp.rem`; NaN-by-zero + large-magnitude edges), and `float_is_nan` / `float_is_infinite` / `nan()` / `infinity()` translate to FP predicates / constants. Also guards mixed `@Float64`/`@Int` ordering as a clean E142 (not a Z3 crash) | | `test_float64_builtins_807.py` | 81 | 491 | #807 — Tier-1 modeling of the modelable `@Float64` builtins. `float_clamp` modeled unconditionally as faithful WASM `f64.min(f64.max(v,lo),hi)` (the NaN-propagation soundness guard distinguishes it from a naive `z3.fpMin`/`fpMax`); `int_to_float` / `float_to_int` concrete-gated (symbolic args defer to Tier 3 — Z3's symbolic FP↔Real reasoning returns spurious counterexamples); `float_to_int` domain obligation (E529) for concrete NaN/Inf/out-of-range args. Verify-vs-run differentials confirm each model agrees with wasmtime bit-for-bit (±0, ±inf, NaN, ties, lo>hi, the 2^53 rounding boundary, i64 max, and the trap cases) | -| `test_build_site.py` | 44 | 647 | 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), 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), and the #1154 `check_fact_coherence` gate on `docs/index.html` ↔ `docs/index.md` (committed pair clean, then tmp_path-copy mutations for each drift class: a bumped percentage, version string, problem/model count, a removed/renamed table row, a changed tier, a dropped editor — plus extraction failure as gate failure for a restructured table, a deleted caveat, a missing editor claim, a missing file, and one file stating a fact two ways) | +| `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), 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), and the #1154 `check_fact_coherence` gate on `docs/index.html` ↔ `docs/index.md` (committed pair clean, then tmp_path-copy mutations for each drift class: a bumped percentage, version string, problem/model count, a removed/renamed table row, a changed tier, a dropped editor — plus extraction failure as gate failure for a restructured table, a deleted caveat, a missing editor claim, a missing file, and one file stating a fact two ways) | | `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. | diff --git a/tests/test_build_site.py b/tests/test_build_site.py index e7bc421f..92b5fc06 100644 --- a/tests/test_build_site.py +++ b/tests/test_build_site.py @@ -468,7 +468,7 @@ def test_fact_coherence_version_badge_divergence_is_caught(tmp_path): pinned it to ``index.md``, which states the same version in its own shape. """ html, md = _landing_pair(tmp_path) - _edit(md, "**Current version:** [0.1", "**Current version:** [9.9") + _sub(md, r"\*\*Current version:\*\* \[\d+\.\d+\.\d+", "**Current version:** [9.9.9") errors = _check.check_fact_coherence(html, md) joined = _joined(errors) assert errors, "a diverged version badge must fail the gate" @@ -645,3 +645,54 @@ def test_fact_coherence_conflicting_values_within_one_file_is_caught(tmp_path): assert "VeraBench version" in joined assert "9.9.9" in joined assert str(md) in joined +def _last_md_bench_row(md): + """Locate the final data row of the Markdown benchmark table. + + Anchored on the same header regex the checker uses, so these tests + mutate the benchmark table specifically — never some other table the + companion may gain later. + """ + lines = md.read_text(encoding="utf-8").splitlines() + start = next( + i for i, line in enumerate(lines) if _check._MD_BENCH_HEADER.match(line) + ) + j = start + 1 + while j < len(lines) and lines[j].startswith("|"): + j += 1 + return lines, j - 1 + + +def test_fact_coherence_duplicate_md_model_row_is_caught(tmp_path): + """``_index_rows``: one file listing a model twice is its own failure. + + The duplicate is dropped from the comparison, so without this branch a + doubled row would silently shadow whichever copy came second. + """ + html, md = _landing_pair(tmp_path) + lines, last = _last_md_bench_row(md) + model = _check._text_of_md(lines[last].strip().strip("|").split("|")[0]) + lines.insert(last + 1, lines[last]) + md.write_text("\n".join(lines) + "\n", encoding="utf-8") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a duplicated model row must fail the gate" + assert "twice" in joined + assert model in joined + assert str(md) in joined + + +def test_fact_coherence_md_row_cell_count_is_caught(tmp_path): + """``_bench_rows_md``: a row with the wrong cell count fails loudly. + + A malformed row cannot be compared, and skipping it silently would + un-gate that model's figures — the same rule as a missing fact. + """ + html, md = _landing_pair(tmp_path) + lines, last = _last_md_bench_row(md) + lines[last] = lines[last] + " 0% |" + md.write_text("\n".join(lines) + "\n", encoding="utf-8") + errors = _check.check_fact_coherence(html, md) + joined = _joined(errors) + assert errors, "a malformed table row must fail the gate" + assert "cells" in joined + assert str(md) in joined