#!/bin/bash
# Build script for the starG Lean 4 formalization.
# Handles toolchain synchronization with Mathlib automatically.
set -e

echo "=== Step 1/4: Fetching Mathlib ==="
lake update

echo ""
echo "=== Step 2/4: Syncing lean-toolchain to match Mathlib ==="
# Mathlib dictates the required Lean version. Copy its toolchain file
# so our project uses the same version.
if [ -f .lake/packages/mathlib/lean-toolchain ]; then
  cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain
  echo "Toolchain set to: $(cat lean-toolchain)"
elif [ -f lake-packages/mathlib/lean-toolchain ]; then
  cp lake-packages/mathlib/lean-toolchain ./lean-toolchain
  echo "Toolchain set to: $(cat lean-toolchain)"
else
  echo "Warning: could not find Mathlib toolchain file. Using existing."
fi

echo ""
echo "=== Step 3/4: Downloading prebuilt Mathlib oleans ==="
lake exe cache get

echo ""
echo "=== Step 4/4: Building starG ==="
lake build

echo ""
echo "=== Build successful ==="