Hygiene tail: reserve every namespace, name the Byte range, one fixture helper (#1228, #1240, #1246, #1252, #1260) - #1282
Conversation
|
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:
📝 WalkthroughWalkthroughThe checker now enforces reserved ChangesChecker, LSP, fixtures, and validation
Estimated code review effort: 3 (Moderate) | ~25 minutes Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 7 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (7 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## release/v0.1.10 #1282 +/- ##
================================================
Coverage 94.05% 94.05%
================================================
Files 100 100
Lines 35726 35780 +54
Branches 458 458
================================================
+ Hits 33601 33652 +51
- Misses 2112 2115 +3
Partials 13 13
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 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 @.gitignore:
- Around line 66-73: Update the artifact ignore rules near /hello.txt to also
ignore /examples/hello.txt, preserving the existing root-level rule and
documenting both supported output locations.
In `@tests/module_fixture_helpers.py`:
- Around line 8-16: Update the documentation for resolved_module() in
tests/module_fixture_helpers.py lines 8-16 and TESTING.md lines 534-548 to state
that it parses from a real temporary file, preserves parse-time file provenance,
and deletes the file before returning unless a caller explicitly needs to reopen
it. Distinguish fake_resolved_module() by its in-memory parsing and synthetic
path, not by whether the file exists; no implementation change is required.
In `@vera/checker/expressions.py`:
- Around line 158-188: The Byte contextual path in the literal-checking logic
must suppress or remove any earlier unconstrained range E149 for the same
literal before reporting the `@Byte-specific` E149, so refinement comparisons
produce exactly one diagnostic naming the 0..255 bound. Update the relevant
handling near the visible Byte check in vera/checker/expressions.py, and add the
regression in tests/test_checker_types.py covering the `@Byte` refinement
comparison with the large literal, asserting exactly one E149 mentioning 255.
🪄 Autofix
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 Plus
Run ID: f80a8b46-1bec-42c1-96d1-97c44cb7f0b4
⛔ Files ignored due to path filters (8)
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/ch08_reserved_vera_prefix_ability_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_constructor_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_effect_rejected.verais excluded by!**/*.vera
📒 Files selected for processing (25)
.gitignoreAGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/08-modules.mdtests/conformance/manifest.jsontests/module_fixture_helpers.pytests/test_checker_modules.pytests/test_checker_types.pytests/test_codegen_modules.pytests/test_codegen_nat_guards.pytests/test_lsp.pytests/test_monomorphize_differential.pytests/test_naming_env_provenance_1208.pytests/test_refinement_binder_convergence_1208.pyvera/README.mdvera/checker/expressions.pyvera/checker/registration.pyvera/errors.pyvera/lsp/features.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Adversarial review record — round 1 (
|
Round-1 dispositions (
|
There was a problem hiding this comment.
Actionable comments posted: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
TESTING.md (1)
243-247: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate the conformance skip total.
The three new check-level programmes add six skipped stage rows. The table now contains 87 level-limited skips and 4 environment-gated skips, but Line 251 still states 85. Change the total to 91, or state clearly that environment-gated rows are excluded and use 87.
As per path instructions:
**/*.md: Review Markdown files for factual accuracy against the codebase, broken links, and outdated information.Also applies to: 309-314
🤖 Prompt for 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. In `@TESTING.md` around lines 243 - 247, Update the conformance skip total in TESTING.md to match the current table: use 91 for all skipped rows, or explicitly exclude the 4 environment-gated rows and use 87. Ensure the surrounding explanation consistently reflects the chosen counting convention.Source: Path instructions
🤖 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 `@spec/04-expressions.md`:
- Line 23: Update the integer literal range-checking logic in the expression
checker branch that classifies negative values as INT to also reject values
below the signed 64-bit minimum with E149, while allowing -9223372036854775808.
Add coverage for both the valid minimum and the out-of-range
-9223372036854775809 case, preserving the existing upper-bound and Nat/Byte
checks.
In `@vera/lsp/convert.py`:
- Around line 60-62: Update the URI conversion flow in the relevant function to
call urllib.parse.urlsplit() before applying the scheme guard, then compare
parsed.scheme.lower() with "file" so mixed-case file schemes are accepted while
non-file schemes still return unchanged. Add a regression test covering a
mixed-case FILE URI.
In `@vera/lsp/features.py`:
- Around line 114-116: Update the verification flow around
session.verify_source() to append result.check_diagnostics to
analysis.diagnostics before result.verify_diagnostics, ensuring resolver errors
such as missing imports are published even when verification stops. Add an
integration test covering a source file that imports a missing module and
asserts the resulting LSP diagnostics include the resolver error.
---
Outside diff comments:
In `@TESTING.md`:
- Around line 243-247: Update the conformance skip total in TESTING.md to match
the current table: use 91 for all skipped rows, or explicitly exclude the 4
environment-gated rows and use 87. Ensure the surrounding explanation
consistently reflects the chosen counting convention.
🪄 Autofix
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 Plus
Run ID: 52e3c6fe-ab16-4770-a1bf-bce0cad21328
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (19)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdLSP_SERVER.mdREADME.mdROADMAP.mdTESTING.mdexamples/README.mdscripts/check_doc_counts.pyspec/04-expressions.mdtests/conformance/manifest.jsontests/test_checker_modules.pytests/test_codegen_modules.pytests/test_lsp.pyvera/README.mdvera/checker/registration.pyvera/lsp/convert.pyvera/lsp/features.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Verify pass (independent,
|
Closing round (
|
Closing-round verification (independent,
|
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/README.md (1)
87-87: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate the documented line count for
vera/checker/registration.py. The file contains 863 lines, not 817. Thevera/lsp/convert.pycount of 207 is correct.🤖 Prompt for 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. In `@vera/README.md` at line 87, Update the README table entry for vera/checker/registration.py from 817 to 863, leaving the vera/lsp/convert.py line count unchanged.
🤖 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 `@tests/module_fixture_helpers.py`:
- Around line 5-39: Update the resolved_module temporary-file setup so cleanup
begins before writing: assign the temporary path immediately after
NamedTemporaryFile opens, wrap write and flush operations in the try block, and
unlink the path in finally even when either operation fails. Apply the same
change to fake_resolved_module if it contains the duplicated pattern, and add a
regression test covering a write or flush failure.
In `@vera/lsp/convert.py`:
- Around line 83-91: Wrap the urllib.parse.urlsplit call in the URI conversion
function with a ValueError handler that returns the original URI when parsing
fails, while preserving the existing scheme, host, and pathname handling for
valid URIs. Add a regression test covering the malformed URI file://[.
---
Outside diff comments:
In `@vera/README.md`:
- Line 87: Update the README table entry for vera/checker/registration.py from
817 to 863, leaving the vera/lsp/convert.py line count unchanged.
🪄 Autofix
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 Plus
Run ID: 46ea4724-b36f-432a-9b1b-b378ff6d37fa
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (15)
CHANGELOG.mdFAQ.mdLSP_SERVER.mdREADME.mdROADMAP.mdTESTING.mdscripts/check_doc_counts.pytests/module_fixture_helpers.pytests/test_checker_modules.pytests/test_checker_types.pytests/test_lsp.pyvera/README.mdvera/checker/core.pyvera/checker/expressions.pyvera/lsp/convert.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
E154 closed the type namespace as a trio sharing one anchored regex — declare, bind, reference — and stopped there, so `effect VeraZed`, `ability VeraZed` and a `VeraZed(Int)` constructor all checked clean. Effect, ability and constructor names now go through the same regex, via one shared `_check_reserved_decl_name` the type/alias gate also calls, so the five rails cannot drift apart. The fix text is right per namespace: only a type position can be answered by writing the type out or declaring an alias, so the three new namespaces say rename and nothing else. `Veranda`, `Vera_thing` and a bare `Vera` stay ordinary names in all of them; the corpus was swept and nothing in it moved. Three conformance negatives complete the family, and the spec sentence, the E154 registry summary, the gate docstrings and the #1221 CHANGELOG bullet that anchored the open question are updated in lockstep. Closes #1260 Co-Authored-By: Claude <noreply@anthropic.invalid>
Two diagnostics that described a consequence rather than the cause. The LSP's per-function tier hints were synthesised from the whole obligation stream, which carries the imported modules an entry program pulls in. Those obligations' line numbers index the module that declared them, so an imported generic's hint was published at that line number in the CURRENT document — on whatever text happened to share it, or past the end. publishDiagnostics is per-URI, so a foreign obligation is not this document's to publish under any line; #1239's ProofObligation.file is what finally makes them distinguishable. A record with no file at all came from outside a verifier run, not from another module, so it keeps its hint. The literal range check knew the i64 and u64 bounds but not the Byte one, so a @byte context took 0..255 and let everything else fall through to @nat — and the literal's mistake was then described by whichever mismatch that produced downstream: E301 in a join, E202 at an argument, E170 under a let, E331 at a handler initialiser, a return-type mismatch in a body. All five are one E149 at the literal now, naming 0..255, and the literal keeps the type its context asked for so nothing cascades behind it. Three tests that pinned the old downstream wording assert the range message instead. Closes #1246 Closes #1252 Co-Authored-By: Claude <noreply@anthropic.invalid>
Six test files across five suites carried independent copies of the same temp-file ResolvedModule pattern — eleven definitions, since four were re-declared inside individual test bodies. They had drifted: one wrote its temp file and never unlinked it, leaking one per fixture built. tests/module_fixture_helpers.py holds the two shapes those copies were conflating. resolved_module parses a real temporary file, so file_path names something the pipeline can open; fake_resolved_module parses in memory under a deliberately non-existent /fake/ path, for the tests that never open it — the fake path fails loudly if one ever does. Both apply TESTING.md's Windows-portability rules, and TESTING.md now points at them from the section that states those rules, so the next multi-module test imports rather than writing a seventh copy. Proof: each of the six files runs the same number of tests before and after (116, 61, 186, 46, 45, 16), and breaking each helper turns all six red — so the shared module is load-bearing in every one. The #1240 remainder: examples/file_io.vera writes the RELATIVE path hello.txt and the host resolves it against the process CWD, so the documented `vera run examples/file_io.vera` from the repository root drops it in the ROOT — which is where `git add -A` twice picked it up — while the ignore rule named examples/hello.txt, the path a run from inside examples/ produces. Both are ignored now and the comment states the mechanism. Sweeping the corpus found no other example writing a relative path (IO.write_file is the only file-writing operation and file_io.vera is its only user), and `pytest tests/` from the repository root leaves `git status --short` clean. Closes #1228 Closes #1240 Co-Authored-By: Claude <noreply@anthropic.invalid>
Eight findings, one round. E154's rationale claimed a consequence that cannot happen on three of the four rails. The prelude's reserved namespace holds six type ALIASES and five type PARAMETERS and nothing else, so there is nothing for a reserved effect, ability or constructor name to re-type — with the gate bypassed, a reserved-name constructor compiles and runs, returning 42. The rationale now branches the way the fix-text already did: the type/alias rail keeps the re-typing consequence, the other three state the forward reason #1260 was decided on. A test asserts the branch per rail, and a second asserts the premise it rests on by walking the prelude — so a future prelude effect in that namespace fails there first. No automated gate can catch a false rationale; check_diagnostic_fields checks presence, not truth. The LSP fix from the previous commit was inert on the shipped path. server.py hands analyze() the document URI, and the pipeline uses its file= as a path — the module resolver reads imports from Path(file).parent, which for file:///a/b.vera is the directory `file:`. So a multi-module document resolved no imports, produced zero obligations and zero hints, and reported nothing: verify_source returns resolver errors as check_diagnostics, which analyze does not collect. uri_to_path joins the three coordinate conversions at that boundary, and Analysis carries both spellings because they answer different questions — the URI is what the client is told (a definition Location must carry one), the path is what the compiler was told and therefore what an obligation's file compares against. Non-file schemes pass through, which is what an unsaved buffer needs; LSP_SERVER.md's limitation row says so. E149's spec sentence enumerated Int and Nat only; it now states the Byte range and the refinement rule. A differential against the base measured the #1252 radius: eight shapes reroute, and a join with more than one out-of-range literal now reports one error per literal instead of one about the branches disagreeing. Positions that never push the Byte expectation into the literal are unchanged. The CHANGELOG bullet says what was measured rather than the five sites originally claimed. Also: the corpus-count gate read TESTING.md alone, so CLAUDE.md's and AGENTS.md's citations went stale where the gate's own output could not show them — all three are read now, anchored on the script name rather than a bare numeral. Six temp-file sites in test_codegen_modules.py never unlinked; one shared helper parses and removes, which is this PR's theme and takes that file's stray count to zero. The three new conformance fixtures take a `reserved_name` family tag, since an effect name is not a type name. examples/README.md credited io_operations.vera with three operations it does not call; a sweep of every Demonstrates cell found no others. Co-Authored-By: Claude <noreply@anthropic.invalid>
uri_to_path raised an uncaught URLError on any file:// URI with a
non-localhost authority under Python 3.14, which is the project's own
venv: url2pathname validates the authority itself and raises before the
UNC fold that was meant to handle it ever ran. analyze() calls the
conversion outside its try/except and analyze_and_publish has none, so it
left the didOpen/didChange handler. The old fold was wrong on every
version, not only 3.14 — 3.13 returned a //host/... string, which on
POSIX is a stray local path rather than a UNC mount.
The authority is decided here now, so the answer no longer depends on the
interpreter: this process can only open a local file, so a remote
authority names none and the URI comes back unchanged, as the opaque
label the pipeline already carries for non-file schemes. Same for a
degenerate URI decoding to the empty string — an empty file= is not "no
file" downstream, it is the process CWD, which is how an unrelated module
gets pulled into an unrelated document — and for anything url2pathname
rejects, caught as a backstop so a future validation cannot reopen the
escape. file:/// still means the root directory, which IS a path. Scheme
matching is case-insensitive per RFC 3986. Tests cover the foreign
authority, an IP authority, both degenerate forms, the root URI, the
uppercase scheme, and analyze() itself over every shape.
A refinement predicate's operands are synthesised twice, so
{ @byte | @Byte.0 < 18446744073709551616 } drew two E149s for one literal
naming two different bounds; the existing duplicate collapse could not see
it, since the messages differ. The unconstrained pass is a guess — u64
because nothing told it the target — so a contextual verdict supersedes it
and the guess is withdrawn. The reverse never happens, and an
unconstrained verdict standing alone is the #812 gate itself. Keyed on
the literal's occurrence, so two 999s in one call still report two errors.
Also from review: the module-fixture builders' docstrings claimed
resolved_module produced "a file the pipeline can open", which was never
true after the unlink — they differ by parse provenance, not by file
existence, and neither leaves a file behind; TESTING.md said the same
thing and a new test pins the real contract, including a cross-module
type-check against an already-deleted path. The corpus-count gate's
"reworded row is an error" held per document, so rewording one of
TESTING.md's two rows stayed green; each document now declares how many
citations it carries. The #1252 CHANGELOG note gains the non-join count
increase: g(999) against a two-parameter g reports the range violation
beside the arity mismatch, both true.
Co-Authored-By: Claude <noreply@anthropic.invalid>
The warm session rooted a ModuleResolver at Path(file).parent whenever it
had a file at all, and a document naming no location gives '.' — the
process CWD. So an untitled: buffer, a non-file: URI, a degenerate file:
or file://, or an empty label searched for imports wherever the language
server was started; a probe measured an unrelated glib.vera being pulled
out of that directory into a document that never referred to it.
Pre-existing rather than a regression, and never silent — the imports it
did NOT find still warned E230 — but what it did find, it used.
The resolver is now built only when file names a directory that exists and
is not '.'; anything else gets resolved_modules=[] and is analysed alone,
its relative imports reported through the same E230 because they cannot
meaningfully resolve. The rule sits at the session so both verify_source
callers obey it rather than one call site getting a special case — and the
second caller needed it: speculative_edit still passed the raw URI, so
after analyze moved onto the path earlier in this cycle the proof delta
was comparing two differently-keyed streams. An identical-text edit
reported unchanged: 0 with every obligation removed. The suite missed it
because its baseline was a second verify_source call spelling the document
the same way the speculative side did; it goes through analyze now, as the
server does.
My earlier note claimed returning the URI unchanged from uri_to_path
prevented the CWD rooting. It does not — Path("file:") is exactly as
directory-less as Path("") — and the test pinned the returned string
rather than the property, so it passed for the wrong reason. Both
docstrings say what is actually true, and the reviewer's probe is now the
test: same source, analysed from a directory that holds an importable
module and from one that does not, asserting no obligation belongs to a
foreign file, with the importable-from-a-real-path premise beside it so
the pair cannot both hold vacuously.
Windows CI repairs, same seam: two new TestUriToPath assertions compared
url2pathname output against POSIX-shaped literals, which that converter
only returns off Windows. Both are relational now — case-insensitivity is
"every spelling gives the lowercase spelling's answer, and is not the
input", and file:/// is "converted, and the result has no filename and is
its own parent", which holds of / and \ alike. The other seven assertions
in the class were audited and are already portable: they compare against a
path the test built, or against the input returned unchanged. TESTING.md
gains the rule as the assertion-side twin of the two path rules it already
carries, and CLAUDE.md's "three Windows-portability rules" is now five,
with the two it had never listed.
Co-Authored-By: Claude <noreply@anthropic.invalid>
Rebasing onto 3a7e928 (PR #1280) conflicted only in count-bearing prose and the negative-fixture rosters — no code file conflicted, and the diff-of-diffs confirms every one of the twenty-odd code files contributes byte-identically to what it contributed before the rebase. Both sides' additions are unions rather than choices. The conformance suite is 213: C8's three run-level programs and my three check-level negatives are disjoint. The corpus is 261. KNOWN_ISSUES' Bugs table is C8's row-id set exactly — #1281, #1277, #1268, #996 — with nothing dropped, nothing added and no duplicate #1277, which was the specific hazard since C8's branch carried that row. CHANGELOG keeps all five [Unreleased] bullets from the conflicting section, three of C8's and two of mine, and the sections merged cleanly elsewhere. Every number here is the oracle's at the merged tree, not arithmetic on the two branches: 10,282 tests across 160 files, 213 conformance programs, 261 corpus programs, 38 check-level entries, 31 negatives. docs/ is regenerated rather than hand-merged. One repair the oracle could not have caught. Resolving the first conflicted commit with `git checkout --ours TESTING.md` replaced the whole file, discarding the roster edits the same commit had auto-merged into untouched regions — the counts stayed right while the prose naming the fixtures silently reverted. The remaining commits were resolved hunk by hunk instead, and the roster is restored and checked against the manifest: all 31 negatives named in TESTING.md, CLAUDE.md and AGENTS.md, six E154s in the E-code list, and the six skip-table rows back. A count gate cannot see a missing name, so that check is a set comparison against the manifest rather than a number. Co-Authored-By: Claude <noreply@anthropic.invalid>
Final motion (
|
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
tests/test_lsp.py (1)
1059-1096: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winUse the converted-path baseline in the strengthening-edit test.
The new
SPEC_URIbaseline fixes the other speculative-edit tests, buttest_strengthening_edit_reports_newly_dischargedstill creates its baseline with rawfile:///w.vera.speculative_editconverts that URI to/w.vera, so obligation identities differ byfile. The assertion can pass even when the delta reports replacement rather than strengthening.Build that baseline through
analyze()and useSPEC_URIfor the speculative call.🤖 Prompt for 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. In `@tests/test_lsp.py` around lines 1059 - 1096, Update test_strengthening_edit_reports_newly_discharged to build its baseline through analyze() using SPEC_URI, matching the server’s converted-path baseline. Pass SPEC_URI to speculative_edit as well, so obligation identities use the same file value and the strengthening assertion validates the intended delta.
♻️ Duplicate comments (1)
vera/lsp/convert.py (1)
87-87: 🩺 Stability & Availability | 🟠 Major | ⚡ Quick winRestore handling for malformed file URIs.
urllib.parse.urlsplit()can raiseValueErrorforfile://[. The exception occurs before theURLErrorhandler. It can abort an LSP request and violates the total-function contract. CatchValueErrorand return the original URI. Keep the malformed-URI regression test.#!/bin/bash set -euo pipefail sed -n '80,100p' vera/lsp/convert.py python - <<'PY' from urllib.parse import urlsplit try: urlsplit("file://[") except ValueError: print("Confirmed: malformed file URI raises ValueError.") else: raise SystemExit("Expected ValueError for malformed file URI") PY🤖 Prompt for 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. In `@vera/lsp/convert.py` at line 87, Update the URI conversion flow around urllib.parse.urlsplit in the relevant conversion function to catch ValueError for malformed file URIs such as "file://[" and return the original URI, while preserving existing URLError handling and the malformed-URI regression test.
🤖 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 `@FAQ.md`:
- Line 280: Update the test total in the project status entry of FAQ.md from
10,282 to the verified 10,118 pytest tests, preserving the existing
conformance-suite detail.
In `@vera/obligations/session.py`:
- Around line 173-179: Update the parent-directory condition in the
import-resolution flow around ModuleResolver so Path(".") is accepted when
path.is_file() is true, preserving resolution for existing relative files.
Retain the current exclusion for opaque or non-existent labels and continue
returning no resolved modules in those cases.
---
Outside diff comments:
In `@tests/test_lsp.py`:
- Around line 1059-1096: Update test_strengthening_edit_reports_newly_discharged
to build its baseline through analyze() using SPEC_URI, matching the server’s
converted-path baseline. Pass SPEC_URI to speculative_edit as well, so
obligation identities use the same file value and the strengthening assertion
validates the intended delta.
---
Duplicate comments:
In `@vera/lsp/convert.py`:
- Line 87: Update the URI conversion flow around urllib.parse.urlsplit in the
relevant conversion function to catch ValueError for malformed file URIs such as
"file://[" and return the original URI, while preserving existing URLError
handling and the malformed-URI regression test.
🪄 Autofix
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 Plus
Run ID: c7e94a55-35e2-42ba-9569-97dfd93f04d9
⛔ 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 (16)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/08-modules.mdtests/conformance/manifest.jsontests/test_lsp.pytests/test_monomorphize_differential.pyvera/README.mdvera/lsp/convert.pyvera/lsp/extensions.pyvera/obligations/session.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
💤 Files with no reviewable changes (1)
- TESTING.md
The path-less isolation rule keyed on "the parent directory is '.'",
which is true of an untitled: buffer and equally true of entry.vera — a
real file whose directory happens to be the process CWD. So the rule
that stopped a path-less document borrowing the CWD's modules also took
the siblings away from a genuine relative-path one, measured at three
obligations instead of four with the import silently gone. is_file()
separates them: a document that exists on disk resolves against the
directory it actually lives in, whatever spelling names it.
analyze type-checks module-blind and then calls verify_source, which
type-checks module-aware, and only the second sees the resolver's errors
or anything needing an imported signature to detect. Those came back as
check_diagnostics and were dropped on the floor: glib::takes_int("nope")
published one warning, produced no obligations, and said nothing about
the E202 that had stopped verification; a missing import lost its E012
the same way. Appended now, minus what the blind check already reported,
because the module-aware pass re-derives those and a straight append
shows each twice — both halves are mutation-proved.
uri_to_path was still not total: urlsplit raises ValueError on a bad
authority (file://[ is "Invalid IPv6 URL") from inside the split itself,
before the guards that make the rest of it total, on the same
didOpen/didChange path the URLError escaped from.
Spec §4.2 described the integer range check in the wrong place. An
integer literal is always non-negative — a leading minus is negation over
the magnitude — so the upper bounds are checked on the literal and the
lower bound on the negation, whose operand may reach 2^63 and no further.
Both were already enforced; only the prose was wrong. Measured rather
than assumed: every IntLit the parser produces carries a non-negative
value, including for -9223372036854775809.
Also from review: the fixture builder's try/finally started after the
write, so a failed write stranded the file the contract promises to
remove; the strengthening-edit test still built its baseline from a raw
URI, so it passed whatever the delta said, and now goes through analyze
like its siblings, asserting that the surviving nat_sub obligation is
re-proved rather than replaced; TESTING.md's conformance-stage skip total
said 85 against a table of 91 and pytest's own 91, and is now gated
against that table — the third count in this PR that no gate was reading.
Two review findings verified and skipped. The scheme guard already
lowercases through urlsplit and is tested across three spellings. The
FAQ's 10,290 is the collected total, which is the convention the gate
reads and TESTING.md's headline uses; 10,126 is the passed count, and
that line is gated, at check_doc_counts' FAQ headline check.
Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai On the three outside-diff findings: TESTING.md (the conformance skip total) — real, fixed in efb8f5f: ground truth measured two ways (pytest reports 91 skipped; the table has 91 rows; the prose said 85), corrected AND anchored into check_doc_counts — the third count this PR has brought under the gate — with the gate proven red on both a stale total and a reworded-away sentence. vera/README.md (module-map line counts) — registration.py was already corrected to 863 in the rebase commit; the adjacent claim that convert.py's 207 was current went stale within this very round (the malformed-URI guard took it to 218, under the 10% threshold the oracle allows) — corrected. tests/test_lsp.py (the strengthening-edit test) — real, the same URI-keying bug one test over: it built its baseline from the raw file:// spelling while speculative_edit converts to the path, missed because it bypasses the fixed helper. Now routed through analyze — and the first repair's assertion was itself wrong (removed == [] fails legitimately since the requires text changes across the edit); the real discriminator is that the surviving nat_sub obligation must not appear in removed. Mutation-proved by reverting extensions.py. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '--- relevant symbols ---'
ast-grep outline scripts/check_doc_counts.py --items all --type function --view expanded
ast-grep outline tests/test_lsp.py --items all --type function --match 'strengthen|speculative|edit' --view expanded || true
printf '%s\n' '--- skip-total and gate references ---'
rg -n -C 3 '91 skipped|91.*skipp|skip.*91|conformance.*skip|skipped' TESTING.md scripts/check_doc_counts.py
printf '%s\n' '--- module-map line counts ---'
rg -n -C 2 'checker/registration\.py|lsp/convert\.py|863|218' vera/README.md
printf '%s\n' '--- strengthening-edit URI-keying assertions ---'
rg -n -C 8 'speculative_edit\s*\(|analyze\s*\(|nat_sub|removed' tests/test_lsp.pyLength of output: 129532
I verified the source changes. I did not execute the test suite. ✏️ Learnings added
🧠 Learnings usedYou are interacting with an AI system. |
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 `@CHANGELOG.md`:
- Line 25: Correct the CHANGELOG entry’s description of resolved_module to state
that the temporary file is deleted before the helper returns, so file_path is
not openable afterward. Describe the preserved parse provenance instead, and
align the wording with the corresponding TESTING.md and
tests/module_fixture_helpers.py documentation.
In `@tests/test_checker_modules.py`:
- Around line 57-73: Update resolved_module so the NamedTemporaryFile is closed
before os.unlink is called: move cleanup outside the with block while preserving
removal when f.write raises. Keep test_a_failed_write_leaves_no_temp_file
validating the original TypeError and run the test suite on a Windows worker.
🪄 Autofix
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 Plus
Run ID: 7cb9394b-adfc-4262-bad1-846f5e4bf640
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (14)
CHANGELOG.mdFAQ.mdREADME.mdROADMAP.mdTESTING.mdscripts/check_doc_counts.pyspec/04-expressions.mdtests/module_fixture_helpers.pytests/test_checker_modules.pytests/test_lsp.pyvera/README.mdvera/lsp/convert.pyvera/lsp/features.pyvera/obligations/session.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
The leak fix from the previous round was green on POSIX and red on all three Windows cells. Two rules meet in that helper and the obvious arrangement satisfies only one: delete=False means the temp file outlives its with-block, so a failed write must still remove it — but Windows cannot delete a file whose handle is open, so the unlink I put in an except beside the write is PermissionError WinError 32 there, not a cleanup. That is TESTING.md's own first fixture rule, broken by the fix for its own corollary. One cleanup site now covers every path: the name is captured and the try entered before anything that can fail, the with closes the handle however it exits, and the finally unlinks after it. The sibling helper in test_codegen_modules.py had the same latent write-failure window and takes the same shape. The ordering is observable without a Windows machine — record whether the handle is closed at the moment each unlink is issued — so it is a test rather than a note, and it goes red on the exact shape CI rejected. An AST sweep for the general form (an unlink anywhere inside an open NamedTemporaryFile block) found that one site and now finds none; the first, text-based version of that sweep reported a clean zero because a multi-line with-header defeated its indentation scan, which is why it was rewritten before being trusted. TESTING.md records the sequencing corollary under the rule it belongs to, with both shapes. Also from review: the CHANGELOG still described resolved_module as producing "a file the pipeline can open" — the claim the docstring and TESTING.md had already been corrected away from in this PR, and the one place I missed. It now says what the other two say: parse provenance, deleted before return, neither builder leaving a file behind. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai On the outside-diff finding for vera/README.md line 87 (registration.py 817 → 863): verified at the MERGED tip — the table already reads 863, matching the file's measured 863 lines exactly, and convert.py's entry reads 218 matching its 218. The correction landed in the rebase-reconciliation commit (f30e353) before this review's suggestion was posted against an earlier head; the later closing rounds then kept both counts current as the files grew. Nothing outstanding. |
|
Tip For best results, initiate chat on the files or code changes.
You are interacting with an AI system. |
test_a_failed_write_leaves_no_temp_file snapshotted gettempdir() for *.vera either side of the call it measures. CI runs pytest -n auto, so that directory is shared by every xdist worker, each writing its own tmp*.vera: a sibling worker's fixture, alive for the microseconds between the snapshot and the assertion, counted as litter this test had left. It did -- AssertionError over a C:\...\tmp*.vera on worker gw1 in the v0.1.10 release push, an hour after the identical tree passed, and reproduced here at 210/300 with a second PROCESS writing into that directory. A thread cannot stand in for the worker: it reaches this process's patched globals, which no worker can, and produced failures of its own that the fixed test is right to ignore. The evidence is now the ONE path the call created, captured from NamedTemporaryFile the way the sibling ordering test captures handles. No shared directory is read at all, so the race is removed rather than relocated to a private TMPDIR -- which would still assert over a directory, and would additionally have to reset tempfile's cached tempdir for the env override to take effect. Same instrument: 0/300. A len(created) == 1 guard keeps the check from passing over an empty list should the builder stop creating its file that way. Both halves are mutation-validated: the pre-aallan#1282 leaking cleanup turns it red naming the stranded path, and switching the builder to mkstemp turns it red on the guard. The siblings from that PR were audited and need no isolation. test_the_handle_is_closed_before_every_unlink asserts over in-process traces (its own handle list and unlink log) that a separate worker cannot reach -- 0/60 under the same adversary -- and test_neither_builder_leaves_a_file_behind names its own unique path rather than reading the directory it sits in. TESTING.md records the rule under Test Fixture Conventions, where CI's parallelism makes it general: evidence about temp files names them. Also, from the release-surface audit: README's status line and HISTORY's "By the numbers" total both said 206 releases against 207 tags -- accurate at v0.1.5, two behind since v0.1.8, and agreeing with each other the whole way down, which is why the cross-check between them never saw it. Both now say 208 (207 tags plus the v0.1.10 tag release.yml creates after the merge), and check_doc_counts.py reads git tag as the oracle: exact equality once the version is tagged, the single pending tag of a release being cut as the only slack, and a printed skip where a checkout has no tags, since that is absence of evidence rather than zero releases. Co-Authored-By: Claude <noreply@anthropic.invalid>
1 participant
Part of the #1213 burndown (PR C.6) — the hygiene tail. Three commits, six items.
What this changes
#1260 — the
Vera-prefix reservation covers every declaration namespace (86e4283f; maintainer-ratified language change, full DESIGN.md derivation on the issue).effect VeraZed,ability VeraZed, and a constructorVeraZed(Int)— all accepted at base, RED-proofed — are now E154, through one shared_check_reserved_decl_namethat the type, alias, effect, ability, and constructor rails all call: one regex, five rails, none can drift. Fix-text is per-namespace (only the type-reference gate offers the alias escape; the three new rails say rename). Three conformance negatives complete the family; spec §8.4.1 states the full scope. Corpus blast radius re-measured: zero.#1252 — an out-of-range Byte literal is named for what it is (
e65205da). The right fix was routing, not rewording:@Bytewas absent from the literal range check entirely, so the violation surfaced as whatever downstream disagreement it caused — E301 in a join, E202 at an argument, E170 under alet, E331 at a handler initialiser, or a return-type mismatch. A literal outside 0..255 is now E149 ("out of range for@Byte; the range is 0..255") at the source, with no cascade, replacing the misleading message at all five sites.#1246 — LSP tier hints stay in their own document (
e65205da). A hint from an obligation whosefileis another module no longer lands at the current document's line numbers; records without a file (built outside a verifier run) keep their hints, pinned separately.#1228 — one fixture-helper module (
265244ab). The six duplicated_resolvedhelpers (plus four re-declared inside test bodies) consolidate intotests/module_fixture_helpers.py— the copies were genuinely TWO semantics (real-temp-file vs in-memory), both preserved and exported. One leaked temp file fixed in passing. Identical per-file pass counts before/after, and a raise-mutation proves the shared module is load-bearing in every consumer.#1240 — the example litter is actually caught now (
265244ab). The previously-landed ignore was aimed at/examples/hello.txt, buthost_write_fileis CWD-relative, so the documentedvera run examples/file_io.veradropshello.txtin the repo ROOT — reproduced, both paths now ignored with the mechanism stated correctly. Sweep:IO.write_filehas exactly one user across examples and conformance; four fullpytestruns from the root leavegit status --shortclean.#1217 — no change needed: already fixed at base by PR #1224's explain-slots work (the issue carries the maintainer's close-at-release comment; verified live — where-helper tables print, with the CLI citing the issue). Deliberately not claimed here; the release PR carries its close line.
Closes #1228.
Closes #1240.
Closes #1246.
Closes #1252.
Closes #1260.
(Keywords take effect at the release PR. #1217's close line rides the release PR directly, its fix having shipped in #1224.)
Summary by CodeRabbit
Bug Fixes
@Byteliteral validation, accepting values from 0–255 with clearer diagnostics.Documentation