#!/usr/bin/env bash
# Typecheck the Monty Hall proof and print its axiom footprint.
# Exit 0 with no error lines = QED (Lean's kernel accepted the proof).
#
# Finds `lean` on PATH or in the usual elan and Nix profile locations.
# Install Lean using https://lean-lang.org/install/. No import graph or lake
# project is needed: the proof is a single self-contained file.
set -euo pipefail
export PATH="$HOME/.elan/bin:$HOME/.nix-profile/bin:$PATH"
HERE="$(cd "$(dirname "$0")" && pwd)"
command -v lean >/dev/null 2>&1 || {
  echo "Lean not found. Install Lean using https://lean-lang.org/install/, then re-run." >&2
  exit 127
}
echo "Lean: $(lean --version)"
echo "Typechecking MontyHall.lean …"
lean "$HERE/MontyHall.lean"
echo "✓ typechecks (no errors above)."
echo
echo "Axiom footprint (these theorems depend on NO axioms — cleaner than [propext, Quot.sound]):"
lean "$HERE/MontyHall.lean" 2>&1 | grep -i "axiom\|does not depend" || true