From cdfbc91aee82588e9c297fcf86448c2eee89cc2a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 21:09:40 +0000 Subject: [PATCH 1/2] Auto-install pinned Zig toolchain in setup + devcontainer The Zig FFI bridge is half of the ABI-FFI standard, but nothing installed Zig: .tool-versions only lists it (commented), setup.sh stops at `just`, and the devcontainer's `postCreateCommand: just deps` referenced a `deps` recipe that did not exist. Unlike the other toolchain pieces, Zig is not distributed via GitHub releases, so it must come from ziglang.org. Add scripts/install-zig.sh: an idempotent, fail-soft installer for the pinned Zig 0.14.0 (arch/OS-aware, uses the system CA store the agent proxy populates, never --insecure). If ziglang.org is not on the session's egress allowlist the download 403s and the script exits 0 with an actionable message, so it never blocks setup or a session. Wire it in via the two paths the project already uses: a "Step 1b" in setup.sh (where the template exposes that step), and a new `deps` Justfile recipe backing the devcontainer postCreateCommand. Once ziglang.org is allowlisted, future setups and dev containers install Zig automatically. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- Justfile | 6 +++++ scripts/install-zig.sh | 59 ++++++++++++++++++++++++++++++++++++++++++ setup.sh | 9 +++++++ 3 files changed, 74 insertions(+) create mode 100755 scripts/install-zig.sh diff --git a/Justfile b/Justfile index 26e2a23..7472e61 100644 --- a/Justfile +++ b/Justfile @@ -128,3 +128,9 @@ crg-badge: D) color="orange" ;; E) color="red" ;; F) color="critical" ;; \ *) color="lightgrey" ;; esac; \ echo "[![CRG $$grade](https://img.shields.io/badge/CRG-$$grade-$$color?style=flat-square)](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)" + +# Install dev dependencies (invoked by the devcontainer postCreateCommand). +# Installs the pinned Zig FFI toolchain, then warms the Cargo cache. +deps: + ./scripts/install-zig.sh + cargo fetch diff --git a/scripts/install-zig.sh b/scripts/install-zig.sh new file mode 100755 index 0000000..63edd64 --- /dev/null +++ b/scripts/install-zig.sh @@ -0,0 +1,59 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# install-zig.sh — install the pinned Zig toolchain (the Zig FFI bridge half of +# the ABI-FFI standard). Idempotent and fail-soft: it never aborts the caller. +# +# Egress note: Zig is NOT distributed via GitHub releases, so it is fetched from +# ziglang.org. Inside a Claude Code session, outbound HTTPS goes through the +# policy-enforcing agent proxy; github.com is allowlisted by default but +# ziglang.org must be added explicitly, or this download returns 403. We use the +# system CA store the proxy already populated — never pass --insecure. +set -eu + +ZIG_VERSION="${ZIG_VERSION:-0.14.0}" +PREFIX="${ZIG_PREFIX:-/usr/local}" + +# Already at the pinned version? Done. +if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then + echo "install-zig: zig $ZIG_VERSION already installed" + exit 0 +fi + +# Map host arch/OS to Zig's release naming. +case "$(uname -m)" in + x86_64|amd64) zarch="x86_64" ;; + aarch64|arm64) zarch="aarch64" ;; + *) echo "install-zig: unsupported arch $(uname -m); install Zig $ZIG_VERSION manually" >&2; exit 0 ;; +esac +case "$(uname -s)" in + Linux) zos="linux" ;; + Darwin) zos="macos" ;; + *) echo "install-zig: unsupported OS $(uname -s); install Zig $ZIG_VERSION manually" >&2; exit 0 ;; +esac + +tarball="zig-${zos}-${zarch}-${ZIG_VERSION}.tar.xz" +url="https://ziglang.org/download/${ZIG_VERSION}/${tarball}" +dest="${PREFIX}/lib/zig-${ZIG_VERSION}" + +tmp="$(mktemp -d)" +trap 'rm -rf "$tmp"' EXIT + +echo "install-zig: fetching $url" +if ! curl -fsSL --retry 2 -o "$tmp/$tarball" "$url"; then + echo "install-zig: download failed (HTTP error or blocked host)." >&2 + echo "install-zig: if this is a Claude Code session, add 'ziglang.org' to the" >&2 + echo " egress allowlist — github.com is allowed but ziglang.org is not." >&2 + exit 0 # fail-soft: a missing Zig must not block setup or session start +fi + +mkdir -p "$dest" "${PREFIX}/bin" +tar -xJf "$tmp/$tarball" -C "$dest" --strip-components=1 +ln -sf "$dest/zig" "${PREFIX}/bin/zig" + +if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then + echo "install-zig: installed zig $(zig version)" +else + echo "install-zig: installed to ${PREFIX}/bin/zig — ensure ${PREFIX}/bin is on PATH" >&2 +fi diff --git a/setup.sh b/setup.sh index 7e2c769..83af887 100755 --- a/setup.sh +++ b/setup.sh @@ -194,6 +194,15 @@ main() { printf "%sStep 1: Install task runner%s\n" "$BOLD" "$RESET" install_just || { fail "Cannot proceed without just"; exit 1; } printf "\n" + # Step 1b: Install the pinned Zig toolchain (the Zig FFI bridge half of the + # ABI-FFI standard). Best-effort — see scripts/install-zig.sh. + printf "%sStep 1b: Install Zig toolchain%s\n" "$BOLD" "$RESET" + if [ -x ./scripts/install-zig.sh ]; then + ./scripts/install-zig.sh || warn "Zig install skipped (see scripts/install-zig.sh)" + else + warn "scripts/install-zig.sh not found — skipping Zig install" + fi + printf "\n" # Step 2: Check if we're in the repo directory if [ ! -f "Justfile" ] && [ ! -f "justfile" ]; then From fd86ce993dec6d8503228d3fc5c5118d37d74a27 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 22:59:34 +0000 Subject: [PATCH 2/2] =?UTF-8?q?ci:=20add=20ABI=E2=86=94FFI=20conformance?= =?UTF-8?q?=20gate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds scripts/abi-ffi-gate.py (fails on a declared ABI C function with no Zig export, a mismatched result-code map, or an unrendered template token) and a .github/workflows/abi-ffi-gate.yml that runs it plus a Zig 0.14.0 build/test of the FFI. The Idris2 ABI is the source of truth. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- .github/workflows/abi-ffi-gate.yml | 38 +++++++++++ scripts/abi-ffi-gate.py | 103 +++++++++++++++++++++++++++++ 2 files changed, 141 insertions(+) create mode 100644 .github/workflows/abi-ffi-gate.yml create mode 100755 scripts/abi-ffi-gate.py diff --git a/.github/workflows/abi-ffi-gate.yml b/.github/workflows/abi-ffi-gate.yml new file mode 100644 index 0000000..269464d --- /dev/null +++ b/.github/workflows/abi-ffi-gate.yml @@ -0,0 +1,38 @@ +# SPDX-License-Identifier: MPL-2.0 +# abi-ffi-gate.yml — enforce that the Zig FFI conforms to the Idris2 ABI. +# +# The Idris2 ABI (src/interface/abi) is the source of truth. This gate fails if +# the Zig FFI (src/interface/ffi) drifts from it: a declared C function with no +# export, a mismatched result-code map, or an unrendered template token. A +# second job builds + tests the Zig FFI under the pinned Zig 0.14.0. +name: ABI-FFI Gate + +on: + pull_request: + push: + branches: [main, master] + +permissions: + contents: read + +jobs: + conformance: + name: ABI ↔ FFI structural conformance + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Run ABI-FFI gate + run: python3 scripts/abi-ffi-gate.py + + zig-build: + name: Zig FFI builds + tests (Zig 0.14.0) + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install Zig 0.14.0 + run: | + curl -fsSL https://ziglang.org/download/0.14.0/zig-linux-x86_64-0.14.0.tar.xz -o /tmp/zig.tar.xz + tar -xf /tmp/zig.tar.xz -C /tmp + echo "/tmp/zig-linux-x86_64-0.14.0" >> "$GITHUB_PATH" + - name: zig test FFI + run: zig test src/interface/ffi/src/main.zig -lc diff --git a/scripts/abi-ffi-gate.py b/scripts/abi-ffi-gate.py new file mode 100755 index 0000000..9ee96db --- /dev/null +++ b/scripts/abi-ffi-gate.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# abi-ffi-gate.py — fail (exit 1) if the Zig FFI does not conform to the Idris2 +# ABI. The Idris2 ABI is the source of truth. Checks, with no toolchain needed: +# +# 1. the Zig FFI carries no unrendered `{{...}}` template tokens; +# 2. every `%foreign "C:"` symbol declared anywhere in the ABI .idr +# sources is exported by the Zig FFI (`export fn `); +# 3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH +# names and integer values (the `Error`/`err` spelling is treated as one). +# +# Usage: python3 scripts/abi-ffi-gate.py [repo_root] (defaults to cwd) + +import os +import re +import sys +import glob + + +def camel_to_snake(s): + return re.sub(r"(? len(best): + best = variants + return best + + +def main(): + root = sys.argv[1] if len(sys.argv) > 1 else "." + name = os.path.basename(os.path.abspath(root)) + abi_dir = os.path.join(root, "src/interface/abi") + zig_path = os.path.join(root, "src/interface/ffi/src/main.zig") + errs = [] + + idr_files = [ + p for p in glob.glob(os.path.join(abi_dir, "**", "*.idr"), recursive=True) + if os.sep + "build" + os.sep not in p + ] + if not idr_files: + print(f"ABI-FFI GATE: SKIP ({name}) — no Idris2 ABI .idr files under {abi_dir}") + return 0 + if not os.path.exists(zig_path): + print(f"ABI-FFI GATE: FAIL ({name}) — no Zig FFI at {zig_path}") + return 1 + + idr = "\n".join(open(p, encoding="utf-8").read() for p in idr_files) + zig = open(zig_path, encoding="utf-8").read() + + # 1. unrendered template tokens + toks = sorted(set(re.findall(r"\{\{[A-Za-z0-9_]+\}\}", zig))) + if toks: + errs.append(f"Zig FFI has unrendered template tokens: {toks}") + + # 2. foreign C symbols must be exported + csyms = sorted(set(re.findall(r"C:([A-Za-z0-9_]+)", idr))) + exports = set(re.findall(r"export fn ([A-Za-z0-9_]+)", zig)) + missing = [s for s in csyms if s not in exports] + if missing: + errs.append(f"{len(missing)} ABI function(s) not exported by the Zig FFI: {missing}") + + # 3. result-code map (names + values) must agree + idr_rc = {} + for m in re.finditer(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr): + idr_rc[canon_rc(camel_to_snake(m.group(1)))] = int(m.group(2)) + zig_rc = find_result_enum(zig) + if idr_rc and not zig_rc: + errs.append("no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes") + elif idr_rc and zig_rc and idr_rc != zig_rc: + errs.append( + "Result-code map differs (name or value):\n" + f" Idris resultToInt: {dict(sorted(idr_rc.items()))}\n" + f" Zig Result enum: {dict(sorted(zig_rc.items()))}" + ) + + if errs: + print(f"ABI-FFI GATE: FAIL ({name})") + for e in errs: + print(" - " + e) + return 1 + print(f"ABI-FFI GATE: OK ({name}) — {len(csyms)} ABI functions exported, " + f"{len(idr_rc)} result codes match") + return 0 + + +if __name__ == "__main__": + sys.exit(main())