From ef172eecd974a542baee5f3c5ecb28118a5f2afd Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 17:24:52 +0100 Subject: [PATCH] ci(idris2): bump pinned version 0.7.0 -> 0.8.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The CI workflow pinned idris2 0.7.0 across four reference locations (matrix, cache path, cache key, git-clone branch in the docs job) while the source code is written against 0.8.0 semantics. Owner flagged this on standards#132's reconciliation comment as "the 0.7.0/0.8.0 CI mismatch makes the build oracle unsound (HIGH)" and listed the bump as "separate, recommended next". What this changes: - L27 matrix entry: `['0.7.0']` -> `['0.8.0']` - L96 cache-path glob: `~/idris2-0.7.0` -> `~/idris2-0.8.0` - L97 cache-key prefix: `idris2-0.7.0-` -> `idris2-0.8.0-` - L102 git-clone tag: `--branch v0.7.0` -> `--branch v0.8.0` What this may surface: The owner's diagnosis was that `SafeMath`/`SafeSRI`/`SafeCSRF` Proofs.idr files are "false-green" under 0.7.0 — they elaborate under 0.7.0 stdlib semantics but may not under 0.8.0. Local verification was not possible (Idris2 base-package binaries on the maintainer's machine are not currently compatible with the installed compiler), so this PR cannot guarantee the bumped CI will stay green. If CI goes red after this lands, the failures are the genuine proof debt the version mismatch was hiding — close the real issues, do NOT revert this bump. No `.idr` files touched; behaviour change is in CI only. Refs hyperpolymath/standards#124, sub-issue standards#132. Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/workflows/idris2-ci.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/idris2-ci.yml b/.github/workflows/idris2-ci.yml index 14420b30..daabd031 100644 --- a/.github/workflows/idris2-ci.yml +++ b/.github/workflows/idris2-ci.yml @@ -24,7 +24,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - idris2-version: ['0.7.0'] + idris2-version: ['0.8.0'] steps: - name: Checkout @@ -93,14 +93,14 @@ jobs: with: path: | ~/.idris2 - ~/idris2-0.7.0 - key: idris2-0.7.0-${{ runner.os }} + ~/idris2-0.8.0 + key: idris2-0.8.0-${{ runner.os }} - name: Install Idris 2 if: steps.cache-idris2.outputs.cache-hit != 'true' run: | - git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2.git ~/idris2-0.7.0 - cd ~/idris2-0.7.0 + git clone --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2.git ~/idris2-0.8.0 + cd ~/idris2-0.8.0 make bootstrap SCHEME=chezscheme make install