[isabelle-dev] HOL-Mirabelle-ex

Makarius makarius at sketis.net
Sat Sep 22 13:35:53 CEST 2012

This is just a note on the sporadic failures of HOL-Mirabelle-ex we see 
recently from isatest. Technically, the ML/bash invocation 
somehow "hangs".

I first thought it would be related to the polyml-5.5.0 update, but I've 
seen the same with polyml-5.4.1 occasionally.

Maybe it is again some odd boundary cases with signal handlers in perl, on 
different platforms and different perl compilations.

This requires further investigation.


More information about the isabelle-dev mailing list