On Tue, 21 Jun 2011, Aleks Kissinger wrote:
On a related note, any idea why Par_List.exists would raise the
"EXCEPTIONS []" exception? The predicate function shouldn't be throwing
exceptions (at least it doesn't with List.exists substituted in), and
doesn't use side effects.
EXCEPTIONS [] means spontanous cancellation, say via external interrupt or
internal sigalling from peer task groups. E.g. there could be a stack
overflow in one future task. The Poly/ML runtime systems turns this into
exception Interrupt, which the future scheduler will propagate to other
futures of the same group, turning it into EXCEPTIONS [] at some point.
(There can also some boundary cases with *incorrect* treatment in my
implementation. I have had rare situations where there are some surprises
concerning this.)
Anyway, you can check with Multithreading.max_threads := 1 without any
special things getting in between. If you now see Interrupt it means
Poly/ML RTS failure, typically stack overflow (max. 64MB) or virtual
memory exhaustion (max. 2GB). You can then try with x86_64 to see if the
problem persists, although it might lead to disk thrashing instead.
Assuming that you have Isabelle2011, this is how to configure x86_64 in
your $HOME/.isabelle/etc/settings file:
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$ISABELLE_HOME/contrib/polyml-5.4.0/$ML_PLATFORM"
ML_SYSTEM=polyml-5.4.0
ML_OPTIONS="-H 1000"
ML_SOURCES="$ML_HOME/../src"
You then need to build Pure for that platform:
Isabelle2011/build Pure
or on Mac OS X:
Isabelle2011.app/Isabelle/build Pure
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
