Yosuke Ito (Nov 19 2020 at 02:02): Yosuke Ito (Nov 19 2020 at 02:02):Hello everyone.
I upgraded Coq and CoqIDE from 8.12.0 to 8.12.1 yesterday, but CoqIDE doesn't work well.
If I click "File" tab, CoqIDE shutdowns abruptly. Error message on Terminal is "segmentation fault coqide".
Does anyone have ideas to fix it? (I tried downgrading Coq and CoqIDE, but the situation didn't change.)
I use macOS Big Sur (11.0.1), MacBook Air (13-inch, Mid 2013).
Théo Zimmermann (Nov 19 2020 at 07:54):How did you install Coq and CoqIDE? With opam?
Yosuke Ito (Nov 19 2020 at 07:58):Thank you for your reply.
Yes, I installed with opam, using Terminal.
Théo Zimmermann (Nov 19 2020 at 08:17):And you say you've now downgraded Coq and CoqIDE but still get the segmentation fault failure?
Théo Zimmermann (Nov 19 2020 at 08:18):What do coqtop --version and coqide --version give?
Yosuke Ito (Nov 19 2020 at 08:34):Yes. I've tried downgrading Coq and CoqIDE to 8.11.2, but I still get segmentation fault failure.
(This sounds strange, because I didn't get the failure in the older versions...)
The information of versions are as follows.
coqtop --version
The Coq Proof Assistant, version 8.11.2 (November 2020)
compiled on Nov 19 2020 7:39:38 with OCaml 4.11.1
coqide --version
Invalid character ' ' in identifier "The Coq Proof Assistant, version 8.11.2 (November 2020)".
Théo Zimmermann (Nov 19 2020 at 09:35):So you initially had Coq + CoqIDE 8.12.0 and it worked fine, then you upgraded to 8.12.1 and you started getting segfaults, then you downgraded to 8.11.2 and you kept getting segfaults.
Théo Zimmermann (Nov 19 2020 at 09:37):Could it be that meanwhile you updated some CoqIDE dependencies on your system? E.g. with brew?
Michael Soegtrop (Nov 19 2020 at 09:38):Also macOS Big Sur is pretty new - are you sure that your previous tests where not with a different version of macOS?
Théo Zimmermann (Nov 19 2020 at 09:40):Ah yes! If you upgraded your macOS version before upgrading Coq, that could also explain the seemingly inexplicable behavior that you observe.
Yosuke Ito (Nov 19 2020 at 10:04):I just did opam install coq=8.11.2, then I got the error. So I didn't change the dependencies of CoqIDE.
As you point out, I upgraded mac OS THEN upgraded Coq. Did I have to upgrade Coq first?
(Sorry for not being familiar with computers...)
Paolo Giarrusso (Nov 19 2020 at 10:19):rather than “upgrade coq first”, are you confident coq ever worked after upgrading to big sur?
Paolo Giarrusso (Nov 19 2020 at 10:20):or *coqide rather
Paolo Giarrusso (Nov 19 2020 at 10:20):your message says that coqide fails, but maybe coq would work with other clients.
Théo Zimmermann (Nov 19 2020 at 11:24):Do we have other macOS users already on BigSur that could confirm whether CoqIDE works over there?
Paolo Giarrusso (Nov 19 2020 at 12:28):My Big Sur VM isn’t too fast, but I can try if you’re desperate.
Paolo Giarrusso (Nov 19 2020 at 12:30):Dual booting or downgrading is not easy, so my usual advice is to not upgrade macOS major releases, until all “unusual” apps you use officially support the new one.
Yosuke Ito (Nov 19 2020 at 12:35):I'm sure that CoqIDE 8.12.0 worked correctly after updating macOS to Big Sur. The error happened soon after the upgrade to 8.12.1.
As you mention, maybe I should not have upgraded macOS too early.
If there is no way to fix it, I'll try another interface such as Proof-General...
Paolo Giarrusso (Nov 19 2020 at 15:39):Yeah... If you hate Emacs (it has a learning curve) you might like VsCoq
Paolo Giarrusso (Nov 19 2020 at 15:40):Since it builds on visual studio code which is more intuitive
Paolo Giarrusso (Nov 19 2020 at 15:41):VsCoq itself is less mature... But search for the version by @Fabian Kunze (link on this zulip)
Paolo Giarrusso (Nov 19 2020 at 15:41):Wait, are you sure you uninstalled 8.12.1 properly?
Gaëtan Gilbert (Nov 19 2020 at 15:41):what does opam list say about coq and coqide versions?
Paolo Giarrusso (Nov 19 2020 at 15:42):(Also, if you're sure that 8.12.0 worked, you might want to go back to that version)
Michael Soegtrop (Nov 19 2020 at 16:32):A few more things you can try:
./.config/coq/coqiderc file - maybe you have something strange in there (or better move it / rename it so that coqide doesn't find it and send it to us in case this fixes it)../.config/coq/coqide.keys Michael Soegtrop (Nov 19 2020 at 16:38):P.S.: you might also try my Coq platform install scripts from here: https://github.com/coq/platform/tree/v8.12 (latest) or here https://github.com/coq/platform/tree/v8.12.0+beta1 (most recent official release). I put a lot of effort in putting everything into a sane state. In case this does not work for you, I can help investigating why. This is much easier with these scripts, because one can already exclude a lot of things which are covered by the scripts. But I must admit I didn't test them on Big Sur (will do so soon).
Emilio Jesús Gallego Arias (Nov 20 2020 at 01:26):Are you aware folks of https://github.com/garrigue/lablgtk/issues/120#issuecomment-730381518
Paolo Giarrusso (Nov 20 2020 at 03:15):Okay, it crashes "not always but very often", on all gtk versions. So if 8.12 worked correctly, it might have been an accident.
Paolo Giarrusso (Nov 20 2020 at 03:19):Sb please rename the topic to "coqide crashes on macOS 11 (BigSur)" :-)
Yosuke Ito (Nov 20 2020 at 03:53):Thank you for your help. I renamed "CoqIDE shutdown" to "coqide crashes on macOS 11 (BigSur)".
In reply to "what does opam list say about coq and coqide versions?", the result is:
coq 8.11.2
coqide 8.11.2
But now I'm trying to build Coq from scratch.
Théo Zimmermann (Nov 20 2020 at 08:47):It looks like until this bug is fixed, your only hope is to switch to Proof General or VsCoq
Enrico Tassi (Nov 20 2020 at 09:03):Apparently the internet says that "visual studio code works on BigSur" (but not visual studio for Mac, whatever it is)
Théo Zimmermann (Nov 20 2020 at 09:09):Visual Studio is the monster proprietary IDE that Microsoft has developed for years, long before deciding to give almost the same name to a new open source text editor.
Yosuke Ito (Nov 20 2020 at 11:31):Thank you for your reply.
I reinstalled Coq from scratch, but the error still remains.
For the time being, I'll try another editor.
Last updated: Oct 04 2023 at 20:01 UTC