From 257500fdea64445a12f90ebd0c1735fc67b94906 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 23 Jan 2023 19:24:27 +0100
Subject: [PATCH] [docker] Rework template to make it work with latest solvers.

Enable Marabou once again, and fix the commit for nnenum and SAVer.
---
 docker/Dockerfile.template | 77 +++++++++++++++++++++-----------------
 1 file changed, 43 insertions(+), 34 deletions(-)

diff --git a/docker/Dockerfile.template b/docker/Dockerfile.template
index 858873c..96aa0b3 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
 
-- 
GitLab