Merge branch 'feature/michele/docker-image' into 'master'

Docker image for CAISAR

See merge request laiser/caisar!30

.gitignore

 .merlin
 _build/
+docker/Dockerfile

Makefile

@@ -13,6 +13,9 @@ test:
 promote:
 	dune promote --root=.
 
+docker:
+	$(MAKE) -C docker all
+
 clean:
 	dune clean
 
@@ -45,4 +48,4 @@ release:
 	dune-release opam pkg
 	dune-release opam submit
 
-.PHONY: release clean promote test uninstall install all
+.PHONY: release clean promote test docker uninstall install all

README.md

@@ -7,8 +7,10 @@ artificial intelligence based software.
 
 ## Installation
 
-No binaries are provided at the moment. Installation must be done
-by directly compiling the source.
+No binaries are provided at the moment. Installation must be done by either
+compiling the source code or using a [Docker](https://www.docker.com/) image.
+
+### From source code
 
 **Please note:** CAISAR requires the OCaml package manager [opam](https://opam.ocaml.org/),
 v2.1 or higher, which is typically avaible in all major GNU/Linux distributions.
@@ -29,6 +31,28 @@ To run the tests:
 $ make test
 ```
 
+### Docker image
+
+A ready-to-use [Docker](https://www.docker.com/) image of CAISAR is available on
+[Docker Hub](https://hub.docker.com). To retrieve such an image, do the
+following:
+```
+$ docker pull laiser/caisar:pub
+```
+
+Alternatively, a [Docker](https://www.docker.com/) image for CAISAR can be
+created locally by proceeding as follows:
+```
+$ git clone https://git.frama-c.com/pub/caisar
+$ cd caisar
+$ make docker
+```
+
+To run the CAISAR [Docker](https://www.docker.com/) image, do the following:
+```
+$ docker run -it laiser/caisar:pub sh
+```
+
 ## Usage
 
 To start using CAISAR, please run the command:
@@ -38,8 +62,8 @@ $ caisar --help
 
 ### Property verification
 
-CAISAR can be used to verify properties on neural networks and
-support-vector machines (SVM).
+CAISAR can be used to verify properties on neural networks and support-vector
+machines (SVM).
 
 The prototype command is:
 ```

docker/Dockerfile.template

+##########################################################################
+#                                                                        #
+#  This file is part of CAISAR.                                          #
+#                                                                        #
+#  Copyright (C) 2022                                                    #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  You can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+# Dockerfile for easy install and use of CAISAR.
+
+FROM @UBUNTU_OPAM_BASE@
+
+RUN opam repository set-url default https://opam.ocaml.org && \
+opam update -y && \
+opam install depext -y
+
+# "RUN eval $(opam env)" does not work, so we manually set its variables
+@ENV@
+
+RUN sudo apt-get install -yy git && \
+git clone --depth 1 https://git.frama-c.com/pub/caisar.git
+
+RUN cd caisar && \
+opam depext -y @OPAM_DEPS@ && \
+opam install --deps-only --with-test -y .
+
+# "RUN eval $(opam env)" does not work, so we manually set its variables
+@ENV@
+
+RUN cd caisar && make && make install

docker/Makefile

+##########################################################################
+#                                                                        #
+#  This file is part of CAISAR.                                          #
+#                                                                        #
+#  Copyright (C) 2022                                                    #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  You can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+.PHONY: pub push
+
+OCAML_VERSION?=4.13
+
+all: Dockerfile
+	@echo "You may want to consider adding ARGS=--no-cache to force"
+	@echo "Docker to rebuild all layers."
+	docker build . -t laiser/caisar:pub -f $^ --rm $(ARGS)
+
+push: all
+	@echo "You may need to execute 'docker login' beforehand."
+	docker push laiser/caisar:pub
+
+Dockerfile: Makefile Dockerfile.template env.template
+	sed 's|@UBUNTU_OPAM_BASE@|ocaml/opam:ubuntu-ocaml-@OCAMLV@|g' Dockerfile.template | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_DEPS@|conf-protoc conf-gmp conf-autoconf conf-pkg-config|' | \
+sed 's|@OCAMLV@|'$(OCAML_VERSION)'|g' | \
+cat > $@

docker/env.template

+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/@OCAMLV@"\n
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/@OCAMLV@/lib/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml"\n
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/@OCAMLV@/lib/toplevel"\n
+ENV MANPATH "$MANPATH:/home/opam/.opam/@OCAMLV@/man"\n
+ENV PATH "/home/opam/.opam/@OCAMLV@/bin:$PATH"\n
+\n
+## Avoid prompts for time zone\n
+ENV TZ=Europe/Paris\n
+\n
+## Fix issue with libGL on Windows\n
+ENV LIBGL_ALWAYS_INDIRECT=1\n