Dockerfile

FROM zhangjfbuaa/lean-server:v4.15.0

WORKDIR /home/user/app
COPY --chown=user app.py start.sh .env ./
RUN ls -l /home/user/ && \
    cd /home/user/app && \
    git clone https://github.com/project-numina/kimina-lean-server.git

WORKDIR /home/user/app/kimina-lean-server
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 --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

USER root
RUN apt-get update && apt-get install -y \
    procps \
    net-tools \
    && rm -rf /var/lib/apt/lists/*
USER user

COPY --chown=user kimina_client ./kimina_client
COPY --chown=user minif2f-solved-by-longcat-flash-thinking ./minif2f-solved-by-longcat-flash-thinking
CMD ["bash", "start.sh"]