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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
