Gergely Buday (Sep 06 2022 at 11:06): Gergely Buday (Sep 06 2022 at 11:06):Hi there,
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?
Théo Zimmermann (Sep 06 2022 at 11:26):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?
Gergely Buday (Sep 06 2022 at 12:00):I did:
https://github.com/coq/platform/issues/280
Michael Soegtrop (Sep 06 2022 at 12:21):@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.
Karl Palmskog (Sep 06 2022 at 12:26):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)
Michael Soegtrop (Sep 06 2022 at 12:53):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.
Théo Zimmermann (Sep 06 2022 at 15:08):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.
Théo Zimmermann (Sep 06 2022 at 15:09):But I hear you.
Michael Soegtrop (Sep 06 2022 at 16:28):@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.
Théo Zimmermann (Sep 07 2022 at 11:30):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).
Gergely Buday (Sep 07 2022 at 11:43):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:
https://github.com/coq/platform/issues/280
Thanks indeed for all of your help.
Michael Soegtrop (Sep 07 2022 at 11:56):@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.
Théo Zimmermann (Sep 07 2022 at 11:57):Sure, it all depends on whether it's a bug in the build / dependency specification or in Coq itself.
Michael Soegtrop (Sep 07 2022 at 12:12):Well in this specific case it turned out that your gut feeling was correct ...
Gergely Buday (Sep 07 2022 at 12:51):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.
Théo Zimmermann (Sep 07 2022 at 12:55):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.
Michael Soegtrop (Sep 07 2022 at 12:59):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.
Gergely Buday (Sep 07 2022 at 12:59):@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
Gergely Buday (Sep 07 2022 at 13:04):Interestingly, upon searching on the error message CoqIDE displayed, I got this issue on Github:
https://github.com/coq/coq/issues/7055
Michael Soegtrop (Sep 07 2022 at 14:18):@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: Apr 16 2024 at 07:02 UTC