Stream: Coq Platform devs & users

Topic: Initial Flatpak bundle for Coq and remarks on Flatpak

Donald Sebastian Leung (Jan 18 2021 at 13:38):

Please do not follow the instructions below until you have read the entire message.

I've just created an initial Flatpak bundle with coqc and coq_makefile (no CoqIDE, no external libraries). The method to install is:

1. Set up Flatpak for your distro, even if it is already pre-installed on your system
2. Download the Flatpak bundle: coq-8.13.0-2.flatpak
3. Open the bundle in Software Center and click Install, or run flatpak install coq-8.13.0-2.flatpak in a terminal
4. Run flatpak run org.flatpak.CoqProver in a terminal. This performs initial setup so coqc and coq_makefile can be invoked normally afterwards

However, the Flatpak bundle does this (allowing coqc and coq_makefile to be invoked normally) by prepending $HOME/.local/bin to your PATH variable, then copying all the app binaries and associated library files to subdirectories under $HOME/.local. This means that:

• Extra space is used since there are now two copies of the app (the Flatpak itself, and the installed binaries/library files under $HOME/.local)
• All sandboxing benefits of Flatpak are lost
• If you previously had local binaries with the same name as those in the app, they will be overwritten (serious security risk!)
• Uninstalling the Flatpak does not undo its changes on initialization

In other words, this is an ugly hack with security implications rather than a solution. I have tried other methods I could think of to make coqc and coq_makefile usable as usual and all have failed:

• Creating aliases for coqc --> flatpak run org.flatpak.CoqProver coqc and coq_makefile --> flatpak run org.flatpak.CoqProver coq_makefile: this works when they are invoked directly in the terminal, but the Makefile generated by coq_makefile fails to make use of the coqc alias
• Creating symlinks in $HOME/.local/bin to /app/bin in the Flatpak app: this doesn't work since /app only exists within the Flatpak app and not in the base system, so we are left with dangling links

To summarize, while attempting to package the Coq ecosystem for Flatpak was an interesting and educational exercise, my experience with it indicates that it is unsuitable for bundling an entire ecosystem, though it might shine as an open-source alternative to Snaps for bundling single, standalone applications.

Related: Improved CLI application experience

Donald Sebastian Leung (Jan 18 2021 at 13:54):

As for the repo, I have archived it as I can find no sane way of packaging it as a Flatpak bundle. But if anyone is interested in taking this further and figuring out whether this can be done, feel free to drop me an email and I will happily transfer repo ownership to you.

Guillaume Melquiond (Jan 18 2021 at 13:55):

Instead of completely copying coq_makefile into .local/bin, perhaps the following would be sufficient:

flatpak run org.flatpak.CoqProver coq_makefile COQBIN = "$HOME/.local/bin/" "$@"

Enrico Tassi (Jan 18 2021 at 13:57):

Indeed I do something similar in the snap (but there I point COQBIN inside the snap, which has a bin directory containing coqc.

Guillaume Melquiond (Jan 18 2021 at 13:58):

How do you know the extracted (?) directory of the snap? Is it deterministic?

Enrico Tassi (Jan 18 2021 at 13:58):

I'm sorry to see that flatpak has usability issues. I'm not a big fan of the snapstore being "controlled" by Canonical myself, but I also see how they did an incredible job in making these things simple.

Enrico Tassi (Jan 18 2021 at 14:00):

It is deterministic but not predictable at compilation time. But you can recover the path of coqc from the one of coq_makefile (see https://github.com/coq/platform/blob/v8.13/linux/snap/coq_wrapper )

Guillaume Melquiond (Jan 18 2021 at 14:00):

Makes sense. Possibly the same could work for flatpak.

Last updated: Apr 18 2024 at 17:02 UTC