Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)



On 09/17/2012 12:39 AM, Rafal Kolanski wrote:
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.

changeset:   45486:600682331b79
user:        wenzelm
date:        Mon Nov 14 16:16:49 2011 +0100
files:       src/Pure/Isar/runtime.ML
description:
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
Isabelle internals.

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.
Just to clarify my intentions in this example of a feature request here:
Certain features, as the one mentioned above, can be implemented perfectly in Isabelle's "user space". For the implementing developer, many functions then appear to be important for a decent library and we would like to add them to "kernel" modules to make our contribution more visible. However, Isabelle's slogan "fight features" (p.3 of the Isabelle implementation manual) just as the often cited LCF approach forbid to modify and extend kernel modules, just because of a temporal state of mind. Coincidently, Makarius is the person, who enforces these matters in our system and repository---Hence, the statement "We can't get it past Makarius", really means we do not have any substantial reason to modify the kernel.

Nonetheless, the story of some feature usually does not end here. If developers are quite proud of their functionality, they try to advertise it, as we did. One such way is certainly the Isabelle developer tutorial, another is to find others that need the functionality. This usually ends up in temporal clones here und there till the pressure is large enough for one of the developers to take another round of iteration of some subject.

Unlike some other developers, I was in the fortunate position to learn this way of system development from Makarius and many others in the group in Munich.

But again, this thread (as many other threads before) is getting largely off-topic.

Lukas






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.