FROM mathcomp/mathcomp:1.12.0-coq-8.13

ENV PROBSA=/ProBsa/
WORKDIR ${PROBSA}

RUN set -x \ 
    && sudo chown -R coq:coq ${PROBSA} \ 
    && eval $(opam env)

RUN set -x \
    && echo "[ProBsa] Updating opam packages..." \
    && opam update -y -u \
    && opam clean -a -c -s --logs \
    && opam list

RUN set -x \
    && echo "[ProBsa] Compiling Prosa..." \
    && git clone https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git prosa \
    && cd prosa \
    && git checkout 0b7a65db \
    && opam install -v -y -j "${NJOBS}" . \
    && echo "[ProBsa] Prosa has been installed & compiled." \ 
    && opam show coq-prosa

RUN set -x \ 
    && echo "[ProBsa] Compiling Coq-Proba..." \
    && git clone https://github.com/jtassarotti/coq-proba proba \ 
    && cd proba \    
    && git checkout 11d69b22 \
    && opam install -v -y -j "${NJOBS}" . \
    && echo "[ProBsa] Coq-Proba has been installed & compiled." \ 
    && opam show coq-proba