Commit e1edebe
authored
fix(ci): idris2-abi install via apt + tag-archive fallback — replaces 404 URL (#168)
## Summary
- `Type-check Idris2 ABI definitions` has failed on every run since at
least 2026-05-18 (5+ consecutive `failure`s in `gh run list --workflow
"Idris2 ABI Type-Check" --branch main`) because `curl -fsSL
https://github.com/idris-lang/Idris2/releases/download/v0.8.0/Idris2-0.8.0-Linux-x86_64.tar.gz`
returns HTTP 404.
- Root cause: Idris2 v0.8.0's release-asset array is empty — the project
did not publish a prebuilt Linux tarball for that tag. The
release-download URL therefore 404s. The same constraint is already
documented inline in `live-provers.yml:184-201`, which uses a working
install pattern.
- Fix: port the live-provers pattern into `idris2-abi-ci.yml`. Prefer
Ubuntu 24.04 universe `idris2`; fall back to a source build from
`archive/refs/tags/v0.8.0.tar.gz` (the archive API resolves for any
tag).
- Side cleanup: drop the `IDRIS2_PREFIX: /opt/idris2` env hint on the
Type-check step — neither install path lands binaries at `/opt/idris2`,
so it was steering Idris2 at a non-existent prefix.
## Why this matters now
This is the upstream-source fix the merge ruleset asks for. Removes the
baseline red so the rest of the queue (including #166's TacticRecord
round-trip lemmas, which this job will now exercise) can land without
`--admin`. Stops a 2-week-old failed-installation message from masking
any future regression in `src/abi/`.
## Test plan
- [x] `python3 -c "import yaml; yaml.safe_load(...)"` parses OK
- [x] Local check (Idris2 0.8.0 + base) succeeds on the same
`src/abi/echidnaabi.ipkg` with no `IDRIS2_PREFIX` override
- [ ] `Type-check Idris2 ABI definitions` job → success on this PR
Refs the 2026-05-18 → 2026-05-30 consecutive curl(22) run history.1 parent fff57dc commit e1edebe
1 file changed
Lines changed: 20 additions & 10 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
28 | 28 | | |
29 | 29 | | |
30 | 30 | | |
31 | | - | |
32 | | - | |
33 | | - | |
34 | | - | |
35 | | - | |
36 | | - | |
37 | | - | |
38 | | - | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
39 | 51 | | |
40 | 52 | | |
41 | 53 | | |
42 | | - | |
43 | | - | |
44 | 54 | | |
45 | 55 | | |
46 | 56 | | |
| |||
0 commit comments