I have installed Coq prover using snap.
Now, when I try to start CoqIDE, I get
Unable to init server: Could not connect: Connection refused Fatal error: exception Gtk.Error("GtkMain.init: initialization failed\nml_gtk_init: initialization failed")
Other X programs do work. What is lurking here?
I have not seen this before, but this looks like a bug worth reporting. Can you open an issue on the coq/platform repo about your problem with all your configuration details?
@Théo Zimmermann : please remember that most bugs in CoqIDE are actually bugs in CoqIDE and not in Coq Platform and should be reported there. I would ask users to first install coqide via opam (or via the platform scripts with level "i/IDE") and see if it works then. It is a bug in Coq Platform only if it works via opam but not via a Coq Platform installer.
I can confirm that
coqide works fine for me on Ubuntu via the Coq Platform snap. This might be a problem specific to the Coq platform snap on Debian. So not obvious which repo to start in (best to start somewhere and then move it to the right place)
Yes, sure. I just think that issues should in general first be reported to the package and then to the distribution, not the other way around. For CoqIDE this seems to have swapped since a while. There were some Platform specific issues with the Mac installer, but otherwise I am not aware of any, so I think this is hardly justified.
When there is a bug in the software itself, sure, you should skip the distribution and report upstream directly, but when you cannot launch a basic command after following the normal installation procedure, I think the expected and traditional path is to report to the distribution first, and the distribution maintainers decide whether to forward.
But I hear you.
@Théo Zimmermann : I think it is a bit different if you have distributions like debian where the OS and packages are in one. Coq Platform is a multi platform distribution of Coq and I don't do that much OS platform specific stuff (some opam depext fixes or the like). My assumption is that the Coq team delivers a working opam package on supported platforms (the builds are checked in opam CI) and I take it from there.
OK, this point of view is reasonable. However note that this assumption is incorrect:
My assumption is that the Coq team delivers a working opam package on supported platforms
The Coq team declines responsibility of the opam packages. Some volunteer Coq users together with the opam-repository and opam-coq-archive maintainers are taking care of ensuring that the opam packages work. In particular, any bug in the opam packages should be directed first at the opam-repository and opam-coq-archive bug trackers (rather than the coq bug tracker).
Compiling Coq full through
resulted in a working CoqIDE. So it is indeed a problem with Coq Platform. I wrote this at the Github issue as well:
Thanks indeed for all of your help.
@Théo Zimmermann : OK, but what if CoqIDE does not work on a supported platform (not sure if these are officially named ...). Opam is more or less a computer readable form of the build instructions, so I would say it is highly likely that if CoqIDE doesn't work via opam, it doesn't work via manual build either - more on the contrary since Opam does a good job in managing the not so well documented system dependencies.
Sure, it all depends on whether it's a bug in the build / dependency specification or in Coq itself.
Well in this specific case it turned out that your gut feeling was correct ...
Sorry for this whole story: without much reading I followed some web page to install CoqIDE on Debian. That's why I used snap.
It turned out that Debian 11.4 does have CoqIDE in the distribution, so I could install it via apt-get install. It works.
No worries. Coq Platform is the officially recommended installation method, so it should work on Debian, and it is useful to know if it is not the case. If you are still available to help debug this, we might ask you to provide some more details on your exact setting.
Indeed, if things don't work we need to know about it. There are various methods with various advantages and disadvantages. E.g. if you install via apt, you have a smaller selection of pre compiled coq packages compare to snap.
@Théo Zimmermann yes I am willing to discuss this, I'm interested in debugging.
Also, the vanilla Debian CoqIDE is running Coq 8.12.0 (November 2020), while the opam runs Coq 8.15.2
Interestingly, upon searching on the error message CoqIDE displayed, I got this issue on Github:
@Gergely Buday : you mean the snap coqide does work now? If so I would guess that one of the other install activities you did (either opam or apt) installed required system dependencies.
Last updated: Jun 10 2023 at 23:01 UTC