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

[Gerwin Klein]

On 04/04/2013, at 12:42 PM, Makarius <makarius at sketis.net> wrote:

> On Thu, 4 Apr 2013, Thomas Sewell wrote:
>
>> David's investigation explains a problem we had a few years ago where some custom tactics of mine were killing my colleagues' ProofGeneral sessions when they encountered errors. The workaround at the time was to remove all potentially useful debugging information (terms, in particular) from the relevant exceptions. Unfortunately this made tracking down the bugs in the tactics somewhat challenging.
>>
>> In hindsight, I should probably put the debug terms in the tracebuffer and thrown a vanilla exception. Hindsight is perfect, of course.
>
> So why did none of you guys ever report that?  We have a very reactive isabelle-users mailing list, compared to most other project's "issue trackers".  It is also possible to discuss anything for inter-release Isabelle versions here on isabelle-dev, although its reactivity needs to be specifically slowed down to avoid hazards in the development process.

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

The response to David was to wait until an expert gets around to reviewing the problem, with a pool of available experts of size 1 and this expert being very busy. If it's a minor problem like this, which probably inconveniences only a small number of people, it's clear that it won't get high priority.

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.


> Instead we have a lot of wasted time here with patches that are proposed in a way to make it an urgent and immediate issue to be "fixed" while you wait.

This is probably just a matter of perception and culture clash. To me, David was just trying to help, not pressing any urgency and fixes. Most open source projects would be more than happy to get a detailed description of the problem, analysis, and proposed code change in one go. Most other projects get "help, stuff doesn't work, make it go away".

Sending patches doesn't mean they have to be applied as is the same day. It can also just mean there's something more concrete to talk about. The patches can even be ignored if there's the feeling the problem hasn't been well enough understood yet for code. Alex provided a few good pointers that David can work on.

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. Maybe we need a README_CULTURE.

It takes time to do this, but there is benefit as well. Helping people to contribute small things means there will be more experts around over time and less strain on single people.

We might all have to do the unthinkable and maybe slightly relax ;-)

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.