#!/usr/bin/env bash
# One-command, idempotent setup of the Rust -> Charon -> Aeneas -> Lean toolchain under /apps.
# Nothing is written under /home or /tmp (see env.sh: HOME/RUSTUP_HOME/CARGO_HOME/OPAMROOT/ELAN_HOME/TMPDIR
# are all redirected to /apps/development/rlhf/toolchains). CPU: nice -n 15, <= 4 build jobs.
# Usage: bash bugfind/setup_toolchain.sh [--skip-lean-lib] [--skip-smoke]
set -euo pipefail
HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
AENEAS_COMMIT=6c2788d1366f09d69fd55b2b9be71cd17d28a9ab   # see TOOLCHAIN.md; charon pin is read from its charon-pin file
source "$HERE/env.sh"
case "$TC" in /apps/*) ;; *) echo "TC must be under /apps"; exit 1;; esac
NICE="nice -n 15"
log() { echo "[setup $(date +%H:%M:%S)] $*"; }
home_free_before=$(df -m --output=avail /home | tail -1)
SRC=$TC/src; mkdir -p "$SRC" "$TC/bin" "$HOME/.cache"

# 1. rustup (no default toolchain; Charon's rust-toolchain file pulls the pinned nightly) and elan.
if [ ! -x "$CARGO_HOME/bin/rustup" ]; then
  log "rustup"; curl -sSf https://sh.rustup.rs -o "$SRC/rustup-init.sh"
  $NICE sh "$SRC/rustup-init.sh" -y --no-modify-path --profile minimal --default-toolchain none
fi
if [ ! -x "$ELAN_HOME/bin/elan" ]; then
  log "elan"; curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o "$SRC/elan-init.sh"
  $NICE sh "$SRC/elan-init.sh" -y --no-modify-path --default-toolchain none
fi

# 2. gmp (headers are absent on this box; build a private copy instead of touching the system) and opam.
if [ ! -f "$LOCAL_PREFIX/include/gmp.h" ]; then
  log "gmp 6.3.0"; (cd "$SRC" && curl -sSfL -o gmp.tar.xz https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz && tar xf gmp.tar.xz &&
    cd gmp-6.3.0 && $NICE ./configure --prefix="$LOCAL_PREFIX" >/dev/null && $NICE make -j4 >/dev/null && make install >/dev/null)
fi
if [ ! -x "$TC/bin/opam" ]; then
  log "opam 2.6.1"; curl -sSfL -o "$TC/bin/opam" https://github.com/ocaml/opam/releases/download/2.6.1/opam-2.6.1-x86_64-linux; chmod +x "$TC/bin/opam"
fi
[ -d "$OPAMROOT/5.3.0" ] || { log "opam init + switch 5.3.0"; $NICE opam init --bare --disable-sandboxing --no-setup -y; $NICE opam switch create 5.3.0 -y; }
eval "$(opam env --switch=5.3.0 --set-switch)"
mkdir -p "$XDG_CONFIG_HOME/dune"; printf '(lang dune 3.0)\n(jobs 4)\n' > "$XDG_CONFIG_HOME/dune/config"

# 3. Aeneas + the Charon commit it pins.
[ -d "$SRC/aeneas/.git" ] || git clone -q https://github.com/AeneasVerif/aeneas "$SRC/aeneas"
cd "$SRC/aeneas"; git checkout -q "$AENEAS_COMMIT"
CHARON_COMMIT=$(tail -1 charon-pin)
if [ ! -d charon/.git ]; then git clone -q https://github.com/AeneasVerif/charon charon; fi
(cd charon && git fetch -q origin && git checkout -q "$CHARON_COMMIT" && git submodule update --init --recursive)
if [ ! -x charon/bin/charon ]; then
  log "charon (cargo build, nightly pinned by charon/charon/rust-toolchain)"
  (cd charon && $NICE make build-dev-charon-rust CARGO_BUILD_JOBS=4 2>&1 | tail -3) || true
  (cd charon && mkdir -p bin && cp -f charon/target/debug/charon charon/target/debug/charon-driver bin/)
fi
if [ ! -x bin/aeneas ]; then
  log "opam deps for aeneas"; (cd src && $NICE opam install . --deps-only -y -j4)
  log "aeneas (dune)"; rm -f src/_build/.lock tests/test_runner/_build/.lock
  MAKEFLAGS= $NICE make build-dev
fi

# 4. Lean toolchain pinned by Aeneas + its Lean library (mathlib cache comes from cache.mathlib.org).
LEAN_TC=$(cat backends/lean/lean-toolchain)
$NICE elan toolchain install "$LEAN_TC"
if [ "${1:-}" != "--skip-lean-lib" ] && [ "${2:-}" != "--skip-lean-lib" ]; then
  log "Aeneas Lean library (lake exe cache get; lake build)"
  (cd backends/lean && $NICE taskset -c 0-3 bash -c 'lake exe cache get && lake build Aeneas AeneasMeta')
fi

# 5. Smoke test.
if [ "${1:-}" != "--skip-smoke" ] && [ "${2:-}" != "--skip-smoke" ]; then bash "$HERE/smoke/run_smoke.sh"; fi

home_free_after=$(df -m --output=avail /home | tail -1)
log "done. /home free MB before=$home_free_before after=$home_free_after (must not drop because of this script)"