#!/bin/sh
# Type-check the Lean development (Lean 4, core only, no Mathlib) and reject `sorry`/`axiom`.
set -e
cd "$(dirname "$0")"
LEAN=${LEAN:-lean}
command -v "$LEAN" >/dev/null 2>&1 || LEAN="$HOME/.elan/bin/lean"
if grep -nE '\bsorry\b|^axiom ' IconologicalGeometry.lean | grep -v '^\s*--'; then
  echo "FAIL: sorry/axiom found"; exit 1
fi
OUT=$("$LEAN" IconologicalGeometry.lean 2>&1) || { echo "$OUT"; echo "FAIL"; exit 1; }
echo "$OUT"
if echo "$OUT" | grep -q "error\|sorry"; then echo "FAIL"; exit 1; fi
# axiom audit of the main theorems
TMP=$(mktemp -t iconaxioms.XXXXXX)
cp IconologicalGeometry.lean "$TMP.lean"
cat >> "$TMP.lean" <<'EOT'
open IconologicalGeometry in
#print axioms projStatic_iff
open IconologicalGeometry in
#print axioms projDyn_iff
open IconologicalGeometry in
#print axioms exists_sim_of_valid
open IconologicalGeometry in
#print axioms example_dynamic
EOT
"$LEAN" "$TMP.lean" 2>&1 | grep -A2 "axioms" || true
rm -f "$TMP" "$TMP.lean"
echo "OK: IconologicalGeometry.lean checks, no sorry."
# Additions.lean (suggested additional results): imports IconologicalGeometry
if grep -nE '\bsorry\b|^axiom ' Additions.lean | grep -v '^\s*--'; then
  echo "FAIL: sorry/axiom in Additions.lean"; exit 1
fi
ADD=$(mktemp -d -t iconadd.XXXXXX)
"$LEAN" -o "$ADD/IconologicalGeometry.olean" IconologicalGeometry.lean >/dev/null 2>&1 || { echo "FAIL: olean"; exit 1; }
OUT=$(LEAN_PATH="$ADD" "$LEAN" Additions.lean 2>&1) || { echo "$OUT"; echo "FAIL"; exit 1; }
echo "$OUT"
if echo "$OUT" | grep -q "error\|sorry"; then echo "FAIL"; exit 1; fi
rm -rf "$ADD"
echo "OK: Additions.lean checks, no sorry."