The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Also note that on MacOS, brew now supports (thanks Tej!) installing the 
latest PG with --HEAD.

On 02/19/2016 09:51 AM, Clément Pit--Claudel wrote:
> Hi Scott,
> 
> PG 4.2 is from 2012; can you try reproducing the issue with 4.4pre? 
> https://github.com/ProofGeneral/PG
> 
> Clément.
> 
> On 02/19/2016 09:39 AM, scott constable wrote:
>> Hi All,
>>
>> I've been having some trouble with CoqIDE on OSX, so I decided to give PG 
>> a try instead. I followed the directions from Lance Pollard here:
>>
>> http://lancejpollard.github.io/how-to-install-coq-on-a-mac/
>>
>> Everything is working fine so far, except that with every proof step, the 
>> goal window grows, and the response window shrinks. I have the 
>> proof-three-window-enable option on, which according to the PG manual 
>> "also prevents Emacs automatically resizing windows between proof steps." 
>> But this doesn't seem to be working properly. Is this a bug? If so, would 
>> the problem be with PG or with Aquamacs?
>>
>> What follows is my software platform:
>> OSX 10.11.3
>> Aquamacs 3.2
>> PG 4.2
>> Coq 8.5
>>
>> Thanks in advance,
>>
>> ~Scott Constable
>

Attachment: signature.asc
Description: OpenPGP digital signature