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

Thomas Sewell Thomas.Sewell at nicta.com.au
Thu Apr 4 06:07:16 CEST 2013


Just my two cents, but I'd like to see this problem fixed as well.

David's investigation explains a problem we had a few years ago where 
some custom tactics of mine were killing my colleagues' ProofGeneral 
sessions when they encountered errors. The workaround at the time was to 
remove all potentially useful debugging information (terms, in 
particular) from the relevant exceptions. Unfortunately this made 
tracking down the bugs in the tactics somewhat challenging.

In hindsight, I should probably put the debug terms in the tracebuffer 
and thrown a vanilla exception. Hindsight is perfect, of course.

Yours,
     Thomas.

On 04/04/13 13:50, David Greenaway wrote:
> 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.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list