makarius at sketis.net
Mon Sep 24 16:09:36 CEST 2012
On Sat, 22 Sep 2012, Makarius wrote:
> 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.
After some days of desparately bisecting Poly/ML versions and pondering
perl signal handlers, I've now looked more closely at Mirabelle itself,
resulting in the following changeset
date: Mon Sep 24 15:37:58 2012 +0200
Mirabelle appears to work better in single-threaded mode;
So we seem to be back to a variant of the persistent options problem. In
the image attempts to hardwire options for threading and parallel proofs
(even with some FIXME from 2010), but the new build options are managed
differently for the prover, such that the hardwiring fails.
This is why HOL-Mirabelle-ex ran by accident with the normal multithreaded
proof checking for several weeks, and did not cause any problems by mere
luck until it was run on Mac OS Lion / Mountain Lion more frequently
(macbroy6, macbroy30). There is some hope that with the brakes put into
place again in the above changeset, isatest will succeed tonight.
It also shows though, that the assumption of sequentialism is a very
strong one. Relying on it will inevitably cause surprises again. Anything
that is remotely relevant for end-users needs to run naturally on the
More information about the isabelle-dev