[isabelle-dev] PG 3.x vs. 4.x settings

Makarius makarius at sketis.net
Wed Dec 12 19:29:23 CET 2012


This is a continuation of a never-ending thread about Proof General 4.x 
being weak in holding its persistent settings persistent, see the 
isabelle-users thread "PG/Isabelle: Problem with Auto-Trace options (with 
workaround)" 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-September/msg00019.html

See also the corresponding Trac item 
http://proofgeneral.inf.ed.ac.uk/trac/ticket/452 where I re-opened the 
already closed issue, but it seems to be deferred to Proof General 4.3 
now.  Are there actually Isabelle / Proof General 4.2 users around?


For the coming Isabelle release, I need some hint if there will be a 
version of Proof General shipped with it at all, and which version it 
should be.  If it is Proof General 3.x there is no point to work on 
workarounds for 4.x.  On the other hand, "fixing" things for 4.x might 
also break 3.x and I am testing none of that again.

"Doing nothing for nor against" Proof General does not mean that I just do 
nothing at all, or apply arbitrary changes to the ML side of its protocol 
implementation.  Doing this carelessly would mean accelerated decay and 
thus doing something against it.


 	Makarius


More information about the isabelle-dev mailing list