From d15bf4f65fa0f5453cd523301abcf64749dfe29f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 2 Oct 2026 18:54:08 +0100
Subject: [PATCH 1/2] CI: restore #3's Debian proofs job lost in the #4 merge;
 split the oracle job so a silent R start-up failure is visible

The merge of main into feat/aldex2 kept #3's step name but the old Agda
2.7.0.1 download body (no curl in debian:13-slim, exit 127) and dropped the
checkout. The oracle job exits 1 with no message while loading RCall; the
new steps load ALDEx2 in R, then R through RCall, then the extension, one
at a time.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Y6e175rh1LbrsEhQvCrJ1
---
 .github/workflows/ci.yml | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 98ae8ef..2e03e3a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -43,17 +43,13 @@ jobs:
     steps:
       - name: Install the pinned Debian toolchain
         run: |
-          set -euo pipefail
-          curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" \
-            https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz
-          echo "${AGDA_SHA256}  $RUNNER_TEMP/agda.tar.xz" | sha256sum --check
-          tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP"
-          echo "Agda_datadir=$RUNNER_TEMP/Agda-v2.7.0.1/data" >> "$GITHUB_ENV"
-          echo "AGDA_BIN=$RUNNER_TEMP/Agda-v2.7.0.1/bin/agda" >> "$GITHUB_ENV"
-      - name: Type-check and axiom audit
-        run: proofs/bootstrap.sh
-      - name: Gate self-test (the gate must reject planted defects)
-        run: proofs/tests/gate-selftest.sh
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+        with:
+          persist-credentials: false
+      - name: Proof gate (axiom audit, type-check, reject controls, gate self-test)
+        run: proofs/check.sh
   oracle:
     name: R reference oracle (R 4.5.0, Bioconductor 3.22)
     runs-on: ubuntu-24.04
@@ -82,11 +78,17 @@ jobs:
         with:
           version: '1.12'
       - uses: julia-actions/cache@d10a6fd8f31b12404a54613ebad242900567f2b9 # v2
-      - name: Native vs reference agreement
+      - name: R can load ALDEx2
+        run: Rscript -e 'library(ALDEx2); cat(R.version.string, "ALDEx2", as.character(packageVersion("ALDEx2")), "\n")'
+      - name: Julia can start R through RCall
         run: |
           export R_HOME="$(R RHOME)"
-          # Skip Pkg's bulk precompile: it reports a failed extension without its error.
-          # Loading directly below surfaces the real error if there is one.
+          echo "R_HOME=$R_HOME"
           JULIA_PKG_PRECOMPILE_AUTO=0 julia --project=test/oracle -e 'using Pkg; Pkg.develop(path="."); Pkg.instantiate()'
-          julia --project=test/oracle -e 'using CompositionalDA, RCall; @assert Base.get_extension(CompositionalDA, :CompositionalDARCallExt) !== nothing'
+          for l in ~/.julia/scratchspaces/*/*/build.log; do echo "== $l"; cat "$l"; done
+          julia --project=test/oracle -e 'using RCall; println(rcopy(R"R.version.string"))'
+          julia --project=test/oracle -e 'using CompositionalDA, RCall; @assert Base.get_extension(CompositionalDA, :CompositionalDARCallExt) !== nothing; println("extension loaded")'
+      - name: Native vs reference agreement
+        run: |
+          export R_HOME="$(R RHOME)"
           julia --project=test/oracle test/oracle/runoracle.jl

From d0871c4a589ae92a51c978619fc4cb70b132fdfa Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 2 Oct 2026 19:08:39 +0100
Subject: [PATCH 2/2] CI oracle: put libR's directory on LD_LIBRARY_PATH, as
 RCall.jl's own CI does

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Y6e175rh1LbrsEhQvCrJ1
---
 .github/workflows/ci.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2e03e3a..2b15764 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -78,6 +78,9 @@ jobs:
         with:
           version: '1.12'
       - uses: julia-actions/cache@d10a6fd8f31b12404a54613ebad242900567f2b9 # v2
+      # RCall.jl's own CI does the same: libR's directory must be on the loader path.
+      - name: Put libR on the loader path
+        run: echo "LD_LIBRARY_PATH=$(R RHOME)/lib${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}" >> "$GITHUB_ENV"
       - name: R can load ALDEx2
         run: Rscript -e 'library(ALDEx2); cat(R.version.string, "ALDEx2", as.character(packageVersion("ALDEx2")), "\n")'
       - name: Julia can start R through RCall