The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Clément,

I just tried:

$ brew remove proof-general

$ brew install --HEAD proof-general

which succeeded, and then I launched Aquamacs, which gave a ProofGeneral 4.4pre splash screen. But I'm still witnessing the same behavior with the resizing windows.

Thanks,

~Scott

On Fri, Feb 19, 2016 at 9:56 AM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

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
>