The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Arthur,

I have also experienced this exact problem on OS X 10.11.3. But I've noticed that it only occurs when I open CoqIDE from the launchpad. If I instead invoke it from the terminal, I do not experience this issue. If you used the .dmg installer like I did, you'll either need to add <Coq install location>/Contents/MacOS/ to your $PATH variable, or soft link the coqide binary into your /usr/bin. Then from your working directory, run

$ coqide &

Best,

~Scott

On Sun, Feb 7, 2016 at 5:45 PM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hello,

An issue similar to what you describe has already been reported. We
suspect that it comes from a GTK bug under OSX but we are still
investigating.

Sorry for the inconvenience.

Maxime.

On 02/07/16 21:55, Arthur Ryman wrote:
> I am a new Coq user. I would like to use Coq to create a formal
> specification for a new language, SHACL, being developed at W3C.
>
> I have been experiencing intermittent crashes of CoqIDE on Mac OS X. I
> am using El Capitan 10.11.3 and CoqIDE 8.5.
>
> The crashes often occur when I undo proof steps.
>
> Is this a known problem? Is there a FAQ? Any workaround?
>
> I have switched to using Proof General, but I'd prefer to use CoqIDE.
> Thanks in advance for any help.
>
> -- Arthur Ryman
>