[isabelle-dev] Proof General 4.1pre

[Gerwin Klein]

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