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).
How did you install Coq and CoqIDE? With
Thank you for your reply.
Yes, I installed with
opam, using Terminal.
And you say you've now downgraded Coq and CoqIDE but still get the segmentation fault failure?
coqtop --version and
coqide --version give?
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.
The Coq Proof Assistant, version 8.11.2 (November 2020)
compiled on Nov 19 2020 7:39:38 with OCaml 4.11.1
Invalid character ' ' in identifier "The Coq Proof Assistant, version 8.11.2 (November 2020)".
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.
Could it be that meanwhile you updated some CoqIDE dependencies on your system? E.g. with
Also macOS Big Sur is pretty new - are you sure that your previous tests where not with a different version of macOS?
Ah yes! If you upgraded your macOS version before upgrading Coq, that could also explain the seemingly inexplicable behavior that you observe.
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...)
rather than “upgrade coq first”, are you confident coq ever worked after upgrading to big sur?
or *coqide rather
your message says that coqide fails, but maybe coq would work with other clients.
Do we have other macOS users already on BigSur that could confirm whether CoqIDE works over there?
My Big Sur VM isn’t too fast, but I can try if you’re desperate.
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.
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...
Yeah... If you hate Emacs (it has a learning curve) you might like VsCoq
Since it builds on visual studio code which is more intuitive
VsCoq itself is less mature... But search for the version by @Fabian Kunze (link on this zulip)
Wait, are you sure you uninstalled 8.12.1 properly?
what does opam list say about coq and coqide versions?
(Also, if you're sure that 8.12.0 worked, you might want to go back to that version)
A few more things you can try:
./.config/coq/coqidercfile - 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).
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).
Are you aware folks of https://github.com/garrigue/lablgtk/issues/120#issuecomment-730381518
Okay, it crashes "not always but very often", on all gtk versions. So if 8.12 worked correctly, it might have been an accident.
Sb please rename the topic to "coqide crashes on macOS 11 (BigSur)" :-)
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:
But now I'm trying to build Coq from scratch.
It looks like until this bug is fixed, your only hope is to switch to Proof General or VsCoq
Apparently the internet says that "visual studio code works on BigSur" (but not visual studio for Mac, whatever it is)
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.
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: Jan 31 2023 at 14:03 UTC