[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

That's interesting. I suspected one of the "continuous_on" rules would
be the cause. In any case, I don't know how the unification works
exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
apply to this goal at all due to its restrictive type class constraint.

What puzzles me the most is the fact that this behaviour seems to depend
on the underlying hardware, and it appears to be 100% reproducible on
machines where it does happen. If this is a race condition, it must be
one of the strangest one I have ever seen (note that it even happens in
single-threaded mode).

Perhaps it might also be of interest to try this with different versions
of Poly/ML, just to make sure it's not an issue with the underlying ML
environment.

Manuel


On 31/08/2018 21:53, Makarius wrote:
> On 31/08/18 15:06, Manuel Eberl wrote:
>> Update: I pushed another changeset and now everything is green again (if
>> you excuse the pun).
>>
>> I tracked the problem to a diverging invocation of "blast":
>> https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default&fileviewer=file-view-default#Derivs.thy-165
>>
>> However, this "blast" does not diverge on any of my machines, no matter
>> if single-threaded or multi-threaded, no matter if "isabelle build" or
>> Isabelle/jEdit. It actually terminates almost instantaneously.
>>
>> It does, however, seem to diverge reliably on the Testboard, on the
>> workermtahpc, and on isabelle-server. I found this "blast" invocation by
>> running "isabelle jedit" on isabelle-server via XForwarding, and there
>> it was continuously purple and remained purple forever.
> 
> This is indeed a bit strange. Apart from the various AMD machines above,
> I see the same effect on my own Intel Xeon E5-2620 v3.
> 
> 
>> I have no idea why it does that; the proof in question is actually very
>> simple. It does use "continuous_intros" and my changeset does introduce
>> a few new "continuous_intros" rules and also some "intro" rules, but
>> none of them match the goal here at all, so I cannot see how that would
>> influence anything. And I am certainly stumped as to how this kind of
>> non-deterministic behaviour could come about.
> 
> A diff of the two versions of continuous_intros produces the included
> a.patch
> 
> The first rule "continuous_on ?A ?f" is continuous_on_discrete, and
> removing is already sufficient to recover the original proof:
> 
>   supply [continuous_intros del] = continuous_on_discrete
>   by (blast intro!: continuous_intros C1_differentiable_on_pair intro:
> C1_differentiable_on_subset elim: )
> 
> This finishes in 0.250s on my Intel Xeon.
> 
> 
> It would be still nice to understand the problem: maybe something odd
> with higher-order unification, or the unification within blast.
> 
> 
> 	Makarius
>