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.
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
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.
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?
(A reboot might also help ...)
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.
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).
What about opening a wiki on the Platform repo to collect all the documentation related to things that are not officially supported?
@Théo Zimmermann : this might work quite well - with some moderation
Yes (the idea in wikis is that moderation happens a posteriori, but I assume that's what you mean).
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.
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 ...
Another problem with issues is that one can't edit them.
as owner, I can edit any issue in coq-community (but I'd only do it for clarity or factual reasons)
a properly tagged issue is in my experience a lot easier to find on GitHub than some section in a wiki page
I mean one can't rearrange / collect / ... the comments in an issue (afaik).
you can approximate that by repeatedly editing the first comment in the issue
I still think and issue which redirects to a Wiki page would make more sense.
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: Jun 03 2023 at 03:01 UTC