Skip to content
Merged
126 changes: 126 additions & 0 deletions tools/setup/common/curl-fetch.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,126 @@
#!/usr/bin/env bash
#
# tools/setup/common/curl-fetch.sh — sourceable helper for
# fetching URLs with uniform retry behaviour during install.
#
# WHY
# ===
# Human maintainer 2026-04-28: external-infra failures
# (upstream package mirrors returning 5xx, transient curl-22
# / network blips) should be absorbed by retry-with-backoff
# inside the install path, not kicked out to a workflow-rerun
# discipline. Quote: *"curl 502 pattern i mean why should a
# PR ever fail for this? our code does not handle the retries
# already?"*
#
# This file centralises the retry policy so every call site
# uses the same flags. Previously the policy was inlined in
# `tools/setup/common/verifiers.sh` and missing entirely from
# `linux.sh` (mise install), `macos.sh` (Homebrew install),
# and `elan.sh` (Lean toolchain install). Follow-up framing:
# *"sounds like a common helper would help too rather than
Comment thread
AceHack marked this conversation as resolved.
Outdated
# copy/paste."*
#
# TWO FUNCTIONS — file-output vs streamed
# =======================================
# Two helpers are exposed because the safe retry policy
# differs by output mode. Code review on the original single-
# function form flagged the partial-output-replay risk for
# pipe-to-shell call sites:
#
# curl_fetch — for file-output downloads
# (`-o`/`--output` to disk). Uses
# `--retry-all-errors` because curl
# restarts the file from scratch on
# retry, so partial-output replay
# cannot happen.
#
# curl_fetch_stream — for streamed-to-shell installers
# (`curl ... | sh`, `bash -c "$(curl
# ...)"`). Uses bare `--retry`
# (without `--retry-all-errors`) so
# curl will only retry on transient
# conditions where nothing has been
# written yet — avoiding the risk of
# a partial install script being
# piped, then the retry's full output
# appended on top.
Comment thread
AceHack marked this conversation as resolved.
Outdated
#
# USAGE
# =====
# Source this file, then call the appropriate helper:
#
# # shellcheck source=/dev/null
# source "$REPO_ROOT/tools/setup/common/curl-fetch.sh"
#
# # File output (safe with full retries):
# curl_fetch --output "$path" "$url"
#
# # Streamed pipe (must use the stream variant):
# curl_fetch_stream https://example.com/install.sh | sh
#
# # Command substitution (capture to var first; see
# # IDEMPOTENCE / SET-E note below):
# INSTALLER="$(curl_fetch_stream https://example.com/install.sh)"
# /bin/bash -c "$INSTALLER"
#
# RETRY POLICY (rationale)
# ========================
# --retry 5 — five attempts total. Empirically
# covers the upstream 5xx blips
# this install path has hit.
# --retry-delay 2 — 2-second base delay between retries.
# --retry-all-errors — (file-output only) retry on ALL
# transient errors including HTTP
# 5xx without `Retry-After`. Curl's
# default `--retry` only retries
# connect / DNS / 408 / 429 / 5xx-
# with-Retry-After.
# -fsSL — original flags preserved:
# -f: fail on HTTP errors
# -s: silent (no progress meter)
# -S: show errors when silent
# -L: follow redirects
#
# COMMAND-SUBSTITUTION + SET-E
# ============================
# Calling `bash -c "$(curl_fetch_stream ...)"` directly will
# silently swallow curl failures under `set -e` because the
# outer `bash -c` succeeds with an empty string. The pattern
# we use everywhere is: capture to a named variable first,
# then exec the variable. That way a curl failure aborts the
# variable assignment, which set -e *does* honour.
Comment thread
AceHack marked this conversation as resolved.
Outdated
#
# IDEMPOTENCE
# ===========
# Re-sourcing this file is a no-op once both helpers are
# loaded. The guard uses a file-local sentinel variable
# (`_CURL_FETCH_LOADED`) instead of probing for an
# existing `curl_fetch` function: a function-name probe
# would silently skip BOTH definitions if the caller
# environment already had an unrelated `curl_fetch`
# function, leaving `curl_fetch_stream` undefined and
# breaking the streamed callers (`linux.sh` / `macos.sh`
# / `elan.sh`) at runtime with `curl_fetch_stream:
# command not found`. Sentinel-based guarding ties the
# load decision to "did this file load?" instead of "does
# that name exist?" — collisions in the caller environment
# can no longer accidentally suppress our definitions.

