diff --git a/docker/Dockerfile.template b/docker/Dockerfile.template index 858873c3d4de25a1fe825b86e1de50c753ace3e0..96aa0b3400185096b4fd0b6b3b164482341e6812 100644 --- a/docker/Dockerfile.template +++ b/docker/Dockerfile.template @@ -31,20 +31,21 @@ opam-2.1 update -y # "RUN eval $(opam-2.1 env)" does not work, so we manually set its variables @ENV@ -RUN sudo apt-get install -yy git +# System dependencies -# External provers - -## Pyrat -### install python package dependencies -RUN sudo apt-get update && \ +RUN sudo apt update && \ sudo apt install apt-utils && \ - sudo apt-get install -y wget cmake protobuf-compiler libopenblas-dev zip python3-pip zip && \ - sudo apt-get clean && \ + sudo apt install -yy git wget gfortran cmake protobuf-compiler libprotobuf-dev libboost-all-dev libopenblas-dev zip python3-pip zip && \ + sudo apt clean && \ sudo rm -rf /var/lib/apt/lists/ ENV PATH "/home/opam/.local/bin:$PATH" + +# External provers + +## Pyrat + RUN git clone https://git.frama-c.com/pub/pyrat.git && \ git -C pyrat checkout 43c7389e5ce203b445ad3c7bfdcbf6bf408f3214 @@ -57,45 +58,53 @@ RUN chmod u+x /home/opam/pyrat/pyrat RUN pyrat -h -# # Download Marabou and install system dependencies -# RUN sudo apt-get update && sudo apt-get install -yy cmake gfortran wget libprotobuf-dev libopenblas-dev && \ -# git clone https://github.com/NeuralNetworkVerification/Marabou.git && \ -# git -C Marabou checkout e7ea6028320a13cf0a5f92c14cc7b89b99fb6aeb - -# # Build Marabou -# RUN cd Marabou && \ -# mkdir build && \ -# cd build && \ -# cmake .. \ -# -DBUILD_PYTHON=OFF \ -# -DRUN_UNIT_TEST=OFF \ -# -DRUN_MEMORY_TEST=OFF \ -# -DCMAKE_CXX_FLAGS="-Wno-error -Wno-sign-compare" && \ -# cmake --build . - -# # Extend PATH with path to the Marabou binary -# ENV PATH "/home/opam/Marabou/build:$PATH" - -# Download, build and install SAVer -RUN git clone --depth 1 https://github.com/svm-abstract-verifier/saver.git && \ -cd saver/src && \ +## Marabou + +RUN git clone https://github.com/NeuralNetworkVerification/Marabou.git && \ +git -C Marabou checkout 14dd0f1446e3c980d408839150d342327ab73527 + +RUN cd Marabou && \ +mkdir build && \ +cd build && \ +cmake .. \ +-DBUILD_PYTHON=OFF \ +-DRUN_UNIT_TEST=OFF \ +-DRUN_MEMORY_TEST=OFF \ +-DCMAKE_CXX_FLAGS="-Wno-error -Wno-sign-compare" && \ +cmake --build . + +ENV PATH "/home/opam/Marabou/build:$PATH" + + +## SAVer + +RUN git clone https://github.com/svm-abstract-verifier/saver.git && \ +git -C saver checkout de7a6d674680a1879db6a230bca8ef277a00d940 + +RUN cd saver/src && \ make && \ make install -# Extend PATH with path to the SAVer binary ENV PATH "/home/opam/saver/bin:$PATH" + ## NNenum -RUN git clone https://github.com/stanleybak/nnenum.git -RUN cd nnenum && pip3 install -r requirements.txt +RUN git clone https://github.com/stanleybak/nnenum.git && \ +git -C nnenum checkout cf7c0e72c13543011a7ac3fbe0f5c59c3aafa77e + +RUN cd nnenum && \ +pip3 install -r requirements.txt ENV PYTHONPATH "$PYTHONPATH:/home/opam/nnenum/src" + +# CAISAR + RUN git clone https://git.frama-c.com/pub/caisar.git && \ git -C caisar checkout @CAISAR_COMMIT@ -RUN cd caisar && sudo apt-get update && opam-2.1 install --deps-only --with-test -y . +RUN cd caisar && sudo apt update && opam-2.1 install --deps-only --with-test -y . RUN cd caisar && make && make install