[isabelle-dev] Proof General 4.1pre

Alexander Krauss krauss at in.tum.de
Thu Jan 13 16:04:47 CET 2011


> 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.

I've been using PG 4.1 for a while now from cvs, and it works nicely, 
except that I've regularly experienced sync losses in connection with 
the undo-on-edit feature. I couldn't track this down enough to come up 
with a useful bug report yet, but it seems that switching off this 
feature solves the problem.

Thus, if 4.1 is going to be used, I would recommend having undo-on-edit 
switched off by default (maybe this is the case anyway, I am not sure...)


Alex



More information about the isabelle-dev mailing list