Repository navigation
fix(ci): panel-clades-abi pins Idris2 by commit, drops the checkout token, shows the log tail - #146
Merged
Merged
Conversation
…rnel
PanelClades.ABI.Grades grades a clade's resource contract in typed-wasm's
Idris2 grade kernel (TypedWasm.ABI.ResourceAlgebra, transcribed from
hyperpolymath/resource-algebra), imported at a pin, not re-declared:
- panel state by OCCUPANCY (HWM): StateWithin, and phasesWithin, the
reclamation law at the panel (a second phase fits in what the first
left);
- the Panel-N -> Panel-W crossing by LOSS: LossWithin (total collapse is
never within tolerance), crossTwice (losses add, lossSeq), betterOfTwo
(the less lossy translation, lossAlt);
- CladeResourceContract, its {grade, algebra} pairs (TaggedGrade), and the
neurosym-bridge contract: state peak 48 / drift 16 within 64, crossing
loss 2 within 3. DESIGNED: declared values for the owner to confirm,
not measurements;
- the computed separation at the panel: two phases occupy 64 but cost 96.
panel-clades/scripts/fetch-siblings.sh pins typed-wasm at main 9403258
(the kernel's landing, typed-wasm#271). panel-clades/scripts/check-abi.sh
builds the kernel there, builds panel-clades-grades.ipkg against it (exit 0
and no Error line), and requires tests/reject/{OverBudget,
CollapseWithinTolerance}.idr to be refused at their invalid declarations
for the intended reason. It runs as job panel-clades-abi in
build-validation.yml (Idris2 0.8.0 built from its tag; no binaries exist).
schema/typell-grade.schema.json is the {grade, algebra} wire payload for
TypeLL (DESIGNED: the Panel-L JSON-RPC wiring is not built).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
The ABI README said "Verified by: Idris2 0.8.0 type checker" with every proof CLOSED. Checked today: Types.idr / Layout.idr / Foreign.idr do not typecheck. Their module names (PanelClades.ABI.*) do not match their paths, so Idris2 refuses them outright, and laid out at matching paths Types.idr still has 11 errors (ElabReflection not enabled, DecEq without Decidable.Equality, unprovable So auto-proofs, Bits used as a type, pattern matching on types, an auto-bound cladeKindCount). The README now says which module does typecheck (Grades.idr, via scripts/check-abi.sh) and lists those errors; fixing them is left to the owner, as some need redesign. Also: SPDX header on that README, a pointer from the TypeLL clade README to the grade schema, and a CHANGELOG entry. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…xLub typed-wasm #273 and #274 have merged, so the pin moves from 9403258 (the kernel's landing, #271) to main 117bbf8. #273 added maxLub to the kernel's Nat lemmas, so Grades.idr's local copy (maxLeast) goes and phasesWithin uses the kernel's. check-abi.sh passes at the new pin (1 module, 0 errors, 2 rejections). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…ild directly shellcheck SC2164 and SC2181, the likely source of CodeFactor's one finding on #145. The script runs without `set -e` (it collects failures), so a failed cd would have carried on in the wrong directory. The kernel-build test now checks the subshell's status directly. Both failure branches still fail the gate (checked with an idris2 shim that refuses the build, and one that prints Error: but exits 0). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…tail CodeRabbit on #145: - build-validation.yml fetched Idris2 by its v0.8.0 tag, which can move (CWE-494). It now fetches 15a3e4e70843f7a34100f6470c04b791330788df, the commit that tag names, checks HEAD against it, and tags it v0.8.0 locally so the Makefile still reports 0.8.0 (without a tag it appends the short SHA). - The panel-clades-abi checkout sets persist-credentials: false; the job needs no token after checkout (the sibling fetch is anonymous https). - check-abi.sh printed nothing when idris2 failed without an `Error` line (an INTERNAL ERROR, say). Both build branches now fall back to the log tail; checked with an idris2 shim that fails with no Error line. shellcheck clean; check-abi.sh passes (1 module, 0 errors, 2 rejections). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
# Conflicts: # .github/workflows/build-validation.yml # panel-clades/scripts/check-abi.sh
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 46 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
hyperpolymath
marked this pull request as ready for review
October 14, 2026 02:01
Owner
Author
|
These red checks are not this PR's. Each one is red on
This PR's own check is Build Validation / panel-clades-abi, which builds Idris2 from the pinned commit. It is still running. Generated by Claude Code |
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
## Summary #147 cannot go green on its own: every red check on it is also red on `main`. This branch is **#147's seven commits plus five fixes**, one per root cause. It is stacked on #147 rather than based on `main` for two reasons: - #147 rewrites every workflow's `uses:` and adds `actions.lock`. - Each fix here changes a workflow or the lock, and has to agree with #147's lock. **Merge order (owner's choice):** merge #147 first, and this PR's diff shrinks to the five fixes. Or merge this PR alone, which lands both. | Check (red on #147 and `main`) | Root cause | Fix | |---|---|---| | Governance / Workflow security linter | `main-estate-audit.yml` was an inline copy pasted by `rollout_estate.sh`: no SPDX header, no `permissions:`, gates pinned 3 weeks stale. | Replaced with the thin caller `rsr-template-repo` ships, calling cicd-suite's reusable at `4f54042`. Lock updated. | | Central Estate CI/CD Audit | 734 untracked debt markers. 726 of them are the stub line #107 put in every `.affine` file. | Real debt is linked: `TODO(#148)` for the stubs, `TODO(#149)` for four FFI/ABI gaps. Four hits that are not debt (a marker scanner, a test's expected labels) go in `.cicd-hygiene-allow`, each with its reason. | | Dogfood Gate / Validate K9 contracts | The validator was locked at k9-ecosystem `89f3c27`, from before its Nickel-dialect repair, and 102 configs had no K9 marker. | Lock resolves `@main` to `20f6be5`. `magic_number = "K9!"` added to 98 clade configs and 4 layouts. | | Rust CI | `gossamer-rs = { path = "../gossamer/…" }`, a sibling checkout CI never has. | Git dependency pinned to gossamer `c234fea`, optional behind a `gossamer` feature that the desktop bin requires. That exposed `cargo fmt` drift and one clippy lint; both fixed. E2E's Rust job installs Zig 0.15.2 and builds the shell. | | Build Validation / `validate`, E2E Deno jobs | They built and tested the ReScript frontend that #107 deleted, through the `deno.json` that #108 deleted. `pcc` scans `.res` files. | **Owner decision:** the frontend is ported to AffineScript, with no restore, and the dead gates are removed now (#137 allowed "removed"). The tests stay in `tests/`; #148 re-adds the gates. The bench job's `\| tee` had been hiding its failure, so it showed a false green. | ## CI on this branch On the first push (4 fixes), these went green for the first time: - `rust-ci` check, clippy and fmt; `rust-ci` test - Workflow security linter - Actions lockfile verify - estate-audit - Validate K9 contracts - Rust Backend — Build + Check, which links the desktop shell in CI The fifth commit removes the remaining dead gates. ## Verified locally (before each push) - **Estate gates:** all 26 cicd-suite gates pass at `1aa6bfb`, including the DEED (`f9d999b`) and K9 (`2155aa2`) validators nested in `manifest-check`. The K9 validator at `20f6be5` scans 110 files with 0 errors, and `nickel 1.18 export` succeeds on all 98 clade configs. The 4 layouts already failed `nickel export` before this PR, on a destructuring error in their import, and still do. - **Rust:** check, fmt, `clippy -D warnings` and test pass on rustc 1.97.0 and 1.99.0. The desktop shell builds and links with Zig 0.15.2 and the GTK/WebKit dev packages. - **Lock:** gh actions-lock v0.1.6 `--verify-local` is valid, and the standards and rsr-template-repo `check-lock-sync.sh` both pass. Every reusable pin (standards `092deda`, `412a703`; cicd-suite `4f54042`) is reachable from its repo's `main`. ## Not fixed here - **SonarCloud** reports "C Security Rating on New Code". It first appeared on #147; #146 was green. It is not a required context, and the estate treats Sonar as advisory. The likely trigger is #147's move from SHA pins to lock-managed tag refs, but `sonarcloud.io` is unreachable from the agent sandbox, so this is not confirmed. - **Mirror** is push-only, not a PR check. The Gitea job runs `ssh-keyscan` with an empty `vars.GITEA_HOST`, and the Disroot repository does not exist. Both are settings fixes. Refs #137. Tracking issues opened: #148, #149. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01BCQeL169ZnUirUVaDXQLA3 --------- Co-authored-by: Claude <noreply@anthropic.com>
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
2 participants
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
This carries CodeRabbit's three review findings on #145. #145 was merged at
a188675, a minute before the fix commit (42dbbbe) was pushed, so the fixes never reachedmain. The three review threads on #145 say "fixed in 42dbbbe"; this PR is where that commit lands.Changes
build-validation.yml/panel-clades-abi:15a3e4e70843f7a34100f6470c04b791330788df(the commitv0.8.0names) and checksHEADagainst it. Then it tags that commitv0.8.0locally: without a tag, Idris2's Makefile reports the version as0.8.0-<sha>.persist-credentials: false. Nothing in the job needs the token after checkout, because the sibling fetch is anonymous https.panel-clades/scripts/check-abi.sh: both build branches (kernel and grades) print the log tail whenidris2fails without anErrorline, for example on an INTERNAL ERROR. Before, they printed nothing.The branch merges
main(#145's squash) instead of being force-pushed, so the diff againstmainis only these two files.Testing
GIT_SHA1is15a3e4e70before the local tag and empty after it.check-abi.sh.bash panel-clades/scripts/check-abi.sh→OK: panel-clades grades ABI — builds against the kernel, 2 rejection(s).FAIL: panel-clades-grades.ipkg (exit 1).The other red checks are the same pre-existing ones listed on #145, all red on
maintoo:validate(nodeno.json), Rust CI (gossamer-rspath dependency), the Governance lockfile and workflow linter, K9 contracts, and the estate-audit hygiene gate. CodeRabbit's docstring-coverage warning counts the four one-line bash helpers (pass,err,die,fetch); I've left it as is.🤖 Generated with Claude Code
https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Generated by Claude Code