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



On Fri, 14 Sep 2012, Rafal Kolanski wrote:

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.

What you "throw" and "catch" on the Java Virtual Machine is slightly different from what you "raise" and "handle" in ML. A JVM Exception object is much more heavy than in ML. Nonetheless, you can use the "reraise" function in Isabelle/ML to pass some of the original information through an exception handler, most importantly the source position.

Searching through the Isabelle sources for "reraise" reveals some examples -- typically some administrative operation.

The implementation manual section 0.5 http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf has some further overview of the overall picture of exceptions, interrupts etc. In particular, the infamous "handle _ => " from the SML/NJ library book must never be used.


	Makarius





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