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

David Greenaway david.greenaway at nicta.com.au
Fri Apr 5 00:25:59 CEST 2013


On 04/04/13 23:41, Makarius wrote:
> On Thu, 4 Apr 2013, Gerwin Klein wrote:
[...]
>> 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.

Would it be helpful to have volunteers to help out in some of these
areas? What practical things could such volunteers do that you would
find helpful?

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

I don't think anybody is proposing that we abandon strict quality
controls on incoming patches.

What I was hoping for was that outside contributions would be welcomed
and constructively critiqued. That such patches could be iterated by the
authors, until finally reaching a point were the existing experts became
satisfied and the patch could be applied. (Or, alternatively, until the
existing experts become convinced that the feature/bug-fix is
undesirable, and inform the submitter of such.)

Again, I apologise if my initial emails came across as having the
expectation that my patches should be unconditionally applied to
Isabelle in their initial state.

Cheers,
David


________________________________

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.



More information about the isabelle-dev mailing list