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
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.
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
changeset: 49549:3b0a60eee56e
tag: tip
user: wenzelm
date: Mon Sep 24 15:37:58 2012 +0200
files: src/HOL/Mirabelle/lib/scripts/mirabelle.pl
description:
Mirabelle appears to work better in single-threaded mode;
So we seem to be back to a variant of the persistent options problem. In
http://isabelle.in.tum.de/repos/isabelle/annotate/3b0a60eee56e/src/HOL/Mirabelle/Mirabelle.thy
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
multithreaded system.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
