File size: 1,011 Bytes
63f41a6 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | #!/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
|