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



On 17/09/2012 10:47, Makarius wrote:
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?

With PolyML 5.3 and earlier, if you had a handler that caught only exception foo but you had raised bar then exception_trace would show the whole stack trace from the point where you raised bar. With 5.4 and later an exception handler of the form
handle foo => ... is rewritten as though it were
handle x => (case x of foo => ... | x => reraise x)
So exception_trace only shows the stack from the point where bar was reraised. That may well not be as helpful.

I understand the problem; it's just that making this change greatly simplified the exception mechanism and speeded it up.

David





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