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



On Mon, 17 Sep 2012, Rafal Kolanski wrote:

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:

f1(1)
f2(1)
f3(1)
f4(1)
f5(1)
f5(1)
f6(1)
f7(1)
f8(1)
f9(1)
<top level>
CODETREE().genCode(2)(1)
COMPILER_BODY().baseCompiler(4)executeCode(1)
End of trace

Output in PolyML 5.4+:

f6(1)
f7(1)
f8(1)
f9(1)
<top level>
CODETREE().genCode(2)(1)
COMPILER_BODY().baseCompiler(4)executeCode(1)
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.

OK, this is a reasonable report on the situation after all.


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.

It addresses exactly that for the Isar toplevel, but it cannot change the situation for user-code, of course.


	Makarius





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