diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b9115f0c..e4fcdfeb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -330,7 +330,7 @@ jobs: uses: erlef/setup-beam@v1.24.1 with: elixir-version: '1.19.4' - otp-version: '28.3' + otp-version: '28.5.0.8' - name: Restore Mix cache uses: actions/cache@v6.1.0 @@ -338,9 +338,9 @@ jobs: path: | deps _build - key: mix-dogfood-${{ runner.os }}-${{ hashFiles('mix.lock') }} + key: mix-dogfood-${{ runner.os }}-otp28.5.0.8-${{ hashFiles('mix.lock') }} restore-keys: | - mix-dogfood-${{ runner.os }}- + mix-dogfood-${{ runner.os }}-otp28.5.0.8- - name: Fetch dependencies run: mix deps.get @@ -457,7 +457,7 @@ jobs: uses: erlef/setup-beam@v1.24.1 with: elixir-version: '1.19.4' - otp-version: '28.3' + otp-version: '28.5.0.8' - name: Restore Mix cache uses: actions/cache@v6.1.0 @@ -465,9 +465,9 @@ jobs: path: | deps _build - key: mix-dogfood-${{ runner.os }}-${{ hashFiles('mix.lock') }} + key: mix-dogfood-${{ runner.os }}-otp28.5.0.8-${{ hashFiles('mix.lock') }} restore-keys: | - mix-dogfood-${{ runner.os }}- + mix-dogfood-${{ runner.os }}-otp28.5.0.8- - uses: oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6 # v2.2.0 diff --git a/.github/workflows/rsr-oracle.yml b/.github/workflows/rsr-oracle.yml index 61a90f98..5afc712d 100644 --- a/.github/workflows/rsr-oracle.yml +++ b/.github/workflows/rsr-oracle.yml @@ -105,7 +105,7 @@ on: description: Erlang/OTP version for the oracle. type: string required: false - default: '28.3' + default: '28.5.0.8' outputs: tier: description: Tier reported by the oracle (none|bronze|silver|gold|rhodium). diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 16d8e368..4265a4cc 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -12,31 +12,22 @@ https://semver.org/[Semantic Versioning]. === Changed -==== Lean engineering proofs move to Idris2 (2026-11-09) - -* `RateLimiting`, `BayesianUpdate`, `ParserTotality`, `PageRankInvariants` - and `ESNSpectralScaling` are now Idris2 (`verification/proofs/idris2/`, - `%default total`), theorem for theorem (PROOF-POLICY §3; owner decision). - Four of them had rested on the Lean kernel axioms `propext` and - `Quot.sound`; the ledger rows are now `proven`, which makes the census - 22 proven of 42. -* `verification/proofs/lean4/` is removed. The `lake build` job becomes - `Lean hole re-check (HYP-01 control)`, which keeps the pinned Lean only for - the verdict fixture. - -==== Proof claims follow the machine proof ledger (2026-11-09) - -* `EXPLAINME.adoc` is back at the repository root, as README-EXPLAINME - requires, and every claim in it was re-checked against the tree. It gains - a `#proof-ledger` section that cites `verification/proof-ledger.jsonl`. The - README's own overclaims are listed under its known gaps. -* README, AFFIRMATION and EXPLAINME quote the ledger's census, and - `scripts/proof-ledger.sh claims` fails CI when a quoted census and the - ledger disagree. -* The neural-convergence handover is rewritten: Agda first, over - constructive reals, with no Mathlib, which PROOF-POLICY forbids. - `docs/proofs/needs.adoc` now points at the ledger instead of keeping a - list of its own. +==== The oracle and CI toolchain move to OTP 28.5.0.8 (2026-11-09) + +`rsr-oracle.yml` now defaults to OTP `28.5.0.8`, and the `elixir-compile` +jobs in `ci.yml` use it as well. An OTP version matrix (#1032) found the +following: + +* Commit `be98f74` crashes with a segfault on every run when it is compiled + and run on OTP 28.1, 28.2 or 28.3. The crash is in `sweep_off_heap` + under `beam_jit_bs_init_bits`. +* The same tree is clean on OTP 27.3, 28.0 and 28.5.0.8. + +The likely cause is the compiler bug that OTP 28.4 fixed (OTP-19951, +erlang/otp#10588). This is inferred, not proven. + +The Mix cache key now carries the OTP version. A `_build` compiled under one +OTP release is therefore never restored under another. ==== WH013 reads steps with RE001's workflow reader (2026-11-04) diff --git a/docs/consumers/rsr-oracle.adoc b/docs/consumers/rsr-oracle.adoc index ef542fc8..0b4585e7 100644 --- a/docs/consumers/rsr-oracle.adoc +++ b/docs/consumers/rsr-oracle.adoc @@ -38,7 +38,7 @@ paid for that on 2026-10-25: fix was written, because the ref in use was `main`. The fix (this repository's `elixir-compile` job) now compiles the tree on every -PR using the exact toolchain the gate uses — Elixir `1.19.4` / OTP `28.3` — so +PR using the exact toolchain the gate uses — Elixir `1.19.4` / OTP `28.5.0.8` — so the same defect cannot reach `main` again. The pin is what keeps a *consumer* safe when something else slips through anyway. @@ -120,7 +120,7 @@ product; the tier gate is a policy each repository adopts when it is ready. A == Local use The oracle is a mix task; there is nothing to install beyond Elixir 1.19.4 / -OTP 28.3: +OTP 28.5.0.8: [source,bash] ---- diff --git a/docs/consumers/standards-governance.adoc b/docs/consumers/standards-governance.adoc index 40bd4f50..abb46349 100644 --- a/docs/consumers/standards-governance.adoc +++ b/docs/consumers/standards-governance.adoc @@ -228,7 +228,7 @@ bash scripts/standards-integration/check-standards-integration.sh \ == Runtime prerequisites (explicit) * Runner: `ubuntu-latest` only. The reusables install their own - toolchain (Elixir 1.19.4 / OTP 28.3 via `erlef/setup-beam`) — no + toolchain (Elixir 1.19.4 / OTP 28.5.0.8 via `erlef/setup-beam`) — no consumer-side Elixir, Rust or Zig setup is required for the scan or governance lanes. * Repository Actions policy must allow