Release v0.0.156#688
Merged
Merged
Conversation
Bundles the #674 (`vera test` classifier) + #675 (E500 fix-text) + 2026-05-18 compiler-review docs sweep work that landed across PR #684 and #685 under the `[Unreleased]` section. First external code contribution from @rzyns lands in this release (#685). ## Version bumps - pyproject.toml, vera/__init__.py, uv.lock, docs/index.html - README.md project-status line (v0.0.155 → v0.0.156; 155 releases → 156 releases) ## CHANGELOG - Renamed `[Unreleased]` → `[0.0.156] - 2026-05-19` - Added an `### Added` entry for the new public `TestSummary.unlisted_errors: int` field exposed in `vera test --json` output (was missing from the [Unreleased] section even though it's a public API addition) - Updated link references at the bottom of CHANGELOG.md ## HISTORY - New v0.0.156 row crediting @rzyns's first external code contribution - Footer bumped: 155 → 156 tagged releases, 58 → 59 active development days ## Doc sweep findings (release-PR scoped) The release-PR doc sweep surfaced stale references that the in-context Explore agent and a manual cross-check found: 1. **SKILL.md "Known Bugs and Workarounds"** had a stale row for #602 (string-returning function call in interpolation — closed COMPLETED on 2026-05-08). Replaced the empty-bug-table leftover with the established "No known bugs." convention (matching `KNOWN_ISSUES.md`). 2. **KNOWN_ISSUES.md limitation entry for #607** (Int <: Nat subtyping docs gap) — closed COMPLETED on 2026-05-11 when the doc gap was filled. Removed the row. 3. **KNOWN_ISSUES.md, SKILL.md, vera/README.md limitation entries citing #608 (umbrella)** — #608 was closed COMPLETED on 2026-05-11. The underlying implementation tracking issues (#609 JSPI sleep, #610 ANSI subset) remain open and the limitation is still real, so re-pointed the citations to those two issues directly. 4. **`data invariant(...)` references citing the closed #560** — 4 sites across SKILL.md, spec/02-types.md, and spec/06-contracts.md described the feature as NYI and pointed at #560 as the tracking issue. #560 was closed COMPLETED on 2026-05-11 but the closure was about removing the broken spec examples, NOT about implementing the feature. Filed [#686](#686) as the successor tracking issue with explicit acceptance criteria; updated all 4 references. Added #686 to ROADMAP's Verification-depth section. ## Tacit context capture Items added inline (highest impact for new contributors / cold- context maintainers / AI agents working from the repo alone): - **CONTRIBUTING.md** — note on the first-time-contributor `action_required` CI gate (would have helped @rzyns; took manual approval on every push of #685 until I started pushing cleanup commits on the branch). - **CLAUDE.md** — "No known bugs." convention for empty KNOWN_ISSUES/SKILL bug tables. Plus the `Skip-changelog:` commit trailer as the documented escape hatch for the CHANGELOG-update gate when a change genuinely doesn't merit a release-note bullet. Lower-priority tacit-context items filed as [#687](#687) (CodeRabbit reply nuances, JSON output stability contract, doc-count gate awareness, modular-verification design-principle signposting). Added to ROADMAP's CI tooling section so they don't fall through. ## Validation - pytest 3,887 / 3,887 ✓ - mypy clean ✓ - ruff S clean ✓ - conformance 86/86 ✓ - examples 34/34 ✓ - doc counts consistent (3,917 total tests across 32 files) ✓ - version sync consistent (0.0.156 across 6 files) ✓ - limitations sync consistent (27 in KNOWN_ISSUES, 17 in vera/README, 4 in spec/*) ✓ - SKILL.md + spec code blocks parse ✓ - site assets up-to-date ✓ - All 18 pre-commit hooks green ✓ ## What this isn't - No new behavioural code changes — bug fixes shipped in PR #684 and PR #685 already; this PR just promotes them to a tagged release. - Not a fix for #686 (`data invariant(...)`) or #687 (tacit context items) — both filed during this sweep, both queued for follow-up. Co-Authored-By: Claude <noreply@anthropic.invalid>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #688 +/- ##
=======================================
Coverage 91.07% 91.07%
=======================================
Files 60 60
Lines 23458 23458
Branches 259 259
=======================================
Hits 21364 21364
Misses 2087 2087
Partials 7 7
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (8)
📝 WalkthroughWalkthroughUpdates project version to v0.0.156, adds CHANGELOG/HISTORY/README entries for the release and TestSummary.unlisted_errors, documents stable machine-readable JSON output, consolidates issue references (560→686, 608→609+610), adds contributor/process guidance, and makes small test and spec bookkeeping edits. Changesv0.0.156 Release Bump and Documentation
Estimated code review effort🎯 2 (Simple) | ⏱️ ~10 minutes Possibly related issues
Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@HISTORY.md`:
- Line 344: The two active-day counts in HISTORY.md are inconsistent: one
occurrence reads "59 active development days" (in the "Total: **810+ commits,
156 tagged releases, 59 active development days.**" line) while the other reads
"58 active development days" near the top; update the incorrect occurrence so
both statements match (choose the correct current total from the codebase/logs
and replace the mismatched "58" or "59" text accordingly) ensuring both
instances of "active development days" in HISTORY.md are identical.
In `@ROADMAP.md`:
- Line 180: The spec section reference for ADT invariants is incorrect: update
the text that mentions "data invariant(...)" so it cites Chapter 2 §2.4.1 (not
§2.6) while keeping the existing Chapter 6 §6.2.3 reference; ensure the sentence
reads something like "specified in Chapter 2 §2.4.1 (and Chapter 6 §6.2.3)" and
verify any link or anchor to the spec is corrected to point to §2.4.1 rather
than §2.6.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: b3f661b2-dee0-4e28-9f45-45bcc8284ea5
⛔ Files ignored due to path filters (7)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**docs/sitemap.xmlis excluded by!docs/**uv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (13)
CHANGELOG.mdCLAUDE.mdCONTRIBUTING.mdHISTORY.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdpyproject.tomlspec/02-types.mdspec/06-contracts.mdvera/README.mdvera/__init__.py
Two small follow-ups to the v0.0.156 release sweep: **1. Add #686 to KNOWN_ISSUES.md Limitations** When I filed #686 (data invariant() NYI, successor to closed #560) during the release sweep, I added it to ROADMAP.md but missed the KNOWN_ISSUES.md entry. #686 belongs in both: - ROADMAP.md = future planning/tracking ✓ (already done) - KNOWN_ISSUES.md = current user-facing limitations (the spec describes `data invariant(...)` as a working feature; users attempting to use it hit E130; that's a current limitation worth documenting alongside the Tier 2 verification limitation with the same shape) Added a row right after the Tier 2 entry since they're structurally similar ("specified in spec §X but not yet implemented in reference compiler"). **2. Clean test_codegen.py:8514 stale test-development scaffolding** `test_basic_string` in `TestStringInterpolation` had a dead `source` variable defined but never executed, plus a misleading comment about a "string_concat workaround". The `source` program references `@String.0` in a function body that has no `@String` binding (would fail typecheck if actually run); the working program was always `source2` (renamed to `source` after this cleanup). The misleading comment "Pass a string via string_concat workaround — use a known string / Instead, use a function that builds the interpolated string" suggested an active workaround for #602 (string-returning function in interpolation, closed COMPLETED 2026-05-08), but the actual test code is just a straightforward let-bind-then-interpolate. Surfaced during the release-PR workaround sweep; not a release blocker but worth cleaning while in the area. Net: test_codegen.py shrinks by 7 lines (18,979 → 18,972). Doc-count updated in TESTING.md. Validation: pytest 3887/3887 (test still passes), mypy clean, ruff S clean, doc-counts consistent, limitations sync consistent (27 → 28 in KNOWN_ISSUES.md after adding #686). Co-Authored-By: Claude <noreply@anthropic.invalid>
Two CodeRabbit comments + three of the five tacit-context items from #687 inline. The other two #687 items (CodeRabbit reply workflow nuances, two-instance review workflow) skipped per maintainer direction — neither rises to a doc gap worth closing in this release. Closing #687 as the actionable subset is done. **CR Finding 1: HISTORY.md 58/59 active days mismatch**. Line 3 read "58 active development days" while the footer (line 344) read "59" after my v0.0.156 row. Fixed line 3 to match the footer (the canonical current state). **CR Finding 2: §2.6 → §2.4.1 for `data invariant(...)` spec location**. `spec/02-types.md` has §2.4.1 "ADT Invariants" as the actual spec location of the invariant feature; §2.6 is "Refinement Types" (the workaround mentioned). Fixed the spec-location citation in ROADMAP.md and KNOWN_ISSUES.md. The parallel "Refinement types (§2.6)" mentions in the same rows are correct — those reference the workaround section, not the invariant feature. Net: two citations changed, four left intentionally as §2.6. **#687 item 1: JSON output as a public API contract**. Added in two places: - `spec/00-introduction.md` §0.5.8 "Machine-Readable Output (`--json`)" — sits inside the existing §0.5 diagnostics chapter because the JSON output is the machine-readable mirror of the human-readable diagnostic format. States the stability rules (fields MAY be added, MUST NOT be removed/renamed/semantically- changed; `ok` is the canonical gate; consumers MUST tolerate unknowns). Cross-references TESTING.md for the field set. - `TESTING.md` new "JSON Output Stability" section between Validation Scripts and Pre-commit Hooks. Documents the per-command field tables (`vera check --json`, `vera verify --json`, `vera test --json`) including the new v0.0.156 `summary.unlisted_errors` field. Provides the concrete contract that tests in `tests/test_cli.py` assert against. (Considered a separate `JSON-OUTPUT.md` file and rejected it per maintainer direction — putting it in the spec where diagnostics already live keeps the narrative arc intact.) **#687 item 2: Doc-count gate awareness in CONTRIBUTING.md**. Added a paragraph in the "Running Tests" section explaining `scripts/check_doc_counts.py` — what it checks, how to run it locally, the pre-commit / CI gating, and why the gate exists. Stops new contributors from learning this from CI failures. **#687 item 3: Modular verification design principle**. `spec/06-contracts.md` §6.4.2 already had a one-liner about modularity; expanded it with the practical implication that's the actual source of confusion: a buggy `bad` fn produces E500 on its body, but a caller `main` reading `bad`'s declared contract is still verified. Names why this is intentional (compositional verification bounded by per-function complexity) and why downstream consumers MUST surface the E500 (soundness chain). **ROADMAP.md cleanup**. Removed the #687 row since this PR closes the issue. **Skipped per maintainer direction**: - CodeRabbit reply workflow nuances — judged not worth a doc bump; the convention is implicit-but-consistent and new contributors pick it up by example - Two-instance review workflow — likely a personal workflow, out of repo scope Validation: pytest 3,887/3,887, mypy clean, ruff S clean, spec examples pass, doc-counts consistent, limitations sync consistent (28/17/4), site assets up-to-date. Closes #687. Co-Authored-By: Claude <noreply@anthropic.invalid>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Release v0.0.156 — bundles the [Unreleased] work from PR #684 (2026-05-18 compiler-review docs sweep + #675 E500 fix-text) and PR #685 (#674
vera testclassifier fix from external contributor @rzyns), plus a release-PR doc sweep that surfaced and addressed several stale references.This is the third time the bug-tracker section has been empty since ~v0.0.80.
What's in this release
Added
TestSummary.unlisted_errors: int— new public field onvera.tester.TestSummaryexposed invera test --jsonoutput undersummary.unlisted_errors. Counts verifier-error diagnostics whose attributable function isn't in the displayedfunctionslist (e.g. when--fnfilters to a subset, or for private functions). Downstream CI consumers can read the structured count instead of re-running regex attribution.Fixed
#675 — E500 (
Postcondition does not hold)fix=text now names all three repair classes neutrally with implementation-repair first. External report from @rzyns.#674 —
vera testnow fails closed when the verifier reports E500/E501/E502 diagnostics. JSON output setsok: false, preserves the verifier diagnostics, and exits non-zero. E501 call-site precondition failures attributed to the caller;--fnkeeps function rows filtered but whole-file verifier errors still fail closed. First external code contribution from @rzyns.Documentation
Release-PR doc sweep — additional fixes
The release-PR sweep surfaced four stale issue references that previously slipped through:
SKILL.md"Known Bugs"KNOWN_ISSUES.mdLimitationsKNOWN_ISSUES.md+SKILL.md+vera/README.mdSKILL.md+spec/02-types.md+spec/06-contracts.md(×2)data invariant(...)feature is documented as NYI in 4 places, all citing the closed #560. The closure was about removing the broken spec examples, not implementing the feature. Filed #686 as the successor tracking issue.Tacit context capture
High-impact items added inline (would have helped @rzyns / cold-context maintainers / AI agents working from the repo alone):
CONTRIBUTING.md— explicit note on the first-time-contributoraction_requiredCI gate. This caused friction during Fix vera test verifier error handling (#674) #685's CI runs.CLAUDE.md—No known bugs.convention for emptyKNOWN_ISSUES.md/SKILL.mdbug tables, and theSkip-changelog:commit trailer as the documented escape hatch for the changelog-update gate.Lower-priority items were initially filed as #687, then triaged inline in this PR per maintainer direction — three of the five items landed in this PR; two were judged not worth a doc bump. Closing #687 with this PR as the actionable subset.
Addressed inline (commit
0793938):spec/00-introduction.md§0.5.8 "Machine-Readable Output (--json)" stating the stability rules (fields MAY be added; MUST NOT be removed/renamed/semantically-changed;okis the canonical gate; consumers MUST tolerate unknowns). NewTESTING.md"JSON Output Stability" section with per-command field tables (check / verify / test) including the new v0.0.156summary.unlisted_errorsfield. No separateJSON-OUTPUT.mdfile — putting it in the spec keeps the diagnostics-narrative arc intact.CONTRIBUTING.md"Running Tests" section explainingscripts/check_doc_counts.py, how to run it locally, and that pre-commit catches stale counts before CI does.spec/06-contracts.md§6.4.2's existing one-liner with the practical implication that's the actual source of confusion: a buggybadproduces E500 on its body, but a callermainreadingbad's declared contract is still verified. Names why (compositional verification bounded by per-function complexity) and why downstream consumers MUST surface the E500 (soundness chain).Skipped per maintainer direction:
#686 (data invariant follow-up) added to ROADMAP and KNOWN_ISSUES under appropriate sections in commit
afe2ac9.Additional CR findings (commit
0793938)Two CodeRabbit comments on the v0.0.156 commit, both fixed:
data invariant(...)spec location —spec/02-types.mdhas §2.4.1 "ADT Invariants" as the actual spec location (§2.6 is Refinement Types, the workaround). Corrected the spec-location citation in ROADMAP and KNOWN_ISSUES; left the parallel "Refinement types (§2.6)" workaround mentions untouched.Validation
pytest tests/— 3,887 passed, 14 skipped, 16 stress-deselectedmypy vera/cleanruff check --select S vera/cleanpython scripts/check_conformance.py— 86/86python scripts/check_examples.py— 34/34python scripts/check_doc_counts.py— consistent (3,917 total tests across 32 files)python scripts/check_version_sync.py— v0.0.156 across 6 filespython scripts/check_limitations_sync.py— consistent (27/17/4)python scripts/check_skill_examples.py— passpython scripts/check_spec_examples.py— passpython scripts/check_site_assets.py— up-to-dateWorkaround sweep — clean
Checked
examples/andtests/for stale workarounds referencing the now-fixed bugs (#549, #578, #674, #675). No matches. The#602references intests/test_codegen.pyare regression-test docstrings for the closed bug — those are intentional and stay.Closes #687.
Post-merge
Standard release-tag workflow once merged: pull main, tag
v0.0.156on the merge commit, push tag,gh release create v0.0.156with the extracted CHANGELOG section.🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Documentation
Chores
Tests