Michael Soegtrop (Nov 07 2021 at 08:16): Michael Soegtrop (Nov 07 2021 at 08:16):@Julien Puydt : did you consider doing this based on Coq Platform? Since this is now the official user facing distribution of Coq, IMHO a Debian package should include Coq Platform and not just Coq. I also think that without opam a pure Coq package is not terribly useful.
Julien Puydt (Nov 07 2021 at 08:52):Michael Soegtrop said:
Julien Puydt : did you consider doing this based on Coq Platform? Since this is now the official user facing distribution of Coq, IMHO a Debian package should include Coq Platform and not just Coq. I also think that without opam a pure Coq package is not terribly useful.
There are three layers: upstream, distributions and users. Debian and Coq Platform are distributions.
Michael Soegtrop (Nov 08 2021 at 13:01):Julien Puydt : There are three layers: upstream, distributions and users. Debian and Coq Platform are distributions.
I think this is to a good extent a question of definition - IMHO if the coq team decides that Coq Platform is the user facing entity, then distributions might want to follow this. In any case I personally wouldn't find coq package which doesn't somehow integrate with various coq libraries not terribly useful.
Of course one can discuss to create a larger set of debian packages, including a Coq Platform meta package. But then I would use opam to do this in a similar way as Coq Platform creates Mac, Windows and snap packages from opam.
Théo Zimmermann (Nov 08 2021 at 13:24):@Michael Soegtrop Debian packages cannot depend on another package manager like opam. Getting the full platform packaged in Debian would be nice, but probably significant effort for the poor Debian maintainers, at least until the Coq package ecosystem gets a bit more uniform in terms of build systems. NixOS is probably a better target for getting the full platform packaged, given that most packages that it contains are already there.
Michael Soegtrop (Nov 08 2021 at 15:57):@Théo Zimmermann : I meant that opam is used for producing the package - not a dependency at install time. Is this also not allowed? I guess worst case one could auto generate some sort of debian package description file from opam.
Karl Palmskog (Nov 08 2021 at 15:59):as has been discussed above, Debian package policies may necessitate splitting opam packages into several Debian packages, in particular plugin packages that bundle .cmXX files. This information is not easily available via opam.
Karl Palmskog (Nov 08 2021 at 16:00):for plain Coq projects (libraries), though, it should be almost one-to-one in the Platform and Debian, if someone think they are worth packaging in Debian (not a trivial decision still)
Michael Soegtrop (Nov 08 2021 at 16:04):This information is not easily available via opam.
I guess one could derive this by file extension. The Windows and Mac installer generators also do some hacks.
What is the opinion of others on a "Plain Coq" Debian package?
Théo Zimmermann (Nov 08 2021 at 16:14):Michael Soegtrop said:
Théo Zimmermann : I meant that opam is used for producing the package - not a dependency at install time. Is this also not allowed? I guess worst case one could auto generate some sort of debian package description file from opam.
My understanding is indeed that the former is not compatible with Debian way of doing while the latter might be. But I'm far from a Debian expert.
Théo Zimmermann (Nov 08 2021 at 16:17):What is the opinion of others on a "Plain Coq" Debian package?
The platform being still recent and "plain Coq" being packaged in many places, I wouldn't push too hard on replacing "plain Coq" packages by "platform packages". It should be up to the maintainers of the distributions / package managers. I think we can encourage packaging the platform by providing great documentation on how to do this, and we're not there yet.
Meanwhile, given that Coq is already available in Debian, I very much appreciate efforts to keep it up-to-date.
Michael Soegtrop (Nov 08 2021 at 16:20):OK, let's keep this for the future then.
Last updated: Dec 05 2023 at 06:01 UTC