diff --git a/.gitignore b/.gitignore index 7bcace9eb73163dee960bb1adaf02e0394a38cb6..da97bd6308e3fe8b1295acf2609a1a919d932524 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .merlin _build/ +docker/Dockerfile diff --git a/Makefile b/Makefile index a75ea8c4945dd57950cf3101b19255eb81c05053..546233a83fce35b0f7596ad452b8b79f5cc36c0b 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index 87f1508fa68a9180529b6ab352c2c067e496b510..8607f13312cf6b451c80548e2b4ef3dcc41a5a4e 100644 --- a/README.md +++ b/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: ``` diff --git a/docker/Dockerfile.template b/docker/Dockerfile.template new file mode 100644 index 0000000000000000000000000000000000000000..f07fe2dbe0083d8bc3f0b45fa800ca5092df0d92 --- /dev/null +++ b/docker/Dockerfile.template @@ -0,0 +1,44 @@ +########################################################################## +# # +# 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 diff --git a/docker/Makefile b/docker/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..ea386713b37da5f638764328f64ee1a0bc2a5495 --- /dev/null +++ b/docker/Makefile @@ -0,0 +1,41 @@ +########################################################################## +# # +# 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 > $@ diff --git a/docker/env.template b/docker/env.template new file mode 100644 index 0000000000000000000000000000000000000000..14b2666ef03ba5ae6f2ce6f8d718eb9e7b6145b6 --- /dev/null +++ b/docker/env.template @@ -0,0 +1,11 @@ +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