#!/bin/bash
# Rebuild the Lean formalization and fail if it does not compile or contains `sorry`.
set -e
cd "$(dirname "$0")/../theory/lean/wp28proofs"
export PATH="$HOME/.elan/bin:$PATH"
cp ../src/WP28Algebra.lean Wp28proofs/WP28Algebra.lean
out=$(lake build 2>&1)
echo "$out" | grep -q "Build completed successfully" || { echo "$out" | tail -30; exit 1; }
echo "$out" | grep -qi "sorry" && { echo "sorry found"; exit 1; }
echo "Lean: $(grep -c '^theorem' Wp28proofs/WP28Algebra.lean) theorems checked, no sorry"