diff --git a/_posts/2023-02-01-singularity-for-easy-docker-images.md b/_posts/2023-02-01-singularity-for-easy-docker-images.md new file mode 100644 index 0000000000000000000000000000000000000000..094789769b9bf752bad93b220fe5bbbf6b239006 --- /dev/null +++ b/_posts/2023-02-01-singularity-for-easy-docker-images.md @@ -0,0 +1,100 @@ +--- +layout: post +author: André Maroneze (kindly tested by D. Bühler, V. Prevosto et al) +date: 2023-02-01 19:00 +0100 +categories: docker gui +title: "Using Singularity/Apptainer for easy-to-use Docker images" +--- + +The Frama-C Docker images are useful for continuous integration, but for +interactive use, they are not very practical: by default, Docker does not +provide access to the local filesystem, and running the Frama-C GUI requires +using derived tools such as [`x11docker`](https://github.com/mviereck/x11docker). +In this post, we briefly show an alternative, with +[Singularity](https://en.wikipedia.org/wiki/Singularity_(software)), which has +the advantages of including, by default, host filesystem integration and +graphical application support without additional configuration. + +## Singularity for Frama-C, in a nutshell + +Singularity (now split in two projects, Apptainer and SingularityCE), in this +post, is seen as a Linux-based application to run a Frama-C-based Docker image. +Its advantage is that the user does not have to install and manage Frama-C and +its dependencies (OCaml, opam, etc), like when using the Docker image; but also, +when running `frama-c` or `frama-c-gui`, the user has direct access to the +local filesystem and to the graphical interface, without having to use tools +such as `x11docker`, or mounting volumes. This should, hopefully, make Frama-C +*very* easy to test on simple examples, at the cost of increased disk space +usage. + +## Instructions for running Frama-C via SingularityCE on a Ubuntu + +The following has been tested on a Ubuntu 22.04 machine. Hopefully, similar +steps should work for other versions of Ubuntu as well as for Debian-based +systems. For other Linux distributions, such as Fedora, there are existing +packages that allow skipping the first few steps. + +For Ubuntu 22.04: + +- Go to https://github.com/sylabs/singularity/releases and download the + DEB package for your Ubuntu release (e.g., `jammy` for Ubuntu 22.04); +- Run `sudo apt install ./<downloaded_file>.deb`; this will install + the locally-downloaded package. *Note:* in our test machine, we had to add + `--fix-broken` to the above command, to make sure some required dependencies + were also installed. +- Singularity can build its instances from several sources, such as local + Docker images, or images from the Docker Hub. For the latter, we can run + the following command: + + singularity instance start docker://framac/frama-c-gui:26.0 fc26 + + This will (1) download the `framac/frama-c-gui:26.0` image from the Docker + Hub, then create an instance and name it `fc26`. You can change `fc26` to + the name you prefer; a short one should make it easier to type + (as seen below). You can also use Frama-C's `dev` images (replacing `26.0` + with `dev`) to obtain an image based on the current development version + of Frama-C (public Git). +- Now, whenever you want to run a command from the instance, such as + `frama-c file.c <options>`, you just need to prefix it with + `singularity exec instance://fc26`. For instance, inside the Frama-C source + distribution there is a `tests/idct` directory. We can `cd` to it and run: + + singularity exec instance://fc26 frama-c-gui *.c -eva + + This should get the Frama-C GUI running, run Eva and then display the + AST and analysis result. + +**Note**: a similar setup has been tested on Arch Linux (with Sway), and on +Fedora (with both X and Wayland). The Fedora + Wayland setup required changing +some settings related to X (`xhost +local:`). All this to say, your mileage +may vary, but hopefully it should be easier than using the Docker image +directly. + +## Limits of the Singularity filesystem integration + +Singularity tries to provide a seamless integration between its instance and +the host system (including e.g. access to the filesystem), but some unexpected +behaviors may happen; Frama-C has not been exhaustively tested inside this +environment! + +For instance, GTK applications may try to access data in temporary folders +which are made read-only by Singularity, resulting in warnings and error +messages. Still, in our (limited) tests, most GUI features seemed to work +fine despite the warnings. + +Also, note that the mixture between the "host" filesystem and the container's +can cause unintuitive behaviors. For instance, if you want to run WP +(and thus need to run `why3 config detect` beforehand), the command +`singularity exec instance://fc26 why3 config detect` will overwrite +the `~/.why3.conf` file in *the host's* home directory, but the file will +mention paths which only exist inside the container. This can lead to +problematic situations, especially if you later install Frama-C in the host +machine as well. + +## Conclusion + +Singularity offers an easier approach to "running a container integrated with +its host" than Docker: having access to the graphical interface and the host +filesystem by default is extremely useful when trying to run Frama-C on Linux, +without having to install and configure OCaml-related tools, or manage opam +switches.