On 14/01/2011, at 1:39 AM, Makarius wrote:

> There is now a development snapshot of Proof General 4.1pre, provided by 
> David Aspinall:
> 
> http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.1pre110112.tgz
> 
> It looks pretty stable to me.  There are only few remaining entries at 
> http://proofgeneral.inf.ed.ac.uk/trac/
> 
> 
> Are there still users of PG 3.x with recent Isabelle snapshots or versions 
> from the repository?

I'm still using PG 3.7.1.1 (with different Isabelle versions from 2009-1 to 
current dev). 

Maybe I'm turning into one of these people who never want to update, but 
whenever I tried there were was some combination of annoying issues that I 
couldn't solve in less then 5 min, so I kept the old version because it works 
and does what I want. 

It's not just PG, but finding the correct combination of 
PG/xemacs/emacs/platform/fonts/packages/etc. I haven't tried 4.1pre yet, though.


> The question is if PG 4.1 converges sufficiently fast for Isabelle2011, and 
> if we should switch to the PGIP update for floating point settings. This 
> would mean to discontinue 4.0 and 3.x altogether.
> 
> If there is the slightest doubt we can also keep the odd treatment of pgreal 
> values in Isabelle2011 -- PG 4.1 would work nonetheless, despite our abuse of 
> the protocol.

If it's trivial to keep, we should leave it in and give one release warning for 
users to switch. Even I should manage then ;-)

There's always someone out there with an older setup, and it's quite annoying 
if things stop working without warning.

Cheers,
Gerwin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to