[isabelle-dev] Future of ProofGeneral

[Makarius]

On Tue, 17 Apr 2012, Peter Lammich wrote:

>> Anyway, who is maintaining Isabelle ProofGeneral now?  The repository 
>> version does not work with Emacs 23 for several months already.  It 
>> seems that nobody cares about it anymore.
>>
>> For the release, I will package up official ProofGeneral-4.1 as last 
>> time. It is then up to its users to test it and report problems in the 
>> usual testing stage before the release.
>
> I guess most of the PG users work on the release version, and would be 
> quite annoyed if the next release contains a buggy PG.

(I've switched the thread of this, because the Future of ProofGeneral is a 
serious issue in its own right.)

The plan for the comining release (which will happen within a couple of 
weeks) is to keep the status-quo of Isabelle2011-1.  This means 
ProofGeneral will be not more buggy than everybody is used to anyway. 
Today I've made some quick tests with Emacs on Mac OS X already, and it 
looks not worse than last fall.

In the longer run, the proponents of ProofGeneral need to find a solution 
for themselves, and organize a maintenance scheme -- I have pointed this 
out several times before.  BTW, there is quite a lot of recent activity on 
the ProofGeneral CVS, so it is not quite dead yet.


 	Makarius