[blog] post about Singularity

_posts/2023-02-01-singularity-for-easy-docker-images.md

+---
+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.