debug server

Dockerfile

@@ -7,13 +7,23 @@ RUN ls -l /home/user/ && \
     git clone https://github.com/project-numina/kimina-lean-server.git
 
 WORKDIR /home/user/app/kimina-lean-server
-RUN git checkout 069576742afb4ca6c086898787a0e91abf91893c --detach
+RUN git checkout e3bb327e9f1a737decf24ecd861662f6a5f3f801 --detach
 ENV LEAN_SERVER_REPL_PATH=/home/user/repl/.lake/build/bin/repl
 ENV LEAN_SERVER_PROJECT_DIR=/home/user/mathlib4
 ENV PYTHONPATH=$PYTHONPATH:/home/user/app/kimina-lean-server
-RUN python3 -m pip install --user -r requirements.txt && \
-    python3 -m pip install --user -e .
+RUN python3 -m pip install --upgrade pip --extra-index-url https://pypi.org/simple && \
+    python3 -m pip install -r requirements.txt --extra-index-url https://pypi.org/simple && \
+    python3 -m pip install . --extra-index-url https://pypi.org/simple && \
+    prisma generate
 RUN cp /home/user/app/.env /home/user/app/kimina-lean-server/
+ENV PATH="/home/user/.elan/bin:${PATH}"
+RUN which lake && \
+    which elan && \
+    lake --version && \
+    elan --version && \
+    lean --version && \
+    elan toolchain list && \
+    echo ${PATH}
 
 WORKDIR /home/user/app
 EXPOSE 7860

config.py

@@ -0,0 +1,50 @@
+import os
+from typing import Optional
+
+
+class Settings:
+    """Global settings for the application"""
+
+    # Server configuration
+    HOST: str = os.getenv("LEANSERVER_HOST", "0.0.0.0")
+    PORT: int = int(os.getenv("LEANSERVER_PORT", 8888))
+    API_KEY: Optional[str] = os.getenv("LEANSERVER_API_KEY")
+
+    # Logging configuration
+    LOG_DIR: str = os.getenv("LEANSERVER_LOG_DIR", "./logs")
+    LOG_LEVEL: str = os.getenv("LEANSERVER_LOG_LEVEL", "INFO")
+
+    # Workspace configuration
+    WORKSPACE: Optional[str] = os.getenv("LEANSERVER_WORKSPACE")
+
+    # Concurrency configuration
+    MAX_REPLS: int = int(os.getenv("LEANSERVER_MAX_REPLS", 1))
+    MAX_CONCURRENT_REQUESTS: int = int(os.getenv("LEANSERVER_MAX_CONCURRENT_REQUESTS", 1))
+
+    # Health check thresholds
+    HEALTHCHECK_CPU_USAGE_THRESHOLD: Optional[float] = (
+        float(os.getenv("LEANSERVER_HEALTHCHECK_CPU_USAGE_THRESHOLD"))
+        if os.getenv("LEANSERVER_HEALTHCHECK_CPU_USAGE_THRESHOLD")
+        else None
+    )
+    HEALTHCHECK_MEMORY_USAGE_THRESHOLD: Optional[float] = (
+        float(os.getenv("LEANSERVER_HEALTHCHECK_MEMORY_USAGE_THRESHOLD"))
+        if os.getenv("LEANSERVER_HEALTHCHECK_MEMORY_USAGE_THRESHOLD")
+        else None
+    )
+
+    # REPL memory management
+    REPL_MEMORY_LIMIT_GB: Optional[float] = (
+        float(os.getenv("LEANSERVER_REPL_MEMORY_LIMIT_GB"))
+        if os.getenv("LEANSERVER_REPL_MEMORY_LIMIT_GB")
+        else None
+    )
+    REPL_MEMORY_CHECK_INTERVAL: Optional[int] = (
+        int(os.getenv("LEANSERVER_REPL_MEMORY_CHECK_INTERVAL"))
+        if os.getenv("LEANSERVER_REPL_MEMORY_CHECK_INTERVAL")
+        else None
+    )
+
+
+settings = Settings()
+

healthcheck.py

@@ -0,0 +1,84 @@
+from fastapi import APIRouter, Depends, HTTPException
+from typing import Optional
+import psutil
+import subprocess
+from loguru import logger
+
+from .config import settings
+from .server import require_access_dep
+
+router = APIRouter()
+
+
+def get_lean_version() -> str:
+    """Get Lean 4 version"""
+    try:
+        result = subprocess.run(
+            ["lean", "--version"],
+            capture_output=True,
+            text=True,
+            timeout=10
+        )
+        if result.returncode == 0:
+            return result.stdout.strip()
+        else:
+            return "unknown"
+    except Exception as e:
+        logger.warning(f"Failed to get lean version: {e}")
+        return "unknown"
+
+
+def get_cpu_usage() -> Optional[float]:
+    """Get current CPU usage percentage"""
+    try:
+        return psutil.cpu_percent(interval=1)
+    except Exception as e:
+        logger.warning(f"Failed to get CPU usage: {e}")
+        return None
+
+
+def get_memory_usage() -> Optional[float]:
+    """Get current memory usage percentage"""
+    try:
+        memory = psutil.virtual_memory()
+        return memory.percent
+    except Exception as e:
+        logger.warning(f"Failed to get memory usage: {e}")
+        return None
+
+
+def check_health_thresholds(cpu_usage: Optional[float], memory_usage: Optional[float]) -> bool:
+    """Check if CPU and memory usage are within thresholds"""
+    if settings.HEALTHCHECK_CPU_USAGE_THRESHOLD is not None and cpu_usage is not None:
+        if cpu_usage > settings.HEALTHCHECK_CPU_USAGE_THRESHOLD:
+            return False
+
+    if settings.HEALTHCHECK_MEMORY_USAGE_THRESHOLD is not None and memory_usage is not None:
+        if memory_usage > settings.HEALTHCHECK_MEMORY_USAGE_THRESHOLD:
+            return False
+
+    return True
+
+
+@router.get("/health")
+async def health_check(access: None = Depends(require_access_dep)):
+    """Health check endpoint"""
+    lean_version = get_lean_version()
+    cpu_usage = get_cpu_usage()
+    memory_usage = get_memory_usage()
+
+    is_healthy = check_health_thresholds(cpu_usage, memory_usage)
+
+    if not is_healthy:
+        raise HTTPException(
+            status_code=503,
+            detail=f"Service unhealthy: lean_version={lean_version}, cpu_usage={cpu_usage}, memory_usage={memory_usage}"
+        )
+
+    return {
+        "status": "healthy",
+        "lean_version": lean_version,
+        "cpu_usage": cpu_usage,
+        "memory_usage": memory_usage
+    }
+

start.sh

@@ -1,7 +1,6 @@
 #!/bin/bash
 set -e
 
-export PATH="~/.elan/bin:${PATH}"
 which lake
 which elan
 lake --version
@@ -41,6 +40,8 @@ echo "curl -v http://localhost:8888/docs"
 curl -v http://localhost:8888/docs
 echo "curl -v http://localhost:8888/verify"
 curl -v http://localhost:8888/verify
+curl -v http://localhost:8888/openapi.json
+curl -v http://localhost:8888/redoc
 
 cd /home/user/app
 ls -l