# ===== Base Rocq + MathComp =====
FROM mathcomp/mathcomp-dev:rocq-prover-9.0

# ===== Install Coq-LSP + PET =====
RUN opam update && \
    opam install -y logs lwt coq-lsp

# ===== Install Miniconda (clean Python env) =====
USER root
ENV CONDA_DIR=/opt/conda
RUN apt-get update && apt-get install -y wget bzip2 && \
    wget -q https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh -O /tmp/miniconda.sh && \
    bash /tmp/miniconda.sh -b -p $CONDA_DIR && \
    rm /tmp/miniconda.sh && \
    $CONDA_DIR/bin/conda clean -afy
ENV PATH=$CONDA_DIR/bin:$PATH

RUN conda tos accept --override-channels --channel https://repo.anaconda.com/pkgs/main && \
    conda tos accept --override-channels --channel https://repo.anaconda.com/pkgs/r

RUN conda create -y -n petanque python=3.11 fastapi uvicorn requests && \
    conda clean -afy
ENV PATH=$CONDA_DIR/envs/appenv/bin:$PATH

# ===== Install pytanque from GitHub =====
RUN git clone https://github.com/LLM4Rocq/pytanque.git /tmp/pytanque && \
    pip install -e /tmp/pytanque && \
    rm -rf /tmp/pytanque