| # 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 | |