Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
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
[isabelle-dev] Where are the error messages?
Hi, theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all Isar commands involving Toplevel.no_timing. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Where are the error messages?
On Wed, 3 Apr 2013, Dmitriy Traytel wrote: theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all Isar commands involving Toplevel.no_timing. This is bad. I will take a look as soon as possible. If you need a quick workaround, you can set parallel proofs to 0 in Isabelle/jEdit. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Where are the error messages?
On Wed, 3 Apr 2013, Dmitriy Traytel wrote: theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all Isar commands involving Toplevel.no_timing. I had messed that up yesterday in 8e9746e584c9. It was an adverse effect on diag commands, and Toplevel.no_timing is just just another coincidence. (Early adopters might have noticed already that commands like 'thm', 'ML_val', 'quickcheck', 'sledgehammer' are now forked by default.) I've made various refinements leading up to ee3398dfee9a, so this detail should work again. There are further things involved, and it all needs a bit more convergence to just 1 way of doing certain things, not 2 or 3 slightly different ways. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
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 9 spaces x 9 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 9
spaces. Presumably the assumption is that PolyML will decide that it
can't possibly fit 9 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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
