#!/bin/sh
# Rebuild everything from scratch and fail on any error or `sorry`.
set -e
cd "$(dirname "$0")"
rm -rf .lake
lake build 2>&1 | tee /tmp/antidyn_build.log
if grep -q "sorry" /tmp/antidyn_build.log; then echo "FOUND sorry"; exit 1; fi
if grep -rn "sorry" AntiDynamics/ | grep -v "^AntiDynamics/Core.lean:23"; then echo "FOUND sorry"; exit 1; fi
echo "OK: all files check, no sorry."