Skip to content

Commit 13208cd

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
iseriser: auto-install pinned Zig toolchain in setup + devcontainer (#70)
* iseriser: codegen emits verified, compiling Idris2 ABI (P2) The scaffold generator still emitted the old flat, never-compiled ABI template: files at `src/interface/abi/{Types,Layout,Foreign}.idr` with a namespace they didn't match, a `Layout.idr` whose `modNatNZ ... == 0` proof does not reduce at the type level, no `Proofs.idr`, and no `.ipkg`. Every newly-generated -iser therefore started with a broken ABI — exactly the bug a prior session hand-fixed across the family. Rewrite the Idris2 ABI generators to emit the verified reference pattern, proven to compile clean under Idris2 0.7.0 (zero warnings, no believe_me/postulate/holes): - Nested modules at `src/interface/abi/<Mod>/ABI/{Types,Layout,Foreign, Proofs}.idr` so each file's path matches its namespace, plus `src/interface/abi/<iser>-abi.ipkg` (sourcedir=".", lists all four). - Types: `Result` with a complete `DecEq` (explicit off-diagonals, not `No absurd`), a non-null `Handle` built via `choose`, and a primitive enum with a tag-based `Eq` that is warning-free for any arity. - Layout: real `Divides`/`StructLayout`/`FieldsAligned` machinery and one concrete, provably C-ABI-compliant context layout. - Proofs: a non-vacuous `CABICompliant` theorem (each offset pinned by `DivideBy k Refl`, qualified layout name so it doesn't auto-bind), the result-code round-trip, and a Nat-level negative control. Verified: perturbing a field offset makes the proof fail to typecheck. Tests: assert the generated tree is self-consistent (every ipkg module present at its namespace path, no leftover template tokens, old flat path gone) and add an end-to-end test that runs `idris2 --build` on the generated ABI when the toolchain is present (no-op otherwise, so CI without idris2 stays green). Update the integration tests for the new paths and the real proof module. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH * iseriser: 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: - `setup.sh` gains a "Step 1b: Install Zig toolchain" that runs it. - a new `deps` Justfile recipe (installs Zig, warms Cargo) backs the devcontainer `postCreateCommand: just deps`, which previously errored. Once ziglang.org is allowlisted, future setups and dev containers install Zig automatically with no further change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 1b23126 commit 13208cd

3 files changed

Lines changed: 75 additions & 0 deletions

File tree

‎Justfile‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,3 +133,9 @@ crg-badge:
133133
D) color="orange" ;; E) color="red" ;; F) color="critical" ;; \
134134
*) color="lightgrey" ;; esac; \
135135
echo "[![CRG $$grade](https://img.shields.io/badge/CRG-$$grade-$$color?style=flat-square)](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)"
136+
137+
# Install dev dependencies (invoked by the devcontainer postCreateCommand).
138+
# Installs the pinned Zig FFI toolchain, then warms the Cargo cache.
139+
deps:
140+
./scripts/install-zig.sh
141+
cargo fetch

‎scripts/install-zig.sh‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
#!/bin/sh
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
#
5+
# install-zig.sh — install the pinned Zig toolchain (the Zig FFI bridge half of
6+
# the ABI-FFI standard). Idempotent and fail-soft: it never aborts the caller.
7+
#
8+
# Egress note: Zig is NOT distributed via GitHub releases, so it is fetched from
9+
# ziglang.org. Inside a Claude Code session, outbound HTTPS goes through the
10+
# policy-enforcing agent proxy; github.com is allowlisted by default but
11+
# ziglang.org must be added explicitly, or this download returns 403. We use the
12+
# system CA store the proxy already populated — never pass --insecure.
13+
set -eu
14+
15+
ZIG_VERSION="${ZIG_VERSION:-0.14.0}"
16+
PREFIX="${ZIG_PREFIX:-/usr/local}"
17+
18+
# Already at the pinned version? Done.
19+
if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then
20+
echo "install-zig: zig $ZIG_VERSION already installed"
21+
exit 0
22+
fi
23+
24+
# Map host arch/OS to Zig's release naming.
25+
case "$(uname -m)" in
26+
x86_64|amd64) zarch="x86_64" ;;
27+
aarch64|arm64) zarch="aarch64" ;;
28+
*) echo "install-zig: unsupported arch $(uname -m); install Zig $ZIG_VERSION manually" >&2; exit 0 ;;
29+
esac
30+
case "$(uname -s)" in
31+
Linux) zos="linux" ;;
32+
Darwin) zos="macos" ;;
33+
*) echo "install-zig: unsupported OS $(uname -s); install Zig $ZIG_VERSION manually" >&2; exit 0 ;;
34+
esac
35+
36+
tarball="zig-${zos}-${zarch}-${ZIG_VERSION}.tar.xz"
37+
url="https://ziglang.org/download/${ZIG_VERSION}/${tarball}"
38+
dest="${PREFIX}/lib/zig-${ZIG_VERSION}"
39+
40+
tmp="$(mktemp -d)"
41+
trap 'rm -rf "$tmp"' EXIT
42+
43+
echo "install-zig: fetching $url"
44+
if ! curl -fsSL --retry 2 -o "$tmp/$tarball" "$url"; then
45+
echo "install-zig: download failed (HTTP error or blocked host)." >&2
46+
echo "install-zig: if this is a Claude Code session, add 'ziglang.org' to the" >&2
47+
echo " egress allowlist — github.com is allowed but ziglang.org is not." >&2
48+
exit 0 # fail-soft: a missing Zig must not block setup or session start
49+
fi
50+
51+
mkdir -p "$dest" "${PREFIX}/bin"
52+
tar -xJf "$tmp/$tarball" -C "$dest" --strip-components=1
53+
ln -sf "$dest/zig" "${PREFIX}/bin/zig"
54+
55+
if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then
56+
echo "install-zig: installed zig $(zig version)"
57+
else
58+
echo "install-zig: installed to ${PREFIX}/bin/zig — ensure ${PREFIX}/bin is on PATH" >&2
59+
fi

‎setup.sh‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -195,6 +195,16 @@ main() {
195195
install_just || { fail "Cannot proceed without just"; exit 1; }
196196
printf "\n"
197197

198+
# Step 1b: Install the pinned Zig toolchain (the Zig FFI bridge half of the
199+
# ABI-FFI standard). Best-effort — see scripts/install-zig.sh.
200+
printf "%sStep 1b: Install Zig toolchain%s\n" "$BOLD" "$RESET"
201+
if [ -x ./scripts/install-zig.sh ]; then
202+
./scripts/install-zig.sh || warn "Zig install skipped (see scripts/install-zig.sh)"
203+
else
204+
warn "scripts/install-zig.sh not found — skipping Zig install"
205+
fi
206+
printf "\n"
207+
198208
# Step 2: Check if we're in the repo directory
199209
if [ ! -f "Justfile" ] && [ ! -f "justfile" ]; then
200210
warn "Not in a repo directory (no Justfile found)"

0 commit comments

Comments
 (0)