File size: 1,120 Bytes
c475135 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 | #!/usr/bin/env bash
# Verify Lean 4 proof stub files exist and have 'sorry' placeholders.
# Exit 0 on success; non-zero on any missing file or missing sorry.
set -euo pipefail
cd "$(dirname "$0")/.."
echo "=== Lean 4 Proof Verification ==="
PROOF_FILES=(
"proofs/PostSemClaw/BirkhoffClosure.lean"
"proofs/PostSemClaw/SpectralBound.lean"
"proofs/PostSemClaw/OjaConvergence.lean"
"proofs/PostSemClaw/Discretization.lean"
"proofs/PostSemClaw/SDRCollision.lean"
"proofs/PostSemClaw/HestiaAnnealing.lean"
)
echo "Checking proof stub files exist..."
for f in "${PROOF_FILES[@]}"; do
[ -f "$f" ] || { echo "FAIL: $f not found"; exit 1; }
grep -q "sorry" "$f" || { echo "FAIL: $f has no 'sorry' (expected Phase 1 stub)"; exit 1; }
echo " OK: $f"
done
echo "All ${#PROOF_FILES[@]} proof stubs verified."
if command -v lake &>/dev/null; then
echo ""
echo "Running: lake build"
lake build || echo "WARNING: lake build failed — 'sorry' stubs are expected to warn, not error"
else
echo ""
echo "SKIP: Lean 4 (lake) not installed. Install via elan to verify proofs."
fi
|