feat: typed holes (#226)#436
Merged
Merged
Conversation
Add ? as a typed hole expression for partial programs. vera check reports each hole as a W001 warning (not an error) with the expected type and all available De Bruijn slot bindings. Programs with holes type-check successfully (ok: true) but cannot compile (E614). Changes: - grammar.lark: add hole_expr rule (? token in primary_expr) - ast.py: add HoleExpr node - transform.py: add hole_expr transformer method - checker/expressions.py: _check_hole() synthesises warning with expected type and full binding context; returns expected type so surrounding code type-checks without cascading errors - codegen/core.py: _find_holes() + _walk_node() reject programs at compile time with E614 - errors.py: add W001 (typed hole) and E614 (holes block compilation); extend error code format validation to allow W-prefix codes - formatter.py: format HoleExpr as ? - tests: 7 new tests (6 checker, 1 codegen) - tests/conformance/ch03_typed_holes.vera: new conformance program (72 total) - SKILL.md: Typed Holes section, best-practices tip, error code table - AGENTS.md: workflow section + error code table updated - Version bump: 0.0.104 -> 0.0.105 - All doc counts updated (72 conformance, 3199 tests) 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 typed-hole support ( Changes
*Files under Sequence Diagram(s)sequenceDiagram
participant User as User
participant Grammar as Grammar
participant Transformer as Transformer
participant Checker as Checker
participant Codegen as Codegen
User ->> Grammar: Submit Vera source containing `?`
Grammar ->> Transformer: Emit `hole_expr` node
Transformer ->> Checker: AST with HoleExpr(span=...)
Checker ->> Checker: _synth_expr routes to _check_hole(expected)
Checker ->> Checker: Collect in-scope bindings (inner→outer) as `@Type.index`
Checker -->> User: Emit W001 warning (expected type + bindings)
Checker ->> Codegen: Pass typed AST onward
Codegen ->> Codegen: _find_holes pre-pass scans AST
alt holes found
Codegen -->> User: Emit E614 per hole and return empty CompileResult (no wasm)
else no holes
Codegen ->> Codegen: Proceed with compilation passes
Codegen -->> User: Produce WASM
end
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 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 #436 +/- ##
==========================================
+ Coverage 90.29% 90.31% +0.01%
==========================================
Files 49 49
Lines 19230 19278 +48
Branches 220 220
==========================================
+ Hits 17363 17410 +47
- Misses 1863 1864 +1
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:
|
There was a problem hiding this comment.
Actionable comments posted: 8
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@AGENTS.md`:
- Line 11: The current sentence overstated guarantees by claiming every
conformance program "parse, type-check, verify, and (mostly) run correctly";
replace it with wording that limits the guarantee to the CI-enforced declared
verification level — e.g., change the sentence to say the conformance suite
contains 72 small programs that serve as minimal examples and that "Each Vera
conformance program in the suite must pass its declared verification level (see
manifest.json for mappings)" so it no longer promises full
parsing/verification/run success beyond the declared level.
In `@CHANGELOG.md`:
- Line 13: Update the broken anchor in the changelog entry by changing the
in-page link "[Typed Holes](`#typed-holes`)" to point to the SKILL.md file section
as "SKILL.md#typed-holes"; edit the line containing the SKILL.md mention (the
text that currently reads "SKILL.md: new [Typed Holes](`#typed-holes`) ...") so
the link target is SKILL.md#typed-holes and verify the anchor name matches the
header in SKILL.md (e.g., "Typed Holes") to prevent a dead link.
In `@HISTORY.md`:
- Around line 220-221: Add a single blank line between the table row containing
"v0.0.105 | 30 Mar | **Typed holes**" and the following horizontal rule '---' so
the table is separated by a blank line, satisfying markdownlint MD058; edit the
block that contains the "v0.0.105" row (look for that version string) and insert
one empty line immediately before the '---'.
In `@ROADMAP.md`:
- Line 27: The ROADMAP.md contains an internal inconsistency: the VeraBench line
claims "Typescript comparison is the next step" while the "Where we are" section
already states canonical TypeScript solutions/results are complete; update
ROADMAP.md so both the VeraBench bullet and the "Where we are" section reflect
the same factual status (either mark TypeScript comparison as completed or as
pending), editing the VeraBench sentence that mentions "Typescript comparison is
the next step" and/or the "Where we are" text so they consistently state the
current state of TypeScript solutions/results for VeraBench.
In `@SKILL.md`:
- Around line 443-446: The fenced code block containing "Warning [W001]: Typed
hole: expected Int." is missing a language tag; update that code fence (the
block starting with the line "Warning [W001]: Typed hole: expected Int.") to
include a language identifier such as text (e.g., change ``` to ```text) so the
markdown linter MD040 is satisfied; ensure you only add the language label to
the opening fence and do not modify the inner warning text.
In `@tests/test_checker.py`:
- Around line 5606-5629: Add assertions to lock binding order and the
zero-binding hint shape: in test_hole_fix_hint_includes_bindings (using
_warnings and warnings[0].fix) assert that the De Bruijn order is preserved by
checking warnings[0].fix.find("@Int.0") < warnings[0].fix.find("@Int.1"); in
test_hole_with_no_bindings assert the clean hint contains the type but no slot
bindings by checking "Int" is present and that there are no "@"-style bindings
in warnings[0].fix (e.g. assert "@" not in warnings[0].fix).
In `@tests/test_codegen.py`:
- Around line 10089-10100: Extend the test_hole_compile_rejected in
tests/test_codegen.py to include at least one nested-hole input (e.g. expression
with "1 + ?", a let binding like "let `@Int` = ?;", or a hole in call arguments)
in addition to the existing top-level "{ ? }" case; call the same _compile(src)
for the nested source, collect error diagnostics as is done currently, and
assert that an error with error_code "E614" is present and result.wasm_bytes ==
b"" to ensure _find_holes() recursively rejects holes in non-root positions.
In `@vera/codegen/core.py`:
- Line 185: The E614 diagnostic currently creates a SourceLocation with
file=None which omits the filename; update the code in core.py where loc =
SourceLocation(file=None) to use self.file instead (i.e., loc =
SourceLocation(file=self.file)) so the E614 error includes the filename
consistent with other diagnostics (refer to SourceLocation and the E614
diagnostic creation in the same function/class).
🪄 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: 6ca995db-6762-4c9f-a865-1f58c0250662
⛔ Files ignored due to path filters (6)
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/**tests/conformance/ch03_typed_holes.verais excluded by!**/*.vera
📒 Files selected for processing (22)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdHISTORY.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdpyproject.tomlscripts/check_skill_examples.pytests/conformance/manifest.jsontests/test_checker.pytests/test_codegen.pyvera/__init__.pyvera/ast.pyvera/checker/expressions.pyvera/codegen/core.pyvera/errors.pyvera/formatter.pyvera/grammar.larkvera/transform.py
- AGENTS.md: limit conformance suite guarantee to declared level; remove overclaim that all programs parse/verify/run correctly - CHANGELOG.md: fix broken anchor #typed-holes -> SKILL.md#typed-holes - HISTORY.md: add blank line before --- separator after v0.0.105 row - ROADMAP.md: remove TypeScript inconsistency in Where we are - SKILL.md: add 'text' language tag to W001 warning code fence (MD040) - tests/test_checker.py: assert De Bruijn order in fix hint; fix no-bindings test to check @int absent - tests/test_codegen.py: add test_hole_nested_compile_rejected - vera/codegen/core.py: use self.file in E614 SourceLocation Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
ROADMAP.md (1)
129-129:⚠️ Potential issue | 🟠 MajorRemove closed issue
#226from the roadmap backlog.
#226 Typed holesis still listed as pending, but this PR states it is implemented and closes#226. Keep ROADMAP as forward-looking only, and record shipment in HISTORY instead.Suggested change
-- [`#226`](https://github.com/aallan/vera/issues/226) **Typed holes** — partial program generation where the agent leaves `?` placeholders and the compiler reports the expected type at each hole site. Improves LLM completion quality by providing type context mid-generation.As per coding guidelines:
{ROADMAP.md,HISTORY.md}: Completed issues closed by PRs must be deleted from ROADMAP.md entirely (not struck through) and summarized with a one-liner in the relevant version row in HISTORY.md Stage 9 table.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@ROADMAP.md` at line 129, Remove the closed item “[`#226`] Typed holes …” entirely from ROADMAP.md (do not strike through) and add a one-line entry in HISTORY.md under the Stage 9 table noting the shipment, e.g. “Typed holes — partial program generation with `?` placeholders (closed `#226`)”; ensure the HISTORY entry is placed in the correct Stage 9 row and mirrors project style/tense.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@AGENTS.md`:
- Around line 21-24: The two new fenced code blocks (the block starting with
"Warning [W001]: Typed hole: expected Int." and the block containing "write
skeleton with ? -> vera check (get W001 hints) -> fill holes -> vera check ->
vera verify") must declare a language to satisfy markdownlint; change the
opening fences from ``` to ```text for each block so they become ```text ...
```; ensure all other newly added fences mentioned in the comment (also the ones
at lines referenced as "Also applies to: 28-30") are updated the same way.
---
Outside diff comments:
In `@ROADMAP.md`:
- Line 129: Remove the closed item “[`#226`] Typed holes …” entirely from
ROADMAP.md (do not strike through) and add a one-line entry in HISTORY.md under
the Stage 9 table noting the shipment, e.g. “Typed holes — partial program
generation with `?` placeholders (closed `#226`)”; ensure the HISTORY entry is
placed in the correct Stage 9 row and mirrors project style/tense.
🪄 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: b3dee233-5a1c-479e-a751-5f8e7b9b3426
⛔ Files ignored due to path filters (2)
docs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (9)
AGENTS.mdCHANGELOG.mdHISTORY.mdROADMAP.mdSKILL.mdTESTING.mdtests/test_checker.pytests/test_codegen.pyvera/codegen/core.py
…shipped #226 from ROADMAP Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai Fixed in commit 20a58fc — removed the |
|
Tip For best results, initiate chat on the files or code changes.
🧠 Learnings used |
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@AGENTS.md`:
- Around line 15-17: The markdown code fence containing "write .vera file ->
vera check -> fix errors -> vera verify -> fix errors -> done" is missing a
language identifier; update that fenced block in AGENTS.md to use the same style
as other workflow fences by adding the text language identifier (e.g., replace
the opening ``` with ```text) so markdownlint no longer flags it.
🪄 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: 1ab0f044-e16c-418c-8295-18e03bb2ead0
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (2)
AGENTS.mdROADMAP.md
Co-Authored-By: Claude <noreply@anthropic.invalid>
Complete cross-language comparison with Claude Sonnet 4: TypeScript (79% run_correct) is surprisingly below Vera full-spec (83%), with the gap widening at Tier 5 where TypeScript drops to 33%. Updated key findings to lead with the TypeScript result. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
♻️ Duplicate comments (1)
ROADMAP.md (1)
13-13:⚠️ Potential issue | 🟡 MinorTypeScript solution status inconsistency.
Line 13 states "canonical Vera and Python solutions" but line 27 states "canonical solutions written in Vera, Python, and Typescript", and the benchmark tables (lines 48, 50) show "TypeScript baseline" at 100% run_correct. The detailed TypeScript analysis (lines 63-69) further confirms TypeScript solutions exist. Please align line 13 with the rest of the document.
📝 Proposed fix to align TypeScript status
-Significant progress has been made towards Vera being a viable agent target. [VeraBench](https://github.com/aallan/vera-bench) — a 50-problem benchmark across 5 difficulty tiers with canonical Vera and Python solutions — is complete and has produced initial results: Claude Sonnet 4 achieves 96% check@1 and 83% run_correct on Vera versus 92% on Python, a 9-percentage-point gap that is smaller than might be expected for a new language. The dominant failure mode is De Bruijn slot ordering, confirming the hypothesis that `@T.n` indexing is the main learning curve for models. The remaining gaps are empirical breadth (more model baselines, Phase 3 reporting), standard library depth (HTTP hardening, server effects), and tooling integration (LSP). +Significant progress has been made towards Vera being a viable agent target. [VeraBench](https://github.com/aallan/vera-bench) — a 50-problem benchmark across 5 difficulty tiers with canonical Vera, Python, and TypeScript solutions — is complete and has produced initial results: Claude Sonnet 4 achieves 96% check@1 and 83% run_correct on Vera versus 92% on Python, a 9-percentage-point gap that is smaller than might be expected for a new language. The dominant failure mode is De Bruijn slot ordering, confirming the hypothesis that `@T.n` indexing is the main learning curve for models. The remaining gaps are empirical breadth (more model baselines, Phase 3 reporting), standard library depth (HTTP hardening, server effects), and tooling integration (LSP).As per coding guidelines:
**/*.md: Review Markdown files for factual accuracy against the codebase, broken links, and outdated information.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@ROADMAP.md` at line 13, Update the inconsistent statement that currently reads "canonical Vera and Python solutions" so it matches the rest of the document which mentions TypeScript; replace that phrase with "canonical solutions written in Vera, Python, and TypeScript" (aligning with the later line that says "canonical solutions written in Vera, Python, and Typescript" and the benchmark tables referencing "TypeScript baseline") and ensure spelling/capitalization of "TypeScript" matches other occurrences.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@ROADMAP.md`:
- Line 13: Update the inconsistent statement that currently reads "canonical
Vera and Python solutions" so it matches the rest of the document which mentions
TypeScript; replace that phrase with "canonical solutions written in Vera,
Python, and TypeScript" (aligning with the later line that says "canonical
solutions written in Vera, Python, and Typescript" and the benchmark tables
referencing "TypeScript baseline") and ensure spelling/capitalization of
"TypeScript" matches other occurrences.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 332339ad-b92e-4d4e-a79e-c4c4ea4f8c5b
📒 Files selected for processing (1)
ROADMAP.md
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
hole_exprinprimary_exprHoleExprnode_check_hole()emits W001 warning with expected type and all available De Bruijn slot bindings; returns the expected type so surrounding code type-checks without cascading errors_find_holes()rejects programs at compile time with E614HoleExprformats as?Test plan
vera checkon a file with?reports W001, exits 0vera check --jsonincludes W001 in warnings array with expected type and fix hintvera compileon a file with?reports E614, exits 1Closes #226
Summary by CodeRabbit
New Features
?placeholder;vera checkemits W001 warnings (expected type + available bindings); programs with holes type‑check but fail compilation with E614;--jsonincludes hole warnings and machine‑readable hints.Tests
Documentation
Chores