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



Hi David,

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 :/

Sincerely,

Rafal Kolanski.





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