Stream: Coq Platform devs & users

Topic: Initial Flatpak bundle for Coq and remarks on Flatpak


view this post on Zulip 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:

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:

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

The Flatpak can now be used as follows: Install the Flatpak Initialize the Flatpak by running flatpak run org.flatpak.CoqProver Now usual Coq commands such as coqc and coq_makefile work as intende...
From what I've read of the documentation there are 3 things that seem to be missing for command line tools: Custom commands for running the app, having to do flatpak --run org.bla.bla every tim...

view this post on Zulip 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.

Manifest and associated files for building a working Coq environment for Flatpak (WIP) - DonaldKellett/flatpak-CoqProver

view this post on Zulip 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/" "$@"

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Jan 18 2021 at 13:58):

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

view this post on Zulip 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.

view this post on Zulip 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 )

Multi platform setup for Coq, Coq libraries and tools - coq/platform

view this post on Zulip Guillaume Melquiond (Jan 18 2021 at 14:00):

Makes sense. Possibly the same could work for flatpak.


Last updated: Jan 30 2023 at 10:03 UTC