[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks

[Makarius]

On Thu, 4 Apr 2013, Gerwin Klein wrote:

> It was on these very mailing lists that it was proclaimed that PG is 
> dead and people shouldn't bother reporting problems, because there is 
> nobody there to maintain it. I'm not even disagreeing with it, I 
> certainly don't have the time to maintain PG/Isabelle any more, but it 
> means such things will just disappear under local workarounds that are 
> not of a quality that anyone wants to share (or receive).

I did not perceive the problem as specific to PG.

Concerning the status of PG, I never "proclaimed" its death or rather 
zombie status.  I merely informed about it for several years, and 
encouraged people to take over its maintenance.  I still do so -- if 
nothing is done there, PG will rot rather quickly -- and I will be again 
blamed for having maintained it for so long, but have stopped that.


> Again, I don't even disagree, it should get low priority and there are 
> good reasons for many of the traditional ways Isabelle development 
> happens. But the process clearly puts a lot of strain and time 
> consumption on the expert (you in this case) and makes for a natural 
> bottle neck.

I know myself that I am a bottle neck for a long time.  As I've pointed 
out earlier, it is either due to things that nobody else can do or nobody 
else wants to do, or just things where nobody else cares.

Apart from that we still have >1 people with some atheletic spirit left to 
do substantial things.


The general problem is not solved by having a lot of uneducated hackers on 
the code base.  On the contrary.  We even have concrete experience with 
near-desaster already, e.g. in Isabelle2004 and Isabelle2007.  After 
Isabelle2008 things became much more stable, but also harder to change.

We should make some serious moves towards actual education of able people, 
to work professionally with Isabelle, and potentially on Isabelle. 
Hardly anything has happended there in recent years.


> Sure, the wording wasn't the approved Isabelle culture and style, but it 
> takes a year of participation to get that (and about 10 to come to agree 
> with some of it). It's not going to happen at first contact. Being 
> geographically distributed means this is harder than it used to be and 
> costs more time to achieve. Expecting every new person to pick up such 
> things when they post to a mailing list is clearly not working.

Note that it was not first contact here, but already a followup-thread by 
David, where he still did not show any signs to have studied earlier 
answers carefully.  Taking time to study things is an important 
prerequisite to any work with the Isabelle sources.


 	Makarius