fix(verus): the new gate failed its first run — bazel //... walked an agent worktree - #367
Merged
Conversation
… agent worktree verus.yml (#366) ran once and FAILED. Diagnosing it is the point: the workflow existed for about an hour and immediately surfaced two real problems, one of them repo-wide. ROOT CAUSE — not the proofs. `bazel query 'kind("verus_test rule", //...)'` never got as far as the proofs: ERROR: error loading package '.claude/worktrees/rules_verus': Label '//verus:defs.bzl' ... `//...` walks agent worktrees under .claude, which contain SIBLING repos (rules_verus, rules_lean) whose BUILD files are not part of this module. Bazel tries to load them and dies. My empty-set guard then fired correctly — "no verus_test targets found" — so the workflow failed loudly rather than passing green having verified nothing. The guard did its job; the query was wrong. TWO FIXES, because one of them is bigger than this workflow: 1. .bazelignore with `.claude`. ANY workflow using `//...` hits this same wall; scoping each query around it treats the symptom. The repo had no .bazelignore at all. Verified: `kind("verus_test rule", //...)` goes from ERROR to 19 targets. 2. Scope the query to `//:*` anyway. Every verus_test is declared in the root BUILD.bazel, so the narrower query is both correct and immune to whatever else appears in the tree later. Belt and braces — measured, both forms now return 19. ALSO: the step was still named "Kernel-check every Lean proof". verus.yml was generated from lean.yml and I renamed the workflow, the job and the command but not the step label — so the failing step in the UI claimed to be checking Lean proofs while running a Verus query. Same class as the "invoked 2+ times" log that stated a threshold the code did not implement. Renamed to "Run every Verus proof". Worth recording what this run bought: an entire proof track had been silent for its whole existence, and within one run of enforcing it we learned the Bazel query surface was broken repo-wide. That is what the track being unenforced was hiding — not necessarily failing proofs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
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.
Verify-Filter: (has-tag "verus")
verus.yml(#366) ran once and failed. Diagnosing it is the point: the workflow existed for about an hour and immediately surfaced two real problems, one of them repo-wide.Root cause — not the proofs
The query never got as far as them:
//...walks agent worktrees under.claude, which contain sibling repos (rules_verus,rules_lean) whose BUILD files are not part of this module. Bazel tries to load them and dies.My empty-set guard then fired correctly — "no verus_test targets found" — so the workflow failed loudly instead of passing green having verified nothing. The guard did its job; the query was wrong.
Two fixes, because one is bigger than this workflow
1 ·
.bazelignorewith.claude. Any workflow using//...hits this same wall; scoping each query around it treats the symptom. The repo had no.bazelignoreat all.Verified:
kind("verus_test rule", //...)goes from ERROR → 19 targets.2 · Scope the query to
//:*anyway. Everyverus_testis declared in the rootBUILD.bazel, so the narrower query is both correct and immune to whatever else appears in the tree later. Measured — both forms now return 19.Also: the step name lied
It was still
"Kernel-check every Lean proof".verus.ymlwas generated fromlean.yml; I renamed the workflow, the job and the command but not the step label — so the failing step in the UI claimed to be checking Lean proofs while running a Verus query.Same class as the
"invoked 2+ times"log that stated a threshold the code didn’t implement. Renamed to "Run every Verus proof".What this run bought
An entire proof track had been silent for its whole existence, and within one run of enforcing it we learned the Bazel query surface was broken repo-wide. That is what the unenforced track was hiding — not necessarily failing proofs.
🤖 Generated with Claude Code