#!/usr/bin/env bash
set -euo pipefail

if [[ $# -ne 3 ]]; then
  echo "usage: $0 LEAN_PROJECT_DIRECTORY IMPORT_MODULE THEOREM_NAME" >&2
  exit 2
fi
project=$(realpath "$1")
module=$2
theorem=$3
root=$(cd "$(dirname "$0")/.." && pwd)

"$root/check_answer/verify-lean.sh" "$project"

tmp=$(mktemp --suffix=.lean)
trap 'rm -f "$tmp"' EXIT
printf 'import %s\n#print axioms %s\n' "$module" "$theorem" >"$tmp"
export PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH"
out=$(cd "$project" && lake env lean "$tmp" 2>&1)
printf '%s\n' "$out"

AXIOM_OUTPUT="$out" THEOREM_NAME="$theorem" python3 - <<'PY'
import os,re,sys
out=os.environ['AXIOM_OUTPUT']
thm=os.environ['THEOREM_NAME']
# Lean may wrap the bracketed list over several lines.
m=re.search(r"'"+re.escape(thm)+r"' depends on axioms:\s*\[(.*?)\]",out,re.S)
if not m:
    print('FAIL: could not parse #print axioms output',file=sys.stderr)
    sys.exit(1)
found={x.strip() for x in m.group(1).split(',') if x.strip()}
allowed={'propext','Classical.choice','Quot.sound'}
extra=found-allowed
if extra:
    print('FAIL: theorem uses forbidden or unreviewed axioms: '+', '.join(sorted(extra)),file=sys.stderr)
    sys.exit(1)
print('PASS: theorem axiom audit; only '+', '.join(sorted(found)))
PY
