Clarify static build helper side effects and failure behavior

.github/scripts/build-static.sh

@@ -0,0 +1,173 @@
+#!/bin/sh
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Build a fully static x86_64-linux-musl `ddraig` binary:
+#
+#   Ddraig.idr --(Idris 2 RefC backend)--> C --(zig cc, musl, -static)--> dist/ddraig
+#
+# linked against GMP and the Idris 2 C runtimes, both rebuilt here for musl
+# because the copies in the image are built for glibc. Why RefC and Zig, and
+# what this does not yet guarantee: RELEASING.adoc.
+#
+# DRAFT: written without running it. Run from the repository root inside the
+# digest-pinned idris2-pack image that ci.yml and release.yml use. Needs idris2,
+# git, make and gcc (in the image) plus curl, xz and m4 (installed by
+# release.yml). readelf comes with gcc's binutils.
+
+set -eu
+
+# --- Pins ---------------------------------------------------------------------
+# Zig: version and SHA-256 of the x86_64-linux tarball, from
+# https://ziglang.org/download/index.json, recorded 2026-10-13.
+ZIG_VERSION=0.16.0
+ZIG_SHA256=70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00
+# GMP: SHA-256 of gmp-6.3.0.tar.xz, computed 2026-10-13 from both gmplib.org and
+# ftp.gnu.org (identical). The GNU mirror is used because gmplib.org has
+# rate-limited CI runners in the past.
+GMP_VERSION=6.3.0
+GMP_SHA256=a3c2b80201b89e68616f4ad30bc66aee4927c3ce50e33929ca819d5c43538898
+# The Idris 2 commit inside the pinned image (its pack state holds
+# install/<commit>/idris2). The C runtimes are rebuilt from this commit, so it
+# must be the compiler's own commit; check_idris enforces that.
+IDRIS2_COMMIT=6ca00e72e32849cb35e5c262904e9c3cffc1a9a4
+
+TARGET=x86_64-linux-musl
+ROOT=$(pwd)
+WORK="$ROOT/build/static"
+DIST="$ROOT/dist"
+
+# log MESSAGE...: print a build progress message to stdout.
+log() { printf '==> %s\n' "$*"; }
+# die MESSAGE...: print a build error to stderr and exit with status 1.
+die() { printf 'build-static: %s\n' "$*" >&2; exit 1; }
+
+# fetch URL SHA256 DEST: download over HTTPS to DEST and verify its SHA-256.
+# Overwrites DEST; leaves it in place on checksum failure. Download or checksum
+# failures terminate the script with the failing command's exit status.
+fetch() {
+  curl --fail --silent --show-error --location --proto '=https' --tlsv1.2 \
+       --output "$3" "$1"
+  printf '%s  %s\n' "$2" "$3" | sha256sum --check --strict -
+}
+
+# The runtime sources must belong to the compiler that generates the C:
+#   1. the idris2 on PATH reports the pinned commit in its version string;
+#   2. pack has that commit installed;
+#   3. every RefC and C-support header it installed equals the source's.
+# Uses SRC as the source tree and PACK_STATE_DIR as pack's state directory.
+# Missing pack state or a version, layout or header mismatch exits the script
+# with status 1; idris2 --version failures propagate their exit status.
+check_idris() {
+  short=$(printf '%s' "$IDRIS2_COMMIT" | cut -c1-9)
+  version=$(idris2 --version)
+  case "$version" in
+    *"$short"*) ;;
+    *) die "idris2 reports '$version', not commit $short; update IDRIS2_COMMIT when the image digest changes" ;;
+  esac
+  [ -n "${PACK_STATE_DIR:-}" ] \
+    || die "PACK_STATE_DIR is unset; run inside the pinned idris2-pack image"
+  set -- "$PACK_STATE_DIR/install/$IDRIS2_COMMIT/idris2"/idris2-*
+  [ $# -eq 1 ] && [ -d "$1" ] \
+    || die "expected one idris2-<version> directory for commit $IDRIS2_COMMIT, found: $*"
+  inst=$1
+  for h in "$SRC"/support/refc/*.h "$SRC"/support/c/*.h; do
+    sub=$(basename "$(dirname "$h")")
+    [ -f "$inst/support/$sub/$(basename "$h")" ] \
+      || die "the image has no support/$sub/$(basename "$h")"
+    cmp -s "$h" "$inst/support/$sub/$(basename "$h")" \
+      || die "support/$sub/$(basename "$h") differs between the image and Idris 2 $IDRIS2_COMMIT"
+  done
+}
+
+mkdir -p "$WORK" "$DIST"
+
+# --- Zig ----------------------------------------------------------------------
+log "Zig $ZIG_VERSION"
+zig_dir="$WORK/zig-x86_64-linux-$ZIG_VERSION"
+if [ ! -x "$zig_dir/zig" ]; then
+  fetch "https://ziglang.org/download/$ZIG_VERSION/zig-x86_64-linux-$ZIG_VERSION.tar.xz" \
+        "$ZIG_SHA256" "$WORK/zig.tar.xz"
+  tar -xJf "$WORK/zig.tar.xz" -C "$WORK"
+fi
+ZIG="$zig_dir/zig"
+"$ZIG" version
+# ccm ARG...: invoke Zig's C compiler for TARGET at -O2, forwarding ARG.
+ccm() { "$ZIG" cc -target "$TARGET" -O2 "$@"; }
+
+# --- Idris 2 runtime sources, at the compiler's commit ------------------------
+log "Idris 2 sources at $IDRIS2_COMMIT"
+SRC="$WORK/idris2-src"
+if [ ! -d "$SRC/.git" ]; then
+  git init --quiet "$SRC"
+  git -C "$SRC" fetch --quiet --depth 1 https://github.com/idris-lang/Idris2 "$IDRIS2_COMMIT"
+  git -C "$SRC" checkout --quiet FETCH_HEAD
+fi
+[ "$(git -C "$SRC" rev-parse HEAD)" = "$IDRIS2_COMMIT" ] \
+  || die "checked out the wrong Idris 2 commit"
+check_idris
+
+# --- GMP, static, for musl ----------------------------------------------------
+log "GMP $GMP_VERSION for $TARGET"
+GMP="$WORK/gmp-$TARGET"
+if [ ! -f "$GMP/lib/libgmp.a" ]; then
+  fetch "https://ftp.gnu.org/gnu/gmp/gmp-$GMP_VERSION.tar.xz" "$GMP_SHA256" "$WORK/gmp.tar.xz"
+  rm -rf "$WORK/gmp-$GMP_VERSION"
+  tar -xJf "$WORK/gmp.tar.xz" -C "$WORK"
+  (
+    cd "$WORK/gmp-$GMP_VERSION"
+    # Portable C only (--disable-assembly): Ddraig's Integer use is trivial,
+    # and generic C avoids assembler differences between gcc and zig cc.
+    ./configure --prefix="$GMP" --disable-shared --enable-static --disable-assembly \
+      CC="$ZIG cc -target $TARGET" AR="$ZIG ar" RANLIB="$ZIG ranlib" CFLAGS=-O2
+    make -j"$(nproc)"
+    make check
+    make install
+  )
+fi
+
+# --- Idris 2 C runtimes, static, for musl -------------------------------------
+# Same sources and flags as support/c/Makefile and support/refc/Makefile
+# (every *.c in the directory, -O2), compiled with zig cc instead of gcc.
+log "Idris 2 C runtimes for $TARGET"
+RT="$WORK/runtime-$TARGET"
+rm -rf "$RT"
+mkdir -p "$RT"
+for f in "$SRC"/support/c/*.c; do
+  ccm -I"$SRC/support/c" -I"$GMP/include" -c "$f" -o "$RT/c_$(basename "$f" .c).o"
+done
+"$ZIG" ar rcs "$RT/libidris2_support.a" "$RT"/c_*.o
+for f in "$SRC"/support/refc/*.c; do
+  ccm -I"$SRC/support/refc" -I"$SRC/support/c" -I"$GMP/include" \
+      -c "$f" -o "$RT/refc_$(basename "$f" .c).o"
+done
+"$ZIG" ar rcs "$RT/libidris2_refc.a" "$RT"/refc_*.o
+
+# --- Ddraig -> C -> static binary ---------------------------------------------
+# RefC writes build/exec/ddraig-refc.c and then links a glibc binary with the
+# image's gcc. We keep only the C file and link it ourselves.
+log "RefC: Ddraig.idr -> C"
+idris2 --cg refc Ddraig.idr -o ddraig-refc
+CSRC="$ROOT/build/exec/ddraig-refc.c"
+[ -f "$CSRC" ] || die "RefC did not leave $CSRC"
+
+log "Link static $TARGET binary"
+ccm -static -s \
+    -I"$SRC/support/refc" -I"$SRC/support/c" -I"$GMP/include" \
+    "$CSRC" "$RT/libidris2_refc.a" "$RT/libidris2_support.a" "$GMP/lib/libgmp.a" -lm \
+    -o "$DIST/ddraig"
+
+log "Check the binary is fully static"
+# Capture readelf's output first: piping it straight into grep would let a
+# readelf failure pass silently, because sh has no pipefail.
+command -v readelf > /dev/null || die "readelf not found (binutils)"
+headers=$(readelf --wide --program-headers "$DIST/ddraig")
+dynamic=$(readelf --wide --dynamic "$DIST/ddraig")
+case "$headers" in
+  *INTERP*) die "dist/ddraig asks for a dynamic loader (PT_INTERP)" ;;
+esac
+case "$dynamic" in
+  *NEEDED*) die "dist/ddraig needs shared libraries (DT_NEEDED)" ;;
+esac
+"$DIST/ddraig" --version
+sha256sum "$DIST/ddraig"

.github/scripts/check-idris-version.sh

@@ -0,0 +1,31 @@
+#!/bin/sh
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Fail unless the idris2 on PATH is at least the minimum version this project
+# supports (README.adoc: "Requires idris2 >= 0.8.0").
+#
+# usage: check-idris-version.sh [MINIMUM]     (default 0.8.0)
+#
+# DRAFT: not yet run. See RELEASING.adoc.
+
+set -eu
+
+min=${1:-0.8.0}
+out=$(idris2 --version)
+printf '%s\n' "$out"
+
+# "Idris 2, version 0.8.0-6ca00e72e" -> "0.8.0"
+ver=$(printf '%s\n' "$out" |
+      sed -n 's/.*version \([0-9][0-9]*\.[0-9][0-9]*\.[0-9][0-9]*\).*/\1/p')
+if [ -z "$ver" ]; then
+  printf 'check-idris-version: cannot read a version from: %s\n' "$out" >&2
+  exit 1
+fi
+
+lowest=$(printf '%s\n%s\n' "$min" "$ver" | sort -V | head -n 1)
+if [ "$lowest" != "$min" ]; then
+  printf 'check-idris-version: Idris 2 %s is older than the minimum %s\n' "$ver" "$min" >&2
+  exit 1
+fi
+printf 'OK: Idris 2 %s >= %s\n' "$ver" "$min"

.github/scripts/test-static.sh

@@ -0,0 +1,164 @@
+#!/bin/sh
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Check the static release binary (RefC backend) against the reference binary
+# (Chez backend, the one CI tests). They must behave identically:
+#
+#   1. every CI test subcommand passes and prints exactly what the reference prints;
+#   2. validate-state accepts this repo's STATE descriptile;
+#   3. building examples/ and a fixture site gives byte-identical output trees;
+#   4. a large page builds without crashing (C stack depth; see RELEASING.adoc)
+#      and also matches the reference.
+#
+# usage: test-static.sh STATIC_BINARY REFERENCE_BINARY
+#
+# DRAFT: not yet run. See RELEASING.adoc.
+#
+# Run from the repository root. The fixture site written below adds what
+# examples/ lacks: a nested page, a draft, and more Markdown constructs.
+#
+# Known false alarm: the attestation file records the build day, so if the two
+# builds straddle 00:00 UTC their output trees differ. Re-run.
+
+set -eu
+
+[ $# -eq 2 ] || { echo "usage: $0 STATIC_BINARY REFERENCE_BINARY" >&2; exit 2; }
+static=$1
+ref=$2
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+
+# fail MESSAGE...: print a failed check to stderr and exit with status 1.
+fail() { printf 'test-static: FAIL: %s\n' "$*" >&2; exit 1; }
+# pass MESSAGE...: print a successful check to stdout.
+pass() { printf 'test-static: ok: %s\n' "$*"; }
+
+# same_output NAME CMD...: run CMD with each binary; both must succeed and
+# print the same bytes.
+same_output() {
+  name=$1
+  shift
+  "$static" "$@" > "$work/$name.static" 2>&1 || fail "$name: static binary exited non-zero"
+  "$ref" "$@" > "$work/$name.ref" 2>&1 || fail "$name: reference binary exited non-zero"
+  if ! cmp -s "$work/$name.ref" "$work/$name.static"; then
+    diff -u "$work/$name.ref" "$work/$name.static" | head -n 60
+    fail "$name: output differs from the reference"
+  fi
+  pass "$name"
+}
+
+# same_site NAME SRC: build SRC with each binary and compare the output trees.
+same_site() {
+  name=$1
+  src=$2
+  "$static" build "$src" "$work/$name.out.static" https://example.org > "$work/$name.log.static" 2>&1 \
+    || { cat "$work/$name.log.static"; fail "$name: static build failed"; }
+  "$ref" build "$src" "$work/$name.out.ref" https://example.org > "$work/$name.log.ref" 2>&1 \
+    || { cat "$work/$name.log.ref"; fail "$name: reference build failed"; }
+  if ! diff -r "$work/$name.out.ref" "$work/$name.out.static" > "$work/$name.diff"; then
+    head -n 60 "$work/$name.diff"
+    fail "$name: output tree differs from the reference"
+  fi
+  pass "$name ($(find "$work/$name.out.static" -type f | wc -l) files identical)"
+}
+
+# --- 1 and 2: CLI and test subcommands ---------------------------------------
+same_output version --version
+for t in test-markdown test-frontmatter test-full test-state test-attest; do
+  same_output "$t" "$t"
+done
+same_output validate-state validate-state .machine_readable/descriptiles/STATE.a2ml
+
+# --- 3: examples/ and a fixture site -------------------------------------------
+same_site examples examples
+# Every page has exactly one h1 and no skipped heading levels, or the build's
+# accessibility certification (O3) fails it.
+site="$work/site"
+mkdir -p "$site/blog" "$site/public"
+cat > "$site/index.md" <<'EOF'
+---
+title: Home
+date: 2026-01-15
+description: Fixture home page
+site: Fixture
+tags: [idris, ssg]
+---
+
+# Home
+
+Some **bold**, *italic*, ~~struck~~ and `code` text with a [link](https://example.org/x).
+
+![A red dragon](dragon.png)
+
+## Lists
+
+- one
+- two
+  - nested
+1. first
+2. second
+
+> a quote
+
+| a | b |
+|---|---|
+| 1 | 2 |
+
+```idris
+main : IO ()
+```
+
+---
+EOF
+cat > "$site/blog/post.md" <<'EOF'
+---
+title: A post
+date: 2026-02-01T09:30:00Z
+description: Second page
+---
+
+# A post
+
+## Part one
+
+### Detail
+
+Text & entities < > "quotes".
+EOF
+cat > "$site/draft.md" <<'EOF'
+---
+title: Not yet
+draft: true
+---
+
+# Not yet
+EOF
+printf 'User-agent: *\nAllow: /\n' > "$site/public/robots.txt"
+same_site fixture "$site"
+[ ! -e "$work/fixture.out.static/draft.html" ] || fail "fixture: draft page was built"
+
+# --- 4: large page -------------------------------------------------------------
+# The C stack does not grow the way Chez's does, so deep non-tail recursion is
+# the most likely way for the static binary to fail where the reference
+# succeeds. The block parser recurses once per block, so this page has many
+# short blocks. BIG_BLOCKS (default 5000, a very long article) sets the size;
+# the fork dry-run records where each binary actually fails (RELEASING.adoc).
+# One long paragraph would be the wrong stress test: the inline parser re-packs
+# the rest of the paragraph at every delimiter, which is quadratic in its length.
+n=${BIG_BLOCKS:-5000}
+big="$work/big"
+mkdir -p "$big"
+{
+  printf '%s\n' '---' 'title: Large' 'date: 2026-03-01' '---' '' '# Large' ''
+  awk -v n="$n" 'BEGIN {
+    for (i = 0; i < n; i++) {
+      if (i % 50 == 0) printf "## Section %d\n\n", i / 50
+      printf "Paragraph %d has **bold**, `code` and a [link](https://example.org/%d).\n\n", i, i
+    }
+  }'
+} > "$big/index.md"
+pass "large page: $n blocks, $(wc -c < "$big/index.md") bytes"
+same_site large "$big"
+
+echo "test-static: all checks passed"