Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
On Wed, 3 Apr 2013, Alexander Krauss wrote: Thanks Alex, it always helps if someone else with substantial experience explains things, so that I am not the lone voice in the desert. I let your nice explanations stand as is. The area of your issue (interaction with the underlying ML system) is maintained by Makarius pretty much exclusively. Just one concrete note here: it is David Matthews working here with me for many years, to make it work very smoothly with Poly/ML while keeping SML/NJ and older versions of Poly/ML on board somehow. I started myself with ML pretty printing already in 1993, and can't say that will ever be finished. In the mid-1990-ies there were certain gross shortcomings that were even officially documented. Note that when I venture myself to propose actual patches to Poly/ML, the first thing David usually does is to turn the idea behind it in a proper implementation in the sense of his code base, where he is the proven expert. I am glad that he does take the time, and not just apply the proposed patch and thus endanger the system integrity. Also note that when I improved myself exception printing just some months before the Isabelle2013, I messed up SML/NJ in a subtle way that was not immediately visible. As a consequence some software archeologists who try to reactivate Isabelle2013 in the distant future will have problems working with it practically, because ML errors just produce exception Option raised. So a change can never be a fix. It is just some entropy on the code base. Special efforts and attention is required to keep a positive balance in the end. 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
On Thu, 4 Apr 2013, Thomas Sewell wrote: 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. So why did none of you guys ever report that? We have a very reactive isabelle-users mailing list, compared to most other project's issue trackers. It is also possible to discuss anything for inter-release Isabelle versions here on isabelle-dev, although its reactivity needs to be specifically slowed down to avoid hazards in the development process. Having a certain observation or undesirable behaviour on someone's TODO list for 1-2 years already, it is like to be a matter of the past now. Instead we have a lot of wasted time here with patches that are proposed in a way to make it an urgent and immediate issue to be fixed while you wait. 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
On 04/04/2013, at 12:42 PM, Makarius makar...@sketis.net wrote: On Thu, 4 Apr 2013, Thomas Sewell wrote: 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. So why did none of you guys ever report that? We have a very reactive isabelle-users mailing list, compared to most other project's issue trackers. It is also possible to discuss anything for inter-release Isabelle versions here on isabelle-dev, although its reactivity needs to be specifically slowed down to avoid hazards in the development process. It was on these very mailing lists that it was proclaimed that PG is dead and people shouldn't bother reporting problems, because there is nobody there to maintain it. I'm not even disagreeing with it, I certainly don't have the time to maintain PG/Isabelle any more, but it means such things will just disappear under local workarounds that are not of a quality that anyone wants to share (or receive). The response to David was to wait until an expert gets around to reviewing the problem, with a pool of available experts of size 1 and this expert being very busy. If it's a minor problem like this, which probably inconveniences only a small number of people, it's clear that it won't get high priority. Again, I don't even disagree, it should get low priority and there are good reasons for many of the traditional ways Isabelle development happens. But the process clearly puts a lot of strain and time consumption on the expert (you in this case) and makes for a natural bottle neck. Instead we have a lot of wasted time here with patches that are proposed in a way to make it an urgent and immediate issue to be fixed while you wait. This is probably just a matter of perception and culture clash. To me, David was just trying to help, not pressing any urgency and fixes. Most open source projects would be more than happy to get a detailed description of the problem, analysis, and proposed code change in one go. Most other projects get help, stuff doesn't work, make it go away. Sending patches doesn't mean they have to be applied as is the same day. It can also just mean there's something more concrete to talk about. The patches can even be ignored if there's the feeling the problem hasn't been well enough understood yet for code. Alex provided a few good pointers that David can work on. Sure, the wording wasn't the approved Isabelle culture and style, but it takes a year of participation to get that (and about 10 to come to agree with some of it). It's not going to happen at first contact. Being geographically distributed means this is harder than it used to be and costs more time to achieve. Expecting every new person to pick up such things when they post to a mailing list is clearly not working. Maybe we need a README_CULTURE. It takes time to do this, but there is benefit as well. Helping people to contribute small things means there will be more experts around over time and less strain on single people. We might all have to do the unthinkable and maybe slightly relax ;-) Cheers, Gerwin 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
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
On Fri, 5 Apr 2013, David Greenaway wrote: What practical things could such volunteers do that you would find helpful? So how about maintaining Proof General, seriously, no-nonse? And there are other unmaintained parts, such as WWW_Find. (Note that several other people have worked there in the meantime, and they should be included in the discussion, to benefit from the experience gained from certain find_theorems experiements that never hit the repository so far.) 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
On 05/04/13 09:32, Makarius wrote: On Fri, 5 Apr 2013, David Greenaway wrote: What practical things could such volunteers do that you would find helpful? So how about maintaining Proof General, seriously, no-nonse? As somebody who isn't a Proof General user, nor an Emacs user, nor has ever worked with elisp, this doesn't fall particularly well within my skill-set, unfortunately. And there are other unmaintained parts, such as WWW_Find. (Note that several other people have worked there in the meantime, and they should be included in the discussion, to benefit from the experience gained from certain find_theorems experiements that never hit the repository so far.) WWW_Find is perhaps closer to my skill set, but still not a tool I use. Volunteers, counter-intuitively, require payment. Sometimes such payment is a simple thanks on a public mailing list or a changeset being accepted into the official repository. Other times it requires seeing an itch that they have been facing being scratched. If we wanted to start a discussion about replacing WWW_Find with a custom server that the inbuilt find_theorems command could be set up to automatically probe...: find_theorems (_ :: word32) + _ 2 ^ 32 searched for: _ + _ 2 ^ 32 0 theorem(s) found in current session. 2 theorem(s) found from theorem server example.com: WordLemmaBucket.word_add_power_off: [...] (requires import of WordLemmaBucket) LemmaBucket.word_add_bits: [...] (requires import of LemmaBucket) ...then we would be talking about an itch that I would be willing to volunteer some time to scratch. 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
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
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
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
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). Dear David, 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
Hi all,
I have noticed that in c ertain circumstances both Isabelle/jEdit and
Isabelle/ProofGeneral will render certain constructs with a large number
of spaces in them.
The problem can be seen with the following testcase:
definition test a b ≡ undefined
notation (output) test (test // (_) // (_))
ML {* raise (CTERM (test, [@{cterm test x y }])) *}
The root cause is related to the interaction between Isabelle and
PolyML's pretty-printers. A problem arises when converting from
Isabelle's format to PolyML's format, in that the former supports
forced line breaks while the latter does not. The current solution is
to expand such line-breaks into a directive to print a large number of
spaces (9, to be precise), preventing PolyML from fitting the spaces
on a line, and hence forcing it to produce a line-break.
This approach, unfortunately, falls down in two areas:
PolyML.makestring renders the large amount of spaces, producing
undesirable results. Similarly, General.exnMessage in PolyML simply
calls PolyML.makestring, and hence has the same problem.
This attached patch fixes one instance of this problem by using an
alternative mechanism to pretty-print unhanded exceptions which prevents
the large number of spaces being rendered, fixing the problem above.
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).
The patch is based off the current Isabelle tip, which is d40aec502416
at time of writing.
Thanks so much,
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
