On Mon, 3 Mar 2014, David Matthews wrote:
InternalError exceptions are assertions within the compiler. I would
expect them to be deterministic unlike assertions in the GC which depend
a lot on timing of threads. It should be possible to get to the bottom
of this if I'm able to get the ML code that is causing the problem.
Over the years I have seen Poly/ML compiler crashes occasionally, but
rather rarely. Usually I managed to point David to some spots in his ML
sources, by putting the PolyML.exception_trace combinator just in the
right place of the system.
Since Isabelle/ML invokes PolyML.compiler on its own, this often works
relatively easily, but sometimes I went through the actual Poly/ML sources
and made educated guesses where to make a trace.
Maybe the following may serve as an example how to invoke and manage the
PolyML compiler under program control:
(1) short version (Isabelle/Pure bootstrap):
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Systems/compiler_polyml.ML#l40
(2) long version (full Isabelle/ML managed compilation with IDE markup)
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML/ml_compiler_polyml.ML#l184
In both cases, the critical bit is the two-stage invocation of
PolyML.compiler: first the static then the dynamic phase.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
