chore: unblock CI — revert 5 dependabot major bumps + .trusted-base-ignore FP fix + deno.lock populate#128
Merged
hyperpolymath merged 3 commits intoMay 30, 2026
Conversation
Five dependabot major bumps merged 2026-05-29 in a single chain without the call sites being updated: #120 axum 0.7.9 → 0.8.9 #121 rand 0.9.4 → 0.10.1 #122 criterion 0.5.1 → 0.8.2 #123 nom 7.1.3 → 8.0.0 #124 rustyline 15.0.0 → 18.0.0 All five auto-merged green (per the estate's auto-merge hook) because `Validate K9 contracts` / `governance / Code quality` are content checks that don't compile the workspace. The real `Rust CI` job and the `Live Provers` workflow have been red on `main` for every push since: error[E0599]: no method named `random_range` found for struct `StdRng` in the current scope --> src/rust/agent/swarm.rs:250:32 ::: .../rand-0.10.1/src/rng.rs:159:8 error[E0618]: expected function, found `Choice<(fn(_) -> Result<…>> --> src/rust/provers/lean.rs:24:38 [nom 8's `alt(...)` no longer returns a callable closure] Root cause: each bump shipped a real API break that needed call-site updates: * rand 0.10 renamed the `Rng` trait to `RngExt` (because upstream `rand_core` renamed `RngCore` → `Rng`). Existing `use rand::Rng` no longer imports `random_range` / `random` methods. * nom 8 moved from closure-based to trait-based combinators — `alt(args)(input)` is now `alt(args).parse(input)` everywhere. * axum 0.8, criterion 0.8, rustyline 18 also ship breaking changes that the call sites have not been updated for (reverted in the same commit to keep CI green; bumping any one of them individually requires the matching code update). Resolution: revert all five back to the May-28 working state. Locally `cargo check --lib` cleans in ~2 min against this lockfile. The bumps are NOT being thrown away — they should land again as 5 follow-up PRs, each bundling the matching code update. That keeps "dependabot caught a major version" signal alive while preventing this class of break. Effect: `Rust CI`, `Live Provers` (Tier-1 + Tier-2 matrices) and `MVP Smoke` should return green on this branch. Refs: #92 (broader baseline failures — this PR addresses the compile-error slice that gates everything downstream).
3 tasks
…kfile `deno.lock` has been an empty (0-byte) file since commit 3b03087 ("chore: track (empty) deno.lock for M5 sweep", 2026-05-21). Deno 2.x treats empty lockfiles as a parse error: error: Failed reading lockfile at '/.../deno.lock' Caused by: Lockfile was empty The estate governance check (`governance / Language / package anti-pattern policy` in governance-reusable.yml) runs `deno run --allow-read .standards-checkout/scripts/check-ts-allowlist.ts` which fails on lockfile parse before reaching the actual `.ts` walk. Fix: write the minimal valid Deno-2 lockfile JSON: { "version": "4", "remote": {} } This preserves the "track lockfile" intent of 3b03087 (the file stays committed and visible to estate-wide sweeps) while letting Deno 2.x parse it. When real remote imports are added, `deno cache --lock` will populate the `remote` object on its own. Effect: `governance / Language / package anti-pattern policy` returns green; the check-ts-allowlist.ts walker actually runs. Refs: #92 (the broader baseline failures, this PR addresses the language anti-pattern slice only).
2 tasks
The estate's check-trusted-base.sh (standards#203) flagged 12 markers on main since #112 (2026-05-28) — all 12 are detector-pattern false positives, structurally identical to the believe_me FP audit recorded in docs/PROOF-NEEDS.md §"believe_me audit (2026-05-18)" (21 hits, zero real escapes). Resolution: * 10 Rust hits across 4 files are pattern-detector tables. Each holds a `Vec<DangerousPattern>` (or equivalent) that *enumerates* the very `unsafePerformIO` / `unsafeCoerce` / `Obj.magic` strings the scanner is hunting. The scanner's naive substring grep can't tell "uses the pattern" from "names the pattern in a detector table". Added a new `.trusted-base-ignore` (whole-path exemption, format mirrors the scanner's documented spec) covering the four files: - src/rust/verification/axiom_tracker.rs - crates/echidna-core-spark/src/axiom_tracker.rs - src/rust/corpus/agda.rs - src/rust/corpus/idris2.rs * 2 Agda postulates are real well-justified axioms: - `funext` (function extensionality) in proofs/agda/Basic.agda - `Conflicts` (abstract parameter) in proofs/agda/SoundnessPreservation.agda Both already had INTENTIONAL AXIOM / INTENTIONAL PARAMETER prose documentation, but outside the script's 5-line preceding-marker window. Added an `-- AXIOM:` / `-- TRUSTED:` magic-word line immediately before each `postulate` so the scanner sees it. Effect: `governance / Trusted-base reduction policy` should now report [OK] (12 markers exempted via .trusted-base-ignore + inline magic), up from the 12/12 undocumented failure on main. Refs: #92 (broader baseline failures, this PR addresses the trusted-base slice only).
3 tasks
hyperpolymath
changed the title
This was referenced May 30, 2026
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
`MVP Smoke (Best Effort)` has been failing with exit code 127 on every push: /home/runner/work/_temp/…/sh: line 1: just: command not found ##[error]Process completed with exit code 127. The workflow's final step is `just --justfile Justfile mvp-env`, but the `ubuntu-latest` runner image does not include `just` and no step installs it. Adding the canonical SHA-pinned `taiki-e/install-action` between `Cache Cargo` and `Build release` (also runtime-relevant for the smoke recipe) restores green. SHA pin (`184183c… # v2.78.1`) matches the estate convention already used across hypatia (ci.yml, security.yml, tests.yml, build-gossamer-gui.yml). Tool selector `tool: just` is the standard single-package form. Effect: `MVP Smoke (Best Effort)` returns success on this branch and on every subsequent push to `main`. Refs: noted as one of the orthogonal failures on PR #128's checks during the 2026-05-30 dependabot-deadlock triage.
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
…ridge Chapel-CI has been red on every push since the workflow + sources were authored (commit e44815a, 2026-04-20) — zero successful runs in the 100-run history. Two independent pre-existing breakages: ## Job 1: `Compile Chapel Metalayer` — `extern "C" { ... }` parse error `chapel_ffi_exports.chpl` wrapped its 35 prover-id / category-id `c_int` constants in a single `extern "C" { ... }` block. That syntax is the Chapel "extern blocks" feature, which requires the Chapel compiler to be built with LLVM + clang headers available. The official `chapel-2.3.0-1.ubuntu24.amd64.deb` the workflow installs is not built with that combination — so the parser bails at line 29: chapel_ffi_exports.chpl:29: syntax error: near '{' … parallel_proof_search.chpl:186: syntax error: near 'proc' (cascade) The constants are also `#define`d on the C side in `src/zig_ffi/chapel_ffi_exports.h` — that is the canonical copy any non-Chapel consumer reads. The Chapel copy only needs to be visible to Chapel code; emitting it as a C-visible symbol via an `extern` block is unnecessary. Dropping the wrapper and keeping the 35 declarations as plain module-level `const`s fixes the parse without losing any contract. (Documented in-place; the comment block above the constants points to the C header as the source of truth.) ## Job 2: `Build & Test Zig FFI Bridge` — Zig 0.14 API on 0.13 install `src/zig_ffi/build.zig` line 1 already documents `// Compatible with Zig 0.14+/0.15+`. Lines 23, 52, 74 use `b.addLibrary(.{ ... .linkage = … })` which is the 0.14+ unified `Build.addLibrary` API; Zig 0.13 only exposes the older `addSharedLibrary` / `addStaticLibrary`. The workflow pinned `mlugg/setup-zig@… with: version: 0.13.0` for both `zig-ffi` and `rust-chapel-real` jobs, so every run hit: build.zig:23:18: error: no field or member function named 'addLibrary' in 'Build' Bumping both pins to `0.14.0` matches what the source already declares. ## Effect Both jobs should compile on this branch. `rust-chapel-feature` (Job 3) was previously skipped via the `needs: zig-ffi` dependency — with Job 2 green, Job 3 actually runs. Job 4 (`rust-chapel-real`) is `continue-on-error: true` so its outcome stays advisory. Surfaced during the 2026-05-30 dependabot-deadlock triage as one of the orthogonal failures on PR #128. None of these jobs are required checks, so this PR doesn't unblock anything blocking the merge queue — it just makes Chapel L2.1 actually verifiable on CI for the first time, which matters as L2.2-L2.7 land. Refs: handover/TODO.md P3 "L2.1 ✅ Done" — the "done" status was based on local builds; CI verification has been broken from day 1.
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
## Summary
Targeted sync of five drifted rows in `docs/ROADMAP.md` to what
`handover/TODO.md`, `handover/STATE.md`, `docs/PROVER_COUNT.md`, and the
commit history actually say. No new claims, no scope change — pure
stale-row cleanup.
## Corrections
| Row | Before | After | Authority |
|---|---|---|---|
| §2 stage 1c | `[in progress, 28 to go]` | `[done 2026‑04‑26 ✓ — 50/50
named extractors]` | TODO.md S1 batches (12+20+6 = 50) |
| §2 stage 4c | `[86/91 done; 5 suggest_tactics stubs remain]` | `[91/91
real impl ✓; 5 still heuristic-only — GNN-ranking is end-state]` |
PROVER_COUNT.md §TL;DR |
| §3 row "Every important solver" Today | `5 suggest_tactics stubs` |
`91/91 with real suggest_tactics (5 still heuristic-only)` | same |
| §4 row S1 status | `in flight` | `done 2026‑04‑26 ✓ (50/50)` | same |
| §4 row S4 status | `design pending — needs Verisim schema` | `wired
2026‑04‑27 ✓` (read paths + write path + tests/s4_loop_closure.rs) | The
doc's own §4 "Sprint critical path" subsection already says this |
| §4 row S5 status | `partly done — 86/91 already real` | `mostly done —
91/91 real; gnn_augment_tactics wired into 5 pilots per c4bc272` |
PROVER_COUNT.md + commit log |
| Header "Last revised" | 2026‑04‑20 | 2026‑05‑30 (prior date preserved)
| this PR |
## Why now
Found during a wider triage of open issues + active CI work. The 5 rows
above conflict with documents/commits/code that explicitly disagree; per
§7 ("When a stage sub-item lands, mark its line [done YYYY‑MM‑DD ✓]"),
they were due for an update.
## Test plan
- [x] Each correction verified against the cited authority.
- [x] No new claims; only stale-row sync.
- [ ] CI: no code changes, governance/lint should pass.
## Notes
This PR addresses **only** the truthfulness drift. The broader CI red on
`main` (compile errors from the dependabot major bumps) is being
addressed in PR #128.
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
…ridge (#131) ## Summary Fixes two pre-existing, independent breakages that have kept `Chapel Accelerator CI` red on every run since it was first authored (2026-04-20, commit e44815a) — zero successes in the 100-run history. | Job | Symptom | Root cause | Fix | |---|---|---|---| | `Compile Chapel Metalayer` | `chapel_ffi_exports.chpl:29: syntax error: near '{'` (cascading into parallel_proof_search.chpl) | `extern \"C\" { ... }` is Chapel's "extern blocks" feature, requiring Chapel built with LLVM + clang headers. The official `chapel-2.3.0-1.ubuntu24.amd64.deb` is not. | Drop the wrapper. The 35 prover-id / category-id `c_int` constants are also `#define`d in `src/zig_ffi/chapel_ffi_exports.h` — that's the canonical source for any non-Chapel consumer. The Chapel copies only need module-level scope. | | `Build & Test Zig FFI Bridge` | `build.zig:23: no field or member function named 'addLibrary' in 'Build'` | `build.zig` line 1 declares "Compatible with Zig 0.14+/0.15+" and uses the unified `Build.addLibrary` API. Workflow pinned `mlugg/setup-zig@… with: version: 0.13.0`. | Bump the two `version: 0.13.0` lines in chapel-ci.yml to `0.14.0` (matches what build.zig declares). | ## Test plan - [ ] CI: `Compile Chapel Metalayer` returns success on this branch. - [ ] CI: `Build & Test Zig FFI Bridge` returns success on this branch. - [ ] CI: `Rust Build with Chapel Feature` (Job 3) actually runs (was previously skipped because Job 2 failed). ## Note on scope None of these are required checks; this PR doesn't unblock anything blocking the merge queue. It makes Chapel L2.1 actually CI-verifiable for the first time — `handover/TODO.md`'s "L2.1 ✅ Done" status was based on local builds only. Surfaced during the 2026-05-30 dependabot-deadlock triage (alongside PR #128 + PR #130).
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
) ## Summary Adds a SHA-pinned `taiki-e/install-action` step that installs `just` before the `MVP Smoke (Best Effort)` job runs `just --justfile Justfile mvp-env`. ## Why The workflow has been failing on every push with: \`\`\` /home/runner/work/_temp/…/sh: line 1: just: command not found ##[error]Process completed with exit code 127. \`\`\` The `ubuntu-latest` runner image doesn't ship `just`, and no step installed it. Surfaced during the 2026-05-30 triage of orthogonal CI failures alongside the dependabot deadlock (PR #128). ## SHA pin `taiki-e/install-action@184183c2401be73c3bf42c2e61268aa5855379c1` (v2.78.1) — matches the estate convention used across `hypatia/.github/workflows/{ci,security,tests,build-gossamer-gui}.yml`. ## Test plan - [ ] CI: `MVP Smoke (Best Effort)` returns success on this branch.
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.
Summary — auto-merge deadlock breaker
This branch bundles three required-check fixes that had been split across PRs #126, #127, #128 — but each PR's required-checks failed because they depended on the others. Solo PRs deadlocked; this PR closes the chain.
Bundled commits
chore(deps): revert 5 dependabot major-version bumps that broke CI(original chore: unblock CI — revert 5 dependabot major bumps + .trusted-base-ignore FP fix + deno.lock populate #128 scope)Five dependabot major bumps merged 2026-05-29 without call-site updates: axum 0.7→0.8 (chore(deps): bump axum from 0.7.9 to 0.8.9 #120), rand 0.9→0.10 (chore(deps): bump rand from 0.9.4 to 0.10.1 #121), criterion 0.5→0.8 (chore(deps): bump criterion from 0.5.1 to 0.8.2 #122), nom 7→8 (chore(deps): bump nom from 7.1.3 to 8.0.0 #123), rustyline 15→18 (chore(deps): bump rustyline from 15.0.0 to 18.0.0 #124). Each shipped real API breaks:
Rng→RngExt(because upstreamrand_corerenamedRngCore→Rng);use rand::Rngno longer bringsrandom_range/randomin scope.alt(args)(input)→alt(args).parse(input)).follow_redirect/policy/mod.rs).Reverts all 5 back to the May-28 working state.
cargo check --libcleans in ~2 min locally.chore(governance): populate empty deno.lock with minimal valid v4 lockfile(was chore(governance): populate empty deno.lock with minimal valid v4 lockfile #127)Replaces the 0-byte
deno.lock(tracked since 3b03087 for sweep visibility) with{"version":"4","remote":{}}. Unblocksgovernance / Language / package anti-pattern policywhich fails ondeno runlockfile parse before reaching the actual.tswalk.chore(governance): clear 12 trusted-base false-positive escape hatches(was chore(governance): clear 12 trusted-base false-positive escape hatches #126)Adds
.trusted-base-ignorefor 4 Rust pattern-detector tables (10 hits) — same FP class as the believe_me audit indocs/PROOF-NEEDS.md(zero real escapes). Adds-- AXIOM:/-- TRUSTED:magic-word lines in the script's 5-line window for two real Agda postulates (funext,Conflicts).Why bundled
Each individual PR failed its OWN required checks because it depended on the others' fixes:
governance / Language / package anti-pattern policy→ fixed in chore(governance): populate empty deno.lock with minimal valid v4 lockfile #127governance / Trusted-base reduction policy→ fixed in chore(governance): clear 12 trusted-base false-positive escape hatches #126T1 / *live-provers GREEN → fixed in chore: unblock CI — revert 5 dependabot major bumps + .trusted-base-ignore FP fix + deno.lock populate #128Bundling resolves the chicken-and-egg. #126 and #127 are closed as superseded with backlinks.
Verification
cargo check --libclean (1m 52s).Trusted-base reduction policy: SUCCESSandValidate K9 / A2ML / eclexiaiser: SUCCESSbefore being closed — proves the fix works in isolation.Language / package anti-pattern policy: SUCCESSbefore being closed.Seam-gaps captured (out of scope)
Dependabot major bumps + always-auto-merge interact badly. Per the standing estate hook
feedback_always_automerge_prs, auto-merge is universal. For major bumps without paired code updates, that's structurally unsafe — the only checks that DID gate the merges (validation gates) don't compile the workspace. Worth a follow-up: either Dependabot config to draft major bumps, or a per-repo guard requiring manual review for major-version-only PRs.standards check-ts-allowlist.tscould pass--no-lock— the script is a read-only file walker that doesn't import anything, so the lockfile is irrelevant. Adding--no-lockmakes it robust to this entire failure class estate-wide.standards rust-ci-reusabledoesn't pass--locked—cargo check/cargo testhappily auto-update Cargo.lock during CI, masking version drift. Adding--lockedto the reusable would surface drift the first time it happens, instead of when the next major hits.Test plan
cargo check --libclean.T1 / z3,T1 / vampire,T1 / spassGREEN (already verified GREEN on the first push of chore: unblock CI — revert 5 dependabot major bumps + .trusted-base-ignore FP fix + deno.lock populate #128).Refs: #92 (broader baseline failures — this PR addresses the compile + trusted-base + language-policy slices). Supersedes #126, #127.