FROM docker.io/runpod/autoresearch:1.0.7-cuda1281-ubuntu2204

# Install Lean 4 toolchain
RUN curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh && \
    sh /tmp/elan-init.sh -y --default-toolchain none && \
    rm /tmp/elan-init.sh

ENV ELAN_HOME=/root/.elan
ENV PATH=$ELAN_HOME/bin:$PATH

# Install SilverSight toolchain
COPY SilverSight/lean-toolchain /tmp/lean-toolchain
RUN elan toolchain install $(cat /tmp/lean-toolchain) && \
    elan default $(cat /tmp/lean-toolchain) && \
    rm /tmp/lean-toolchain

# Copy autoresearch scripts (prove.py with 5-check pipeline, verify_lean.py)
COPY autoresearch/prove.py /opt/autoresearch/prove.py
COPY autoresearch/verify_lean.py /opt/autoresearch/verify_lean.py
COPY autoresearch/frozen_template/ /opt/autoresearch/frozen_template/

# Install Python deps
RUN pip install requests 2>/dev/null || true

WORKDIR /root/SilverSight
ENTRYPOINT ["/bin/bash", "-c"]