Stream: Coq users

Topic: coqide crashes on macOS 11 (BigSur)


view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Nov 19 2020 at 07:54):

How did you install Coq and CoqIDE? With opam?

view this post on Zulip Yosuke Ito (Nov 19 2020 at 07:58):

Thank you for your reply.
Yes, I installed with opam, using Terminal.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Nov 19 2020 at 08:18):

What do coqtop --version and coqide --version give?

view this post on Zulip 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)".

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 10:19):

rather than “upgrade coq first”, are you confident coq ever worked after upgrading to big sur?

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 10:20):

or *coqide rather

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 10:20):

your message says that coqide fails, but maybe coq would work with other clients.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 12:28):

My Big Sur VM isn’t too fast, but I can try if you’re desperate.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 15:39):

Yeah... If you hate Emacs (it has a learning curve) you might like VsCoq

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 15:40):

Since it builds on visual studio code which is more intuitive

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 15:41):

Wait, are you sure you uninstalled 8.12.1 properly?

view this post on Zulip Gaëtan Gilbert (Nov 19 2020 at 15:41):

what does opam list say about coq and coqide versions?

view this post on Zulip 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)

view this post on Zulip Michael Soegtrop (Nov 19 2020 at 16:32):

A few more things you can try:

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 20 2020 at 03:19):

Sb please rename the topic to "coqide crashes on macOS 11 (BigSur)" :-)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC