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

On 17/09/12 19:47, Makarius wrote:
> On Mon, 17 Sep 2012, 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);
> Before continuing the meta-discussion, which requires more time to study
> to make sense in the response, just back to the technical question:
> Which aspect of ML expection trace is no longer working, camparing
> Isabelle2012 to some more distant past?
> David Matthews improved something on his side in SVN 1110, I followed in
> my side in 600682331b79, so it should be all back.  What is the
> remaining problem that was not spelled out explicitly so far?

Consider this code:

  exception TFX;
  exception IRR;

  fun f1 x = raise TFX;
  fun f2 x = f1 x + 1;
  fun f3 x = f2 x + 1;
  fun f4 x = f3 x + 1;
  fun f5 x = (f4 x + 1) handle IRR => raise IRR;
  fun f6 x = f5 x + 1;
  fun f7 x = f6 x + 1;
  fun f8 x = f7 x + 1;
  fun f9 x = f8 x + 1;

Output of "f9 1" in PolyML 5.3:

<top level>
End of trace

Output in PolyML 5.4+:

<top level>
End of trace

TFX has not been handled at any point, but in newer releases its origin
is obscured by the handler for IRR, and will be obscured by any handler.

David Matthews has kindly explained the design decision to me and said
he will think on whether it is possible the old behaviour back without
taking a non-trivial penalty. That's really all I hoped for in raising
the backtrace issue originally. I also considered that maybe I'm not the
first ML-level Isabelle user to run into this, and so someone might have
a (hacky) workaround.

I'll honestly say that I don't at present understand what issue your
changeset 600682331b79 addresses and do not possess the free time to
find out, but it appears to not be the one I am describing.


Rafal Kolanski.

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