Alternative way to install Coq Platform · Coq Platform devs & users

Honestly I'm not willing to pointlessly spend hours configuring packages. The Coq Platform is a really attractive way to quickly install all the packages I'd need. But... I'm not willing to spend CPU cycles compiling packages either. And the Snap distribution, I don't like Snap for a multitude of reasons. Sandboxing not well thought out, snaps are always mysteriously slower and especially, it always takes centuries to download a package! APT downloads are fast but Snap downloads are always slow. Do you have an alternative way to install the Coq Platform without having to compile the world on my machine?

Karl Palmskog (Jan 24 2023 at 07:18):

I think it's unlikely there will be any other binary installers than the existing ones for the foreseeable future. But the Platform scripts don't force you to install the whole Platform, you can install "base level" (Coq and Dune) or "IDE level" (base level and CoqIDE). Even the "full level" leaves out some packages that take a long time to install, like CompCert and VST.

Michael Soegtrop (Jan 24 2023 at 08:16):

@Huỳnh Trần Khanh : there are also Debian packages for most packages in Coq Platform and we try to keep the versions in sync as much as possible.

Michael Soegtrop (Jan 24 2023 at 08:18):

Here is an overview which compares what is in Coq Platform and in Debian. Maybe we should mention this in the Coq Platform readme.

Michael Soegtrop (Jan 24 2023 at 08:19):

Other binary installers are planned but IMHO a prerequisite would be that .VO files are platform independent, at least for all 64 bit platforms. I don't want to keep platform specific variants of VO files.

Notification Bot (Jan 24 2023 at 08:59):

Julien Puydt (Jan 24 2023 at 09:49):

We're in a freeze so I don't think I'll be able to put 8.17 as soon as I would like, but Coq 8.16.1 is in Debian since it was published.

Michael Soegtrop (Jan 24 2023 at 09:52):

@Julien Puydt : ah yes, sorry - the list is outdated on the Coq Platform side - not the Debian side. Can you please update the Coq Platform side of it?

Julien Puydt (Jan 24 2023 at 09:56):

Michael Soegtrop (Jan 24 2023 at 09:59):

@Julien Puydt : Coq Platform is 8.16.1 - your page lists 8.15.2. There was a release recently (sorry, I should have pinged you).

Julien Puydt (Jan 24 2023 at 10:03):

Julien Puydt (Jan 24 2023 at 10:12):

Michael Soegtrop (Jan 24 2023 at 10:27):

@Julien Puydt : thanks for your efforts to provide Coq / Coq Platform as Debian packages! The package lists are usually available quite a bit before the final release. Do you want to get involved early in the package list creation? I don't expect many updates for the 2023.03 release, though.

Michael Soegtrop (Jan 24 2023 at 10:30):

Julien Puydt (Jan 24 2023 at 10:39):

Well, as I said Debian is in a freeze now, so I won't be able to upload to the main archive anytime soon. [I'll still update my packages in their repositories and locally though!]

Julien Puydt (Jan 24 2023 at 10:48):

Michael Soegtrop (Jan 24 2023 at 11:13):

@Julien Puydt : what I mean is that when I inform you as early as possible that e.g. packages are added, we could fill the timeline better.

Julien Puydt (Jan 24 2023 at 11:27):

Ah, yes. For example coqword and coq-itauto -- I could probably have packaged them if I had known sooner.

Théo Zimmermann (Jan 24 2023 at 12:35):

What does it mean for aac-tactics to be at version 8.17.0 when Coq is only at version 8.16.1? AFAIK, AAC Tactics is never compatible with more than one version of Coq at once.

Karl Palmskog (Jan 24 2023 at 12:37):

hmm, AAC Tactics 8.17.0 is only packaged in extra-dev for opam, with requirements on 8.17 only. Did it get packaged in Debian?

Karl Palmskog (Jan 24 2023 at 12:38):

it occasionally happens that AAC Tactics is compatible across Coq major versions, but this is not at all supported by the maintainer (me), and I'd prefer if packagers didn't do cross-compatible versions, e.g., both compatible with Coq 8.16 and 8.17

Julien Puydt (Jan 24 2023 at 13:03):

Well, it built and passed tests, so I uploaded it... there are other packages where a 8.17-compatible version was released but wasn't compatible, so I didn't upload.

Paolo Giarrusso (Jan 24 2023 at 14:05):

coqc --version | grep -q '8.16' || { echo "Unsupported Coq version"; exit 1; }

I wonder how much documentation would be needed to discourage (other) maintainers effectively from patching this out?

Paolo Giarrusso (Jan 24 2023 at 14:06):

Julien Puydt (Jan 24 2023 at 14:17):

Well, indeed now I see the opam says coq >= 8.17, but as I said, I just tried to compile and load and it seems to just work.

Théo Zimmermann (Jan 24 2023 at 14:26):

Théo Zimmermann (Jan 24 2023 at 14:27):

Michael Soegtrop (Jan 24 2023 at 14:47):

In any case I would recommend to use for all packages with a Coq version in the version the version matching Coq. These should be updated together.

Karl Palmskog (Jan 24 2023 at 14:50):

if packaging becomes incongruent with maintainer intention, I guess we have to detect and act on various ENV variables and other commands to prevent this [unsupported builds]

Karl Palmskog (Jan 24 2023 at 14:54):

as far as I'm concerned, the opam package in released expresses what is actually supported

Stream: Coq Platform devs & users

Topic: Alternative way to install Coq Platform

Huỳnh Trần Khanh (Jan 24 2023 at 04:22):