#!/bin/bash
# Launch kimina-lean-server pinned to OUR Lean 4.9.0-rc1 + Mathlib d1d1e4b7 (scrubbed env).
set -e
K=/apps/development/rlhf/toolchains/src/kimina/kimina-lean-server
L=/apps/development/rlhf/lean
exec env -i HOME=/apps/development/rlhf/toolchains/home TMPDIR=/apps/development/rlhf/lean/tmp \
  ELAN_HOME=$L/elan XDG_CACHE_HOME=$L/xdg-cache PATH=$L/elan/bin:/usr/bin:/bin LANG=C.UTF-8 MALLOC_ARENA_MAX=2 \
  PYTHONPATH=$K/client:$K \
  LEAN_SERVER_HOST=127.0.0.1 LEAN_SERVER_PORT=${PORT:-18000} LEAN_SERVER_ENVIRONMENT=prod \
  LEAN_SERVER_LEAN_VERSION=v4.9.0-rc1 \
  LEAN_SERVER_REPL_PATH=/apps/development/rlhf/toolchains/work/kimina-repl49/.lake/build/bin/repl \
  LEAN_SERVER_PROJECT_DIR=$L/workspace \
  LEAN_SERVER_MAX_REPLS=${MAX_REPLS:-4} LEAN_SERVER_MAX_REPL_MEM=${MEM:-16G} LEAN_SERVER_MAX_WAIT=3600 LEAN_SERVER_LOG_LEVEL=WARNING \
  /apps/development/rlhf/toolchains/kimina-venv/bin/python -m uvicorn server.main:app --host 127.0.0.1 --port ${PORT:-18000} --app-dir $K --log-level warning