Cannot install via snap · Coq Platform devs & users

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.

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

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.

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?

Michael Soegtrop (Apr 25 2022 at 15:43):

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.

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).

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?

Michael Soegtrop (Apr 25 2022 at 18:04):

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).

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.

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 ...

Michael Soegtrop (Apr 26 2022 at 06:40):

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)

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

Michael Soegtrop (Apr 26 2022 at 07:28):

Karl Palmskog (Apr 26 2022 at 07:29):

Michael Soegtrop (Apr 26 2022 at 07:30):

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.