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

[David Greenaway]

Hi Makarius,

On 02/04/13 21:17, Makarius wrote:
> On Tue, 2 Apr 2013, David Greenaway wrote:
>
>> I would appreciate it if an Isabelle expert could review that patch
>> and, if acceptable, apply it to mainline. (This can be easily done
>> with "hg import <patch-file>").
>
> before you send more patches, can you please go back to the very start
> of the mail thread from last time, which contains a lot of hints how
> things are done, including pointers to the documentation.
>
> I am not going to spend such an amount of time again, especially when
> it looks like it is being wasted.

My apologies if your time has been wasted. It was my hope that sending
a bug report, along with an analysis of its cause and a suggested fix
would waste far less of your time than simply sending through just the
bug report with nothing more.

I also fear that your hints have been too subtle for me. I have re-read
README_REPOSITORY (which appears to be mostly a HG tutorial, which
a short paragraph describing the desired commit message content) and
chapter 0 of the implementation manual (which, amongst other things,
includes a longer discussion of the desired ML style, variables names,
etc). Despite this, I must confess that I am still not sure what I am
doing wrong.

Does my 4 line patch violate the Isabelle style guidelines, or have
I missed something about the correct etiquette for submitting patches?
I would greatly appreciate if someone could let me know what I am doing
wrong, so I can avoid wasting both your time and my time in the future.

A single sentence such as:

   "You should be sending Mercurial bundles instead of patches to the
   list"; or

   "Your name 'str_of_exn' should use the whole word 'string'"; or

   "Your line 'a |> b |> c' should be split into three; existing
   usages where they are on the same line are wrong"; or

   "You are dereferencing 'Pretty.margin_default' unsafely; the existing
   code that does this is wrong"; or

   "Your commit message is far too verbose", etc.

would be immensely useful. Indeed, such a critique need not come from
you Makarius, but from anyone on the list involved with Isabelle
development who knows better than me.

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.