if [[ -z "${_CURL_FETCH_LOADED:-}" ]]; then
_CURL_FETCH_LOADED=1

# File-output variant — safe with --retry-all-errors because
# curl restarts the output file from scratch on each retry.
curl_fetch() {
curl -fsSL --retry 5 --retry-delay 2 --retry-all-errors "$@"
Comment thread
AceHack marked this conversation as resolved.
}

# Streamed variant — bare --retry only, no --retry-all-errors,
# to avoid the partial-output-replay risk on pipe-to-shell or
# command-substitution-into-bash use sites.
curl_fetch_stream() {
curl -fsSL --retry 5 --retry-delay 2 "$@"
}

fi
9 changes: 8 additions & 1 deletion tools/setup/common/elan.sh
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,16 @@

set -euo pipefail

# shellcheck source=curl-fetch.sh
source "$(dirname "${BASH_SOURCE[0]}")/curl-fetch.sh"

if ! command -v elan >/dev/null 2>&1; then
echo "↓ installing elan (Lean 4 toolchain manager)..."
curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
# Use the stream variant (bare --retry only, no
# --retry-all-errors) — the curl output is piped directly
# into sh, and partial-output replay on retry would be a
# supply-chain hazard.
curl_fetch_stream https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
| sh -s -- -y --default-toolchain none
Comment thread
AceHack marked this conversation as resolved.
Outdated
fi

Expand Down
27 changes: 15 additions & 12 deletions tools/setup/common/verifiers.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,18 @@
# (TLC, Alloy) to `tools/tla/` and `tools/alloy/` respectively.
#
# Manifest format: `<target-dir>/<target-file> <url>` per line,
# comments starting with `#`. Per Aaron's round-29 call we do not
# verify checksums (trust-on-first-use); when upstream provides a
# published SHA256SUMS we may revisit.
# comments starting with `#`. Per the human maintainer's round-29
# call we do not verify checksums (trust-on-first-use); when
# upstream provides a published SHA256SUMS we may revisit.
#
# This replaces the legacy tools/install-verifiers.sh in the same
# commit (greenfield — no alias per GOVERNANCE.md §24 fallout).

set -euo pipefail

# shellcheck source=curl-fetch.sh
source "$(dirname "${BASH_SOURCE[0]}")/curl-fetch.sh"

REPO_ROOT="$(cd "$(dirname "$0")/../../.." && pwd)"
MANIFEST="$REPO_ROOT/tools/setup/manifests/verifiers"

