#!/bin/sh
# Compile every file in dependency order; stops at the first failure.
# Usage: sh check.sh     (needs `lean` on PATH or in ~/.elan/bin; no Mathlib needed)
LEAN=${LEAN:-$(command -v lean || echo "$HOME/.elan/bin/lean")}
cd "$(dirname "$0")" || exit 1
mkdir -p build
export LEAN_PATH=build
for f in LCAbstract PropSyntax PropTheory KleeneCore KleeneTheory Sanity Quantifier InfinitelyMany Additions; do
  [ -f "$f.lean" ] || continue
  echo "== $f"
  "$LEAN" -o "build/$f.olean" "$f.lean" || { echo "FAILED: $f"; exit 1; }
done
echo "ALL OK"