Donald Sebastian Leung (Jan 16 2021 at 11:48): Donald Sebastian Leung (Jan 16 2021 at 11:48):So I've been poking through this stream recently and the topic "Linux users, a snap package is available" caught my eye as Snaps allow the latest version(s) of Coq and its associated software to be consistently delivered across multiple Linux distributions which is amazing compared to installing an outdated Coq version from a more traditional package manager or building + installing the latest version through opam. However, I would imagine that a small percentage of Linux users may not be too fond of Snaps for various non-technical reasons.
To this end, are there any plans by the Coq development team on packaging Coq (and its associated libraries + IDE) for Flatpak? Its overall idea is similar to Snaps but does not rely on a central server controlled by a single company for hosting downloadable apps.
Enrico Tassi (Jan 16 2021 at 12:19):I'm the one who packaged the snap, and I'm very happy if you package the flatpak!
I did look at flatpak a little but given limited energy I had to make a choice, there are no plans to work on a flatpak.
If you are interested in doing the packaging work, then it should be done in the context of the coq platform, which now takes care of binary packages for Coq (maybe @Théo Zimmermann can move this thread there). I can provide some help and pointers, but I don't have time to do it myself.
Donald Sebastian Leung (Jan 16 2021 at 12:41):That does sound like an interesting project, I'll see if I have the time to figure it out. Thanks for creating the Snap anyway!
Notification Bot (Jan 16 2021 at 13:25):This topic was moved here from #Coq users > Plans on Flatpak for Coq (+ associated libraries)? by Théo Zimmermann
Donald Sebastian Leung (Jan 16 2021 at 13:46):Just to clarify, is it absolutely required for coqide and coq_makefile to be referenced using their usual names? It seems that Flatpak only supports running apps using flatpak run org.developer.AppName and it's unclear from the documentation whether a single app can export more than one command at all.
Enrico Tassi (Jan 16 2021 at 15:08):Necessary no, but if it is not the case then one has to write some doc. In particular the Coq manual talks about coq_makefile, and suggests to call it from your own scripts.
Paolo Giarrusso (Jan 16 2021 at 15:19):Guess the user would have to separately install (in their home) a wrapper for coq_makefile calling the extra commands?
Paolo Giarrusso (Jan 16 2021 at 15:19):At least if they want to be able to build existing software without changing it
Enrico Tassi (Jan 16 2021 at 16:20):You could also provide a little proxy, eg a shell script that calls it's first argument. This way flapak run fr.inria.coq coq_makefile args would call coq_makefile args while flapak run fr.inria.coq coqide would start coqide. Actually, I do something close to this in the snap as well, see the coq_wrapper_* scripts.
Paolo Giarrusso (Jan 16 2021 at 20:28):You might want both — the proxy against the “one command” restriction, and the “outside proxies” to implement Coq’s standard CLI
Donald Sebastian Leung (Jan 17 2021 at 09:01):I've just successfully built OCaml 4.05.0 with Flatpak and think I've figured out how to allow running multiple commands with one app. Basically, I now have a shell script which just runs a command consisting of all the arguments passed to it, so I can do flatpak run org.flatpak.CoqProver ocaml to run ocaml and flatpak run org.flatpak.CoqProver ocaml --version to run ocaml --version, for example.
Of course, there's still quite a bit to do before the base CoqIDE installation becomes available, and more for external Coq libraries to be integrated into the package, but this initial result has convinced me that creating a Flatpak bundle for Coq is doable. Stay tuned :wink:
Donald Sebastian Leung (Jan 17 2021 at 11:03):Initial work on building the Flatpak is now available at https://github.com/DonaldKellett/flatpak-CoqProver , feel free to try building it yourself (detailed instructions are attached in the README) and ping me if you'd like to collaborate on this effort. I'm currently attempting to troubleshoot issues related to building lablgtk-sourceview3, but once that's figured out, it shouldn't be too long (hopefully) until a build of CoqIDE (without any external Coq libraries) is available.
Enrico Tassi (Jan 17 2021 at 21:09):I had a look at the flatpak script, and this is not exactly what I had in mind when I said it should be based on the platform.
The coq platform provides shell scripts which in turn use opam to install ocaml, coq, and all the selected libraries.
The snap package just runs the script and then purges unneeded files.
If you can follow this path, then the flatpak maintenance is cheap, but if you select and build each single item as you do now, then things becomes more involved. The main problem with the platform scripts is that they need network access (https://github.com/coq/platform/issues/63). So we run the builder in CI rather than in the snapstore's build infrastructure (which builds without networks access).
Donald Sebastian Leung (Jan 18 2021 at 02:35):Noted with thanks, I will look into this shortly :+1:
Donald Sebastian Leung (Jan 18 2021 at 04:34):I've figured out how to enable network access in the build process, but after installing opam and its core dependency bwrap, running EDIT: Just checked the opam FAQ, will try again with opam init gives an error from bwrap stating that unprivileged user namespaces are not permitted. The error message does mention to set the kernel parameter kernel.unprivileged_userns_clone to 1 on Debian-based distributions, but such a parameter (or similarly named ones) does not seem to be available on Fedora 33 which uses the 5.10 kernel. Either way, my bit of Google research suggests that enabling them (if at all possible on kernel 5.10) could open up my system to various exploits. Have you encountered such an issue when building the Snap, and if so, how did you solve it?--disable-sandboxing
Enrico Tassi (Jan 18 2021 at 07:13):I disable sandboxing too.
Last updated: Jun 03 2023 at 04:30 UTC