Expand All @@ -35,7 +38,7 @@ grep -vE '^(#|$)' "$MANIFEST" | while IFS= read -r line; do
mkdir -p "$(dirname "$dest")"
if [ -f "$dest" ]; then
# Trust-on-first-use: if the file exists we assume it's intact.
# Per Aaron's round-29 call we do not re-verify content.
# Per the human maintainer's round-29 call we do not re-verify content.
echo "✓ $target already present"
else
# Download to a .part suffix then atomic-rename. Protects against
Expand All @@ -47,15 +50,15 @@ grep -vE '^(#|$)' "$MANIFEST" | while IFS= read -r line; do
# ~13:52 UTC, hit PR #481 CodeQL csharp + PR #482 markdownlint
# CI runs). Per Otto-285 (don't use determinism to avoid
# edge-case handling — handle the network-non-determinism
# algorithmically), curl handles the retry: `--retry 5` attempts,
# exponential backoff (2/4/8/16/32 s default), `--retry-all-errors`
# so 4xx/5xx server errors retry too (curl's default only retries
# connect / dns / 408 / 429 / 5xx-with-Retry-After). Keeps
# `-fsSL` semantics — fail at the end if all 5 attempts hit
# the same transient.
# algorithmically), curl_fetch (from common/curl-fetch.sh)
# handles the retry: 5 attempts, 2-4-8-16-32 s exponential
# backoff, --retry-all-errors so 4xx/5xx errors retry too.
# Keeps -fsSL semantics — fail at the end if all 5 attempts
# hit the same transient. (Human maintainer 2026-04-28
# framing: helper extracted from copy-pasted call sites; was
# previously inline here.)
echo "↓ downloading $target from $url"
curl -fsSL --retry 5 --retry-delay 2 --retry-all-errors \
-o "$dest.part" "$url"
curl_fetch -o "$dest.part" "$url"
mv "$dest.part" "$dest"
echo "✓ $target"
fi
Expand Down
9 changes: 8 additions & 1 deletion tools/setup/linux.sh
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,9 @@ set -euo pipefail
REPO_ROOT="$(cd "$(dirname "$0")/../.." && pwd)"
SETUP_DIR="$REPO_ROOT/tools/setup"

# shellcheck source=common/curl-fetch.sh
source "$SETUP_DIR/common/curl-fetch.sh"

# ── Detect apt availability (Debian/Ubuntu) ─────────────────────────
if ! command -v apt-get >/dev/null 2>&1; then
echo "error: this script currently supports Debian/Ubuntu only"
Expand Down Expand Up @@ -55,7 +58,11 @@ echo "✓ apt packages up to date"
# ── 2. mise ─────────────────────────────────────────────────────────
if ! command -v mise >/dev/null 2>&1; then
echo "↓ installing mise via the official installer..."
curl -fsSL https://mise.run | sh
# Use the stream variant (bare --retry only, no
# --retry-all-errors) — the curl output is piped directly
# into sh, and partial-output replay on retry would be a
# supply-chain hazard.
curl_fetch_stream https://mise.run | sh
Comment thread
AceHack marked this conversation as resolved.
Outdated
# The installer puts mise at $HOME/.local/bin/mise; ensure we can
# invoke it for the remainder of this script run.
export PATH="$HOME/.local/bin:$PATH"
Expand Down
12 changes: 11 additions & 1 deletion tools/setup/macos.sh
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,9 @@ set -euo pipefail
REPO_ROOT="$(cd "$(dirname "$0")/../.." && pwd)"
SETUP_DIR="$REPO_ROOT/tools/setup"

# shellcheck source=common/curl-fetch.sh
source "$SETUP_DIR/common/curl-fetch.sh"

# ── 1. Xcode Command Line Tools ─────────────────────────────────────
if ! xcode-select -p >/dev/null 2>&1; then
echo "↓ installing Xcode Command Line Tools (non-interactive)..."
Expand All @@ -37,7 +40,14 @@ echo "✓ Xcode CLT at $(xcode-select -p 2>/dev/null || echo 'pending user confi
# ── 2. Homebrew ─────────────────────────────────────────────────────
if ! command -v brew >/dev/null 2>&1; then
echo "↓ installing Homebrew..."
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
# Capture to a named variable first so a curl failure aborts
# the variable assignment under `set -e` — `/bin/bash -c
# "$(failing_curl)"` otherwise silently runs an empty string
# and exits 0. Use the stream variant (no --retry-all-errors)
# because the captured output is then piped into bash; we
# don't want a partial-script retry-replay scenario.
HOMEBREW_INSTALLER="$(curl_fetch_stream https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
/bin/bash -c "$HOMEBREW_INSTALLER"
Comment thread
AceHack marked this conversation as resolved.
Outdated
Comment thread
AceHack marked this conversation as resolved.
# Ensure brew is on PATH for the remainder of this script run.
if [ -x /opt/homebrew/bin/brew ]; then
eval "$(/opt/homebrew/bin/brew shellenv)"
Expand Down
Loading