|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# FFI CI build: standalone surface (now) vs full Idris→Zig pipeline (deferred) |
| 5 | + |
| 6 | +`proven`'s FFI layer compiles Idris 2 to C via the RefC backend and wraps it in |
| 7 | +a stable C ABI with Zig (`Idris2 --codegen refc → .c → zig build → libproven`). |
| 8 | +There are **two** Zig build entry points: |
| 9 | + |
| 10 | +| File | Builds | External deps | Used by | |
| 11 | +|------|--------|---------------|---------| |
| 12 | +| `ffi/zig/build.zig` | full Idris→RefC→Zig `libproven` | `idris2_zig_ffi` (path dep on `nextgen-languages/language-bridges`) + generated RefC C | local dev, full integration | |
| 13 | +| `ffi/zig/build_standalone.zig` | `libproven_ffi.a` from `src/main.zig` only (pure-Zig C-ABI surface) | none | **CI** (`e2e.yml`) | |
| 14 | + |
| 15 | +## Why CI uses the standalone build (ADR-003) |
| 16 | + |
| 17 | +`build.zig` declares its `idris2_zig_ffi` dependency as a Zig **`.path`** |
| 18 | +dependency: |
| 19 | + |
| 20 | + .idris2_zig_ffi = .{ .path = "../../../nextgen-languages/language-bridges/bridges/idris2" } |
| 21 | + |
| 22 | +That points at a **private, cross-owner sibling repo** which CI does not (and |
| 23 | +cannot, without a credential) check out, so `zig build` fails at dependency |
| 24 | +resolution. `build_standalone.zig` compiles `src/main.zig` alone — and that |
| 25 | +file imports only `std`/`builtin` — so it needs neither the bridge nor the |
| 26 | +generated RefC, giving CI a real (if narrower) Zig FFI build + unit-test signal. |
| 27 | + |
| 28 | +`e2e.yml` therefore runs, with Zig provisioned by `mlugg/setup-zig@v1` at |
| 29 | +`0.15.2` (the `build.zig.zon` minimum): |
| 30 | + |
| 31 | + zig build --build-file build_standalone.zig # E2E build |
| 32 | + zig build test --build-file build_standalone.zig # E2E tests |
| 33 | + zig build bench --build-file build_standalone.zig || … # Bench (soft) |
| 34 | + |
| 35 | +## The full pipeline (recipe — Idris half verified locally) |
| 36 | + |
| 37 | +The canonical recipe is the root `Justfile` (`build-refc` + `build-ffi`). |
| 38 | +Verified locally on idris2-0.8.0 + contrib: |
| 39 | + |
| 40 | + # Step 1 — Idris → RefC C (scripts/build-refc.sh, IPKG=proven-ffi.ipkg) |
| 41 | + idris2 --codegen refc --build proven-ffi.ipkg # → build/exec/proven-ffi.c |
| 42 | + # staged to build/refc/ ; the script prints the four paths used below |
| 43 | + |
| 44 | + # Step 2 — Zig links the RefC C + Idris runtime/support into libproven |
| 45 | + PFX=$(idris2 --prefix) |
| 46 | + zig build \ |
| 47 | + -Didris-refc="$PWD/build/refc" \ |
| 48 | + -Didris-refc-runtime="$(find "$PFX" -path '*/support/refc' -type d | head -1)" \ |
| 49 | + -Didris-c-support="$(find "$PFX" -path '*/support/c' -type d | head -1)" \ |
| 50 | + -Didris-support-lib="$(find "$PFX" -path '*/lib/libidris2_support.*' | head -1 | xargs dirname)" |
| 51 | + |
| 52 | +Requires `libgmp` (the RefC runtime links `gmp`/`pthread`/`m`). |
| 53 | + |
| 54 | +## Enabling full integration in CI (deferred — #151) |
| 55 | + |
| 56 | +The default `build.zig` needs `nextgen-languages/language-bridges` present. |
| 57 | +Because it is **private** and **not** a submodule, CI cannot fetch it today. |
| 58 | +To enable: |
| 59 | + |
| 60 | +1. Add `language-bridges` as a **git submodule** inside `proven`, and point |
| 61 | + `ffi/zig/build.zig.zon`'s `.path` at the in-repo submodule location (the |
| 62 | + current `../../../…` escapes the repo, so it must change). |
| 63 | +2. Add a **CI read credential** (deploy key / PAT) and use `actions/checkout` |
| 64 | + with `submodules: true`. |
| 65 | +3. Add/extend a workflow that installs Idris2 + `libgmp`, runs |
| 66 | + `scripts/build-refc.sh`, then the `zig build -Didris-*` invocation above. |
| 67 | + |
| 68 | +Tracked in #151. The interim standalone build is ADR-003. |
0 commit comments