Repository navigation
CI / required is red on main: ci.yml asserts Idris 2 0.7.0 but the digest-pinned image is 0.8.0 (and trope-check.yml requires 0.8.0) #83
Description
Red on main (https://github.com/hyperpolymath/haec/actions/runs/39622697863) and identically on PR #81 (https://github.com/hyperpolymath/haec/actions/runs/40472456460). Recorded so #81, a docs-only pass, does not widen to fix it.
What happens: .github/workflows/ci.yml runs in ghcr.io/stefan-hoeck/idris2-pack@sha256:de97819… and asserts
case "$ver" in *"0.7.0"*) ;; *) echo "::error::expected Idris 2 0.7.0, got: ${ver}"; exit 1 ;; esac
The image reports Idris 2, version 0.8.0-6ca00e72e, so the job fails before idris2 --typecheck abi.ipkg runs. The same digest is used by trope-check.yml and release.yml, and trope-check.yml's comment says the repo requires 0.8.0 (0.7.0 cannot parse Trope/Fidelity.idr). The 0.7.0 assertion in ci.yml is the stale half of an earlier bump.
Fix: change the case arm to *"0.8.0"* (and update the comment above it), matching trope-check.yml. One-line; owner or a CI pass.
Also red on main, same run set: estate-rules (https://github.com/hyperpolymath/haec/actions/runs/39622698373) — scripts/check-root-shape.sh finds 5 root entries not on the allowlist: CHANGELOG.adoc, CONTRIBUTING.adoc, FUNDING, PROOF-PROGRESS.adoc, SECURITY.adoc. Either move them or add justified entries to .machine_readable/root-allow.txt (owner-only file under the Phase 0 brief).
Activity
Revert "fix(ci): Allow AsciiDoc guides, proof progress, and funding d…
hyperpolymath commentedon Oct 27, 2026
Candidate fix for the
estate-ruleshalf of this issue: CodeRabbit's CI-fix agent produced a7f62e4 on #81. It addsCONTRIBUTING.adoc,SECURITY.adoc,CHANGELOG.adoc,FUNDINGandPROOF-PROGRESS.adocto.machine_readable/root-allow.txt, and all five exist at the root onmain. With it,estate-ruleswent green (run 40495010769).It was reverted from #81 (8d34549) to keep that PR docs-only. To adopt it, run
git cherry-pick a7f62e4onto a branch frommain. An estate-wide alternative is to make thestandardsroot-allow template accept the.adocvariants, so each repo does not need its own allowlist edit.Generated by Claude Code
docs(affirmation): cite the CI runs for the Idris2 path and the CI/re…
hyperpolymath commentedon Nov 4, 2026
Half of this is fixed in #85:
ci.ymlnow asserts Idris 2 0.8.0. In run 41928694928 theCI / requiredjob passes the version assertion, theabi.ipkgtypecheck and the Zig FFI tests, and fails only in its last step on the root-shape allowlist, which is the other half of this issue (.machine_readable/root-allow.txt, owner-only; candidategit cherry-pick a7f62e4). After the allowlist is fixed, bothCI / requiredandestate-rulesshould go green and this issue can close.Generated by Claude Code
Phase 0 follow-up: CI/required asserts Idris 2 0.8.0, checker pin bum…