Repository navigation
ci: remove the agda-cicd catalogue gate that could never start - #8
Merged
Merged
Conversation
.github/workflows/agda-cicd.yml (added in #7) called hyperpolymath/standards/.github/workflows/echidna-verify.yml@main as a reusable workflow, but that file declares no workflow_call trigger: it is standards' own lol/proofs + avow corpus gate. GitHub therefore refused the call at plan time and every run recorded failure with zero jobs (run 37231048694 on main; the same on arena 01c5afd). It never passed on any head. The proofs job in ci.yml (proofs/check.sh under Debian 13's Agda 2.6.4.3 and agda-stdlib 2.1) is the repo's proof gate and is green at aa8f6e6. Nothing in the proof corpus changes here. The ISSUE.md checklist line that recorded the gate is struck through with the reason rather than deleted. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AjVQUkziVYywrLNsbPordh
Contributor
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configuration
📒 Files selected for processing (1)
💤 Files with no reviewable changes (1)
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review. 📜 Recent review details⏰ Context from checks skipped due to timeout. (4)
📝 SummarySummary by CodeRabbit
WalkthroughThe pull request deletes the Agda catalogue gate workflow. The removed workflow included push, pull-request, and manual triggers, read-only contents permission, per-ref cancellation, and a job that called a reusable verification workflow. ChangesCatalogue workflow
Priority: ⬇️ Low Estimated code review effort: 1 (Trivial) | ~5 minutes Change: Bug fix Merge Risk: ⚪ Minimal · up to The repository’s local proof gate remains in CI. No concrete merge-blocking regression was established from removing the separate catalogue workflow. 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
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. A rabbit watched the workflow go, Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autopilot |
hyperpolymath
added a commit
that referenced
this pull request
Oct 6, 2026
## What Follow-up to #8, which deleted `.github/workflows/agda-cicd.yml`. The resolution checklist in `.github/ISSUE.md` still listed that file as added, pointing a reader at a workflow that no longer exists. This strikes the line and says what replaced it: the `proofs` job in `.github/workflows/ci.yml` (`proofs/check.sh`, Debian-pinned Agda 2.6.4.3), green on `main` (run 37448320842). One documentation line; no code, proof or workflow change. The edit was written alongside #8 and missed its final commit. ## Notes - `main` carries no rulesets, so nothing is required and nothing is armed (automerge on a repo with no required contexts merges on arming). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01AjVQUkziVYywrLNsbPordh Co-authored-by: Claude Fable 5.1 <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
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.
What
Deletes
.github/workflows/agda-cicd.ymland strikes through the.github/ISSUE.mdchecklist line that recorded it, with the reason.Why
The workflow (added in #7) did
uses: hyperpolymath/standards/.github/workflows/echidna-verify.yml@main. That callee declares noworkflow_calltrigger (grep -c workflow_call= 0; it runs on push / pull_request / schedule / workflow_dispatch only) and is standards' ownlol/proofs+ avow corpus gate. GitHub refuses such a call at plan time, so every run was a startup death:conclusion: failurewith zero jobs (run 37231048694 onmain, also red on arena 01c5afd). It never passed on any head. The catalogue row's "Reusable?" column readsYes; that is recorded as a standards finding in dev-notes, not fixed here.None of the 16 standards workflows that do declare
workflow_callis an Agda gate, so there is nothing to retarget to.What still gates the proofs
The
proofsjob in.github/workflows/ci.yml:proofs/check.shunder Debian 13'sagda-bin=2.6.4.3-1+b2andagda-stdlib=2.1-4in a digest-pinned image. Axiom audit, type-check ofCompositionalDA.All, three reject controls, gate self-test. Green at aa8f6e6. No proof source changes in this PR.maincarries no rulesets (rules/branches/main=[]), so this red blocked nothing; it only misreported the proof corpus as failing.🤖 Generated with Claude Code
https://claude.ai/code/session_01AjVQUkziVYywrLNsbPordh