Repository navigation
fix(abi): review follow-ups from the JNK-01 stack (CodeRabbit on #149, Hypatia on #150) - #152
Conversation
…ESIGNED Two CodeRabbit findings on #149 (merged before they could ride it), plus one stale status line: - ffi/zig/include/januskey.h: the header said Foreign.idr is "checked by the ABI package typecheck". The typecheck does not compare the two files. On this stack the comparison is scripts/check-abi-layout.sh (symbols, status codes, enums, sizes; ledger row A-3), and the comment now names it. - scripts/check-abi-tree.sh: a dangling symlink at src/idris-abi passed `[ -e ]`, so the retired farm could come back as a broken link unnoticed. The check is now `-e || -L`. Reproduced: with `ln -s does-not-exist src/idris-abi` the old gate exits 0 and the new one exits 1 with "src/idris-abi exists (retired symlink farm)". - .github/workflows/agda-proofs.yml: "DESIGNED until its first green run" is no longer true; its first run on #150 was green under Agda 2.6.4.3 with both fixtures refused for their stated reasons. Checks: check-abi-tree OK, check-abi-layout PASS, workflow YAML parses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 44 minutes. View limit details
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 |
Hypatia flagged two warnings on #150, both for the same thing: job `proofs` in agda-proofs.yml had no `timeout-minutes`, so a hung apt install or sibling fetch could hold a runner for the 360-minute default. The job takes about 35 s; 15 minutes matches idris-abi.yml. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
hyperpolymath
changed the title
|
The red checks on Generated by Claude Code |
2 participants
Summary
Small follow-ups to the JNK-01 stack (#149, #150, #151, now on
mainasad85593andbf54181). These findings posted after their PRs merged.ffi/zig/include/januskey.h(CodeRabbit, refactor(abi): one ABI tree — module-path layout, JanusKey casing, symlink farm retired (JNK-01, A of 3) #149). The header saidForeign.idris "checked by the ABI package typecheck", but the typecheck never compares the two files. The comparison isscripts/check-abi-layout.sh(symbols, status codes, enums, sizes; ledger row A-3), and the comment now names it.scripts/check-abi-tree.sh(CodeRabbit, refactor(abi): one ABI tree — module-path layout, JanusKey casing, symlink farm retired (JNK-01, A of 3) #149). A dangling symlink atsrc/idris-abipassed[ -e ], so the retired farm could come back as a broken link unnoticed. The check is now-e || -L..github/workflows/agda-proofs.yml(Hypatia WH006 and missing_timeout_minutes, feat(proofs): reversibility as a Loss grade — Agda kernel module pinned to resource-algebra (JNK-01, B of 3) #150). Jobproofshad notimeout-minutes, so a hang would hold a runner for the 360-minute default. It now has 15 minutes, matchingidris-abi.yml; the job takes about 35 s..github/workflows/agda-proofs.yml. The header still said "DESIGNED until its first green run". Its first run on feat(proofs): reversibility as a Loss grade — Agda kernel module pinned to resource-algebra (JNK-01, B of 3) #150 was green under Agda 2.6.4.3, with both fixtures refused for their stated reasons.Type of change
📌 New pins
None.
How has this been verified?
ln -s does-not-exist src/idris-abi, the oldcheck-abi-tree.shexits 0 and the new one exits 1 withFAIL: src/idris-abi exists (retired symlink farm).bash scripts/check-abi-tree.sh→OK: one ABI tree (4 modules, 1 package).bash scripts/check-abi-layout.sh→PASS. The edited header line contains nothing the layout gate parses.agda-proofs.ymlparses,jobs.proofs.timeout-minutesis 15, and its SPDX header stays on line 1.Checklist
Notes for reviewers
The red checks that are already red on
main(the #135 set) will show here too; #149 has their causes.🤖 Generated with Claude Code
https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9