[isabelle-dev] HOL-Mirabelle-ex

[Makarius]

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