The Coq mailing list

[Arthur Ryman <arthur.ryman AT gmail.com>]

Greg,

Thx. I'll try that too.

-- Arthur

On Mon, Feb 8, 2016 at 1:54 PM, Greg Bush 
<gbush AT kitchenbrains.com>
 wrote:
> This work-around doesn’t seem to work for me, but I’ve still been able to 
> use the 8.5 coqide after noticing that you can now edit text in the green 
> regions and it will automatically undo back to this point.  This type of 
> undo doesn’t seem to cause the same problem.
>
> On Feb 8, 2016, at 1:44 PM, scott constable 
> <sdconsta AT syr.edu<mailto:sdconsta AT syr.edu>>
>  wrote:
>
> 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<mailto: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
>>
>
>