fix(ci): echidna-verify — honest absence Guards for agda-lol & idris2-a2ml - #828
Merged
Merged
Conversation
…-a2ml jobs Both jobs crashed on proof corpora that were permanently evicted from this repo (agda-lol: find/cd lol/proofs failed at the Type-check step after the apt install; idris2-a2ml: cd a2ml failed AFTER an ~18-minute pack bootstrap, every run). idris2-avow got the 'Nothing to type-check' in-step guard long ago; these two never did (issue #748). Each job now opens with a presence Guard right after checkout that emits a honest ::notice and sets present=false; the toolchain-install, type-check and audit steps (a2ml: cache/install/type-check) run only when the corpus is present. If the corpora ever return, the jobs verify them again, unchanged. Job outcome is green-but-honest, not silently-so: the notice says the corpus is absent. Corrected CICD-WORKFLOW-CATALOG.md: the row claimed 'Echidna smart contract verification' — this workflow is the ECHIDNA trust pipeline (Agda/Idris2 proofs), not the smart-contract fuzzer — and now documents the guard behaviour. Validation: PyYAML parse, bash -n on both guard blocks, diff = 2 files +44/-1, working tree clean of foreign edits. Refs #748
Contributor
|
Warning Review limit reachedNext included review available in 41 minutes. View limit detailsLimit details: You’ve used the included review currently available. You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Review configuration: ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (2)
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
added a commit
that referenced
this pull request
Sep 17, 2026
…; no ruleset pins its context) (#836) Refs #748 (eviction half, now sanctioned by the retirement ruling). ## Ruling applied The a2ml project is **officially retired** (owner ruling, 2026-09-17). #828's presence Guards assumed wake-if-corpus-returns; for A2ML the corpus never can, so the `idris2-a2ml` job is **evicted, not guarded**. Job block, `push: paths` filters, detect-job regex alternatives, and `trust-summary` references all removed/reworded. ## Anti-deadlock verification (before removing a check context) - **Live org ruleset** `Optimus-Branch` (#23359343, active, org scope) required contexts: `CodeQL`, `CodeRabbit`, `SonarCloud Code Analysis`, `governance / Code quality + docs`, `.github/dependabot.yml`, `uses ⊆ actions.lock`. **No proof contexts.** - `config/rulesets/*.json` (the canon ruleset files): no proof contexts. - Conclusion: deleting the job cannot deadlock any PR. The in-file claim "`Idris2 - a2ml proofs` is a REQUIRED context" was **stale** — corrected in the filter-rationale comment. ## What survives (unchanged) - `agda-lol` — full gate-set Guard from #828 (lol is not retired). - `idris2-avow` — its original in-step guard. - `trust-summary` — dangling `needs:` removed; the a2ml row becomes an informational `_evicted_` note (a table pretending the job ran would be the new dishonesty). - Always-on-PR shape **deliberately kept** even though the required-context rationale died: the Guards cost seconds, and this workflow doubles as the repo's proof-hygiene canary. ## Validation - PyYAML parse: jobs = `detect-proof-changes, agda-lol, idris2-avow, trust-summary`; no dangling `needs` - Residual `a2ml` mentions are **only** the retirement annotations (scope note, stale-context correction, summary row) - Diff: 2 files, +23/−110 (working-tree dirt quarantined — only the two intended files staged)
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.
Closes #748.
The disease (before this PR)
Neither job carried the
Nothing to type-checkguard thatidris2-avowgot:find lol/proofs/theories/cd lol/proofs— crashes at the Type-check step. Corpora evicted to the lol repo.cd a2ml— crashes AFTER an ~18-minute pack bootstrap, every single run. Corpus evicted to the a2ml repo.The fix
Each job opens with a
Guard — proofs are evicted from this repostep immediately after checkout: if the corpus directory is absent it emits a::notice(honest, visible in the UI) and setspresent=false; the expensive steps (Cache pack,Install Idris2 via pack,Type-check normative A2ML core/Install Agda,Type-check proofs,Postulate audit) are conditioned onsteps.guard.outputs.present == 'true'.Upload logkeepsif: always()(already ignores missing files).Pulling the guard ahead of the toolchain spend is strictly stronger than the avow job's in-step guard — the cron stops burning install/bootstrap minutes on a 404. If a corpus ever returns, the jobs verify it again unchanged; they are dormant, not deleted, so the check names keep reporting on the branch on every proof-touching run.
Also in the PR:
CICD-WORKFLOW-CATALOG.md: row claimed "Echidna smart contract verification" — this is the ECHIDNA trust pipeline (Agda/Idris2 proofs), not the smart-contract fuzzer. Description corrected + guard behaviour documented (docs ride the PR per protocol).Validation
idris2-avowuntouched — 0 newif:lines there)bash -non both extracted guard blocksgit diff origin/main --stat: 2 files, +44/−1; working tree clean of foreign editsClose-out per protocol on merge: evidence comment → close #748 completed → board item → Done; catalog/GLOSSARY sweep already in this diff.