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

[Alexander Krauss]

Hi David,

On 04/03/2013 09:18 AM, David Greenaway wrote:
> On 02/04/13 21:17, Makarius wrote:
>>
>> 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 personally found the patch helpful in clarifying what you think is the 
source of the issue that you are seeing. So I merely read it as "This is 
what I tried and it made the problem go away for me" (even though you 
wrote "Please review and possibly apply"). Such a patch is a 
"constructive proof" of some analysis that you made, which I think is a 
good thing (and it can always easily be ignored when you are totally on 
the wrong track).

However, most problems are deeper rooted and not easily patched away, so 
people are usually very skeptical about such superficial "fixes". The 
usual practice is that the experts in the relevant areas look at the 
problem (not so much the proposed solution) and implement a suitable 
solution if and when possible.

Note that this can take some time, as there are other, more pressing 
things. Here it may help to clarify why the issue is a problem for you 
in real-life applications.

The area of your issue (interaction with the underlying ML system) is 
maintained by Makarius pretty much exclusively.


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

Some points that I noticed (but this is neither exhaustive nor 
authoritative):

- Architecture violation: Isabelle/ML code may not refer to the PolyML 
structure directly, since it must use the compatibility layer. Your code 
does not compile with SML/NJ which is still formally supported. 
Possibly, something similar could be done in the compatibility layer, 
but one has to consider the consequences very carefully.

- Process: You are assuming/proposing a fix, but there has been no 
discussion whether the behavior you are seeing is actually something 
that should be fixed. In particular, you seem to be expecting the 
display of low-level exceptions to be as convenient as user-level pretty 
printing. AFAIK, this is not the case in general. Due to the complexity 
of the system, there are many grey areas that are neither right nor 
wrong. I would say that pretty printing of low-level exceptions is such 
a case.

So you should describe your actual real-life problem, and we can then 
also look for other solutions.

It might also be interesting to know if the problem has always been 
there or has been introduced by some change. I personally saw quite some 
long CTERM exceptions and never noticed strange printing, so it might 
also be a new issue (just speculating here).

- Style: Your commit message is indeed too verbose, according to the 
usual standards, and it has the wrong format. The question whether 
Isabelle's terse style is good or bad is a different issue, but the 
conventions are like that, see README_REPOSITORY.

Hope this helps a bit...

Alex