FROM debian:bookworm-slim

# Install system dependencies
RUN apt-get update && apt-get install -y \
    ca-certificates \
    curl \
    git \
    zstd \
    python3 \
    python3-pip \
    && rm -rf /var/lib/apt/lists/*

#Create python symlink (Debian has python3 but not python)
RUN ln -s /usr/bin/python3 /usr/bin/python

# Install elan (Lean version manager)
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
ENV PATH="/root/.elan/bin:${PATH}"

WORKDIR /app

# Setup Lean project with Mathlib (heavy layer, cache this)
RUN lake new eval_project math
WORKDIR /app/eval_project
RUN lake exe cache get && lake build

# Build REPL tool
WORKDIR /app
RUN git clone --depth 1 https://github.com/leanprover-community/repl.git
WORKDIR /app/repl
RUN lake build

# (Optional): Verify REPL binary exists
RUN test -f /app/repl/.lake/build/bin/repl || (echo "REPL binary not found!" && exit 1)

# Python setup
WORKDIR /app
COPY requirements.txt .
RUN pip install --break-system-packages --no-cache-dir -r requirements.txt

# Copy application code (last to leverage cache)
COPY . .

EXPOSE 7860

CMD ["python3", "app.py"]