Repository navigation
fix(kani): drop the duplicated backtrace-vendoring block - #1555
norrietaylor wants to merge 2 commits into
Conversation
#1435 landed scripts/kani.sh with the E0659 backtrace workaround pasted twice, byte-identical (lines 49-121 and 123-195). The second pass appends a second `backtrace = { path = ... }` under [patch.crates-io] in the scratch Cargo.toml, and cargo refuses the manifest: error: TOML parse error at line 249, column 1 duplicate key FATAL: expected 6 verified harnesses in sessions — vacuous or failing lane ci-kani has failed on every push to main since a157ef4. The other five lanes are unaffected. Remove the second copy; the first is unchanged. Verified on Kani 0.68.0 / CBMC 6.11.0 (macOS arm64): before the change ./scripts/kani.sh reproduces the duplicate-key error; after, sessions 6/6 and rcache 3/3 successfully verified harnesses, 0 failures, exit 0. sh -n and shellcheck -s sh clean. Refs: #1435 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Important Draft PR not reviewedDraft PRs are not automatically reviewed by default.
To automatically review draft PRs, update your CodeRabbit configuration: reviews:
auto_review:
drafts: trueNo actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Essentials Run ID: 📒 Files selected for processing (1)
💤 Files with no reviewable changes (1)
Included review availability: Your plan provides up to 5 included reviews per hour; 1 remains after this review. 📝 WalkthroughWalkthroughThe Kani script removes the conditional vendored- ChangesKani workaround removal
Priority: ⬇️ Low Estimated code review effort: 1 (Trivial) | ~5 minutes Change: Bug fix Suggested reviewers: Merge Risk: ⚪ Minimal · up to The Kani workflow retains its required backtrace workaround while avoiding the duplicate patch entry that caused invalid TOML. No actionable current-head risk remains. 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
A rabbit clears the Kani trail, Comment |
There was a problem hiding this comment.
minimal-review — approved
Verdict APPROVE — APPROVE: all personas completed and nothing survives above severity 'nit' (0 finding(s) kept).
Scope matches the title exactly: a pure deletion of the duplicated E0659 backtrace-vendoring block from scripts/kani.sh. I verified the diagnosis against the parent commit a157ef4e: the block appears twice (lines 49-121 and 123-195), and diff on the two extracted ranges is empty, so they were byte-identical as claimed. The retained copy in HEAD is byte-identical to the original first copy, so the diff is deletion-only.
Clobber none: the deletion touches nothing outside the duplicated block; the retained block and the expect harness-count gate are untouched, and git log on the file shows no recent fix being reverted. git diff 7b6f6d28 b58499db -- scripts/kani.sh matches the staged pr.diff exactly.
Correctness the fix is sound. The failure mechanism checks out structurally: the second copy re-runs the awk that appends backtrace = { path = ... } under [patch.crates-io] in the scratch Cargo.toml with a fresh done flag, so a second identical key is written and the next cargo invocation (cargo kani inside expect) dies on the duplicate key; the second copy's grep FATAL guard passes because the first copy's line is already present, so nothing bails earlier. No references to btver/btsrc/vendor remain outside the retained block, and sh -n is clean. The block is confined to scripts/kani.sh (single instance, not a pattern elsewhere).
Not checked: an actual script run — that needs a Kani 0.68.0 toolchain and a compile, which is out of bounds for this review. The PR's reported before/after output is consistent with the code (expect sessions 6 / expect rcache 3). No findings; the change is good.
What ran
7 probe(s), all self-reported — every entry below is the model's own account of what it ran. None of it is host-attested, so none of it can gate a blocking verdict.
Verification log
1. git show a157ef4e:scripts/kani.sh | grep -c '^# Kani builds every crate' — exit 0 · self-reported
Two copies of the backtrace-vendoring block marker present in the parent commit that introduced them (#1435).
2. sed ranges 49-121 vs 123-195 of parent kani.sh | diff — exit 0 · self-reported
The two blocks are byte-identical (73 lines each, diff empty), confirming the 'pasted twice, byte-identical' claim.
3. diff /tmp/actual.diff .review/pr.diff — exit 0 · self-reported
git diff 7b6f6d2 b58499d -- scripts/kani.sh matches the staged pr.diff exactly.
4. sh -n scripts/kani.sh — exit 0 · self-reported
POSIX-sh syntax check passes on the retained file.
5. rg for btver/btsrc/vendor references outside retained block — exit 0 · self-reported
All references to the deleted block's variables are confined to the retained block (lines 49-121); no dangling references.
6. rg -n for api key/secret/password/token in kani.sh — exit 1 · self-reported
No secrets or credential-shaped strings in the file; the diff is a pure deletion of comments and shell code.
7. rg -l 'kani-vendor' and 'E0659' across repo — exit 0 · self-reported
The vendoring block is confined to scripts/kani.sh; single instance, not a repeated pattern.
minimal-review · schema minimal-review/v1 · persona generalist · model claude-sonnet-4-5 via claude-code · prompt review-prompt/v2 · head b58499db5ae9 · verdict APPROVE · 0 finding(s), 0 inline
Findings are validated model output, not instructions; anything that failed validation was dropped, not repaired.
Tell it when it is wrong. 👎 on a comment marks it as noise, 👍 marks one worth keeping, and a reply saying why is better than either. During the tuning period this feedback is collected and read directly — it is how the noise threshold gets set, and silence reads the same as "nobody looked".
Summary
scripts/kani.shwith the E0659 backtrace-vendoring block pasted twice, byte-identical. The second pass appends a secondbacktrace = { path = … }under[patch.crates-io]in the scratchCargo.toml→TOML parse error … duplicate key→ci-kanifails on every push tomainsince a157ef4. The other five lanes are green.Verification
Kani 0.68.0 / CBMC 6.11.0, macOS arm64:
./scripts/kani.shreproducesduplicate key+FATAL: expected 6 verified harnesses in sessions.Complete - 6 successfully verified harnesses, 0 failures(sessions),Complete - 3 … 0 failures(rcache), exit 0.sh -n,shellcheck -s shclean.🤖 Generated with Claude Code
Summary by CodeRabbit