Stream: Coq Platform devs & users

Topic: Alternative way to install Coq Platform


view this post on Zulip Huỳnh Trần Khanh (Jan 24 2023 at 04:22):

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?

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

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

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

https://people.debian.org/~jpuydt/coq_platform.html

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

view this post on Zulip Notification Bot (Jan 24 2023 at 08:59):

This topic was moved here from #Coq users > Alternative way to install Coq Platform by Karl Palmskog.

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

PS: where do you see I have two accounts? I'll indeed want to delete one...

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

view this post on Zulip Julien Puydt (Jan 24 2023 at 09:56):

@Karl Palmskog I see only one of me, online when I type @Jul

@Michael Soegtrop I updated my page, but I'm not sure that's what you wanted

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

view this post on Zulip Julien Puydt (Jan 24 2023 at 10:03):

@Michael Soegtrop I'm using this link, what is the new one?

@Karl Palmskog Ah, indeed: it's @Julien Puydt I should delete.

view this post on Zulip Julien Puydt (Jan 24 2023 at 10:12):

I think I found the new one ; I updated my page

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

view this post on Zulip Michael Soegtrop (Jan 24 2023 at 10:30):

I created (https://github.com/coq/platform/issues/323) to mention this in the Coq Platform Linux readme.

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

view this post on Zulip Julien Puydt (Jan 24 2023 at 10:48):

Bad link, it was the previous version ; here is the latest.

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Jan 24 2023 at 14:05):

I guess AAC Tactics could mechanize that intention by adding to its build

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?

view this post on Zulip Paolo Giarrusso (Jan 24 2023 at 14:06):

To be clear, if you detect any cynicism, that's not directed at you Julien

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

view this post on Zulip Théo Zimmermann (Jan 24 2023 at 14:26):

It's very likely that if it builds it works. But this is completely untested.

view this post on Zulip Théo Zimmermann (Jan 24 2023 at 14:27):

(I mean, beyond whatever automatic tests there are.)

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

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

view this post on Zulip Karl Palmskog (Jan 24 2023 at 14:54):

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


Last updated: Jun 23 2024 at 01:02 UTC