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

[David Greenaway]

Hi Alexander,

Thanks for your helpful reply.

On 04/04/13 08:58, Alexander Krauss wrote:
> Hi David,
> On 04/03/2013 09:18 AM, David Greenaway wrote:
[...]
>> 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.

Ah, this indeed is a serious problem that I should have considered more
carefully. Thank you for pointing it out.

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

The problem is that Isabelle will sometimes render thm's and cterm's
with a large number of spaces.

For example, in the testcase posted earlier:

    definition "test a b ≡ undefined"
    notation (output) test ("test // (_) // (_)")
    ML {* raise (CTERM ("test", [@{cterm "test x y" }])) *}

jEdit will render to the output:

    "test <99999 spaces> x <99999 spaces> y",

making the "x" and "y" hard to see. For users of ProofGeneral, this will
also tend to lock up emacs for long periods of time (as it attempts to
process the large amount of data). The sheer amount of data will even
give jEdit pause, especially when the number of forced line breaks in
a term starts to increase.

The cause of the problem, as far as I can see, is that when Isabelle is
converting its own pretty-print format into PolyML's pretty-print format
it translates "forced line breaks" into a directive to print 99999
spaces. Presumably the assumption is that PolyML will decide that it
can't possibly fit 99999 spaces on the current line, and convert the
spaces into a newline.

This works most of the time, except in two scenarios:
"PolyML.makestring" assumes that the line width is infinite, so will
simply render the spaces. "General.exnMessage" (which converts
ML exceptions into strings) internally calls "PolyML.makestring", so
suffers the same fate.

The problem arises in practice when developing with Isabelle: unhandled
exceptions containing thm's or cterm's are mis-rendered, and
"PolyML.makestring" can't be used as a debugging aid when these
problematic terms are floating around.

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

The problem has been present for quite some time: I seem to recall
seeing it in Isabelle 2009 up to now. I only recently managed to take
track down the precise cause of the problem (i.e., the interaction
between forced line breaks and PolyML's pretty-printer) this past week.

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

Thank you for the pointer. I misinterpreted the README_REPOSITORY as
being permissive of short messages (as opposed to prescriptive), but
will ensure future commit messages are more concise.

> Hope this helps a bit...

Very much so, thank you.

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.