Skip to content

ci: move the oracle default and elixir-compile to OTP 28.5.0.8 #1037

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Nov 10, 2026
+26 −35
Merged

ci: move the oracle default and elixir-compile to OTP 28.5.0.8 #1037

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f94e829
ci: move the oracle default and elixir-compile to OTP 28.5.0.8
claude Nov 9, 2026
c3a6b39
Merge branch 'main' into claude/gifted-thompson-vsrzhw-otp
hyperpolymath Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -330,17 +330,17 @@ 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
with:
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
Expand Down Expand Up @@ -457,17 +457,17 @@ 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
with:
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

Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/rsr-oracle.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
41 changes: 16 additions & 25 deletions CHANGELOG.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

@chatgpt-codex-connector chatgpt-codex-connector Bot Nov 10, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Preserve the existing unreleased changelog entries

Add this OTP entry without replacing the two newer entries already present in the parent. This change deletes the release notes for “Lean engineering proofs move to Idris2” and “Proof claims follow the machine proof ledger,” even though those changes remain in the tree, leaving the unreleased changelog incomplete.

Useful? React with 👍 / 👎.


`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)

Expand Down
4 changes: 2 additions & 2 deletions docs/consumers/rsr-oracle.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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]
----
Expand Down
2 changes: 1 addition & 1 deletion docs/consumers/standards-governance.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

@chatgpt-codex-connector chatgpt-codex-connector Bot Nov 10, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Keep the prerequisite aligned with the immutable standards pin

Retain OTP 28.3 here until the documented standards revision is updated, or update all five caller pins and their lock entries together. The examples and actual callers in this repository still pin 7641c7fdb01420696b5420ab85d88f599f32f609, which this section identifies as the exact immutable contract; a future standards PR cannot change that commit to install OTP 28.5.0.8, so the published integration's runtime prerequisite is now inaccurate.

Useful? React with 👍 / 👎.

consumer-side Elixir, Rust or Zig setup is required for the scan or
governance lanes.
* Repository Actions policy must allow
Expand Down
Loading