# Dockerfile for LeanTutor Backend
FROM python:3.12-slim-bookworm

# Set timezone to avoid interactive prompt
ENV DEBIAN_FRONTEND=noninteractive
ENV TZ=America/Los_Angeles

# Install system dependencies
RUN apt-get update && apt-get install -y \
    curl \
    git \
    build-essential \
    && rm -rf /var/lib/apt/lists/*

# Install elan (Lean version manager)
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
ENV PATH="/root/.elan/bin:${PATH}"

# Set working directory
WORKDIR /app

# Lean project build
COPY lean-toolchain lakefile.toml lake-manifest.json ./
COPY LeanTutor127/ ./LeanTutor127/
COPY LeanTutor127.lean Main.lean ./

# Build Lean project (downloads and compiles Mathlib) 
RUN lake exe cache get && lake build

# Python dependencies
COPY merge/backend/requirements.txt ./requirements.txt
RUN python3 -m pip install --no-cache-dir uv && \
    uv pip install --system -r requirements.txt

# Pre-build the lean-interact REPL to avoid cold-start compilation
RUN python3 -c "from lean_interact import LeanREPLConfig, LeanServer, LocalProject; \
    config = LeanREPLConfig(project=LocalProject(directory='/app'), verbose=True); \
    server = LeanServer(config); \
    print('REPL pre-built successfully')"

# Copy application code
COPY compiler/ ./compiler/
COPY autoformalizer/ ./autoformalizer/
COPY informalizer/ ./informalizer/
COPY preprocessor_with_retry/ ./preprocessor_with_retry/
COPY pipeline_IO/ ./pipeline_IO/
COPY utils/ ./utils/
COPY run.py run_IO.py ocr.py ./

# Copy backend code and database
COPY merge/backend/ ./merge/backend/
COPY merge/database/ ./database/
COPY pyproject.toml uv.lock ./

# Expose port (Cloud Run uses 8080)
EXPOSE 8080

# Set environment variables
ENV FLASK_APP=merge/backend/app.py
ENV PYTHONUNBUFFERED=1
ENV PORT=8080
ENV ENV=production

# Run the backend
CMD ["python3", "merge/backend/app.py"]