Follow-up to #29 / #31 (Wave-3 Chapel rehabilitation).
The check-abi job in .github/workflows/hpc-ci.yml currently has continue-on-error: true with comment "Idris2 CI setup can be fragile". Empirically: on the rerun of #31, this job failed with idris2: command not found after the Idris2 source-bootstrap step. The source-bootstrap is the fragile bit, not docudactyl's proofs.
To flip the job to strict:
- Replace the
make bootstrap SCHEME=chezscheme source build with either:
pack install (Idris2 package manager) — pulls a tested binary, fast install.- Pre-built tarball from
idris-community/Idris2-pre-built-package or equivalent.
- Setup action like
stefan-hoeck/setup-idris2 if it exists.
- Cache the Idris2 install across runs (currently it builds from source every time, ~7-10 min).
- Remove
continue-on-error: true from the job.
This isn't a docudactyl correctness issue — it's CI hygiene + faster feedback. The actual ABI proofs in src/Docudactyl/ABI/ are the strict gate worth recovering.
Related: see feedback_pre_compact_discipline / estate CI hygiene practices.
Follow-up to #29 / #31 (Wave-3 Chapel rehabilitation).
The
check-abijob in.github/workflows/hpc-ci.ymlcurrently hascontinue-on-error: truewith comment "Idris2 CI setup can be fragile". Empirically: on the rerun of #31, this job failed withidris2: command not foundafter the Idris2 source-bootstrap step. The source-bootstrap is the fragile bit, not docudactyl's proofs.To flip the job to strict:
make bootstrap SCHEME=chezschemesource build with either:packinstall (Idris2 package manager) — pulls a tested binary, fast install.idris-community/Idris2-pre-built-packageor equivalent.stefan-hoeck/setup-idris2if it exists.continue-on-error: truefrom the job.This isn't a docudactyl correctness issue — it's CI hygiene + faster feedback. The actual ABI proofs in
src/Docudactyl/ABI/are the strict gate worth recovering.Related: see
feedback_pre_compact_discipline/ estate CI hygiene practices.