feat: vera check --explain-slots, v0.0.108#446
Conversation
….108 Adds --explain-slots flag to vera check that prints a slot resolution table per function, showing which parameter position each @T.n De Bruijn index refers to. Directly addresses the dominant VeraBench failure mode (De Bruijn slot ordering) by letting agents self-correct via the check, read table, fix loop. - vera/slots.py: new pure utility -- slot_table(), format_slot_table(), slot_table_dict() - vera/cli.py: --explain-slots flag wired through cmd_check and main dispatcher - tests/test_cli.py: 7 new TestExplainSlots tests - SKILL.md: 5 prescriptive improvements (explain-slots workflow, contracts workflow, typed holes imperative rewrite, built-in naming directive, De Bruijn warning) - DE_BRUIJN.md: new debugging section with worked example - spec/ch03: section 3.4.2 development aid note - spec/ch06: Z3 10-second timeout documented - CI: uv lock --check step added to lint job - CONTRIBUTING.md: uv sync recommendation - tests/test_browser.py: prefer venv vera over system path - Closes #445, #183 (wontfix), #390, #391 Co-Authored-By: Claude <noreply@anthropic.invalid>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughAdds Changes
Sequence DiagramsequenceDiagram
participant User as User
participant CLI as "CLI\n(vera check)"
participant Importer as "Importer\n(resolve_imports)"
participant TypeChecker as "TypeChecker\n(typecheck)"
participant Slots as "Slots\n(vera/slots.py)"
participant Formatter as "Formatter"
participant StdOut as StdOut
User->>CLI: vera check file.vera --explain-slots
CLI->>Importer: resolve_imports(program)
Importer-->>CLI: resolved_program
CLI->>TypeChecker: typecheck(resolved_program)
alt type errors
TypeChecker-->>CLI: errors
CLI->>StdOut: print errors (no slot tables)
else type check OK
TypeChecker-->>CLI: success, annotated AST
CLI->>Slots: compute slot tables for each FnDecl
Slots-->>CLI: slot_environments dict
alt --json
CLI->>Formatter: attach slot_environments to JSON result
else human-readable
CLI->>Formatter: format_slot_table per function
end
Formatter-->>StdOut: OK: file.vera + slot tables
end
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes 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 unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #446 +/- ##
==========================================
- Coverage 90.32% 90.31% -0.01%
==========================================
Files 49 50 +1
Lines 19335 19406 +71
Branches 220 220
==========================================
+ Hits 17464 17527 +63
- Misses 1867 1875 +8
Partials 4 4
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:
|
Co-Authored-By: Claude <noreply@anthropic.invalid>
The --explain-slots output block in spec/03-slot-references.md uses a backtick-text fence; check_spec_examples.py did not recognise the text language tag as non-Vera and tried to parse it. Also adds text to the skip lists in check_skill_examples.py, check_readme_examples.py and check_examples_doc.py for consistency. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 7
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
spec/06-contracts.md (1)
332-336:⚠️ Potential issue | 🟡 MinorInconsistency: Tier 1 timeout column contradicts §6.4.3.
Line 232 now states Tier 1 invocations are bounded to 10 seconds, but the summary table at Line 334 still says
None (decidable)for Tier 1 timeout. This is internally inconsistent — if Tier 1 can time out and fall to Tier 3 (as documented above), the table should reflect that.Proposed fix
| Tier | Scope | Solver | Timeout | Failure mode | |------|-------|--------|---------|--------------| -| 1 | Decidable fragment (QF_LIA + length + bool) | Z3 | None (decidable) | Compile error with counterexample | +| 1 | Decidable fragment (QF_LIA + length + bool) | Z3 | 10 seconds | Compile error with counterexample; timeout falls to Tier 3 | | 2 | Extended (function calls, quantifiers, arrays) — [not yet implemented](https://github.com/aallan/vera/issues/427) | Z3 with hints | 10 seconds | Falls to Tier 3 | | 3 | Runtime | None (checks emitted as code) | N/A | Runtime trap |🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@spec/06-contracts.md` around lines 332 - 336, Update the Tier 1 row in the summary table (the "Tier | Scope | Solver | Timeout | Failure mode" entry for Tier 1) to match §6.4.3: change the Timeout cell from "None (decidable)" to "10 seconds" and change the Failure mode from "Compile error with counterexample" to reflect timeout behavior (e.g., "Falls to Tier 3 on timeout" or "Compile error with counterexample; falls to Tier 3 on timeout") so the table and the Tier 1 description are consistent.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In @.github/workflows/ci.yml:
- Around line 126-129: The CI step installs the latest uv which can introduce
transient failures if uv changes; update the workflow so the pip install line
for uv uses a constrained version range (pin to a stable major/minor range) and
keep the subsequent `uv lock --check` step as-is; this ensures the `uv.lock`
currency check remains reproducible and prevents unexpected breaking changes
from the `uv` package in CI.
In `@DE_BRUIJN.md`:
- Around line 404-420: Change the two untyped fenced code blocks so they include
language tags: add "bash" to the first fence containing the command `vera check
--explain-slots your_file.vera` and add "text" to the second fence containing
the Slot environments output; update the opening fences accordingly while
leaving the block contents unchanged and ensure the closing triple-backticks
remain present for both blocks.
In `@HISTORY.md`:
- Line 3: Update the HISTORY.md opening sentence to accurately reflect the
current scope by changing “through Stage 9” to “through Stage 10” (or equivalent
wording that includes Stage 10), and then scan the later section around the
Stage 10 addition (the area corresponding to the existing Stage 10 content
referenced in the comment) to ensure any other stage-coverage statements (e.g.,
in the block around lines 223-230) are also updated for consistency.
In `@scripts/check_skill_examples.py`:
- Around line 69-71: Two entries use the same dictionary key 859 (the tuples
("FRAGMENT", "Regex Result matching example, bare expression") and ("FRAGMENT",
"Float64 predicate and constant examples, ...")), causing the first to be
overwritten; find the dictionary that contains keys 848 and 859 and rename the
duplicated 859 to a unique numeric key (or the correct sequence number) so both
tuples are present, ensuring the tuple values remain unchanged and only the
numeric key is updated.
- Around line 98-100: The ALLOWLIST dictionary contains duplicate integer keys
(1005 and 859) causing earlier entries to be overwritten; locate the ALLOWLIST
definition (symbol ALLOWLIST) and update the duplicate keys so each tuple is
mapped to its correct unique line number (e.g., ensure ("FRAGMENT", "Effect
declarations list"), ("FRAGMENT", "Async effect declarations list"), and
("FRAGMENT", "Async effect declarations, bare clauses") have distinct integer
keys and that ("FRAGMENT", "Regex Result matching example, bare expression")
entries use unique keys), correcting the mistaken 1005/859 values to the actual
line numbers so no entries are duplicated.
In `@SKILL.md`:
- Around line 308-320: The code fences in the new --explain-slots example lack
language identifiers; update the three fenced blocks around the command "vera
check --explain-slots your_file.vera" and the output beginning "Slot
environments (index 0 = last occurrence in signature):" to include language tags
(use bash for the command block and text for the output blocks) so the MD040
warnings are resolved.
In `@vera/cli.py`:
- Line 939: The CLI flag --explain-slots is being parsed into use_explain_slots
but is not documented in the module usage docstring or the USAGE help text;
update the module-level docstring and the USAGE constant/text to include a brief
description and usage example for --explain-slots (mentioning the flag name and
that it sets use_explain_slots), and also add an entry to any help/arguments
list printed by the CLI (where other flags are documented). Update references
around the parsing site (variable use_explain_slots) and the USAGE/usage text
constants so the flag appears in help output.
---
Outside diff comments:
In `@spec/06-contracts.md`:
- Around line 332-336: Update the Tier 1 row in the summary table (the "Tier |
Scope | Solver | Timeout | Failure mode" entry for Tier 1) to match §6.4.3:
change the Timeout cell from "None (decidable)" to "10 seconds" and change the
Failure mode from "Compile error with counterexample" to reflect timeout
behavior (e.g., "Falls to Tier 3 on timeout" or "Compile error with
counterexample; falls to Tier 3 on timeout") so the table and the Tier 1
description are consistent.
🪄 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: ae9f2cdd-f896-49c9-9ca5-a88c04dac40f
⛔ Files ignored due to path filters (5)
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/**
📒 Files selected for processing (20)
.github/workflows/ci.ymlCHANGELOG.mdCLAUDE.mdCONTRIBUTING.mdDE_BRUIJN.mdHISTORY.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdpyproject.tomlscripts/check_skill_examples.pyscripts/check_spec_examples.pyspec/03-slot-references.mdspec/06-contracts.mdtests/test_browser.pytests/test_cli.pyvera/__init__.pyvera/cli.pyvera/slots.py
There was a problem hiding this comment.
♻️ Duplicate comments (2)
HISTORY.md (1)
3-3:⚠️ Potential issue | 🟡 MinorUpdate the opening scope statement to include Stage 10.
Line 3 still says the history runs “through Stage 9”, but this file now includes a Stage 10 section. Please align the opening sentence with the current scope.Suggested edit
-How the Vera compiler was built, from initial commit through Stage 9, across 31 active development days. +How the Vera compiler was built, from initial commit through Stage 10, across 31 active development days.As per coding guidelines, “Review Markdown files for factual accuracy against the codebase, broken links, and outdated information.”
Also applies to: 223-230
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@HISTORY.md` at line 3, The opening sentence currently reads "How the Vera compiler was built, from initial commit through Stage 9, across 31 active development days."—update that sentence to reflect Stage 10 (e.g., "through Stage 10") and adjust any related counts if needed; also scan and update the other referenced section around the "223-230" content to ensure any mentions of "Stage 9" are changed to "Stage 10" and the scope/facts remain consistent.scripts/check_skill_examples.py (1)
69-71:⚠️ Potential issue | 🟠 MajorFix duplicate ALLOWLIST keys; entries are being silently overwritten.
859and1005are each declared twice, so earlier entries are discarded by Python dict semantics. That will make allowlist behaviour incorrect for SKILL example checks.#!/bin/bash # Verify duplicate numeric keys in ALLOWLIST and show the clashing entries. python - <<'PY' import ast from collections import defaultdict from pathlib import Path path = Path("scripts/check_skill_examples.py") src = path.read_text(encoding="utf-8") tree = ast.parse(src) allowlist_node = None for node in tree.body: if isinstance(node, ast.AnnAssign) and getattr(node.target, "id", None) == "ALLOWLIST": allowlist_node = node.value break if allowlist_node is None or not isinstance(allowlist_node, ast.Dict): raise SystemExit("ALLOWLIST dict not found") dups = defaultdict(list) for k, v in zip(allowlist_node.keys, allowlist_node.values): if isinstance(k, ast.Constant) and isinstance(k.value, int): dups[k.value].append((k.lineno, ast.get_source_segment(src, v))) found = False for key in sorted(dups): if len(dups[key]) > 1: found = True print(f"duplicate key {key}:") for lineno, value_src in dups[key]: print(f" line {lineno}: {value_src}") if not found: print("No duplicate integer keys in ALLOWLIST.") PYAs per coding guidelines, “Flag actual duplicate keys within a single dict, but do not flag the pattern itself as suspicious or suggest refactoring it.”
Also applies to: 98-101, 111-111
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@scripts/check_skill_examples.py` around lines 69 - 71, The ALLOWLIST dict in scripts/check_skill_examples.py contains duplicate integer keys (notably 859 and 1005, and the groups around 98-101 and 111) causing earlier entries to be silently overwritten; open the ALLOWLIST dict, locate the duplicate integer keys, and either merge the two value entries into a single unique key (combining lists/tuples) or rename one of the entries to a unique integer so no data is lost, then run the provided AST verification snippet to confirm there are no remaining duplicate integer keys.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@HISTORY.md`:
- Line 3: The opening sentence currently reads "How the Vera compiler was built,
from initial commit through Stage 9, across 31 active development days."—update
that sentence to reflect Stage 10 (e.g., "through Stage 10") and adjust any
related counts if needed; also scan and update the other referenced section
around the "223-230" content to ensure any mentions of "Stage 9" are changed to
"Stage 10" and the scope/facts remain consistent.
In `@scripts/check_skill_examples.py`:
- Around line 69-71: The ALLOWLIST dict in scripts/check_skill_examples.py
contains duplicate integer keys (notably 859 and 1005, and the groups around
98-101 and 111) causing earlier entries to be silently overwritten; open the
ALLOWLIST dict, locate the duplicate integer keys, and either merge the two
value entries into a single unique key (combining lists/tuples) or rename one of
the entries to a unique integer so no data is lost, then run the provided AST
verification snippet to confirm there are no remaining duplicate integer keys.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 1a820154-d709-4712-bfcd-e70a9be5dfdc
📒 Files selected for processing (6)
HISTORY.mdscripts/check_examples_doc.pyscripts/check_readme_examples.pyscripts/check_skill_examples.pyscripts/check_spec_examples.pyspec/03-slot-references.md
- vera/cli.py: add --explain-slots to module docstring usage table - DE_BRUIJN.md, SKILL.md: add bash/text language tags to unfenced blocks - HISTORY.md: update opening sentence to 'through Stage 10' - spec/06-contracts.md: update Tier 1 summary table timeout/failure columns - scripts/check_skill_examples.py: fix duplicate dict keys (859->899 for Float64 predicates, 1005->1130 for Async effect declarations); fix label on key 886 (type conversions, not Float64 predicates) - .github/workflows/ci.yml: pin uv to >=0.5,<2 for reproducibility Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 3
♻️ Duplicate comments (2)
scripts/check_skill_examples.py (1)
98-100:⚠️ Potential issue | 🟠 MajorFix duplicate
ALLOWLISTkeys; current entries are being silently overwritten.Line 100 and Line 146 both use key
1130, so one entry is dropped. Line 114 and Line 150 both use key899, so one is redundant and also overwritten. This can hide intended allowlist coverage and make failures/staleness checks unreliable.Suggested fix
- 1130: ("FRAGMENT", "Async effect row declarations, bare clauses"), ... - # Float64 predicates — bare function calls (shifted by De Bruijn section additions) - 899: ("FRAGMENT", "Float64 predicate and constant examples, bare calls"), + # NOTE: assign unique line keys here (or remove duplicates if accidental): + # - keep one `899` entry only + # - ensure the typed-holes entry currently at duplicate key `1130` uses its real SKILL.md fence line#!/bin/bash # Verify duplicate integer keys inside ALLOWLIST in scripts/check_skill_examples.py python - <<'PY' from pathlib import Path import re from collections import defaultdict p = Path("scripts/check_skill_examples.py") lines = p.read_text(encoding="utf-8").splitlines() in_allow = False brace_depth = 0 hits = defaultdict(list) for i, line in enumerate(lines, start=1): if not in_allow and re.search(r'^\s*ALLOWLIST\s*:', line): in_allow = True if in_allow: brace_depth += line.count("{") m = re.match(r'^\s*(\d+)\s*:\s*\(', line) if m: hits[int(m.group(1))].append((i, line.strip())) brace_depth -= line.count("}") if brace_depth <= 0 and "}" in line: break dupes = {k:v for k,v in hits.items() if len(v) > 1} if not dupes: print("No duplicate ALLOWLIST keys found.") else: print("Duplicate ALLOWLIST keys found:") for k, occur in sorted(dupes.items()): print(f" key {k}:") for ln, txt in occur: print(f" Line {ln}: {txt}") PYAs per coding guidelines, allowlist line-number patterns are expected, but actual duplicate keys in a single dict must be flagged.
Also applies to: 114-150
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@scripts/check_skill_examples.py` around lines 98 - 100, The ALLOWLIST dict contains duplicate integer keys (notably 1130 and 899) so later entries overwrite earlier ones; locate the ALLOWLIST dict and remove the duplicates by either merging the intended entries for key 1130 and for key 899 into a single entry each or by renumbering one of the conflicting keys to a unique integer, then run the provided duplicate-key checker to verify no duplicate numeric keys remain; ensure the merged/renumbered entries preserve the original tuple structure and intended allowlist coverage.vera/cli.py (1)
940-940:⚠️ Potential issue | 🟡 Minor
--explain-slotsis parsed and routed, but still not exposed inUSAGE.Line 940/Line 999/Line 1024-Line 1027 wire the feature correctly, but the
USAGEhelp still advertisescheck [--json|--quiet]and has no--explain-slotsoption entry, soverahelp output remains incomplete.Also applies to: 999-999, 1024-1027
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@vera/cli.py` at line 940, USAGE/help text is missing the newly wired --explain-slots flag; update the USAGE constant (the help text shown by vera) to include an entry for --explain-slots under the check command and any related examples so the flag is documented; locate the USAGE string (or help builder) and add a short description for --explain-slots consistent with other flags, and ensure any usage examples that list check [--json|--quiet] include --explain-slots as appropriate to keep the displayed help in sync with the use_explain_slots parsing and downstream handling.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@HISTORY.md`:
- Line 3: Update the totals section in HISTORY.md so the final totals line
matches the header’s “31 active development days” (replace the existing “30
active development days” text with “31 active development days”); locate the
totals block that currently contains the phrase "30 active development days" and
change it to "31 active development days" to keep the document internally
consistent.
In `@spec/06-contracts.md`:
- Line 334: Update the Tier 1 table row that currently reads "falls to Tier 3 on
timeout" so it matches the broader fallback behavior described elsewhere; change
the wording for the Decidable fragment (QF_LIA + length + bool) row (the Tier 1
table entry) to indicate fallback to Tier 3 on "unknown or timeout" (i.e., align
with the phrase "fallback on `unknown` or timeout" used earlier in the
document).
In `@vera/cli.py`:
- Around line 152-153: The JSON output path omits the slot_environments key on
error paths; update the exception handlers in the cmd_check flow so that when
explain_slots is true they also set result["slot_environments"] = slot_json (or
an empty list) before emitting JSON; locate the explain_slots check and the
FileNotFoundError / VeraError handlers and add the same result assignment there
to keep the schema consistent.
---
Duplicate comments:
In `@scripts/check_skill_examples.py`:
- Around line 98-100: The ALLOWLIST dict contains duplicate integer keys
(notably 1130 and 899) so later entries overwrite earlier ones; locate the
ALLOWLIST dict and remove the duplicates by either merging the intended entries
for key 1130 and for key 899 into a single entry each or by renumbering one of
the conflicting keys to a unique integer, then run the provided duplicate-key
checker to verify no duplicate numeric keys remain; ensure the merged/renumbered
entries preserve the original tuple structure and intended allowlist coverage.
In `@vera/cli.py`:
- Line 940: USAGE/help text is missing the newly wired --explain-slots flag;
update the USAGE constant (the help text shown by vera) to include an entry for
--explain-slots under the check command and any related examples so the flag is
documented; locate the USAGE string (or help builder) and add a short
description for --explain-slots consistent with other flags, and ensure any
usage examples that list check [--json|--quiet] include --explain-slots as
appropriate to keep the displayed help in sync with the use_explain_slots
parsing and downstream handling.
🪄 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: c8bd9b67-b727-4c67-95c8-2d3a55c0a69c
⛔ Files ignored due to path filters (2)
docs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (7)
.github/workflows/ci.ymlDE_BRUIJN.mdHISTORY.mdSKILL.mdscripts/check_skill_examples.pyspec/06-contracts.mdvera/cli.py
Add 5 in-process TestExplainSlots tests covering previously uncovered paths in vera/slots.py (88% coverage, up from 66%): - test_inprocess_single_param: 'only @t' label (n==1 branch) - test_inprocess_mixed_types: mixed unique types - test_inprocess_json: slot_table_dict / JSON output path - test_inprocess_generic_param: NamedType with type_args (Option<Int>) - test_inprocess_three_same_type: 'N from last @t' label (3+ same type) Also update TESTING.md and ROADMAP.md test counts: 3212 -> 3217. Co-Authored-By: Claude <noreply@anthropic.invalid>
- HISTORY.md: fix totals line '30 active development days' -> '31' - spec/06-contracts.md: Tier 1 failure mode now says 'unknown or timeout' to align with section 6.4.3 wording - vera/cli.py: FileNotFoundError and VeraError JSON handlers now include slot_environments: [] when explain_slots=True (schema consistency) - tests/test_cli.py: tighten test_no_output_on_error_json assertion now that slot_environments is always present in JSON output - scripts/check_skill_examples.py: remove duplicate keys 1130 and 899 introduced by previous fix (pre-existing entries already covered those blocks; the new additions in the first dict section were redundant) - .gitignore: remove uv.lock exclusion so lockfile can be committed - uv.lock: commit lockfile so CI uv lock --check can actually run Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (1)
vera/cli.py (1)
7-7:⚠️ Potential issue | 🟡 MinorDocument
--explain-slotsinUSAGEoutput too.Line 7 adds the feature to the module usage block, but the runtime
USAGEtext still omits it (Line 899, Line 900, and the options list around Line 910-Line 919).verahelp remains incomplete for discoverability.Suggested patch
- check [--json|--quiet] Parse and type-check a .vera file - typecheck [--json|--quiet] Same as check (explicit alias) + check [--json|--quiet|--explain-slots] Parse and type-check a .vera file + typecheck [--json|--quiet|--explain-slots] Same as check (explicit alias) @@ --check Check if already canonical (vera fmt) + --explain-slots Print slot-resolution tables after successful check🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@vera/cli.py` at line 7, Update the CLI help text to document the new --explain-slots flag by adding its description into the USAGE string used at runtime (the USAGE variable in vera/cli.py) and include the option in the options list shown in the help output; locate the multi-line USAGE/help text near the bottom of the file (around where other flags are listed) and insert a line like " --explain-slots <file> Show slot resolution table (`@T.n` → parameter)" so the runtime "vera help" output matches the new feature.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@HISTORY.md`:
- Line 267: Update the release-count in the HISTORY.md summary line that
currently reads "Total: **630+ commits, 107 tagged releases, 31 active
development days.**" to reflect the newly added v0.0.108 (i.e., change 107
tagged releases to 108 tagged releases) so the document stays internally
consistent with the Stage 10 entry for v0.0.108.
In `@tests/test_cli.py`:
- Around line 2811-3009: Add a unit test to cover the missing-file
(FileNotFound) JSON path for the new --explain-slots feature: create a new test
method alongside TestExplainSlots (e.g. test_missing_file_json_explain_slots)
that calls the CLI with "--explain-slots --json" on a non-existent file, asserts
the process return code indicates failure, then parses stdout as JSON and
asserts parsed["ok"] is False and parsed["slot_environments"] == []; this
mirrors the existing test_no_output_on_error_json pattern but targets the
missing-file branch so the schema guarantees slot_environments is an empty list.
---
Duplicate comments:
In `@vera/cli.py`:
- Line 7: Update the CLI help text to document the new --explain-slots flag by
adding its description into the USAGE string used at runtime (the USAGE variable
in vera/cli.py) and include the option in the options list shown in the help
output; locate the multi-line USAGE/help text near the bottom of the file
(around where other flags are listed) and insert a line like "
--explain-slots <file> Show slot resolution table (`@T.n` → parameter)" so the
runtime "vera help" output matches the new feature.
🪄 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: 7a08ee43-3a84-4d8e-a4a8-133739d09058
⛔ Files ignored due to path filters (1)
uv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (7)
.gitignoreHISTORY.mdTESTING.mdscripts/check_skill_examples.pyspec/06-contracts.mdtests/test_cli.pyvera/cli.py
💤 Files with no reviewable changes (1)
- .gitignore
- vera/cli.py USAGE constant: add --explain-slots to check/typecheck synopsis lines and to the Options block so 'vera' with no args shows the flag in the printed help - tests/test_cli.py: add test_missing_file_json_explain_slots covering the FileNotFoundError JSON path with --explain-slots (slot_environments: []) - HISTORY.md: fix tagged releases count 107 -> 108 in totals line - TESTING.md / ROADMAP.md: update test counts 3217 -> 3218 Co-Authored-By: Claude <noreply@anthropic.invalid>
Summary
vera check --explain-slots— new flag that prints a slot resolution table per function, showing which parameter position each@T.nDe Bruijn index refers to. Directly addresses the dominant VeraBench failure mode (9pp gap vs Python, root cause: De Bruijn slot ordering) by letting agents self-correct via the check → read table → fix loopuv lock --checkCI step added;CONTRIBUTING.mdupdatedsmt.py:150; spec now documents itTest plan
vera check examples/safe_divide.vera --explain-slotsprints slot tablevera check examples/safe_divide.vera --explain-slots --jsonincludesslot_environmentskeypytest tests/test_cli.py -k explain— 7 new tests passpytest tests/ -v— all 3212 tests passmypy vera/— cleanpython scripts/check_doc_counts.py— consistentpython scripts/check_version_sync.py— v0.0.108 consistentCloses #445
Closes #183
Closes #390
Closes #391
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Documentation
Tests
Chores