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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev