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



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?


	Makarius





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