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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
