From bcb47b82c70920c0db88243c5843385f9c34ba9c Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 11:40:49 +0000 Subject: [PATCH] fix: pin occupancy-types at its merge commit 8f09c0b typed-wasm pinned occupancy-types at 6013483, a commit on the hyperpolymath/occupancy-types#11 branch. That PR was squash-merged as 8f09c0b and its branch deleted. A fresh clone fetches only branches, so it can no longer reach 6013483: fatal: reference is not a tree: 60134839efe2c6f51a31d977a72c1cf94457e71d As a result, the kernel-proofs gate's "Fetch siblings at their pins" step fails on every fresh checkout. 8f09c0b differs from 6013483 only in occupancy-types' own scripts/check-agda.sh; the Agda sources are identical. Also removes a stray "and" from a MinMax.idr header comment. tools/check-kernel-proofs.sh, after a fresh fetch at the new pins: OK (upstream occupancy-types: core proofs and all 2 expected rejections; 33 modules; 11 rejections; 269 equalities in both provers; 4 controls). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 10 ++++++++++ scripts/fetch-siblings.sh | 2 +- src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr | 2 +- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 92ec778..834cca1 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,16 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== occupancy-types pin `6013483` → `8f09c0b` (2026-10-14) + +* `scripts/fetch-siblings.sh` pins occupancy-types at `8f09c0b`, the merge of + hyperpolymath/occupancy-types#11. The old pin was a commit on that PR's + branch, which was deleted at merge, so a fresh clone could no longer fetch + it (`fatal: reference is not a tree`) and the kernel-proofs gate could not + start. The two trees differ only in occupancy-types' own + `scripts/check-agda.sh`; the Agda sources this gate checks are identical. +* `ResourceAlgebra/MinMax.idr`: a header comment loses a stray "and". + ==== MinMax joins the grade kernel (2026-10-14) * New `ResourceAlgebra/MinMax.idr` transcribes resource-algebra diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 7c72800..5d5d3ea 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -22,7 +22,7 @@ set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe}" -OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-60134839efe2c6f51a31d977a72c1cf94457e71d}" +OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-8f09c0bb319dee99d532e261cd5da4d04ace479a}" CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}" fetch() { # fetch diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr index d3c9b8e..2258ad5 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr @@ -20,7 +20,7 @@ -- minMaxSeq = sequence = MAX (the worst hop) — the "⊗", unit Finite 0 -- lossAlt = alternatives = MIN (the better path) — the "⊕", unit Infinity -- Infinity absorbs under sequence but is the identity for alternatives: --- and an unreachable alternative is never chosen. +-- an unreachable alternative is never chosen. -- -- The carrier is shared with Loss ON PURPOSE (upstream Morphism.agda, -- `loss-bottleneck`: the identity on the carrier is a lax morphism Loss →