Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
On 14/09/12 10:11, David Greenaway wrote:
I too had previously thought that the exception traces in Isabelle had
disappeared somewhere around the Isabelle2011-1 time-frame, but when
I tried to reproduce the problem this morning in Isabelle2012 I was
pleasantly surprised to find that the problem had gone away and I could
actually get them again.
As I demonstrated in person, the exception traces only get you as far as
the first exception handler you encounter. So for example if anywhere in
the chain there was a handle BAR, then even though you threw a FOO you
still wouldn't get a trace past that handler.
I think we decided that behaviour appeared in 5.4? Dave Matthews told me
it was a design decision which improved performance and simplified code,
but I am still rather sad it is gone. I wish there was a way to enable
it again for our interactive sessions, even if we have to suffer a speed
penalty. For batch sessions with parallelism, the existing behaviour in
exchange for performance is definitely the right idea.
I guess if the problem is really massively painful, we can always
rebuild with 5.3 and trace with that while head-scratching in parallel :/
This archive was generated by a fusion of
Pipermail (Mailman edition) and