|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +# |
| 5 | +# install-idris2.sh — provision Idris2 for the Ephapax ABI + formal proofs |
| 6 | +# (src/abi/ephapax-abi.ipkg, src/formal/ephapax-formal.ipkg). |
| 7 | +# |
| 8 | +# Follows the `iseriser/scripts/install-zig.sh` doctrine: |
| 9 | +# * curl + tar over HTTPS — NEVER `git clone`. The agent/CI proxy |
| 10 | +# scopes the GIT protocol to one repo (so `git clone idris-lang/Idris2` |
| 11 | +# → 403), but allowlists HTTPS to github.com / codeload.github.com. |
| 12 | +# A source *tarball* from codeload is a normal HTTPS GET → 200. |
| 13 | +# * pinned version (IDRIS2_VERSION), idempotent (early-exit if present), |
| 14 | +# * fail-soft: a missing Idris2 must NOT block setup or session start |
| 15 | +# (exit 0 on any fetch/build failure, with a diagnostic). |
| 16 | +# |
| 17 | +# Egress note: codeload.github.com is allowlisted by default. If your |
| 18 | +# environment's proxy is stricter, add `codeload.github.com` to the |
| 19 | +# HTTPS egress allowlist (same way ziglang.org is added for zig). |
| 20 | + |
| 21 | +set -uo pipefail |
| 22 | + |
| 23 | +IDRIS2_VERSION="${IDRIS2_VERSION:-0.7.0}" |
| 24 | +PREFIX="${PREFIX:-$HOME/.idris2}" |
| 25 | +SCHEME="${SCHEME:-chezscheme}" |
| 26 | + |
| 27 | +note() { printf '[install-idris2] %s\n' "$*" >&2; } |
| 28 | + |
| 29 | +# Idempotent: already the pinned version? Check both PATH *and* the install |
| 30 | +# location ($PREFIX/bin/idris2). The latter matters because callers may run |
| 31 | +# this before adding $PREFIX/bin to PATH, and we must NOT trigger a ~15-min |
| 32 | +# rebuild when idris2 is already installed. |
| 33 | +existing="$(command -v idris2 2>/dev/null || true)" |
| 34 | +[ -z "$existing" ] && [ -x "$PREFIX/bin/idris2" ] && existing="$PREFIX/bin/idris2" |
| 35 | +if [ -n "$existing" ]; then |
| 36 | + have="$("$existing" --version 2>/dev/null | grep -oE '[0-9]+\.[0-9]+\.[0-9]+' | head -1)" |
| 37 | + if [ "$have" = "$IDRIS2_VERSION" ]; then |
| 38 | + note "idris2 $IDRIS2_VERSION already installed ($existing) — skipping." |
| 39 | + exit 0 |
| 40 | + fi |
| 41 | +fi |
| 42 | + |
| 43 | +# Backend + C deps from apt (no cross-repo network). These are the two |
| 44 | +# that bit us the first time: chezscheme (the codegen backend) and |
| 45 | +# libgmp-dev (gmp.h, needed by the refc support lib at `make install`). |
| 46 | +if command -v apt-get >/dev/null 2>&1; then |
| 47 | + sudo apt-get update -qq || note "apt update failed (continuing)" |
| 48 | + sudo apt-get install -y --no-install-recommends \ |
| 49 | + "$SCHEME" libgmp-dev make gcc curl || note "apt install of backend deps failed" |
| 50 | +fi |
| 51 | +if ! command -v "$SCHEME" >/dev/null 2>&1; then |
| 52 | + note "Chez Scheme ($SCHEME) unavailable — cannot build Idris2. Skipping (non-blocking)." |
| 53 | + exit 0 |
| 54 | +fi |
| 55 | + |
| 56 | +work="$(mktemp -d)"; trap 'rm -rf "$work"' EXIT |
| 57 | +url="https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}" |
| 58 | +note "fetching Idris2 ${IDRIS2_VERSION} source via HTTPS (curl, not git): $url" |
| 59 | +if ! curl -fsSL -o "$work/idris2.tar.gz" "$url"; then |
| 60 | + note "download failed (proxy/egress?). Skipping — session start not blocked." |
| 61 | + exit 0 |
| 62 | +fi |
| 63 | +tar -xzf "$work/idris2.tar.gz" -C "$work" || { note "extract failed — skipping."; exit 0; } |
| 64 | +src="$work/Idris2-${IDRIS2_VERSION}" |
| 65 | + |
| 66 | +note "bootstrapping (SCHEME=$SCHEME, PREFIX=$PREFIX) …" |
| 67 | +if make -C "$src" bootstrap SCHEME="$SCHEME" PREFIX="$PREFIX" \ |
| 68 | + && make -C "$src" install PREFIX="$PREFIX"; then |
| 69 | + note "installed → $PREFIX/bin/idris2" |
| 70 | + note "add to PATH: export PATH=\"$PREFIX/bin:\$PATH\"" |
| 71 | + "$PREFIX/bin/idris2" --version >&2 || true |
| 72 | +else |
| 73 | + note "build/install failed — skipping (non-blocking). See logs above." |
| 74 | + exit 0 |
| 75 | +fi |
0 commit comments