fix: pin occupancy-types at its merge commit 8f09c0b

[hyperpolymath]

Summary

This fixes Grade kernel proofs (Idris2 0.8.0 + Agda) on every fresh checkout of main.

scripts/fetch-siblings.sh pins occupancy-types at 6013483. That commit sits on the branch of hyperpolymath/occupancy-types#11. #11 was squash-merged as 8f09c0b at 11:31Z and its branch deleted. fetch-siblings.sh clones and then runs git fetch origin, which fetches branches only, so 6013483 is now unreachable:

$ git clone https://github.com/hyperpolymath/occupancy-types.git && git -C occupancy-types fetch origin
$ git -C occupancy-types checkout --detach 60134839efe2c6f51a31d977a72c1cf94457e71d
fatal: reference is not a tree: 60134839efe2c6f51a31d977a72c1cf94457e71d

This is task #18 from the MinMax work (#276): move the pin once #11 merged.

Changes

• scripts/fetch-siblings.sh: occupancy-types 6013483 → 8f09c0bb319dee99d532e261cd5da4d04ace479a (occupancy-types main).
  • The two trees differ only in occupancy-types' own scripts/check-agda.sh, which CodeRabbit changed on fix(rhodibot): automated RSR compliance fixes #11.
  • The Agda sources this gate checks are identical.
  • No module header cites this pin. The af95728 citations in HWM.idr, typed-wasm.ipkg and LEVEL-STATUS.adoc name the commit that R-1..R-5 were ported from, so they stay.
• ResourceAlgebra/MinMax.idr: the header comment "…the identity for alternatives: and an unreachable alternative…" loses its stray "and".
• CHANGELOG.adoc: an entry.

RSR Quality Checklist

Required

• Tests pass (tools/check-kernel-proofs.sh, see Testing)
• Code is formatted
• Linter is clean
• No banned language patterns
• No unsafe blocks without // SAFETY: comments
• No banned functions (the gate's own check: zero believe_me / assert_total / assert_smaller / idris_crash)
• SPDX license headers present on all new/modified source files (headers unchanged)
• No secrets, credentials, or .env files included

As Applicable

• CHANGELOG or release notes updated

Testing

I ran _build/dependencies from scratch, the way CI does. The commands were scripts/fetch-siblings.sh, then tools/check-kernel-proofs.sh, with Idris2 0.8.0 and Agda 2.6.3:

resource-algebra at 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe
occupancy-types at 8f09c0bb319dee99d532e261cd5da4d04ace479a
choreographic-types at edb784a7d26c276c2abfa8399b773d346dbb101e
PASS: upstream: PASS: core proofs, unit tests and all 8 expected rejections
PASS: upstream occupancy-types: PASS: core proofs and all 2 expected rejections
PASS: upstream choreographic-types: KCut.agda (K-1..K-5) checks against the resource-algebra pin
PASS: idris2 --build typed-wasm.ipkg: 33 module(s) built, 0 errors
PASS: kernel: zero believe_me / assert_total / assert_smaller / idris_crash
… 11 rejections, each at its declaration …
PASS: Agda (pinned resource-algebra) accepts the table by refl: 269 equalities
PASS: Idris2 (port) accepts the table by Refl: 269 equalities
… 4 negative-control rows refused by both provers …
OK: kernel proofs — build, 11 rejection(s), table, and 4 negative control row(s)

🤖 Generated with Claude Code

https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t

---

Generated by Claude Code

[coderabbitai]

Warning

Review limit reached

You'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 28 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: f995bd8b-d5d1-4a5e-9e19-a73bf2de8052

📥 Commits

Reviewing files that changed from the base of the PR and between 9bb4c27 and bcb47b8.

📒 Files selected for processing: 3

• CHANGELOG.adoc
• scripts/fetch-siblings.sh
• src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud