chore(deps): get z3 0.21 a real verdict (#965) — the v0.64 retraction promised one and recreate never fired - #1202
Merged
Merged
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…promised one and `recreate` on a closed PR does nothing v0.64 retracted a fabricated attribution: I closed #1108 as "breaks the Bazel build" on a mechanism the Bazel graph cannot exercise (there is no z3-sys in it — `crates/BUILD.bazel:167-170`), when the actual failure was a 504 fetching bazel-skylib. The retraction, the CHANGELOG and RQ-64-DEPS all say the bump was "sent for recreate and a real verdict". IT WAS NOT. `@dependabot recreate` on a CLOSED PR does nothing, and no z3 bump has reappeared. So the promise in that retraction is currently unkept — which is a smaller version of the same defect the retraction was about: stating an outcome that has not happened. This raises the bump by hand so CI produces the verdict on a current base: z3 0.20 -> 0.21, pulling z3-sys 0.11 -> 0.13. The discriminators are the required `Bazel Build & Proofs` and `Z3 Verification` contexts — the latter being the separate `--features z3-solver` build a plain `cargo test --workspace` never exercises (#836). NO PREDICTION IS MADE HERE about whether it passes. That was the original error. Whatever CI reports is the verdict, read from the failure's CONTENT and not from its job name. z3 is `optional = true` behind `z3-solver` — the differential oracle, not the default engine (ordeal has been default since v0.27) — so this cannot change shipped codegen either way. Refs #965, #849, #836
avrabe
force-pushed
the
chore/z3-021-verdict
branch
from
September 8, 2026 21:02
577f3f1 to
e67e15b
Compare
avrabe
added a commit
that referenced
this pull request
Sep 8, 2026
…roduced; the bump is FINE and the hold has still never caught anything (#1212) v0.64 published a fabricated attribution (#1108 "breaks the Bazel build", on a mechanism `crates/BUILD.bazel:167-170` says cannot occur) and retracted it. The retraction then promised a remedy that never fired: `@dependabot recreate` on a CLOSED PR does nothing. So "sent for recreate and a real verdict" was itself an unkept promise — a smaller instance of the same defect the retraction was about. The bump was raised by hand in #1202 with NO PREDICTION ATTACHED, because predicting was the original error. CI answered: Bazel Build & Proofs pass Z3 Verification pass (the separate --features z3-solver build) 9/9 required, 0 failures z3 0.20.2 -> 0.21.0, pulling z3-sys 0.11 -> 0.13, does NOT break the Bazel build. The 504 fetching bazel-skylib was the whole story. Merged. CONSEQUENCE, stated because it is the part that mattered: the enforced dependabot hold has STILL never caught a breaking 0.x-minor. It remains unfalsified. v0.64 published the opposite as its headline evidence for that gate, which is precisely why the claim was worth retracting — a rule that gets credit it has not earned is worse than one with no evidence, because nobody looks again. Recorded by APPENDING the outcome rather than rewriting the original correction: both the fabrication and its resolution stay visible, which is the same discipline applied to VG-009 and to the FLOORPROSE premise. Verified: rivet at main's 40-error cross-repo baseline with 0 broken cross-refs, status_evidence exit 0, claim_check 62/62. Refs #965, #849, #836
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.
Getting z3 0.21 a real verdict — because the retraction promised one
v0.64 retracted a fabricated attribution: I closed #1108 as "breaks the Bazel
build", blaming
z3-syslinking system libz3, whencrates/BUILD.bazel:167-170says there is no z3-sys in the Bazel graph at all. The real failure was a
504 Gateway Time-out fetching
bazel-skylib.That retraction — and the CHANGELOG, and
RQ-64-DEPS— all say the bump was"sent for recreate and a real verdict."
It wasn't.
@dependabot recreateon a closed PR does nothing, and no z3bump has reappeared. So that promise is unkept, which is a smaller version of the
same defect the retraction was about: stating an outcome that hasn't happened.
This raises the bump by hand so CI can answer on a current base:
z3 0.20 → 0.21, pullingz3-sys 0.11 → 0.13.No prediction is made about the result. That was the original error. The
discriminators are the required
Bazel Build & ProofsandZ3 Verificationcontexts — the latter being the separate
--features z3-solverbuild a plaincargo test --workspacenever exercises (#836). Whatever CI reports is theverdict, read from the failure's content, not its job name.
z3isoptional = truebehindz3-solver— the differential oracle, not thedefault engine (ordeal has been default since v0.27) — so this cannot change
shipped codegen either way.
Refs #965, #849, #836