From 8501d775a1adc3bc3cbb80bd98773724b704e058 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 26 Aug 2026 21:49:40 +0200 Subject: [PATCH] =?UTF-8?q?fix(verus):=20the=20new=20gate=20failed=20its?= =?UTF-8?q?=20first=20run=20=E2=80=94=20bazel=20//...=20walked=20an=20agen?= =?UTF-8?q?t=20worktree?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- .bazelignore | 12 ++++++++++++ .github/workflows/verus.yml | 9 +++++++-- 2 files changed, 19 insertions(+), 2 deletions(-) create mode 100644 .bazelignore diff --git a/.bazelignore b/.bazelignore new file mode 100644 index 0000000..d9080be --- /dev/null +++ b/.bazelignore @@ -0,0 +1,12 @@ +# Agent worktrees and scratch checkouts. These contain sibling repos +# (rules_verus, rules_lean, ...) whose BUILD files are NOT part of this +# module, so `bazel query //...` tries to load them and fails: +# +# ERROR: error loading package '.claude/worktrees/rules_verus': +# Label '//verus:defs.bzl' ... +# +# That broke verus.yml on its very first run. ANY workflow using `//...` +# hits the same wall, so ignore it at the source rather than scoping every +# query around it. Verified: with this file, `bazel query +# 'kind("verus_test rule", //...)'` returns 19 instead of erroring. +.claude diff --git a/.github/workflows/verus.yml b/.github/workflows/verus.yml index 799a4a1..a688f08 100644 --- a/.github/workflows/verus.yml +++ b/.github/workflows/verus.yml @@ -96,7 +96,7 @@ jobs: disk-cache: bazel repository-cache: true - - name: Kernel-check every Lean proof + - name: Run every Verus proof working-directory: relay # //proofs/lean:all is bazel's implicit all-rules target — every # lean_library + lean_proof_test in the package, so a newly added @@ -105,7 +105,12 @@ jobs: # QUERY, do not enumerate. This workflow exists because 19 verus_test # targets were defined and none was ever executed (#364) — a hand-written # target list is exactly the drift that produced that. Discover them. - TARGETS=$(bazel query 'kind("verus_test rule", //...)' 2>/dev/null | tr '\n' ' ') + # Scope to the ROOT package: that is where every verus_test is + # declared. `//...` additionally walks agent worktrees under .claude + # (now covered by .bazelignore too) and dies loading a sibling repo's + # BUILD file — which is exactly how this workflow failed its first + # run. Measured locally: this returns 19. + TARGETS=$(bazel query 'kind("verus_test rule", //:*)' 2>/dev/null | tr '\n' ' ') if [ -z "${TARGETS// /}" ]; then echo "::error::no verus_test targets found — the Verus track would silently verify NOTHING" exit 1