#!/usr/bin/env bash
# Typecheck the McNugget-number proof and print its axiom footprint.
# Exit 0 = QED: Lean's kernel accepted the proof and every axiom footprint is
# exactly [propext, Quot.sound].
#
# Finds `lean` wherever this environment put it: on PATH already, under an elan
# install ($HOME/.elan/bin — the house default when github.com egress is open), or
# under a Nix profile ($HOME/.nix-profile/bin — the github-free route, pulled from
# cache.nixos.org; use research/mcnugget/lean/install-lean-nix.sh). No import graph,
# no lake project — 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 it, then re-run. Two known-good routes:" >&2
  echo "  • elan (if github egress is open):  bash research/sorting-networks/lean/install-lean.sh" >&2
  echo "  • nix  (if github is blocked)     :  bash research/mcnugget/lean/install-lean-nix.sh" >&2
  exit 127
}
echo "Lean: $(lean --version)"
echo "Typechecking McNugget.lean …"
lean "$HERE/McNugget.lean"
echo "✓ typechecks (no errors above)."
echo
echo "Axiom footprint (must be exactly [propext, Quot.sound], NO sorryAx/Classical.choice/native_decide):"
FOOT="$(lean "$HERE/McNugget.lean" 2>&1 | grep -i "depends on axioms" || true)"
echo "$FOOT"
# Asserted, not just printed (claims pass 2026-10-13: this used to print the
# footprint and exit 0 even when a proof had been replaced by sorry).
[ -n "$FOOT" ] || { echo "✗ no axiom footprint reported" >&2; exit 1; }
if echo "$FOOT" | grep -v "depends on axioms: \[propext, Quot.sound\]$" | grep -q .; then
  echo "✗ a footprint is not exactly [propext, Quot.sound]" >&2; exit 1
fi
echo "✓ every footprint is exactly [propext, Quot.sound]."