Skip to content

CI: restore the Debian proofs job; make the oracle's R start-up failure visible #5

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
Oct 2, 2026
Merged

CI: restore the Debian proofs job; make the oracle's R start-up failure visible #5

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d15bf4f
CI: restore #3's Debian proofs job lost in the #4 merge; split the or…
hyperpolymath Oct 2, 2026
d0871c4
CI oracle: put libR's directory on LD_LIBRARY_PATH, as RCall.jl's own…
hyperpolymath Oct 2, 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
35 changes: 20 additions & 15 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -82,11 +78,20 @@ jobs:
with:
version: '1.12'
- uses: julia-actions/cache@d10a6fd8f31b12404a54613ebad242900567f2b9 # v2
- name: Native vs reference agreement
# 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
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")'
Comment thread
coderabbitai[bot] marked this conversation as resolved.
Resolved
- name: Native vs reference agreement
run: |
export R_HOME="$(R RHOME)"
julia --project=test/oracle test/oracle/runoracle.jl
Loading