The Coq mailing list

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

Thanks. In that case, please open a Proof General bug report at 
https://github.com/ProofGeneral/PG/issues , with a slightly more detailed 
description of the problem. In particular, it would be useful to have an 
example of the script that causes this issue, so the devs can try to 
reproduce it.

Cheers,
Clément.

On 02/19/2016 10:14 AM, scott constable wrote:
> 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
>  
> <mailto: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
>     >
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature