#!/bin/sh
# Reproducibility driver for the main results.  Run from the repository root:
#   sh experiments/reproducibility/run_all.sh quick   # exact checks and independent checkers, about 1 minute
#   sh experiments/reproducibility/run_all.sh full    # quick + all Arb recomputations, about 75 minutes on 16 cores
#   sh experiments/reproducibility/run_all.sh lean    # pinned Lean build of the cubic theorem (needs elan/lake)
# PY defaults to the project interpreter .venv/bin/python.  Logs go to experiments/reproducibility/outputs/.
# The full mode rewrites the stored certificate files in place; `git status` afterwards shows whether they changed.
# Since 2026-10-10 the star-bound certificate is certify_star_bounds_arb_owen.py (arc bound enclosed in Arb), with data in
# experiments/arb-certificates/star-bound-arb-owen/; the 2026-10-07 script and data (star-bound-arb/) are not published here.
# Since 2026-10-14 the full mode also runs the problem S-switched (see Theorem 8.2 (`thm:switched4`) of the paper, about 4 minutes), and
# the exact recheck includes it.
set -u
MODE=${1:-quick}
PY=${PY:-.venv/bin/python}
OUT=experiments/reproducibility/outputs
mkdir -p "$OUT"
status=0
run() {  # run <name> <command...>
  name=$1; shift
  printf '%-28s ' "$name"
  start=$(date +%s)
  if "$@" > "$OUT/$name.txt" 2>&1; then r=ok; else r=FAILED; status=1; fi
  echo "$r ($(( $(date +%s) - start ))s)"
}
run main-arithmetic   "$PY" experiments/reproducibility/check_main_arithmetic.py
run star-cells-exact  "$PY" experiments/arb-certificates/check_star_bound_cells.py star-bound-arb-owen
run bootstrap-checks  "$PY" experiments/degree-bootstrap-check.py 4000
if [ "$MODE" = full ]; then
  run F-arb-local       "$PY" experiments/reproducibility/F/arb_F.py
  run F-arb-global      "$PY" experiments/reproducibility/F/arb_F_global.py 0.1401582524
  run F4-arb            "$PY" experiments/arb-certificates/certify_F4.py
  run star-bounds-arb-owen "$PY" experiments/arb-certificates/certify_star_bounds_arb_owen.py
  run star-bounds-arb-owen-switched "$PY" experiments/arb-certificates/certify_star_bounds_arb_owen.py S-switched
  run star-cells-exact2 "$PY" experiments/arb-certificates/check_star_bound_cells.py star-bound-arb-owen
fi
if [ "$MODE" = lean ]; then
  # approved digests: C3Spec.lean 5ffd69d0...dcaff644 (approved 2026-11-03; comment-only update of the
  # version 5c12b94e...aab8125 approved on 2026-10-01), CubicPathwidth.lean dce37d2a...f9ccdf
  run lean-build sh -c 'cd lean && shasum -a 256 CubicPathwidth/C3Spec.lean CubicPathwidth.lean && lake build && lake env lean CubicPathwidth/C3/All.lean'
fi
exit $status