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



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.

All I ask for is a bit of respect. Just because I don't understand the
entire system and its multi-year vision in-depth does not necessarily
mean that all my ideas are stupid. In fact, some of the ideas might be
good, but are in need of a guru suggesting a better implementation,
which is why I mention them anyway.

There are real issues with introspection of proofs in larger projects,
e.g. being able to reliably tag images (you are looking at the most
recent successful build of an image via the wwwfind interface... quick,
please tell me which revision that is, and if the correct image is in
fact loaded without reading through the entire theory dropdown first). I
have also tried discussing this at length, but no one cares except for
our team, so we use custom patches and I gave up. The next big project
will have the exact same problems, and these hacky solutions will get
hacked in again and again, wasting people's time, while every time we
bring them up here we'll get told they are not relevant, because the
Isabelle project itself doesn't need it, and why would you want multiple
instances of an image on the same machine anyway?

> In Isabelle/jEdit the support for Isabelle/ML support (including tracing
> and debugging) is already better in Isabelle/jEdit of Isabelle2012 than
> ever before in the history of Isabelle Proof General.
> 
> There is also clear separation of physical stdin from the protocol
> channel.  So in principle one could negotiate with the raw Poly/ML
> toplevel loop (and its debugger) while Isabelle is running at full
> speed. There is no console window for that in the Prover IDE, though.

Great, so at some point in the future when I change the theorem prover
interface I use, the functionality I'm looking for might be available.
This will be quite an improvement, to be able to run the interactive
debugger at the same time as Isabelle, and when it happens will render
my observations about exception traces mostly irrelevant (still would be
nice if David figured out a magical way to do it).

> In practice, I usually use plain writeln and PolyML.print to see what is
> happening in some ML code (after recompiling), not the debugger.

Yes, I do this too, in my own code. I can't just rewrite some other
person's code and rebuild, because that may take hours. Thanks to David
Matthews and the latest PolyML 5.5 though, we can now build everything
in under 3 hours (down from 8h with -q 0, and 4h with -q 1) on some
machines and then do something which you really dislike: copy the image
from the much faster machine to the much slower one. I recall on this
list someone (you?) telling me that one shouldn't copy binary images
around, and why would anyone want to do that anyway?

So in summary, I may not be the smartest person on this planet, but if
I'm not aware of the intricacies of what exactly happened in Isabelle in
every single commit, it's not because I don't care or take software
decay for granted or something. In fact, if you ask people at Munich who
have talked to me, it's almost the opposite. I have an inherent and
sometimes not-quite-sane instinct to streamline things and make them
more intuitive.

I just have four other projects to work on, and don't really feel
encouraged to try contribute when the answer is nearly always the same:
"your idea sucks || is pointless || we don't have this problem la la la
|| your implementation is not canonical || that isn't a good enough
reason to modify the interface || ...). Look what happened now: I raised
a bug report when I found one, and in the resulting discussion I get
told that I take "software decay for granted".

While your contributions are truly impressive, I would venture a
suggestion to at least try pretend to be a bit more open-minded. You
know, Bill Clinton style. He won't do what you asked for in all
probability anyway, but at least you'll walk away from the discussion
feeling like your idea was given due consideration. I don't know how
else to explain this, other than that the Isabelle users list is great,
helpful and proving stuff is fun and easy to release, working at the ML
level is a depressing experience, and trying to share the results of
one's work doubly so.

Sincerely,

Rafal Kolanski.





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