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

[Makarius]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: a.patch
Type: text/x-patch
Size: 831 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180831/1e0390ad/attachment-0002.bin>