On 17/09/12 04:54, Makarius wrote:
Both of you seem to have taken software decay for granted, and did not
tell anybody here or on isabelle-dev. Isabelle has traditionally very
high ethical standards for software quality, so things are usually put
into shape again quickly, once the problem is known.
This is not really "decay" as such. It is an implementation decision we
were not aware of, and I merely wonder if there isn't some way to get
detailed traces back while maintaining performance. David Matthews
explained the situation to me and said he will think about if and how it
is possible. This is all I wanted, and he has been very helpful throughout.
date: Mon Nov 14 16:16:49 2011 +0100
more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers
reset the trace (cf. Poly/ML SVN 1110);
Please be aware there are very important trade-offs both in life an
work. There is a reason you are a (the?) Isabelle guru. It has to do
with the exposure of time and investment of effort in keeping Isabelle
running, preventing aforementioned code decay while still improving the
feature set. For this reason, you were aware of this situation and tried
to do something about it already.
This is highly relevant work, and work for which we are grateful, but it
is not necessarily *our* work. Our work takes us further out than
Isabelle itself and into the realm of building larger projects with it.
When we identify situations where we need to automate or customise
because of project maintenance, that's when we get to dive back into the
So we have this periodic dance:
On the one hand, we need to be periodically reminded that Isabelle can't
just have features shoved in because we want them, that they need to be
considered within the broader scope of the Isabelle system, and that
there is an "Isabelle way" of doing things. We count on that for you.
Sometimes we get a bit frustrated, but that's an acceptable price to pay.
On the other hand, I think you need to be periodically reminded that
Isabelle has users at various levels of competency/experience, whose
primary work focus is not Isabelle itself. In other words, there is more
to Isabelle than using Isabelle for the sake of Isabelle by means of
Isabelle (similarly Scala and Scala).
Such users have need of interfaces which reflect at least slightly
realistic work that they need to be doing.
Concrete example. During my visit to Munich this year, I wanted to find
out which theorems were used by fastforce to prove a lemma, because my
tactic wouldn't solve it, but fastforce did. Typical
tactical-implementation problem. So, there isn't a feature in Isabelle
called "thms_used_to_prove my_theorem". I look at the ML level, and
realise there isn't one either, there's only a generalised fold over the
proof term structure. It turns out that if you perform a partial
traversal of the proof term (first two levels), you get the required
functionality. But now I've spent the better part of an hour
understanding proof terms to make sure I got it right and bothered Lukas
(who is awesome, BTW) as a result.
So finally, I have my shiny ML function which answers the very useful
question of "which theorems were used to prove this theorem directly,
rather than the entire tree back to Pure". Lukas likes it, Tobias thinks
it is useful.
After further discussion though, Lukas and I conclude that we'll never
get it past you, because we can't substantiate a serious enough
Isabelle-reason for modifying the proof term API to provide this
commonly thought of and convenient functionality. So we put it in the
Isabelle Cookbook. After I left, Lars had the exact same problem, but
now could just look up the solution.
That is how things work for Isabelle non-gurus.