Enrico Tassi (Jul 29 2020 at 10:03): Enrico Tassi (Jul 29 2020 at 10:03):Just a question: is the platform (on Linux) source based? because I guess it is expected to be a binary distribution for Windows. If it is binary, then saying that it has to be built on some Ubuntu LTS is probably just fine, and one can easily make a snap out of it, or test with any CI out there.
Michael Soegtrop (Jul 29 2020 at 10:12):For the beta1 all platforms will be source (opam) based. A binary installer is planned for Windows and macOS for the release, but not for Linux. For Linux I am not sure I will eventually support it. It depends on the achievable usability which needs to be tested. If the disadvantages of a binary installation for Linux are larger than the advantages, there might be no binary Linux release other than a docker image. I must admit I don't see through this fully right now - I see this as #2 priority.
Karl Palmskog (Jul 29 2020 at 12:23):I don't think it's a good idea to support any binary packages on Linux, since there is no format distros agree on
Karl Palmskog (Jul 29 2020 at 12:24):I would be fine with "supplementary" one-shot binary deliveries like a Docker image and a snap, though, but I don't think these need to be "core" platform products
Théo Zimmermann (Jul 29 2020 at 12:30):We should primarily aim at having the Coq platform being packaged by most common distributions anyway.
Enrico Tassi (Jul 29 2020 at 12:39):I think hoping that debian and fedora and nix package what we decide is the platform in a time frame that makes sense to Coq is hopeless. Being able to install the platform on any distro via opam (+ docker and snap if we manage) seems way simpler to me.
Théo Zimmermann (Jul 29 2020 at 12:40):This can be two complementary things.
Théo Zimmermann (Jul 29 2020 at 12:40):Of course being able to install the platform via opam is fundamental.
Karl Palmskog (Jul 29 2020 at 12:40):Docker and snap are also likely the most useful to platform consumers like artifact eval committees
Enrico Tassi (Jul 29 2020 at 12:41):You said "primarily", maybe you did not mean that
Théo Zimmermann (Jul 29 2020 at 12:41):I meant with respect to the binaries.
Théo Zimmermann (Jul 29 2020 at 12:49):To make my point more precise: newcomers to Coq on Linux will continue to install Coq using their system package managers, so taking steps to ensure that major distributions package the platform (and not just Coq and CoqIDE) will significantly impact the newcomer experience. Fortunately, with Ralf Treinen being once more active in OCaml and Coq Debian package maintenance, this significantly helps our cause.
Enrico Tassi (Jul 29 2020 at 12:50):Then I try to clarify my "hopeless".
Running opam install in a docker image (or snap) is simple and under our control.
Unfortunately this procedure is not something Debian of Fedora devs can use to produce their binary packages, way more work is needed.
Eg in order to package, say, compcert in Debian a team has to check the license (which is non free IIRC, so no way it gets in, but say hypothetically this could take weeks) then it has to be properly packaged (along with its dependencies, again weeks) and finally released (up to 2 years). If this is what you mean by "being packaged by common distros" then I believe it will never work for us. Even more speedy distros like Ubuntu release every 6 months.
Théo Zimmermann (Jul 29 2020 at 12:50):Once newcomers are not so new anymore and they are encouraged to update their Coq version, they can learn about using opam.
Théo Zimmermann (Jul 29 2020 at 12:52):Again I insist on the fact that we don't have control of what newcomers do to install Coq. We must accept that most of them will not have an up-to-date Coq (which is OK). But it is great if we can still improve their experience.
Théo Zimmermann (Jul 29 2020 at 12:52):The job of the platform is also to make it easier to package a set of Coq libraries and plugins.
Théo Zimmermann (Jul 29 2020 at 12:52):The question of the licensing of CompCert is relevant, there will probably be two tiers in the platform, or even possibly only the open source parts of CompCert will be part of the platform.
Théo Zimmermann (Jul 29 2020 at 12:53):Providing very precise and good documentation can also significantly speed up the packaging process.
Théo Zimmermann (Jul 29 2020 at 12:55):But of course, providing a Docker image will be both easy and useful, so we should absolutely do it. (And probably a Snap package as well, but this requires some more digging.)
Enrico Tassi (Jul 29 2020 at 13:20):To be honest, If I type "skype" in my Ubuntu software thingy, I do get a snap not a deb. The reason of existence of snap (or similar cross distribution deployment tech) is that the distro way does not work well for end user software. For once, with a Coq-upstream hat on, I don't think it is "just fine" if you use a 2 years old version of Coq: it is 4 releases old at the current pace and it is unmaintained (no fix backported, not even soundness ones).
I do believe having proper deb/rpm packages is a plus, but I would not count on it, not even for beginners. IMHO we should point newcomers to jscoq and provide an updated (binary) bundle in their "software store". Learning OPAM or nix is not an option for a beginner, believe me (or just ask on math-comp for intern frustration stories and the like).
Anyway, I guess I've drifted this thread a bit off. The selection of Coq packages and their version is the main thing. If we disagree on the best way to also provide binaries to final users, well I guess we can live with it ;-)
Théo Zimmermann (Jul 29 2020 at 13:52):In fact, I don't think we disagree that much. It's just our "let's be realistic" strategies which are a bit different. But anyway, that's really more of a topic for the future.
Karl Palmskog (Jul 29 2020 at 13:55):for what it's worth I agree largely with Enrico: Linux packaging by distro devs is hopeless for Coq, and should not be recommended to any potential Coq user
Michael Soegtrop (Jul 29 2020 at 14:42):Enrico Tassi said:
I think hoping that debian and fedora and nix package what we decide is the platform in a time frame that makes sense to Coq is hopeless. Being able to install the platform on any distro via opam (+ docker and snap if we manage) seems way simpler to me.
Without trying this, this is also my thinking. On the other hand settung up a packaging mechanism for each distro is a one time task - the platform version dependent stuff is all opam based and should not depend on this. So supporting Linux binary packages might be a one time effort one can tackle one by one.
Last updated: Jun 03 2023 at 04:30 UTC