This is just a note on the sporadic failures of HOL-Mirabelle-ex we see
recently from isatest. Technically, the ML/bash invocation
http://isabelle.in.tum.de/repos/isabelle/file/355f3d076924/src/HOL/Mirabelle/ex/Ex.thy#l5
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
