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