Stream: Coq Platform devs & users

Topic: Cannot install via snap


view this post on Zulip Andrew Appel (Apr 25 2022 at 15:24):

I am running Ubuntu 20.04.3 under the WSL2 virtual machine. Until recently, with this installation, I could install the Coq Platform without any problem (although, I must admit, I don't remember the details of how this worked, I just followed the instructions at the Coq Platform). But now I can't install it, I have a snap problem:

ubuntu$ sudo snap install coq-prover
[sudo] password for appel:
error: cannot communicate with server: Post http://localhost/v2/snaps/coq-prover: dial unix /run/snapd.socket: connect: no such file or directory
ubuntu$ sudo systemctl restart snapd snapd.socket
System has not been booted with systemd as init system (PID 1). Can't operate.
Failed to connect to bus: Host is down

So, aside from my own immediate question, "I'm not a Linux wizard, what do I do now?" there is the more general problem that installation of the Coq Platform seems more fragile than ever.

view this post on Zulip Karl Palmskog (Apr 25 2022 at 15:28):

I tried installing via snap on Ubuntu 22.04, and that worked at least. So it may be some temporary issue with Snap servers, is my best guess. Not sure how snap stability could be improved

view this post on Zulip Karl Palmskog (Apr 25 2022 at 15:30):

so best approximation at advice: try sudo snap install coq-prover in a few hours again and see if it's the same error. or restart WSL? Never seen that error on regular Ubuntu.

view this post on Zulip Michael Soegtrop (Apr 25 2022 at 15:40):

I would also say that this is a temporary hickup or an issue with your local snap deamon, not with Coq Platform.
Can you install any other snap packages?

view this post on Zulip Michael Soegtrop (Apr 25 2022 at 15:43):

(A reboot might also help ...)

view this post on Zulip Andrew Appel (Apr 25 2022 at 17:00):

I have been reminded that my previous coq-platform Ubuntu-over-WSL2 installs have all been via opam, and (very likely) I have never had a working snap in this Unbuntu.

view this post on Zulip Michael Soegtrop (Apr 25 2022 at 17:06):

At some point we should have WSL specific instructions - it is not officially supported (no way to test in CI) but at least we can collect experience. So it would be interesting to know if snap works for WSL for someone (I have difficulties to test it because I use VirtualBox and this doesn't go well with WSL2).

view this post on Zulip Théo Zimmermann (Apr 25 2022 at 17:28):

What about opening a wiki on the Platform repo to collect all the documentation related to things that are not officially supported?

view this post on Zulip Michael Soegtrop (Apr 25 2022 at 18:04):

@Théo Zimmermann : this might work quite well - with some moderation

view this post on Zulip Théo Zimmermann (Apr 25 2022 at 18:05):

Yes (the idea in wikis is that moderation happens a posteriori, but I assume that's what you mean).

view this post on Zulip Karl Palmskog (Apr 26 2022 at 06:13):

I'm a bit averse to GitHub wikis, since they need significant effort to "take off". Couldn't it be better to have a GitHub issue about "Platform-on-WSL", even if it's not supported? Issues are arguably much more visible.

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 06:39):

Issues is what is happening for Mac M1. The downside is that the topics in the issues get fixed some day - even it is not supported. One could have an issue redirecting to the Wiki ...

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 06:40):

Another problem with issues is that one can't edit them.

view this post on Zulip Karl Palmskog (Apr 26 2022 at 06:49):

as owner, I can edit any issue in coq-community (but I'd only do it for clarity or factual reasons)

view this post on Zulip Karl Palmskog (Apr 26 2022 at 06:53):

a properly tagged issue is in my experience a lot easier to find on GitHub than some section in a wiki page

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 07:28):

I mean one can't rearrange / collect / ... the comments in an issue (afaik).

view this post on Zulip Karl Palmskog (Apr 26 2022 at 07:29):

you can approximate that by repeatedly editing the first comment in the issue

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 07:30):

I still think and issue which redirects to a Wiki page would make more sense.

view this post on Zulip Théo Zimmermann (Apr 26 2022 at 07:44):

My suggestion would have been that the official Platform documentation redirects to the wiki for help on use cases that are not officially supported.


Last updated: Jan 30 2023 at 11:03 UTC