[isabelle-dev] Isabelle2013-2 release

[Makarius]

On Thu, 21 Nov 2013, Peter Lammich wrote:

> Are there currently real proof methods that may run out of stack space 
> or otherwise throw Exn.Interrupt?

The problem of Exn.Interrupt emerging explicitly or implicitly in 
Isabelle/ML is an old one.  I have kept an eye on that routinely in the 
past couple of years.  From this background I consider this as of little 
practical relevance (at least for this release).


Side-remark: David Matthews provides to following flag to get static 
compiler warnings about infamous catch-all exception handlers:

   PolyML.Compiler.reportExhaustiveHandlers := true

This allows to detect infamous "handle _ => ..." or "handle 
My_Undeclared_Exn => ...", which would make ML code subject to the laws of 
physics instead of mathematics.  (Unfortunately some major ML books do 
this all the time.)

I check the above routinely before every release.  There is further 
syntactic "pattern recognition" that I do with hypersearch over all 
sources to see if the flow of interrupts through Isabelle/ML user code is 
right.  This is why it is important to stick to standard idioms of handle 
/ raise in Isabelle/ML and refrain from introducing more aliases and 
variations of that.


Interestingly, OCaml is in a much worse situation here.  Apart from 
ubiquitious catch-all handlers seen in big applications (also provers), 
that platform allows to inject arbitrary exceptions into user code (not 
just interrupts).  This also works in single-threaded OCaml, by using 
POSIX signal handlers.


 	Makarius